---

Step * 2 2 2 2 2 1 1 1 of Lemma sparse-signed-rep-lemma1


∀r:ℤ. ((¬(r = 2 ∈ ℤ)) ⇒ (¬(r = (-2) ∈ ℤ)) ⇒ (|r| = 2 ∈ ℤ) ⇒ False)
BY
{ ((D 0 THENA Auto) THEN (RWO "absval_ifthenelse" 0 THENA Auto) THEN SplitOnConclITE THEN Auto') }

---

Latex:

---

Latex:

\mforall{}r:\mBbbZ{}.  ((\mneg{}(r  =  2))  {}\mRightarrow{}  (\mneg{}(r  =  (-2)))  {}\mRightarrow{}  (|r|  =  2)  {}\mRightarrow{}  False)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWO  "absval\_ifthenelse"  0  THENA  Auto)  THEN  SplitOnConclITE  THEN  Auto')

---

Home Index