---

Step * 1 of Lemma prime-power-divides-product

.....basecase..... 
1. p : ℕ
2. prime(p)
3. n : ℕ+
⊢ ∀x,y:ℤ.  ((¬(p | x)) ⇒ (p^1 | (x * y)) ⇒ (p^1 | y))
BY
{ ((Subst' p^1 ~ p 0 THENA (RepUR ``exp`` 0 THEN Auto))
   THEN Auto
   THEN (D 2 THEN Auto)
   THEN (Assert (p | x) ∨ (p | y) BY
               (BackThruSomeHyp THEN Auto))
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  p  :  \mBbbN{}
2.  prime(p)
3.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  \mforall{}x,y:\mBbbZ{}.    ((\mneg{}(p  |  x))  {}\mRightarrow{}  (p\^{}1  |  (x  *  y))  {}\mRightarrow{}  (p\^{}1  |  y))


By

---

Latex:
((Subst'  p\^{}1  \msim{}  p  0  THENA  (RepUR  ``exp``  0  THEN  Auto))
  THEN  Auto
  THEN  (D  2  THEN  Auto)
  THEN  (Assert  (p  |  x)  \mvee{}  (p  |  y)  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  D  -1
  THEN  Auto)

---

Home Index