---

Step * 1 1 of Lemma ratexp_wf


1. a : ℤ × ℕ+
2. n : ℤ
3. 0 < n
4. ratexp(a;n - 1) ∈ {r:ℤ × ℕ+| ratreal(r) = ratreal(a)^n - 1} 
5. ¬(n = 0 ∈ ℤ)
6. v : ℤ × ℕ+
7. ratreal(v) = ratreal(a)^n - 1
8. ratexp(a;n - 1) = v ∈ {r:ℤ × ℕ+| ratreal(r) = ratreal(a)^n - 1} 
9. ratmul(a;v) = ratmul(a;v) ∈ {r:ℤ × ℕ+| ratreal(r) = (ratreal(a) * ratreal(v))} 
10. x : ℤ × ℕ+
11. ratreal(x) = (ratreal(a) * ratreal(v))
⊢ (ratreal(a) * ratreal(a)^n - 1) = ratreal(a)^n
BY
{ (RWO "rmul_comm" 0 THEN Auto THEN RWO "rnexp_step<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  ratexp(a;n  -  1)  \mmember{}  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  ratreal(a)\^{}n  -  1\} 
5.  \mneg{}(n  =  0)
6.  v  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
7.  ratreal(v)  =  ratreal(a)\^{}n  -  1
8.  ratexp(a;n  -  1)  =  v
9.  ratmul(a;v)  =  ratmul(a;v)
10.  x  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
11.  ratreal(x)  =  (ratreal(a)  *  ratreal(v))
\mvdash{}  (ratreal(a)  *  ratreal(a)\^{}n  -  1)  =  ratreal(a)\^{}n


By

---

Latex:
(RWO  "rmul\_comm"  0  THEN  Auto  THEN  RWO  "rnexp\_step<"  0  THEN  Auto)

---

Home Index