---

Step * 1 2 2 of Lemma rnexp-add


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

---

Latex:

---

Latex:

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


By

---

Latex:
(Subst'  (n  +  m)  -  1  \msim{}  m  0  THEN  Auto')\mcdot{}

---

Home Index