---

Step * 1 of Lemma rabs-rnexp


1. n : ℤ
2. 0 < n
3. ∀[x:ℝ]. (|x^n - 1| = |x|^n - 1)
4. x : ℝ
⊢ |x^n| = |x|^n
BY
{ ((RWO "rnexp-req" 0 THENA Auto) THEN AutoSplit THEN RWW "rabs-rmul -2" 0 THEN Auto THEN RelRST THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[x:\mBbbR{}].  (|x\^{}n  -  1|  =  |x|\^{}n  -  1)
4.  x  :  \mBbbR{}
\mvdash{}  |x\^{}n|  =  |x|\^{}n


By

---

Latex:
((RWO  "rnexp-req"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  RWW  "rabs-rmul  -2"  0
  THEN  Auto
  THEN  RelRST
  THEN  Auto)\mcdot{}

---

Home Index