| Step | Hyp | Ref
| Expression |
| 1 | | uzssz 12899 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 2 | | zssre 12620 |
. . . . . 6
⊢ ℤ
⊆ ℝ |
| 3 | 1, 2 | sstri 3993 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆ ℝ) |
| 5 | | ioodvbdlimc1lem2.m |
. . . . . . 7
⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1) |
| 6 | | ioodvbdlimc1lem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 7 | | ioodvbdlimc1lem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 8 | 6, 7 | resubcld 11691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
| 9 | | ioodvbdlimc1lem2.altb |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
| 10 | 7, 6 | posdifd 11850 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
| 11 | 9, 10 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
| 12 | 11 | gt0ne0d 11827 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
| 13 | 8, 12 | rereccld 12094 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ) |
| 14 | | 0red 11264 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
| 15 | 8, 11 | recgt0d 12202 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴))) |
| 16 | 14, 13, 15 | ltled 11409 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴))) |
| 17 | | flge0nn0 13860 |
. . . . . . . . 9
⊢ (((1 /
(𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤
(1 / (𝐵 − 𝐴))) → (⌊‘(1 /
(𝐵 − 𝐴))) ∈
ℕ0) |
| 18 | 13, 16, 17 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈
ℕ0) |
| 19 | | peano2nn0 12566 |
. . . . . . . 8
⊢
((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ0 →
((⌊‘(1 / (𝐵
− 𝐴))) + 1) ∈
ℕ0) |
| 20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℕ0) |
| 21 | 5, 20 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 22 | 21 | nn0zd 12639 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 23 | | eqid 2737 |
. . . . . 6
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
| 24 | 23 | uzsup 13903 |
. . . . 5
⊢ (𝑀 ∈ ℤ →
sup((ℤ≥‘𝑀), ℝ*, < ) =
+∞) |
| 25 | 22, 24 | syl 17 |
. . . 4
⊢ (𝜑 →
sup((ℤ≥‘𝑀), ℝ*, < ) =
+∞) |
| 26 | | ioodvbdlimc1lem2.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 28 | 7 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈
ℝ*) |
| 30 | 6 | rexrd 11311 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈
ℝ*) |
| 32 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
| 33 | | eluzelre 12889 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℝ) |
| 34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ ℝ) |
| 35 | | 0red 11264 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 ∈
ℝ) |
| 36 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 0 ∈ ℝ) |
| 37 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 1 ∈ ℝ) |
| 38 | 36, 37 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (0 + 1) ∈
ℝ) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ∈
ℝ) |
| 40 | 36 | ltp1d 12198 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 0 < (0 + 1)) |
| 41 | 40 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 < (0 +
1)) |
| 42 | | eluzel2 12883 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 43 | 42 | zred 12722 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
| 45 | 13 | flcld 13838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ) |
| 46 | 45 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ) |
| 47 | | 1red 11262 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) |
| 48 | 18 | nn0ge0d 12590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (⌊‘(1 /
(𝐵 − 𝐴)))) |
| 49 | 14, 46, 47, 48 | leadd1dd 11877 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + 1) ≤
((⌊‘(1 / (𝐵
− 𝐴))) +
1)) |
| 50 | 49, 5 | breqtrrdi 5185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 + 1) ≤ 𝑀) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ≤ 𝑀) |
| 52 | | eluzle 12891 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑗) |
| 54 | 39, 44, 34, 51, 53 | letrd 11418 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ≤ 𝑗) |
| 55 | 35, 39, 34, 41, 54 | ltletrd 11421 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 < 𝑗) |
| 56 | 55 | gt0ne0d 11827 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ≠ 0) |
| 57 | 34, 56 | rereccld 12094 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ∈
ℝ) |
| 58 | 32, 57 | readdcld 11290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ) |
| 59 | 34, 55 | elrpd 13074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ ℝ+) |
| 60 | 59 | rpreccld 13087 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ∈
ℝ+) |
| 61 | 32, 60 | ltaddrpd 13110 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗))) |
| 62 | 21 | nn0red 12588 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 63 | 14, 47 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + 1) ∈
ℝ) |
| 64 | 46, 47 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℝ) |
| 65 | 14 | ltp1d 12198 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (0 +
1)) |
| 66 | 14, 63, 64, 65, 49 | ltletrd 11421 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((⌊‘(1
/ (𝐵 − 𝐴))) + 1)) |
| 67 | 66, 5 | breqtrrdi 5185 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑀) |
| 68 | 67 | gt0ne0d 11827 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≠ 0) |
| 69 | 62, 68 | rereccld 12094 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
| 70 | 69 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑀) ∈ ℝ) |
| 71 | 32, 70 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ) |
| 72 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈ ℝ) |
| 73 | 62, 67 | elrpd 13074 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
| 74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈
ℝ+) |
| 75 | | 1red 11262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 1 ∈
ℝ) |
| 76 | | 0le1 11786 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
| 77 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 ≤
1) |
| 78 | 74, 59, 75, 77, 53 | lediv2ad 13099 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀)) |
| 79 | 57, 70, 32, 78 | leadd2dd 11878 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀))) |
| 80 | 5 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢
((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀 |
| 81 | 80 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (1 /
((⌊‘(1 / (𝐵
− 𝐴))) + 1)) = (1 /
𝑀) |
| 82 | 81, 69 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) ∈
ℝ) |
| 83 | 13, 15 | elrpd 13074 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈
ℝ+) |
| 84 | 64, 66 | elrpd 13074 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℝ+) |
| 85 | | 1rp 13038 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
| 86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ+) |
| 87 | | fllelt 13837 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
(𝐵 − 𝐴)) ∈ ℝ →
((⌊‘(1 / (𝐵
− 𝐴))) ≤ (1 /
(𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
| 88 | 13, 87 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
| 89 | 88 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) |
| 90 | 83, 84, 86, 89 | ltdiv2dd 45306 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴)))) |
| 91 | 8 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
| 92 | 91, 12 | recrecd 12040 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴)) |
| 93 | 90, 92 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴)) |
| 94 | 82, 8, 7, 93 | ltadd2dd 11420 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) < (𝐴 + (𝐵 − 𝐴))) |
| 95 | 5 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (1 /
𝑀) = (1 /
((⌊‘(1 / (𝐵
− 𝐴))) +
1)) |
| 96 | 95 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
| 97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))) |
| 98 | 7 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 99 | 6 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 100 | 98, 99 | pncan3d 11623 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
| 101 | 100 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = (𝐴 + (𝐵 − 𝐴))) |
| 102 | 94, 97, 101 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵) |
| 103 | 102 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵) |
| 104 | 58, 71, 72, 79, 103 | lelttrd 11419 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵) |
| 105 | 29, 31, 58, 61, 104 | eliood 45511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
| 106 | 27, 105 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) |
| 107 | | ioodvbdlimc1lem2.s |
. . . . 5
⊢ 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) |
| 108 | 106, 107 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝑆:(ℤ≥‘𝑀)⟶ℝ) |
| 109 | | ioodvbdlimc1lem2.dmdv |
. . . . . 6
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 110 | | ioodvbdlimc1lem2.dvbd |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) |
| 111 | 7, 6, 9, 26, 109, 110 | dvbdfbdioo 45945 |
. . . . 5
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) |
| 112 | 62 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ) |
| 113 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 114 | 107 | fvmpt2 7027 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈
(ℤ≥‘𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗)))) |
| 115 | 113, 106,
114 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗)))) |
| 116 | 115 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗))))) |
| 117 | 116 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗))))) |
| 118 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) |
| 119 | 105 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
| 120 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗))))) |
| 121 | 120 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)) |
| 122 | 121 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏) |
| 123 | 118, 119,
122 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏) |
| 124 | 117, 123 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏) |
| 125 | 124 | a1d 25 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
| 126 | 125 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
| 127 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗)) |
| 128 | 127 | imbi1d 341 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
| 129 | 128 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
| 130 | 129 | rspcev 3622 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
∀𝑗 ∈
(ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
| 131 | 112, 126,
130 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
| 132 | 131 | ex 412 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
| 133 | 132 | reximdv 3170 |
. . . . 5
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
| 134 | 111, 133 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
| 135 | 4, 25, 108, 134 | limsupre 45656 |
. . 3
⊢ (𝜑 → (lim sup‘𝑆) ∈
ℝ) |
| 136 | 135 | recnd 11289 |
. 2
⊢ (𝜑 → (lim sup‘𝑆) ∈
ℂ) |
| 137 | | eluzelre 12889 |
. . . . . . . . 9
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑗 ∈ ℝ) |
| 138 | 137 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ) |
| 139 | | 0red 11264 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ∈ ℝ) |
| 140 | 45 | peano2zd 12725 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℤ) |
| 141 | 5, 140 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 142 | 141 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
| 143 | 142 | zred 12722 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℝ) |
| 144 | 143 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈ ℝ) |
| 145 | 67 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < 𝑀) |
| 146 | | ioodvbdlimc1lem2.n |
. . . . . . . . . . . . . 14
⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) |
| 147 | | ioodvbdlimc1lem2.y |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) |
| 148 | | ioomidp 45527 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
| 149 | 7, 6, 9, 148 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
| 150 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
| 151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅) |
| 152 | | ioossre 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
| 154 | | dvfre 25989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 155 | 26, 153, 154 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
| 156 | 109 | feq2d 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
| 157 | 155, 156 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
| 158 | 157 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
| 159 | 158 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
| 160 | 159 | abscld 15475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ) |
| 161 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) |
| 162 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ sup(ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) |
| 163 | 151, 160,
110, 161, 162 | suprnmpt 45179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧
∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))) |
| 164 | 163 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈
ℝ) |
| 165 | 147, 164 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 166 | 165 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑌 ∈
ℝ) |
| 167 | | rpre 13043 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 168 | 167 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ) |
| 169 | 168 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ) |
| 170 | 167 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
| 171 | 170 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
| 172 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) |
| 173 | | rpne0 13051 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
| 174 | 173 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
| 175 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
| 176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ≠
0) |
| 177 | 171, 172,
174, 176 | divne0d 12059 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0) |
| 178 | 166, 169,
177 | redivcld 12095 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
| 179 | 178 | flcld 13838 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(𝑌 / (𝑥 / 2))) ∈
ℤ) |
| 180 | 179 | peano2zd 12725 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈
ℤ) |
| 181 | 180, 142 | ifcld 4572 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ) |
| 182 | 146, 181 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℤ) |
| 183 | 182 | zred 12722 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℝ) |
| 184 | 183 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℝ) |
| 185 | 180 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈
ℝ) |
| 186 | | max1 13227 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
→ 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
| 187 | 143, 185,
186 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
| 188 | 187, 146 | breqtrrdi 5185 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ≤ 𝑁) |
| 189 | 188 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ≤ 𝑁) |
| 190 | | eluzle 12891 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑗) |
| 191 | 190 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ 𝑗) |
| 192 | 144, 184,
138, 189, 191 | letrd 11418 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ≤ 𝑗) |
| 193 | 139, 144,
138, 145, 192 | ltletrd 11421 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < 𝑗) |
| 194 | 193 | gt0ne0d 11827 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ≠ 0) |
| 195 | 138, 194 | rereccld 12094 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / 𝑗) ∈ ℝ) |
| 196 | 138, 193 | recgt0d 12202 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < (1 / 𝑗)) |
| 197 | 195, 196 | elrpd 13074 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / 𝑗) ∈
ℝ+) |
| 198 | 197 | adantr 480 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈
ℝ+) |
| 199 | | ioodvbdlimc1lem2.ch |
. . . . . . . . 9
⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) |
| 200 | 199 | biimpi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) |
| 201 | | simp-5l 785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝜑) |
| 202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝜑) |
| 203 | 202, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
| 204 | 200 | simplrd 770 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵)) |
| 205 | 203, 204 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ) |
| 206 | 205 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ) |
| 207 | 202, 108 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑆:(ℤ≥‘𝑀)⟶ℝ) |
| 208 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+) |
| 209 | 200, 208 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑥 ∈ ℝ+) |
| 210 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
| 211 | 142, 182,
188, 210 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘𝑀)) |
| 212 | 202, 209,
211 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 213 | | uzss 12901 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
| 214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
| 215 | | simp-4r 784 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ≥‘𝑁)) |
| 216 | 200, 215 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝑗 ∈ (ℤ≥‘𝑁)) |
| 217 | 214, 216 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 218 | 207, 217 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ) |
| 219 | 218 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ) |
| 220 | 202, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (lim sup‘𝑆) ∈
ℂ) |
| 221 | 206, 219,
220 | npncand 11644 |
. . . . . . . . . . . 12
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆))) |
| 222 | 221 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) |
| 223 | 222 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))) |
| 224 | 205, 218 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ) |
| 225 | 202, 135 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (lim sup‘𝑆) ∈
ℝ) |
| 226 | 218, 225 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ) |
| 227 | 224, 226 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ) |
| 228 | 227 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ) |
| 229 | 228 | abscld 15475 |
. . . . . . . . . . 11
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ) |
| 230 | 224 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ) |
| 231 | 230 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ) |
| 232 | 226 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ) |
| 233 | 232 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ) |
| 234 | 231, 233 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ) |
| 235 | 209 | rpred 13077 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑥 ∈ ℝ) |
| 236 | 230, 232 | abstrid 15495 |
. . . . . . . . . . 11
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))))) |
| 237 | 235 | rehalfcld 12513 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝑥 / 2) ∈ ℝ) |
| 238 | 206, 219 | abssubd 15492 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝑆‘𝑗) − (𝐹‘𝑧)))) |
| 239 | 202, 217,
115 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗)))) |
| 240 | 239 | fvoveq1d 7453 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)))) |
| 241 | 202, 217,
106 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) |
| 242 | 241, 205 | resubcld 11691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℝ) |
| 243 | 242 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℂ) |
| 244 | 243 | abscld 15475 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ∈ ℝ) |
| 245 | 202, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑌 ∈ ℝ) |
| 246 | 202, 217,
58 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ) |
| 247 | 152, 204 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑧 ∈ ℝ) |
| 248 | 246, 247 | resubcld 11691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ) |
| 249 | 245, 248 | remulcld 11291 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ) |
| 250 | 202, 7 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝐴 ∈ ℝ) |
| 251 | 202, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝐵 ∈ ℝ) |
| 252 | 202, 109 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
| 253 | 163 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
| 254 | 147 | breq2i 5151 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
| 255 | 254 | ralbii 3093 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
| 256 | 253, 255 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
| 257 | 202, 256 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
| 258 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥))) |
| 259 | 258 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)) |
| 260 | 259 | cbvralvw 3237 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑤 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
| 261 | 257, 260 | sylibr 234 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌) |
| 262 | 247 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝑧 ∈ ℝ*) |
| 263 | 202, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝐵 ∈
ℝ*) |
| 264 | 247, 250 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℝ) |
| 265 | 264 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℂ) |
| 266 | 265 | abscld 15475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) ∈ ℝ) |
| 267 | 3, 217 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑗 ∈ ℝ) |
| 268 | 202, 217,
56 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑗 ≠ 0) |
| 269 | 267, 268 | rereccld 12094 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (1 / 𝑗) ∈ ℝ) |
| 270 | 264 | leabsd 15453 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑧 − 𝐴) ≤ (abs‘(𝑧 − 𝐴))) |
| 271 | 200 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) |
| 272 | 264, 266,
269, 270, 271 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑧 − 𝐴) < (1 / 𝑗)) |
| 273 | 247, 250,
269 | ltsubadd2d 11861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝑧 − 𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗)))) |
| 274 | 272, 273 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝑧 < (𝐴 + (1 / 𝑗))) |
| 275 | 202, 217,
104 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵) |
| 276 | 262, 263,
246, 274, 275 | eliood 45511 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵)) |
| 277 | 250, 251,
203, 252, 245, 261, 204, 276 | dvbdfbdioolem1 45943 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · (𝐵 − 𝐴)))) |
| 278 | 277 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧))) |
| 279 | 202, 217,
57 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (1 / 𝑗) ∈ ℝ) |
| 280 | 245, 279 | remulcld 11291 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
| 281 | 157, 149 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
| 282 | 281 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
| 283 | 282 | abscld 15475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
| 284 | 282 | absge0d 15483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
| 285 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
| 286 | 147 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ sup(ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌 |
| 287 | 286 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌) |
| 288 | 285, 287 | breq12d 5156 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)) |
| 289 | 288 | rspcva 3620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) →
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌) |
| 290 | 149, 253,
289 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌) |
| 291 | 14, 283, 165, 284, 290 | letrd 11418 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 𝑌) |
| 292 | 202, 291 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 0 ≤ 𝑌) |
| 293 | 202, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝐴 ∈
ℝ*) |
| 294 | | ioogtlb 45508 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑧
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧) |
| 295 | 293, 263,
204, 294 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 𝐴 < 𝑧) |
| 296 | 250, 247,
246, 295 | ltsub2dd 11876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴)) |
| 297 | 202, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 𝐴 ∈ ℂ) |
| 298 | 279 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (1 / 𝑗) ∈ ℂ) |
| 299 | 297, 298 | pncan2d 11622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗)) |
| 300 | 296, 299 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗)) |
| 301 | 248, 269,
300 | ltled 11409 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗)) |
| 302 | 248, 269,
245, 292, 301 | lemul2ad 12208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗))) |
| 303 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
| 304 | 237 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ) |
| 305 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗))) |
| 306 | 298 | mul02d 11459 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (0 · (1 / 𝑗)) = 0) |
| 307 | 305, 306 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0) |
| 308 | 209 | rphalfcld 13089 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑥 / 2) ∈
ℝ+) |
| 309 | 308 | rpgt0d 13080 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 0 < (𝑥 / 2)) |
| 310 | 309 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2)) |
| 311 | 307, 310 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2)) |
| 312 | 303, 304,
311 | ltled 11409 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
| 313 | 245 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ) |
| 314 | 292 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌) |
| 315 | | neqne 2948 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑌 = 0 → 𝑌 ≠ 0) |
| 316 | 315 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0) |
| 317 | 313, 314,
316 | ne0gt0d 11398 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌) |
| 318 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
| 319 | 3, 212 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ∈ ℝ) |
| 320 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 0 ∈
ℝ) |
| 321 | 202, 209,
143 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 𝑀 ∈ ℝ) |
| 322 | 202, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 0 < 𝑀) |
| 323 | 202, 209,
188 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 𝑀 ≤ 𝑁) |
| 324 | 320, 321,
319, 322, 323 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → 0 < 𝑁) |
| 325 | 324 | gt0ne0d 11827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ≠ 0) |
| 326 | 319, 325 | rereccld 12094 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (1 / 𝑁) ∈ ℝ) |
| 327 | 245, 326 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ) |
| 328 | 327 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ) |
| 329 | 237 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ) |
| 330 | 279 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ) |
| 331 | 326 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ) |
| 332 | 245 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ) |
| 333 | 292 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌) |
| 334 | 319, 324 | elrpd 13074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ∈
ℝ+) |
| 335 | 202, 217,
59 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑗 ∈ ℝ+) |
| 336 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 1 ∈
ℝ) |
| 337 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 0 ≤ 1) |
| 338 | 216, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ≤ 𝑗) |
| 339 | 334, 335,
336, 337, 338 | lediv2ad 13099 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁)) |
| 340 | 339 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁)) |
| 341 | 330, 331,
332, 333, 340 | lemul2ad 12208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁))) |
| 342 | 235 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑥 ∈ ℂ) |
| 343 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 2 ∈
ℂ) |
| 344 | 209 | rpne0d 13082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑥 ≠ 0) |
| 345 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 2 ≠ 0) |
| 346 | 342, 343,
344, 345 | divne0d 12059 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → (𝑥 / 2) ≠ 0) |
| 347 | 245, 237,
346 | redivcld 12095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
| 348 | 347 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
| 349 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌) |
| 350 | 309 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2)) |
| 351 | 332, 329,
349, 350 | divgt0d 12203 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2))) |
| 352 | 348, 351 | elrpd 13074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈
ℝ+) |
| 353 | 352 | rprecred 13088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ) |
| 354 | 334 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈
ℝ+) |
| 355 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ) |
| 356 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1) |
| 357 | 347 | flcld 13838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ) |
| 358 | 357 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ) |
| 359 | 358 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) |
| 360 | 202, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜒 → 𝑀 ∈ ℤ) |
| 361 | 358, 360 | ifcld 4572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ) |
| 362 | 146, 361 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑁 ∈ ℤ) |
| 363 | 362 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 𝑁 ∈ ℝ) |
| 364 | | flltp1 13840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1)) |
| 365 | 347, 364 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1)) |
| 366 | 202, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → 𝑀 ∈ ℝ) |
| 367 | | max2 13229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
→ ((⌊‘(𝑌 /
(𝑥 / 2))) + 1) ≤
if(𝑀 ≤
((⌊‘(𝑌 / (𝑥 / 2))) + 1),
((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
| 368 | 366, 359,
367 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
| 369 | 368, 146 | breqtrrdi 5185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁) |
| 370 | 347, 359,
363, 365, 369 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁) |
| 371 | 347, 319,
370 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁) |
| 372 | 371 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁) |
| 373 | 352, 354,
355, 356, 372 | lediv2ad 13099 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2)))) |
| 374 | 331, 353,
332, 333, 373 | lemul2ad 12208 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2))))) |
| 375 | 332 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ) |
| 376 | 348 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ) |
| 377 | 351 | gt0ne0d 11827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0) |
| 378 | 375, 376,
377 | divrecd 12046 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2))))) |
| 379 | 329 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ) |
| 380 | 349 | gt0ne0d 11827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0) |
| 381 | 346 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0) |
| 382 | 375, 379,
380, 381 | ddcand 12063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2)) |
| 383 | 378, 382 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2)) |
| 384 | 374, 383 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2)) |
| 385 | 318, 328,
329, 341, 384 | letrd 11418 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
| 386 | 317, 385 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
| 387 | 312, 386 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
| 388 | 249, 280,
237, 302, 387 | letrd 11418 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2)) |
| 389 | 244, 249,
237, 278, 388 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑥 / 2)) |
| 390 | 240, 389 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) ≤ (𝑥 / 2)) |
| 391 | 238, 390 | eqbrtrd 5165 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2)) |
| 392 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
| 393 | 200, 392 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
| 394 | 231, 233,
237, 237, 391, 393 | leltaddd 11885 |
. . . . . . . . . . . 12
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2))) |
| 395 | 342 | 2halvesd 12512 |
. . . . . . . . . . . 12
⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥) |
| 396 | 394, 395 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥) |
| 397 | 229, 234,
235, 236, 396 | lelttrd 11419 |
. . . . . . . . . 10
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥) |
| 398 | 223, 397 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
| 399 | 199, 398 | sylbir 235 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
| 400 | 399 | adantrl 716 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
| 401 | 400 | ex 412 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
| 402 | 401 | ralrimiva 3146 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
| 403 | | brimralrspcev 5204 |
. . . . 5
⊢ (((1 /
𝑗) ∈
ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
| 404 | 198, 402,
403 | syl2anc 584 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
| 405 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁) |
| 406 | 405 | iftrued 4533 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁) |
| 407 | | uzid 12893 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
| 408 | 182, 407 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘𝑁)) |
| 409 | 408 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ≥‘𝑁)) |
| 410 | 406, 409 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
| 411 | 410 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
| 412 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏) |
| 413 | 412 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏) |
| 414 | 182 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ) |
| 415 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ) |
| 416 | 414 | zred 12722 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ) |
| 417 | 415 | zred 12722 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ) |
| 418 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁) |
| 419 | 416, 417 | ltnled 11408 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁)) |
| 420 | 418, 419 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 < 𝑏) |
| 421 | 416, 417,
420 | ltled 11409 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏) |
| 422 | | eluz2 12884 |
. . . . . . . . . 10
⊢ (𝑏 ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏)) |
| 423 | 414, 415,
421, 422 | syl3anbrc 1344 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ≥‘𝑁)) |
| 424 | 413, 423 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
| 425 | 411, 424 | pm2.61dan 813 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
| 426 | 425 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
| 427 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 428 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
| 429 | 182 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈
ℤ) |
| 430 | 429, 428 | ifcld 4572 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ) |
| 431 | 428 | zred 12722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℝ) |
| 432 | 429 | zred 12722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈
ℝ) |
| 433 | | max1 13227 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) |
| 434 | 431, 432,
433 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) |
| 435 | | eluz2 12884 |
. . . . . . . . . 10
⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
| 436 | 428, 430,
434, 435 | syl3anbrc 1344 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) |
| 437 | 436 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) |
| 438 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
| 439 | 438 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ)) |
| 440 | 438 | fvoveq1d 7453 |
. . . . . . . . . . 11
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))) |
| 441 | 440 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 442 | 439, 441 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
| 443 | 442 | rspccva 3621 |
. . . . . . . 8
⊢
((∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 444 | 427, 437,
443 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 445 | 444 | simprd 495 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) |
| 446 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
| 447 | 446 | fvoveq1d 7453 |
. . . . . . . 8
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))) |
| 448 | 447 | breq1d 5153 |
. . . . . . 7
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 449 | 448 | rspcev 3622 |
. . . . . 6
⊢
((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
| 450 | 426, 445,
449 | syl2anc 584 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
| 451 | | ax-resscn 11212 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
| 452 | 451 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 453 | 26, 452 | fssd 6753 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
| 454 | | dvcn 25957 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 455 | 452, 453,
153, 109, 454 | syl31anc 1375 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 456 | | cncfcdm 24924 |
. . . . . . . . . . . . 13
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
| 457 | 452, 455,
456 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
| 458 | 26, 457 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
| 459 | | ioodvbdlimc1lem2.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) |
| 460 | 105, 459 | fmptd 7134 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅:(ℤ≥‘𝑀)⟶(𝐴(,)𝐵)) |
| 461 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) |
| 462 | | climrel 15528 |
. . . . . . . . . . . . 13
⊢ Rel
⇝ |
| 463 | 462 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → Rel ⇝
) |
| 464 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) ∈ V |
| 465 | 464 | mptex 7243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ 𝐴) ∈ V |
| 466 | 465 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) ∈ V) |
| 467 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)) |
| 468 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴) |
| 469 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
| 470 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
| 471 | 467, 468,
469, 470 | fvmptd 7023 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑚) = 𝐴) |
| 472 | 23, 141, 466, 98, 471 | climconst 15579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) ⇝ 𝐴) |
| 473 | 464 | mptex 7243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V |
| 474 | 459, 473 | eqeltri 2837 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 ∈ V |
| 475 | 474 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ V) |
| 476 | | 1cnd 11256 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
| 477 | | elnnnn0b 12570 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0
∧ 0 < 𝑀)) |
| 478 | 21, 67, 477 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 479 | | divcnvg 45642 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝑀
∈ ℕ) → (𝑗
∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0) |
| 480 | 476, 478,
479 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0) |
| 481 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)) |
| 482 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴) |
| 483 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
| 484 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
| 485 | 481, 482,
483, 484 | fvmptd 7023 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) = 𝐴) |
| 486 | 98 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
| 487 | 485, 486 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ) |
| 488 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))) |
| 489 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖)) |
| 490 | 489 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖)) |
| 491 | 3, 483 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℝ) |
| 492 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 ∈
ℝ) |
| 493 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
| 494 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 < 𝑀) |
| 495 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑖) |
| 496 | 495 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑖) |
| 497 | 492, 493,
491, 494, 496 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 < 𝑖) |
| 498 | 497 | gt0ne0d 11827 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ≠ 0) |
| 499 | 491, 498 | rereccld 12094 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (1 / 𝑖) ∈
ℝ) |
| 500 | 488, 490,
483, 499 | fvmptd 7023 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖)) |
| 501 | 491 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℂ) |
| 502 | 501, 498 | reccld 12036 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (1 / 𝑖) ∈
ℂ) |
| 503 | 500, 502 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ) |
| 504 | 489 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖))) |
| 505 | 484, 499 | readdcld 11290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ) |
| 506 | 459, 504,
483, 505 | fvmptd3 7039 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑖) = (𝐴 + (1 / 𝑖))) |
| 507 | 485, 500 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖))) |
| 508 | 506, 507 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖))) |
| 509 | 23, 141, 472, 475, 480, 487, 503, 508 | climadd 15668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ⇝ (𝐴 + 0)) |
| 510 | 98 | addridd 11461 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
| 511 | 509, 510 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ⇝ 𝐴) |
| 512 | | releldm 5955 |
. . . . . . . . . . . 12
⊢ ((Rel
⇝ ∧ 𝑅 ⇝
𝐴) → 𝑅 ∈ dom ⇝ ) |
| 513 | 463, 511,
512 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ dom ⇝ ) |
| 514 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → (ℤ≥‘𝑙) =
(ℤ≥‘𝑘)) |
| 515 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘)) |
| 516 | 515 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘))) |
| 517 | 516 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘)))) |
| 518 | 517 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
| 519 | 514, 518 | raleqbidv 3346 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀ℎ ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
| 520 | 519 | cbvrabv 3447 |
. . . . . . . . . . . . 13
⊢ {𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
| 521 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖)) |
| 522 | 521 | fvoveq1d 7453 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘)))) |
| 523 | 522 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
| 524 | 523 | cbvralvw 3237 |
. . . . . . . . . . . . . . 15
⊢
(∀ℎ ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) |
| 525 | 524 | rgenw 3065 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
(ℤ≥‘𝑀)(∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) |
| 526 | | rabbi 3467 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(ℤ≥‘𝑀)(∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) ↔ {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}) |
| 527 | 525, 526 | mpbi 230 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
| 528 | 520, 527 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ {𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
| 529 | 528 | infeq1i 9518 |
. . . . . . . . . . 11
⊢
inf({𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
= inf({𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, <
) |
| 530 | 7, 6, 9, 458, 109, 110, 22, 460, 461, 513, 529 | ioodvbdlimc1lem1 45946 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))) |
| 531 | 459 | fvmpt2 7027 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈
(ℤ≥‘𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗))) |
| 532 | 113, 58, 531 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗))) |
| 533 | 532 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅‘𝑗)) |
| 534 | 533 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗))) |
| 535 | 534 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))) |
| 536 | 107, 535 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))) |
| 537 | 536 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))) |
| 538 | 530, 536,
537 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆)) |
| 539 | 464 | mptex 7243 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V |
| 540 | 107, 539 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝑆 ∈ V |
| 541 | 540 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ V) |
| 542 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐)) |
| 543 | 541, 542 | clim 15530 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))) |
| 544 | 538, 543 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧
∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))) |
| 545 | 544 | simprd 495 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)) |
| 546 | 545 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)) |
| 547 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
| 548 | 547 | rphalfcld 13089 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
| 549 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 550 | 549 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
| 551 | 550 | rexralbidv 3223 |
. . . . . . 7
⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
| 552 | 551 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) →
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 553 | 546, 548,
552 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
| 554 | 450, 553 | r19.29a 3162 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈
(ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
| 555 | 404, 554 | r19.29a 3162 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
| 556 | 555 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
| 557 | | ioosscn 13449 |
. . . 4
⊢ (𝐴(,)𝐵) ⊆ ℂ |
| 558 | 557 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
| 559 | 453, 558,
98 | ellimc3 25914 |
. 2
⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 limℂ 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))) |
| 560 | 136, 556,
559 | mpbir2and 713 |
1
⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 limℂ 𝐴)) |