---

Step * of Lemma prime-divides-prime

∀p,q:ℤ.  (prime(p) ⇒ prime(q) ⇒ (p | q) ⇒ (p ~ q))
BY
{ ((Auto THEN D 3) THEN (FLemma `divides-prime` [-1] THENM SplitOrHyps) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}p,q:\mBbbZ{}.    (prime(p)  {}\mRightarrow{}  prime(q)  {}\mRightarrow{}  (p  |  q)  {}\mRightarrow{}  (p  \msim{}  q))


By

---

Latex:
((Auto  THEN  D  3)  THEN  (FLemma  `divides-prime`  [-1]  THENM  SplitOrHyps)  THEN  Auto)

---

Home Index