Step
*
3
1
1
2
1
of Lemma
regularize-k-regular
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ¬↑regular-upto(k;m;f)
5. n : ℕ+
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. (((r((f n) - 2 * k)/r((2 * k) * n)) ≤ (r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k) * seq-min-upper(k;j;f))))
∧ ((r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k) * seq-min-upper(k;j;f))) ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
∧ ((r((f j) - 2 * k)/r((2 * k) * j)) ≤ (r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k) * seq-min-upper(k;j;f))))
∧ ((r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k) * seq-min-upper(k;j;f))) ≤ (r((f j) + (2 * k))/r((2 * k) * j)))
⊢ ∃z@0:ℝ
((((r((k * ((m * ((f seq-min-upper(k;j;f)) + (2 * k))) ÷ seq-min-upper(k;j;f) * k)) - 2 * k)/r((2 * k) * m)) ≤ z@0)
∧ (z@0 ≤ (r((k * ((m * ((f seq-min-upper(k;j;f)) + (2 * k))) ÷ seq-min-upper(k;j;f) * k)) + (2 * k))/r((2 * k)
* m))))
∧ ((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0)
∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
BY
{ (MoveToConcl (-1)
THEN (GenConcl ⌜((f seq-min-upper(k;j;f)) + (2 * k)) = a ∈ ℤ⌝⋅ THENA Auto)
THEN GenConcl ⌜seq-min-upper(k;j;f) = b ∈ ℕ+⌝⋅
THEN Auto) }
1
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ¬↑regular-upto(k;m;f)
5. n : ℕ+
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. a : ℤ
16. ((f seq-min-upper(k;j;f)) + (2 * k)) = a ∈ ℤ
17. b : ℕ+
18. seq-min-upper(k;j;f) = b ∈ ℕ+
19. (r((f n) - 2 * k)/r((2 * k) * n)) ≤ (r(a)/r((2 * k) * b))
20. (r(a)/r((2 * k) * b)) ≤ (r((f n) + (2 * k))/r((2 * k) * n))
21. (r((f j) - 2 * k)/r((2 * k) * j)) ≤ (r(a)/r((2 * k) * b))
22. (r(a)/r((2 * k) * b)) ≤ (r((f j) + (2 * k))/r((2 * k) * j))
⊢ ∃z@0:ℝ
((((r((k * ((m * a) ÷ b * k)) - 2 * k)/r((2 * k) * m)) ≤ z@0)
∧ (z@0 ≤ (r((k * ((m * a) ÷ b * k)) + (2 * k))/r((2 * k) * m))))
∧ ((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0)
∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
Latex:
Latex:
1. k : \mBbbN{}\msupplus{}
2. f : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
3. m : \mBbbN{}\msupplus{}
4. \mneg{}\muparrow{}regular-upto(k;m;f)
5. n : \mBbbN{}\msupplus{}
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)))
15. (((r((f n) - 2 * k)/r((2 * k) * n)) \mleq{} (r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k)
* seq-min-upper(k;j;f))))
\mwedge{} ((r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k) * seq-min-upper(k;j;f))) \mleq{} (r((f n)
+ (2 * k))/r((2 * k) * n))))
\mwedge{} ((r((f j) - 2 * k)/r((2 * k) * j)) \mleq{} (r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k)
* seq-min-upper(k;j;f))))
\mwedge{} ((r((f seq-min-upper(k;j;f)) + (2 * k))/r((2 * k) * seq-min-upper(k;j;f))) \mleq{} (r((f j)
+ (2 * k))/r((2 * k) * j)))
\mvdash{} \mexists{}z@0:\mBbbR{}
((((r((k * ((m * ((f seq-min-upper(k;j;f)) + (2 * k))) \mdiv{} seq-min-upper(k;j;f) * k)) - 2 * k)/r((2
* k)
* m)) \mleq{} z@0)
\mwedge{} (z@0 \mleq{} (r((k * ((m * ((f seq-min-upper(k;j;f)) + (2 * k))) \mdiv{} seq-min-upper(k;j;f) * k))
+ (2 * k))/r((2 * k) * m))))
\mwedge{} ((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))))
By
Latex:
(MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}((f seq-min-upper(k;j;f)) + (2 * k)) = a\mkleeneclose{}\mcdot{} THENA Auto)
THEN GenConcl \mkleeneopen{}seq-min-upper(k;j;f) = b\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index