Step
*
3
1
1
2
1
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. 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))))
BY
{ (InstLemma `rational-approx-property` [⌜(r(a))/(2 * k) * b⌝;⌜m⌝]⋅ THENA 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))
23. |(r(a))/(2 * k) * b - ((r(a))/(2 * k) * b within 1/m)| ≤ (r1/r(m))
⊢ ∃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. a : \mBbbZ{}
16. ((f seq-min-upper(k;j;f)) + (2 * k)) = a
17. b : \mBbbN{}\msupplus{}
18. seq-min-upper(k;j;f) = b
19. (r((f n) - 2 * k)/r((2 * k) * n)) \mleq{} (r(a)/r((2 * k) * b))
20. (r(a)/r((2 * k) * b)) \mleq{} (r((f n) + (2 * k))/r((2 * k) * n))
21. (r((f j) - 2 * k)/r((2 * k) * j)) \mleq{} (r(a)/r((2 * k) * b))
22. (r(a)/r((2 * k) * b)) \mleq{} (r((f j) + (2 * k))/r((2 * k) * j))
\mvdash{} \mexists{}z@0:\mBbbR{}
((((r((k * ((m * a) \mdiv{} b * k)) - 2 * k)/r((2 * k) * m)) \mleq{} z@0)
\mwedge{} (z@0 \mleq{} (r((k * ((m * a) \mdiv{} b * 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:
(InstLemma `rational-approx-property` [\mkleeneopen{}(r(a))/(2 * k) * b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index