---

Step * of Lemma positive-prime-divides-prime

∀[p,q:ℕ].  (p = q ∈ ℕ) supposing ((p | q) and prime(q) and prime(p))
BY
{ (InstLemma `prime-divides-prime` [] THEN RepeatFor 5 (ParallelLast)) }

1
1. ∀p,q:ℤ.  (prime(p) ⇒ prime(q) ⇒ (p | q) ⇒ (p ~ q))
2. p : ℕ
3. ∀q:ℤ. (prime(p) ⇒ prime(q) ⇒ (p | q) ⇒ (p ~ q))
4. q : ℕ
5. prime(p)
6. prime(q)
7. p | q
8. p ~ q
⊢ p = q ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[p,q:\mBbbN{}].    (p  =  q)  supposing  ((p  |  q)  and  prime(q)  and  prime(p))


By

---

Latex:
(InstLemma  `prime-divides-prime`  []  THEN  RepeatFor  5  (ParallelLast))

---

Home Index