---

Step * 1 2 3 of Lemma rnexp-add


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

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst  \mkleeneopen{}(n  +  m)  -  1  \msim{}  (n  -  1)  +  m\mkleeneclose{}  0\mcdot{}  THEN  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto'
  THEN  nRNorm  0
  THEN  RelRST
  THEN  Auto)\mcdot{}

---

Home Index