Step
*
2
1
2
1
1
of Lemma
prime-power-divides-product
.....aux.....
1. p : ℕ
2. prime(p)
3. n : ℤ
4. 0 < n
5. ∀x,y:ℤ. ((¬(p | x))
⇒ (p^n | (x * y))
⇒ (p^n | y))
6. x : ℤ
7. ∀y:ℤ. ((¬(p | x))
⇒ (p^n | (x * y))
⇒ (p^n | y))
8. y : ℤ
9. ¬(p | x)
10. c1 : ℤ
11. (x * y) = (p^(n + 1) * c1) ∈ ℤ
12. c : ℤ
13. y = (p^n * c) ∈ ℤ
⊢ (x * c) = (p * c1) ∈ ℤ
BY
{ (Mul ⌜p^n⌝ 0⋅ THEN Auto THEN NthHypEq (-3) THEN EqCD THEN Auto) }
1
.....subterm..... T:t
2:n
1. p : ℕ
2. prime(p)
3. n : ℤ
4. 0 < n
5. ∀x,y:ℤ. ((¬(p | x))
⇒ (p^n | (x * y))
⇒ (p^n | y))
6. x : ℤ
7. ∀y:ℤ. ((¬(p | x))
⇒ (p^n | (x * y))
⇒ (p^n | y))
8. y : ℤ
9. ¬(p | x)
10. c1 : ℤ
11. (x * y) = (p^(n + 1) * c1) ∈ ℤ
12. c : ℤ
13. y = (p^n * c) ∈ ℤ
⊢ (p^n * x * c) = (x * y) ∈ ℤ
Latex:
Latex:
.....aux.....
1. p : \mBbbN{}
2. prime(p)
3. n : \mBbbZ{}
4. 0 < n
5. \mforall{}x,y:\mBbbZ{}. ((\mneg{}(p | x)) {}\mRightarrow{} (p\^{}n | (x * y)) {}\mRightarrow{} (p\^{}n | y))
6. x : \mBbbZ{}
7. \mforall{}y:\mBbbZ{}. ((\mneg{}(p | x)) {}\mRightarrow{} (p\^{}n | (x * y)) {}\mRightarrow{} (p\^{}n | y))
8. y : \mBbbZ{}
9. \mneg{}(p | x)
10. c1 : \mBbbZ{}
11. (x * y) = (p\^{}(n + 1) * c1)
12. c : \mBbbZ{}
13. y = (p\^{}n * c)
\mvdash{} (x * c) = (p * c1)
By
Latex:
(Mul \mkleeneopen{}p\^{}n\mkleeneclose{} 0\mcdot{} THEN Auto THEN NthHypEq (-3) THEN EqCD THEN Auto)
Home
Index