---

Step * 1 2 of Lemma rnexp-add

.....upcase..... 
1. m : ℕ
2. x : ℝ
3. n : ℤ
4. 0 < n
5. (x^n - 1 * x^m) = x^(n - 1) + m
⊢ (x^n * x^m) = x^n + m
BY
{ ((RW (AddrC [1;1] (LemmaC `rnexp_unroll`)) 0 THENA Auto)
   THEN (RW (AddrC [2] (LemmaC `rnexp_unroll`)) 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN Try (AutoSplit)) }

1
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

2
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)

3
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)

---

Latex:

---

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


By

---

Latex:
((RW  (AddrC  [1;1]  (LemmaC  `rnexp\_unroll`))  0  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (LemmaC  `rnexp\_unroll`))  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Try  (AutoSplit))

---

Home Index