Step
*
2
1
of Lemma
regularize-k-regular
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. m : ℕ+
5. ¬↑regular-upto(k;m;f)
6. ↑regular-upto(k;n;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
14. ∀n,m:ℕ+j + 1.
let j = seq-min-upper(k;j;f) in
let z = (r((f j) + (2 * k))/r((2 * k) * j)) in
(((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z)
∧ (z ≤ (r((f m) + (2 * k))/r((2 * k) * m)))
⊢ ∃z@0:ℝ
((((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0) ∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r(eval j = seq-min-upper(k;j;f) in
k * ((m * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * m)) ≤ z@0)
∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * m))))
BY
{ (InstHyp [⌜n⌝;⌜j⌝] (-1)⋅ THENA Auto) }
1
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. m : ℕ+
6. ¬↑regular-upto(k;m;f)
7. ↑regular-upto(k;n;f)
8. v : ℕ
9. ¬↑regular-upto(k;v;f)
10. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
11. ¬(v = 1 ∈ ℤ)
12. ¬(v = 0 ∈ ℤ)
13. j : ℕ+
14. (v - 1) = j ∈ ℕ+
15. ∀n,m:ℕ+j + 1.
let j = seq-min-upper(k;j;f) in
let z = (r((f j) + (2 * k))/r((2 * k) * j)) in
(((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z)
∧ (z ≤ (r((f m) + (2 * k))/r((2 * k) * m)))
⊢ n < j + 1
2
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. n : ℕ+
4. m : ℕ+
5. ¬↑regular-upto(k;m;f)
6. ↑regular-upto(k;n;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
14. ∀n,m:ℕ+j + 1.
let j = seq-min-upper(k;j;f) in
let z = (r((f j) + (2 * k))/r((2 * k) * j)) in
(((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z)
∧ (z ≤ (r((f m) + (2 * k))/r((2 * k) * m)))
15. let j@0 = seq-min-upper(k;j;f) in
let z = (r((f j@0) + (2 * k))/r((2 * k) * j@0)) in
(((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r((f j) - 2 * k)/r((2 * k) * j)) ≤ z)
∧ (z ≤ (r((f j) + (2 * k))/r((2 * k) * j)))
⊢ ∃z@0:ℝ
((((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0) ∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r(eval j = seq-min-upper(k;j;f) in
k * ((m * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * m)) ≤ z@0)
∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * m))))
Latex:
Latex:
1. k : \mBbbN{}\msupplus{}
2. f : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
3. n : \mBbbN{}\msupplus{}
4. m : \mBbbN{}\msupplus{}
5. \mneg{}\muparrow{}regular-upto(k;m;f)
6. \muparrow{}regular-upto(k;n;f)
7. v : \mBbbN{}
8. \mneg{}\muparrow{}regular-upto(k;v;f)
9. \mforall{}[i:\mBbbN{}]. \mneg{}\mneg{}\muparrow{}regular-upto(k;i;f) supposing i < v
10. \mneg{}(v = 1)
11. \mneg{}(v = 0)
12. j : \mBbbN{}\msupplus{}
13. (v - 1) = j
14. \mforall{}n,m:\mBbbN{}\msupplus{}j + 1.
let j = seq-min-upper(k;j;f) in
let z = (r((f j) + (2 * k))/r((2 * k) * j)) in
(((r((f n) - 2 * k)/r((2 * k) * n)) \mleq{} z) \mwedge{} (z \mleq{} (r((f n) + (2 * k))/r((2 * k) * n))))
\mwedge{} ((r((f m) - 2 * k)/r((2 * k) * m)) \mleq{} z)
\mwedge{} (z \mleq{} (r((f m) + (2 * k))/r((2 * k) * m)))
\mvdash{} \mexists{}z@0:\mBbbR{}
((((r((f n) - 2 * k)/r((2 * k) * n)) \mleq{} z@0) \mwedge{} (z@0 \mleq{} (r((f n) + (2 * k))/r((2 * k) * n))))
\mwedge{} ((r(eval j = seq-min-upper(k;j;f) in
k * ((m * ((f j) + (2 * k))) \mdiv{} j * k) - 2 * k)/r((2 * k) * m)) \mleq{} z@0)
\mwedge{} (z@0 \mleq{} (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) \mdiv{} j * k) + (2 * k))/r((\000C2 * k)
* m))))
By
Latex:
(InstHyp [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
Home
Index