---

Step * 1 of Lemma rnexp-req-iff-even


1. x : ℝ@i
2. y : ℝ@i
⊢ |x| = |y| ⇐⇒ (x * x) = (y * y)
BY
{ ((InstLemma `rnexp-req-iff` [⌜2⌝]⋅ THENA Auto)
   THEN (RWO  "rnexp2" (-1) THENA Auto)
   THEN (RW (AddrC [1] (HypC (-1))) 0 THENA Auto)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. ∀x,y:ℝ.  ((r0 ≤ x) ⇒ (r0 ≤ y) ⇒ (x = y ⇐⇒ (x * x) = (y * y)))
⊢ (|x| * |x|) = (|y| * |y|) ⇐⇒ (x * x) = (y * y)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
\mvdash{}  |x|  =  |y|  \mLeftarrow{}{}\mRightarrow{}  (x  *  x)  =  (y  *  y)


By

---

Latex:
((InstLemma  `rnexp-req-iff`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "rnexp2"  (-1)  THENA  Auto)
  THEN  (RW  (AddrC  [1]  (HypC  (-1)))  0  THENA  Auto))

---

Home Index