---

Step * of Lemma assoced-prime

∀p,q:ℤ.  ((p ~ q) ⇒ prime(p) ⇒ prime(q))
BY
{ (Auto THEN (RWO "assoced_elim" (-2) THENA Auto) THEN D -2 THEN HypSubst' (-2) (-1) THEN Auto THEN ThinVar `p') }

1
1. q : ℤ
2. prime(-q)
⊢ prime(q)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWO  "assoced\_elim"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  HypSubst'  (-2)  (-1)
  THEN  Auto
  THEN  ThinVar  `p')

---

Home Index