---

Step * 1 of Lemma positive-prime-divides-prime


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 ∈ ℕ
BY
{ (RWO "assoced_nelim" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}p,q:\mBbbZ{}.    (prime(p)  {}\mRightarrow{}  prime(q)  {}\mRightarrow{}  (p  |  q)  {}\mRightarrow{}  (p  \msim{}  q))
2.  p  :  \mBbbN{}
3.  \mforall{}q:\mBbbZ{}.  (prime(p)  {}\mRightarrow{}  prime(q)  {}\mRightarrow{}  (p  |  q)  {}\mRightarrow{}  (p  \msim{}  q))
4.  q  :  \mBbbN{}
5.  prime(p)
6.  prime(q)
7.  p  |  q
8.  p  \msim{}  q
\mvdash{}  p  =  q


By

---

Latex:
(RWO  "assoced\_nelim"  (-1)  THEN  Auto)

---

Home Index