Step
*
2
of Lemma
reg-seq-nexp_wf
.....set predicate.....
1. x : ℝ
2. k : ℕ+
3. 1 ≤ 2^k - 1
⊢ (k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1-regular-seq(reg-seq-nexp(x;k))
BY
{ ((RWO "exp-fastexp<" 0 THEN Auto)⋅ THEN (GenConclTerm ⌜canon-bnd(x)⌝⋅ THENA Auto)) }
1
1. x : ℝ
2. k : ℕ+
3. 1 ≤ 2^k - 1
4. v : {k:{3...}| ∀n:ℕ+. (|x n| ≤ (n * k))}
5. canon-bnd(x) = v ∈ {k:{3...}| ∀n:ℕ+. (|x n| ≤ (n * k))}
⊢ (k * ((v^(k - 1) ÷ 2^(k - 1)) + 1)) + 1-regular-seq(reg-seq-nexp(x;k))
Latex:
Latex:
.....set predicate.....
1. x : \mBbbR{}
2. k : \mBbbN{}\msupplus{}
3. 1 \mleq{} 2\^{}k - 1
\mvdash{} (k * ((canon-bnd(x)\^{}k - 1 \mdiv{} 2\^{}k - 1) + 1)) + 1-regular-seq(reg-seq-nexp(x;k))
By
Latex:
((RWO "exp-fastexp<" 0 THEN Auto)\mcdot{} THEN (GenConclTerm \mkleeneopen{}canon-bnd(x)\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index