---

Step * 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 : {r:ℤ × ℕ+| ratreal(r) = ratreal(a)^n - 1} 
7. ratexp(a;n - 1) = v ∈ {r:ℤ × ℕ+| ratreal(r) = ratreal(a)^n - 1} 
⊢ ratmul(a;v) ∈ {r:ℤ × ℕ+| ratreal(r) = ratreal(a)^n} 
BY
{ ((D -2 THEN DoSubsume THEN Auto)
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN RWW "-1 -5" 0
   THEN Auto) }

1
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

---

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  :  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  ratreal(a)\^{}n  -  1\} 
7.  ratexp(a;n  -  1)  =  v
\mvdash{}  ratmul(a;v)  \mmember{}  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  ratreal(a)\^{}n\} 


By

---

Latex:
((D  -2  THEN  DoSubsume  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  RWW  "-1  -5"  0
  THEN  Auto)

---

Home Index