---

Step * 1 2 1 of Lemma rnexp-add


1. m : ℕ
2. x : ℝ
3. n : ℤ
4. n ≠ 0
5. 0 < n
6. (x^n - 1 * x^m) = x^(n - 1) + m
7. n = 1 ∈ ℤ
8. (n + m) = 1 ∈ ℤ
⊢ (x * x^m) = x
BY
{ (Subst ⌜m ~ 0⌝ 0⋅ THEN Reduce 0 THEN Auto' THEN nRNorm 0 THEN RelRST THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  x  :  \mBbbR{}
3.  n  :  \mBbbZ{}
4.  n  \mneq{}  0
5.  0  <  n
6.  (x\^{}n  -  1  *  x\^{}m)  =  x\^{}(n  -  1)  +  m
7.  n  =  1
8.  (n  +  m)  =  1
\mvdash{}  (x  *  x\^{}m)  =  x


By

---

Latex:
(Subst  \mkleeneopen{}m  \msim{}  0\mkleeneclose{}  0\mcdot{}  THEN  Reduce  0  THEN  Auto'  THEN  nRNorm  0  THEN  RelRST  THEN  Auto)\mcdot{}

---

Home Index