---

Step * of Lemma ratexp_wf

∀[a:ℤ × ℕ+]. ∀[n:ℕ].  (ratexp(a;n) ∈ {r:ℤ × ℕ+| ratreal(r) = ratreal(a)^n} )
BY
{ (InductionOnNat
   THEN Unfold `ratexp` 0
   THEN Reduce 0
   THEN (((Assert ¬(n = 0 ∈ ℤ) BY
                 Complete (Auto))
          THEN Reduce 0
          THEN (CallByValueReduce 0 THENA Auto)
          THEN (GenConclTerm ⌜ratexp(a;n - 1)⌝⋅ THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto))
   ORELSE ((MemTypeCD THEN Auto) THEN RWO "ratreal-req" 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 : {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} 

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].    (ratexp(a;n)  \mmember{}  \{r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ratreal(r)  =  ratreal(a)\^{}n\}  )


By

---

Latex:
(InductionOnNat
  THEN  Unfold  `ratexp`  0
  THEN  Reduce  0
  THEN  (((Assert  \mneg{}(n  =  0)  BY
                              Complete  (Auto))
                THEN  Reduce  0
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  (GenConclTerm  \mkleeneopen{}ratexp(a;n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto))
  ORELSE  ((MemTypeCD  THEN  Auto)  THEN  RWO  "ratreal-req"  0  THEN  Auto)
  ))

---

Home Index