---

Step * of Lemma reg-seq-nexp_wf

No Annotations
∀[x:ℝ]. ∀[k:ℕ+].  (reg-seq-nexp(x;k) ∈ {f:ℕ+ ⟶ ℤ| (k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1-regular-seq(f)} )
BY
{ (Auto THEN (Assert 1 ≤ 2^k - 1 BY (RWO "exp-fastexp<" 0 THEN Auto)) THEN MemTypeCD THEN Auto) }

1
1. x : ℝ
2. k : ℕ+
3. 1 ≤ 2^k - 1
⊢ reg-seq-nexp(x;k) ∈ ℕ+ ⟶ ℤ

2
.....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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
    (reg-seq-nexp(x;k)  \mmember{}  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  (k  *  ((canon-bnd(x)\^{}k  -  1  \mdiv{}  2\^{}k  -  1)  +  1))  +  1-regular-seq(f)\}  )


By

---

Latex:
(Auto  THEN  (Assert  1  \mleq{}  2\^{}k  -  1  BY  (RWO  "exp-fastexp<"  0  THEN  Auto))  THEN  MemTypeCD  THEN  Auto)

---

Home Index