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