---

Step * of Lemma rnexp_wf

∀[k:ℕ]. ∀[x:ℝ].  (x^k ∈ ℝ)
BY
{ ((Auto THEN Unfold `rnexp` 0)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN ((CaseNat 0 `k' THEN Reduce 0) THENL [Auto; (OReduce 0 THENA Auto)])
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Fold `reg-seq-nexp` 0
   THEN (GenConclTerm ⌜reg-seq-nexp(x;k)⌝⋅ THENA Auto)
   THEN MemCD
   THEN Try (Trivial)) }

1
.....subterm..... T:t
1:n
1. k : ℕ
2. x : ℝ
3. ¬(k = 0 ∈ ℤ)
4. v : {f:ℕ+ ⟶ ℤ| (k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1-regular-seq(f)} 
5. reg-seq-nexp(x;k) = v ∈ {f:ℕ+ ⟶ ℤ| (k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1-regular-seq(f)} 
⊢ (k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1 ∈ ℕ+

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbR{}].    (x\^{}k  \mmember{}  \mBbbR{})


By

---

Latex:
((Auto  THEN  Unfold  `rnexp`  0)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  ((CaseNat  0  `k'  THEN  Reduce  0)  THENL  [Auto;  (OReduce  0  THENA  Auto)])
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Fold  `reg-seq-nexp`  0
  THEN  (GenConclTerm  \mkleeneopen{}reg-seq-nexp(x;k)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MemCD
  THEN  Try  (Trivial))

---

Home Index