---

Step * of Lemma rnexp-req-iff-even

∀n:ℕ+. ∀x,y:ℝ.  ((↑isEven(n)) ⇒ (|x| = |y| ⇐⇒ x^n = y^n))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (RWO "assert-isEven" (-1) THENA Auto)
   THEN ExRepD
   THEN HypSubst' (-1) 0
   THEN (RWW "rnexp-mul< rnexp2" 0 THENA Auto)
   THEN (RWO "rnexp-req-iff<" 0 THENA Auto)
   THEN All Thin) }

1
1. x : ℝ@i
2. y : ℝ@i
⊢ |x| = |y| ⇐⇒ (x * x) = (y * y)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbR{}.    ((\muparrow{}isEven(n))  {}\mRightarrow{}  (|x|  =  |y|  \mLeftarrow{}{}\mRightarrow{}  x\^{}n  =  y\^{}n))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (RWO  "assert-isEven"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  (RWW  "rnexp-mul<  rnexp2"  0  THENA  Auto)
  THEN  (RWO  "rnexp-req-iff<"  0  THENA  Auto)
  THEN  All  Thin)

---

Home Index