---

Step * of Lemma prime-power-divides-product

No Annotations
∀p:ℕ. (prime(p) ⇒ (∀n:ℕ+. ∀x,y:ℤ.  ((¬(p | x)) ⇒ (p^n | (x * y)) ⇒ (p^n | y))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN InductionOnNat) }

1
.....basecase..... 
1. p : ℕ
2. prime(p)
3. n : ℕ+
⊢ ∀x,y:ℤ.  ((¬(p | x)) ⇒ (p^1 | (x * y)) ⇒ (p^1 | y))

2
.....upcase..... 
1. p : ℕ
2. prime(p)
3. n : ℤ
4. 0 < n
5. ∀x,y:ℤ.  ((¬(p | x)) ⇒ (p^n | (x * y)) ⇒ (p^n | y))
⊢ ∀x,y:ℤ.  ((¬(p | x)) ⇒ (p^(n + 1) | (x * y)) ⇒ (p^(n + 1) | y))

---

Latex:

---

Latex:
No  Annotations
\mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbZ{}.    ((\mneg{}(p  |  x))  {}\mRightarrow{}  (p\^{}n  |  (x  *  y))  {}\mRightarrow{}  (p\^{}n  |  y))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  InductionOnNat)

---

Home Index