Step | Hyp | Ref
| Expression |
1 | | uzssz 11912 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
2 | | zssre 11590 |
. . . . . 6
⊢ ℤ
⊆ ℝ |
3 | 1, 2 | sstri 3761 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆ ℝ) |
5 | | ioodvbdlimc2lem.m |
. . . . . . 7
⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1) |
6 | | ioodvbdlimc2lem.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | ioodvbdlimc2lem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | 6, 7 | resubcld 10663 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
9 | | ioodvbdlimc2lem.altb |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
10 | 7, 6 | posdifd 10819 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
11 | 9, 10 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
12 | 11 | gt0ne0d 10797 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
13 | 8, 12 | rereccld 11057 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ) |
14 | | 0red 10246 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
15 | 8, 11 | recgt0d 11163 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴))) |
16 | 14, 13, 15 | ltled 10390 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴))) |
17 | | flge0nn0 12828 |
. . . . . . . . 9
⊢ (((1 /
(𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤
(1 / (𝐵 − 𝐴))) → (⌊‘(1 /
(𝐵 − 𝐴))) ∈
ℕ0) |
18 | 13, 16, 17 | syl2anc 573 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈
ℕ0) |
19 | | peano2nn0 11539 |
. . . . . . . 8
⊢
((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ0 →
((⌊‘(1 / (𝐵
− 𝐴))) + 1) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℕ0) |
21 | 5, 20 | syl5eqel 2854 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
22 | 21 | nn0zd 11686 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
23 | | eqid 2771 |
. . . . . 6
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
24 | 23 | uzsup 12869 |
. . . . 5
⊢ (𝑀 ∈ ℤ →
sup((ℤ≥‘𝑀), ℝ*, < ) =
+∞) |
25 | 22, 24 | syl 17 |
. . . 4
⊢ (𝜑 →
sup((ℤ≥‘𝑀), ℝ*, < ) =
+∞) |
26 | | ioodvbdlimc2lem.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
27 | 26 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
28 | 7 | rexrd 10294 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
29 | 28 | adantr 466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈
ℝ*) |
30 | 6 | rexrd 10294 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
31 | 30 | adantr 466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈
ℝ*) |
32 | 6 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈ ℝ) |
33 | | eluzelre 11903 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℝ) |
34 | 33 | adantl 467 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ ℝ) |
35 | | 0red 10246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 ∈
ℝ) |
36 | | 0red 10246 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 0 ∈ ℝ) |
37 | | 1red 10260 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 1 ∈ ℝ) |
38 | 36, 37 | readdcld 10274 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (0 + 1) ∈
ℝ) |
39 | 38 | adantl 467 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ∈
ℝ) |
40 | 36 | ltp1d 11159 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 0 < (0 + 1)) |
41 | 40 | adantl 467 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 < (0 +
1)) |
42 | | eluzel2 11897 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
43 | 42 | zred 11688 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) |
44 | 43 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
45 | 13 | flcld 12806 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ) |
46 | 45 | zred 11688 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ) |
47 | | 1red 10260 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) |
48 | 18 | nn0ge0d 11560 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (⌊‘(1 /
(𝐵 − 𝐴)))) |
49 | 14, 46, 47, 48 | leadd1dd 10846 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + 1) ≤
((⌊‘(1 / (𝐵
− 𝐴))) +
1)) |
50 | 49, 5 | syl6breqr 4829 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 + 1) ≤ 𝑀) |
51 | 50 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ≤ 𝑀) |
52 | | eluzle 11905 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
53 | 52 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑗) |
54 | 39, 44, 34, 51, 53 | letrd 10399 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ≤ 𝑗) |
55 | 35, 39, 34, 41, 54 | ltletrd 10402 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 < 𝑗) |
56 | 55 | gt0ne0d 10797 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ≠ 0) |
57 | 34, 56 | rereccld 11057 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ∈
ℝ) |
58 | 32, 57 | resubcld 10663 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ ℝ) |
59 | 7 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
60 | 21 | nn0red 11558 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
61 | 14, 47 | readdcld 10274 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + 1) ∈
ℝ) |
62 | 46, 47 | readdcld 10274 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℝ) |
63 | 14 | ltp1d 11159 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (0 +
1)) |
64 | 14, 61, 62, 63, 49 | ltletrd 10402 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((⌊‘(1
/ (𝐵 − 𝐴))) + 1)) |
65 | 64, 5 | syl6breqr 4829 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑀) |
66 | 65 | gt0ne0d 10797 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≠ 0) |
67 | 60, 66 | rereccld 11057 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
68 | 67 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑀) ∈ ℝ) |
69 | 32, 68 | resubcld 10663 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑀)) ∈ ℝ) |
70 | 5 | eqcomi 2780 |
. . . . . . . . . . . . 13
⊢
((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀 |
71 | 70 | oveq2i 6806 |
. . . . . . . . . . . 12
⊢ (1 /
((⌊‘(1 / (𝐵
− 𝐴))) + 1)) = (1 /
𝑀) |
72 | 71, 67 | syl5eqel 2854 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) ∈
ℝ) |
73 | 13, 15 | elrpd 12071 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈
ℝ+) |
74 | 62, 64 | elrpd 12071 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℝ+) |
75 | | 1rp 12038 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ+) |
77 | | fllelt 12805 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
(𝐵 − 𝐴)) ∈ ℝ →
((⌊‘(1 / (𝐵
− 𝐴))) ≤ (1 /
(𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
78 | 13, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
79 | 78 | simprd 483 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) |
80 | 73, 74, 76, 79 | ltdiv2dd 40022 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴)))) |
81 | 8 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
82 | 81, 12 | recrecd 11003 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴)) |
83 | 80, 82 | breqtrd 4813 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴)) |
84 | 72, 8, 6, 83 | ltsub2dd 10845 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) < (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))) |
85 | 6 | recnd 10273 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
86 | 7 | recnd 10273 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
87 | 85, 86 | nncand 10602 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴) |
88 | 71 | oveq2i 6806 |
. . . . . . . . . . 11
⊢ (𝐵 − (1 / ((⌊‘(1
/ (𝐵 − 𝐴))) + 1))) = (𝐵 − (1 / 𝑀)) |
89 | 88 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) = (𝐵 − (1 / 𝑀))) |
90 | 84, 87, 89 | 3brtr3d 4818 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 < (𝐵 − (1 / 𝑀))) |
91 | 90 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 < (𝐵 − (1 / 𝑀))) |
92 | 60, 65 | elrpd 12071 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
93 | 92 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈
ℝ+) |
94 | 34, 55 | elrpd 12071 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ ℝ+) |
95 | | 1red 10260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 1 ∈
ℝ) |
96 | | 0le1 10756 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 ≤
1) |
98 | 93, 94, 95, 97, 53 | lediv2ad 12096 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀)) |
99 | 57, 68, 32, 98 | lesub2dd 10849 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑀)) ≤ (𝐵 − (1 / 𝑗))) |
100 | 59, 69, 58, 91, 99 | ltletrd 10402 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 < (𝐵 − (1 / 𝑗))) |
101 | 94 | rpreccld 12084 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ∈
ℝ+) |
102 | 32, 101 | ltsubrpd 12106 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑗)) < 𝐵) |
103 | 29, 31, 58, 100, 102 | eliood 40238 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
104 | 27, 103 | ffvelrnd 6505 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ) |
105 | | ioodvbdlimc2lem.s |
. . . . 5
⊢ 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) |
106 | 104, 105 | fmptd 6529 |
. . . 4
⊢ (𝜑 → 𝑆:(ℤ≥‘𝑀)⟶ℝ) |
107 | | ioodvbdlimc2lem.dmdv |
. . . . . 6
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
108 | | ioodvbdlimc2lem.dvbd |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) |
109 | 7, 6, 9, 26, 107, 108 | dvbdfbdioo 40660 |
. . . . 5
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) |
110 | 60 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ) |
111 | | simpr 471 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
112 | 105 | fvmpt2 6435 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈
(ℤ≥‘𝑀) ∧ (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗)))) |
113 | 111, 104,
112 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗)))) |
114 | 113 | fveq2d 6337 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗))))) |
115 | 114 | adantlr 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗))))) |
116 | | simplr 752 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) |
117 | 103 | adantlr 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
118 | | fveq2 6333 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → (𝐹‘𝑥) = (𝐹‘(𝐵 − (1 / 𝑗)))) |
119 | 118 | fveq2d 6337 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗))))) |
120 | 119 | breq1d 4797 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐵 − (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)) |
121 | 120 | rspccva 3459 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏) |
122 | 116, 117,
121 | syl2anc 573 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏) |
123 | 115, 122 | eqbrtrd 4809 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏) |
124 | 123 | a1d 25 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
125 | 124 | ralrimiva 3115 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
126 | | breq1 4790 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗)) |
127 | 126 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
128 | 127 | ralbidv 3135 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
129 | 128 | rspcev 3460 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
∀𝑗 ∈
(ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
130 | 110, 125,
129 | syl2anc 573 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
131 | 130 | ex 397 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
132 | 131 | reximdv 3164 |
. . . . 5
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
133 | 109, 132 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
134 | 4, 25, 106, 133 | limsupre 40388 |
. . 3
⊢ (𝜑 → (lim sup‘𝑆) ∈
ℝ) |
135 | 134 | recnd 10273 |
. 2
⊢ (𝜑 → (lim sup‘𝑆) ∈
ℂ) |
136 | | eluzelre 11903 |
. . . . . . . . 9
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑗 ∈ ℝ) |
137 | 136 | adantl 467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ) |
138 | | 0red 10246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ∈ ℝ) |
139 | 45 | peano2zd 11691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℤ) |
140 | 5, 139 | syl5eqel 2854 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
141 | 140 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
142 | 141 | zred 11688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℝ) |
143 | 142 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈ ℝ) |
144 | 65 | ad2antrr 705 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < 𝑀) |
145 | | ioodvbdlimc2lem.n |
. . . . . . . . . . . . . 14
⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) |
146 | | ioodvbdlimc2lem.y |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) |
147 | | ioomidp 40256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
148 | 7, 6, 9, 147 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
149 | | ne0i 4069 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅) |
151 | | ioossre 12439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴(,)𝐵) ⊆ ℝ |
152 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
153 | | dvfre 23933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
154 | 26, 152, 153 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
155 | 107 | feq2d 6170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
156 | 154, 155 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
157 | 156 | ffvelrnda 6504 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
158 | 157 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
159 | 158 | abscld 14382 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ) |
160 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) |
161 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ sup(ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) |
162 | 150, 159,
108, 160, 161 | suprnmpt 39874 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧
∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))) |
163 | 162 | simpld 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈
ℝ) |
164 | 146, 163 | syl5eqel 2854 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑌 ∈ ℝ) |
165 | 164 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑌 ∈
ℝ) |
166 | | rpre 12041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
167 | 166 | rehalfcld 11485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ) |
168 | 167 | adantl 467 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ) |
169 | 166 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
170 | 169 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
171 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) |
172 | | rpne0 12050 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
173 | 172 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
174 | | 2ne0 11318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ≠
0) |
176 | 170, 171,
173, 175 | divne0d 11022 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0) |
177 | 165, 168,
176 | redivcld 11058 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
178 | 177 | flcld 12806 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(𝑌 / (𝑥 / 2))) ∈
ℤ) |
179 | 178 | peano2zd 11691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈
ℤ) |
180 | 179, 141 | ifcld 4271 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ) |
181 | 145, 180 | syl5eqel 2854 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℤ) |
182 | 181 | zred 11688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℝ) |
183 | 182 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℝ) |
184 | 179 | zred 11688 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈
ℝ) |
185 | | max1 12220 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
→ 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
186 | 142, 184,
185 | syl2anc 573 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
187 | 186, 145 | syl6breqr 4829 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ≤ 𝑁) |
188 | 187 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ≤ 𝑁) |
189 | | eluzle 11905 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑗) |
190 | 189 | adantl 467 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ 𝑗) |
191 | 143, 183,
137, 188, 190 | letrd 10399 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ≤ 𝑗) |
192 | 138, 143,
137, 144, 191 | ltletrd 10402 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < 𝑗) |
193 | 192 | gt0ne0d 10797 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ≠ 0) |
194 | 137, 193 | rereccld 11057 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / 𝑗) ∈ ℝ) |
195 | 137, 192 | recgt0d 11163 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < (1 / 𝑗)) |
196 | 194, 195 | elrpd 12071 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / 𝑗) ∈
ℝ+) |
197 | 196 | adantr 466 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈
ℝ+) |
198 | | ioodvbdlimc2lem.ch |
. . . . . . . . 9
⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) |
199 | 198 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) |
200 | | simp-5l 772 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝜑) |
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝜑) |
202 | 201, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
203 | 199 | simplrd 753 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵)) |
204 | 202, 203 | ffvelrnd 6505 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ) |
205 | 204 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ) |
206 | 201, 106 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑆:(ℤ≥‘𝑀)⟶ℝ) |
207 | | simp-5r 774 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+) |
208 | 199, 207 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑥 ∈ ℝ+) |
209 | | eluz2 11898 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
210 | 141, 181,
187, 209 | syl3anbrc 1428 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘𝑀)) |
211 | 201, 208,
210 | syl2anc 573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑁 ∈ (ℤ≥‘𝑀)) |
212 | | uzss 11913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
214 | | simp-4r 770 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ≥‘𝑁)) |
215 | 199, 214 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝑗 ∈ (ℤ≥‘𝑁)) |
216 | 213, 215 | sseldd 3753 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑗 ∈ (ℤ≥‘𝑀)) |
217 | 206, 216 | ffvelrnd 6505 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ) |
218 | 217 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ) |
219 | 201, 135 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (lim sup‘𝑆) ∈
ℂ) |
220 | 205, 218,
219 | npncand 10621 |
. . . . . . . . . . . 12
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆))) |
221 | 220 | eqcomd 2777 |
. . . . . . . . . . 11
⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) |
222 | 221 | fveq2d 6337 |
. . . . . . . . . 10
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))) |
223 | 204, 217 | resubcld 10663 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ) |
224 | 201, 134 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (lim sup‘𝑆) ∈
ℝ) |
225 | 217, 224 | resubcld 10663 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ) |
226 | 223, 225 | readdcld 10274 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ) |
227 | 226 | recnd 10273 |
. . . . . . . . . . . 12
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ) |
228 | 227 | abscld 14382 |
. . . . . . . . . . 11
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ) |
229 | 223 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ) |
230 | 229 | abscld 14382 |
. . . . . . . . . . . 12
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ) |
231 | 225 | recnd 10273 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ) |
232 | 231 | abscld 14382 |
. . . . . . . . . . . 12
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ) |
233 | 230, 232 | readdcld 10274 |
. . . . . . . . . . 11
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ) |
234 | 208 | rpred 12074 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑥 ∈ ℝ) |
235 | 229, 231 | abstrid 14402 |
. . . . . . . . . . 11
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))))) |
236 | 234 | rehalfcld 11485 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝑥 / 2) ∈ ℝ) |
237 | 201, 216,
113 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐵 − (1 / 𝑗)))) |
238 | 237 | oveq2d 6811 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) = ((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) |
239 | 238 | fveq2d 6337 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗)))))) |
240 | 239, 230 | eqeltrrd 2851 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ∈ ℝ) |
241 | 201, 164 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝑌 ∈ ℝ) |
242 | 151, 203 | sseldi 3750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑧 ∈ ℝ) |
243 | 201, 216,
58 | syl2anc 573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ) |
244 | 242, 243 | resubcld 10663 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ∈ ℝ) |
245 | 241, 244 | remulcld 10275 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∈ ℝ) |
246 | 201, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝐴 ∈ ℝ) |
247 | 201, 6 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝐵 ∈ ℝ) |
248 | 201, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
249 | 162 | simprd 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
250 | 146 | breq2i 4795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
251 | 250 | ralbii 3129 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
252 | 249, 251 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
253 | 201, 252 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
254 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑥 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑥)) |
255 | 254 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥))) |
256 | 255 | breq1d 4797 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)) |
257 | 256 | cbvralv 3320 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
258 | 253, 257 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌) |
259 | 201, 216,
103 | syl2anc 573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
260 | 243 | rexrd 10294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝐵 − (1 / 𝑗)) ∈
ℝ*) |
261 | 201, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝐵 ∈
ℝ*) |
262 | 3, 216 | sseldi 3750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → 𝑗 ∈ ℝ) |
263 | 201, 216,
56 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → 𝑗 ≠ 0) |
264 | 262, 263 | rereccld 11057 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (1 / 𝑗) ∈ ℝ) |
265 | 247, 242 | resubcld 10663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝐵 − 𝑧) ∈ ℝ) |
266 | 242, 247 | resubcld 10663 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑧 − 𝐵) ∈ ℝ) |
267 | 266 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑧 − 𝐵) ∈ ℂ) |
268 | 267 | abscld 14382 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (abs‘(𝑧 − 𝐵)) ∈ ℝ) |
269 | 265 | leabsd 14360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝐵 − 𝑧) ≤ (abs‘(𝐵 − 𝑧))) |
270 | 201, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝐵 ∈ ℂ) |
271 | 242 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑧 ∈ ℂ) |
272 | 270, 271 | abssubd 14399 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (abs‘(𝐵 − 𝑧)) = (abs‘(𝑧 − 𝐵))) |
273 | 269, 272 | breqtrd 4813 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝐵 − 𝑧) ≤ (abs‘(𝑧 − 𝐵))) |
274 | 199 | simprd 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) |
275 | 265, 268,
264, 273, 274 | lelttrd 10400 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝐵 − 𝑧) < (1 / 𝑗)) |
276 | 247, 242,
264, 275 | ltsub23d 10837 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝐵 − (1 / 𝑗)) < 𝑧) |
277 | 201, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝐴 ∈
ℝ*) |
278 | | iooltub 40252 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑧
∈ (𝐴(,)𝐵)) → 𝑧 < 𝐵) |
279 | 277, 261,
203, 278 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑧 < 𝐵) |
280 | 260, 261,
242, 276, 279 | eliood 40238 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑧 ∈ ((𝐵 − (1 / 𝑗))(,)𝐵)) |
281 | 246, 247,
202, 248, 241, 258, 259, 280 | dvbdfbdioolem1 40658 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∧ (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝐵 − 𝐴)))) |
282 | 281 | simpld 482 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗))))) |
283 | 201, 216,
57 | syl2anc 573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (1 / 𝑗) ∈ ℝ) |
284 | 241, 283 | remulcld 10275 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
285 | 156, 148 | ffvelrnd 6505 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
286 | 285 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
287 | 286 | abscld 14382 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
288 | 286 | absge0d 14390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
289 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) |
290 | 289 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
291 | 146 | eqcomi 2780 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ sup(ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌 |
292 | 291 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌) |
293 | 290, 292 | breq12d 4800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)) |
294 | 293 | rspcva 3458 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) →
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌) |
295 | 148, 249,
294 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌) |
296 | 14, 287, 164, 288, 295 | letrd 10399 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ 𝑌) |
297 | 201, 296 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 0 ≤ 𝑌) |
298 | 283 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (1 / 𝑗) ∈ ℂ) |
299 | | sub31 40018 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (1 / 𝑗) ∈ ℂ) → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵 − 𝑧))) |
300 | 271, 270,
298, 299 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵 − 𝑧))) |
301 | 242, 247 | posdifd 10819 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑧 < 𝐵 ↔ 0 < (𝐵 − 𝑧))) |
302 | 279, 301 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 0 < (𝐵 − 𝑧)) |
303 | 265, 302 | elrpd 12071 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝐵 − 𝑧) ∈
ℝ+) |
304 | 283, 303 | ltsubrpd 12106 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → ((1 / 𝑗) − (𝐵 − 𝑧)) < (1 / 𝑗)) |
305 | 300, 304 | eqbrtrd 4809 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) < (1 / 𝑗)) |
306 | 244, 283,
305 | ltled 10390 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ≤ (1 / 𝑗)) |
307 | 244, 283,
241, 297, 306 | lemul2ad 11169 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑌 · (1 / 𝑗))) |
308 | 284 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
309 | 236 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ) |
310 | | oveq1 6802 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗))) |
311 | 298 | mul02d 10439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (0 · (1 / 𝑗)) = 0) |
312 | 310, 311 | sylan9eqr 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0) |
313 | 208 | rphalfcld 12086 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑥 / 2) ∈
ℝ+) |
314 | 313 | rpgt0d 12077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → 0 < (𝑥 / 2)) |
315 | 314 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2)) |
316 | 312, 315 | eqbrtrd 4809 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2)) |
317 | 308, 309,
316 | ltled 10390 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
318 | 241 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ) |
319 | 297 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌) |
320 | | neqne 2951 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑌 = 0 → 𝑌 ≠ 0) |
321 | 320 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0) |
322 | 318, 319,
321 | ne0gt0d 10379 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌) |
323 | 284 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
324 | 3, 211 | sseldi 3750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑁 ∈ ℝ) |
325 | | 0red 10246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → 0 ∈
ℝ) |
326 | 201, 208,
142 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → 𝑀 ∈ ℝ) |
327 | 201, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → 0 < 𝑀) |
328 | 201, 208,
187 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → 𝑀 ≤ 𝑁) |
329 | 325, 326,
324, 327, 328 | ltletrd 10402 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 0 < 𝑁) |
330 | 329 | gt0ne0d 10797 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑁 ≠ 0) |
331 | 324, 330 | rereccld 11057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (1 / 𝑁) ∈ ℝ) |
332 | 241, 331 | remulcld 10275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ) |
333 | 332 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ) |
334 | 236 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ) |
335 | 283 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ) |
336 | 331 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ) |
337 | 241 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ) |
338 | 297 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌) |
339 | 324, 329 | elrpd 12071 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑁 ∈
ℝ+) |
340 | 201, 216,
94 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑗 ∈ ℝ+) |
341 | | 1red 10260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 1 ∈
ℝ) |
342 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 0 ≤ 1) |
343 | 215, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑁 ≤ 𝑗) |
344 | 339, 340,
341, 342, 343 | lediv2ad 12096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁)) |
345 | 344 | adantr 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁)) |
346 | 335, 336,
337, 338, 345 | lemul2ad 11169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁))) |
347 | 234 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 𝑥 ∈ ℂ) |
348 | | 2cnd 11298 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 2 ∈
ℂ) |
349 | 208 | rpne0d 12079 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 𝑥 ≠ 0) |
350 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 2 ≠ 0) |
351 | 347, 348,
349, 350 | divne0d 11022 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → (𝑥 / 2) ≠ 0) |
352 | 241, 236,
351 | redivcld 11058 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
353 | 352 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
354 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌) |
355 | 314 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2)) |
356 | 337, 334,
354, 355 | divgt0d 11164 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2))) |
357 | 353, 356 | elrpd 12071 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈
ℝ+) |
358 | 357 | rprecred 12085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ) |
359 | 339 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈
ℝ+) |
360 | | 1red 10260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ) |
361 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1) |
362 | 352 | flcld 12806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ) |
363 | 362 | peano2zd 11691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ) |
364 | 363 | zred 11688 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) |
365 | 201, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → 𝑀 ∈ ℤ) |
366 | 363, 365 | ifcld 4271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ) |
367 | 145, 366 | syl5eqel 2854 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 𝑁 ∈ ℤ) |
368 | 367 | zred 11688 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 𝑁 ∈ ℝ) |
369 | | flltp1 12808 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1)) |
370 | 352, 369 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1)) |
371 | 201, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑀 ∈ ℝ) |
372 | | max2 12222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
→ ((⌊‘(𝑌 /
(𝑥 / 2))) + 1) ≤
if(𝑀 ≤
((⌊‘(𝑌 / (𝑥 / 2))) + 1),
((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
373 | 371, 364,
372 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
374 | 373, 145 | syl6breqr 4829 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁) |
375 | 352, 364,
368, 370, 374 | ltletrd 10402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁) |
376 | 352, 324,
375 | ltled 10390 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁) |
377 | 376 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁) |
378 | 357, 359,
360, 361, 377 | lediv2ad 12096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2)))) |
379 | 336, 358,
337, 338, 378 | lemul2ad 11169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2))))) |
380 | 337 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ) |
381 | 353 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ) |
382 | 356 | gt0ne0d 10797 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0) |
383 | 380, 381,
382 | divrecd 11009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2))))) |
384 | 334 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ) |
385 | 354 | gt0ne0d 10797 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0) |
386 | 351 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0) |
387 | 380, 384,
385, 386 | ddcand 11026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2)) |
388 | 383, 387 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2)) |
389 | 379, 388 | breqtrd 4813 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2)) |
390 | 323, 333,
334, 346, 389 | letrd 10399 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
391 | 322, 390 | syldan 579 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
392 | 317, 391 | pm2.61dan 814 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
393 | 245, 284,
236, 307, 392 | letrd 10399 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑥 / 2)) |
394 | 240, 245,
236, 282, 393 | letrd 10399 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑥 / 2)) |
395 | 239, 394 | eqbrtrd 4809 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2)) |
396 | | simpllr 760 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
397 | 199, 396 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
398 | 230, 232,
236, 236, 395, 397 | leltaddd 10854 |
. . . . . . . . . . . 12
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2))) |
399 | 347 | 2halvesd 11484 |
. . . . . . . . . . . 12
⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥) |
400 | 398, 399 | breqtrd 4813 |
. . . . . . . . . . 11
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥) |
401 | 228, 233,
234, 235, 400 | lelttrd 10400 |
. . . . . . . . . 10
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥) |
402 | 222, 401 | eqbrtrd 4809 |
. . . . . . . . 9
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
403 | 198, 402 | sylbir 225 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
404 | 403 | adantrl 695 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
405 | 404 | ex 397 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
406 | 405 | ralrimiva 3115 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
407 | | breq2 4791 |
. . . . . . . . 9
⊢ (𝑦 = (1 / 𝑗) → ((abs‘(𝑧 − 𝐵)) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗))) |
408 | 407 | anbi2d 614 |
. . . . . . . 8
⊢ (𝑦 = (1 / 𝑗) → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) ↔ (𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)))) |
409 | 408 | imbi1d 330 |
. . . . . . 7
⊢ (𝑦 = (1 / 𝑗) → (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))) |
410 | 409 | ralbidv 3135 |
. . . . . 6
⊢ (𝑦 = (1 / 𝑗) → (∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥))) |
411 | 410 | rspcev 3460 |
. . . . 5
⊢ (((1 /
𝑗) ∈
ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
412 | 197, 406,
411 | syl2anc 573 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
413 | | simpr 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁) |
414 | 413 | iftrued 4234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁) |
415 | | uzid 11907 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
416 | 181, 415 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘𝑁)) |
417 | 416 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ≥‘𝑁)) |
418 | 414, 417 | eqeltrd 2850 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
419 | 418 | adantlr 694 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
420 | | iffalse 4235 |
. . . . . . . . . 10
⊢ (¬
𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏) |
421 | 420 | adantl 467 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏) |
422 | 181 | ad2antrr 705 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ) |
423 | | simplr 752 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ) |
424 | 422 | zred 11688 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ) |
425 | 423 | zred 11688 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ) |
426 | | simpr 471 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁) |
427 | 424, 425 | ltnled 10389 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁)) |
428 | 426, 427 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 < 𝑏) |
429 | 424, 425,
428 | ltled 10390 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏) |
430 | | eluz2 11898 |
. . . . . . . . . 10
⊢ (𝑏 ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏)) |
431 | 422, 423,
429, 430 | syl3anbrc 1428 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ≥‘𝑁)) |
432 | 421, 431 | eqeltrd 2850 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
433 | 419, 432 | pm2.61dan 814 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
434 | 433 | adantr 466 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
435 | | simpr 471 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
436 | | simpr 471 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
437 | 181 | adantr 466 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈
ℤ) |
438 | 437, 436 | ifcld 4271 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ) |
439 | 436 | zred 11688 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℝ) |
440 | 437 | zred 11688 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈
ℝ) |
441 | | max1 12220 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) |
442 | 439, 440,
441 | syl2anc 573 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) |
443 | | eluz2 11898 |
. . . . . . . . . 10
⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
444 | 436, 438,
442, 443 | syl3anbrc 1428 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) |
445 | 444 | adantr 466 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) |
446 | | fveq2 6333 |
. . . . . . . . . . 11
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
447 | 446 | eleq1d 2835 |
. . . . . . . . . 10
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ)) |
448 | 446 | fvoveq1d 6817 |
. . . . . . . . . . 11
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))) |
449 | 448 | breq1d 4797 |
. . . . . . . . . 10
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
450 | 447, 449 | anbi12d 616 |
. . . . . . . . 9
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
451 | 450 | rspccva 3459 |
. . . . . . . 8
⊢
((∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
452 | 435, 445,
451 | syl2anc 573 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
453 | 452 | simprd 483 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) |
454 | | fveq2 6333 |
. . . . . . . . 9
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
455 | 454 | fvoveq1d 6817 |
. . . . . . . 8
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))) |
456 | 455 | breq1d 4797 |
. . . . . . 7
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
457 | 456 | rspcev 3460 |
. . . . . 6
⊢
((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
458 | 434, 453,
457 | syl2anc 573 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
459 | | ax-resscn 10198 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
460 | 459 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℂ) |
461 | 26, 460 | fssd 6198 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
462 | | dvcn 23903 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
463 | 460, 461,
152, 107, 462 | syl31anc 1479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
464 | | cncffvrn 22920 |
. . . . . . . . . . . . 13
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
465 | 460, 463,
464 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
466 | 26, 465 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
467 | | ioodvbdlimc2lem.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐵 − (1 / 𝑗))) |
468 | 103, 467 | fmptd 6529 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅:(ℤ≥‘𝑀)⟶(𝐴(,)𝐵)) |
469 | | eqid 2771 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) |
470 | | climrel 14430 |
. . . . . . . . . . . . 13
⊢ Rel
⇝ |
471 | 470 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → Rel ⇝
) |
472 | | fvex 6344 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) ∈ V |
473 | 472 | mptex 6632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ 𝐵) ∈ V |
474 | 473 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵) ∈ V) |
475 | | eqidd 2772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)) |
476 | | eqidd 2772 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐵 = 𝐵) |
477 | | simpr 471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
478 | 6 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈ ℝ) |
479 | 475, 476,
477, 478 | fvmptd 6432 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)‘𝑚) = 𝐵) |
480 | 23, 22, 474, 85, 479 | climconst 14481 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵) ⇝ 𝐵) |
481 | 472 | mptex 6632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐵 − (1 / 𝑗))) ∈ V |
482 | 467, 481 | eqeltri 2846 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 ∈ V |
483 | 482 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ V) |
484 | | 1cnd 10261 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
485 | | elnnnn0b 11543 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0
∧ 0 < 𝑀)) |
486 | 21, 65, 485 | sylanbrc 572 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
487 | | divcnvg 40374 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝑀
∈ ℕ) → (𝑗
∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0) |
488 | 484, 486,
487 | syl2anc 573 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0) |
489 | | eqidd 2772 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)) |
490 | | eqidd 2772 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐵 = 𝐵) |
491 | | simpr 471 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
492 | 6 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈ ℝ) |
493 | 489, 490,
491, 492 | fvmptd 6432 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)‘𝑖) = 𝐵) |
494 | 493, 492 | eqeltrd 2850 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)‘𝑖) ∈ ℝ) |
495 | 494 | recnd 10273 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)‘𝑖) ∈ ℂ) |
496 | | eqidd 2772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))) |
497 | | oveq2 6803 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖)) |
498 | 497 | adantl 467 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖)) |
499 | 3, 491 | sseldi 3750 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℝ) |
500 | | 0red 10246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 ∈
ℝ) |
501 | 60 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
502 | 65 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 < 𝑀) |
503 | | eluzle 11905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑖) |
504 | 503 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑖) |
505 | 500, 501,
499, 502, 504 | ltletrd 10402 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 < 𝑖) |
506 | 505 | gt0ne0d 10797 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ≠ 0) |
507 | 499, 506 | rereccld 11057 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (1 / 𝑖) ∈
ℝ) |
508 | 496, 498,
491, 507 | fvmptd 6432 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖)) |
509 | 499 | recnd 10273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℂ) |
510 | 509, 506 | reccld 10999 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (1 / 𝑖) ∈
ℂ) |
511 | 508, 510 | eqeltrd 2850 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ) |
512 | 497 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (𝐵 − (1 / 𝑗)) = (𝐵 − (1 / 𝑖))) |
513 | | ovex 6826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 − (1 / 𝑖)) ∈ V |
514 | 512, 467,
513 | fvmpt 6426 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → (𝑅‘𝑖) = (𝐵 − (1 / 𝑖))) |
515 | 514 | adantl 467 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑖) = (𝐵 − (1 / 𝑖))) |
516 | 493, 508 | oveq12d 6813 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐵 − (1 / 𝑖))) |
517 | 515, 516 | eqtr4d 2808 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖))) |
518 | 23, 22, 480, 483, 488, 495, 511, 517 | climsub 14571 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ⇝ (𝐵 − 0)) |
519 | 85 | subid1d 10586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 0) = 𝐵) |
520 | 518, 519 | breqtrd 4813 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ⇝ 𝐵) |
521 | | releldm 5495 |
. . . . . . . . . . . 12
⊢ ((Rel
⇝ ∧ 𝑅 ⇝
𝐵) → 𝑅 ∈ dom ⇝ ) |
522 | 471, 520,
521 | syl2anc 573 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ dom ⇝ ) |
523 | | fveq2 6333 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → (ℤ≥‘𝑙) =
(ℤ≥‘𝑘)) |
524 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘)) |
525 | 524 | oveq2d 6811 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘))) |
526 | 525 | fveq2d 6337 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘)))) |
527 | 526 | breq1d 4797 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
528 | 523, 527 | raleqbidv 3301 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀ℎ ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
529 | 528 | cbvrabv 3349 |
. . . . . . . . . . . . 13
⊢ {𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
530 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖)) |
531 | 530 | fvoveq1d 6817 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘)))) |
532 | 531 | breq1d 4797 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
533 | 532 | cbvralv 3320 |
. . . . . . . . . . . . . . 15
⊢
(∀ℎ ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) |
534 | 533 | rgenw 3073 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
(ℤ≥‘𝑀)(∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) |
535 | | rabbi 3269 |
. . . . . . . . . . . . . 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))}) |
536 | 534, 535 | mpbi 220 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
537 | 529, 536 | eqtri 2793 |
. . . . . . . . . . . 12
⊢ {𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
538 | 537 | infeq1i 8543 |
. . . . . . . . . . 11
⊢
inf({𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
= inf({𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, <
) |
539 | 7, 6, 9, 466, 107, 108, 22, 468, 469, 522, 538 | ioodvbdlimc1lem1 40661 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))) |
540 | 467 | fvmpt2 6435 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈
(ℤ≥‘𝑀) ∧ (𝐵 − (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐵 − (1 / 𝑗))) |
541 | 111, 58, 540 | syl2anc 573 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑗) = (𝐵 − (1 / 𝑗))) |
542 | 541 | eqcomd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐵 − (1 / 𝑗)) = (𝑅‘𝑗)) |
543 | 542 | fveq2d 6337 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗))) |
544 | 543 | mpteq2dva 4879 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))) |
545 | 105, 544 | syl5eq 2817 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))) |
546 | 545 | fveq2d 6337 |
. . . . . . . . . 10
⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))) |
547 | 539, 545,
546 | 3brtr4d 4819 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆)) |
548 | 472 | mptex 6632 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) ∈ V |
549 | 105, 548 | eqeltri 2846 |
. . . . . . . . . . 11
⊢ 𝑆 ∈ V |
550 | 549 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ V) |
551 | | eqidd 2772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐)) |
552 | 550, 551 | clim 14432 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))) |
553 | 547, 552 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧
∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))) |
554 | 553 | simprd 483 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)) |
555 | 554 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)) |
556 | | simpr 471 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
557 | 556 | rphalfcld 12086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
558 | | breq2 4791 |
. . . . . . . . 9
⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
559 | 558 | anbi2d 614 |
. . . . . . . 8
⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
560 | 559 | rexralbidv 3206 |
. . . . . . 7
⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
561 | 560 | rspccva 3459 |
. . . . . 6
⊢
((∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) →
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
562 | 555, 557,
561 | syl2anc 573 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
563 | 458, 562 | r19.29a 3226 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈
(ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
564 | 412, 563 | r19.29a 3226 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
565 | 564 | ralrimiva 3115 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
566 | | ioosscn 40234 |
. . . 4
⊢ (𝐴(,)𝐵) ⊆ ℂ |
567 | 566 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
568 | 461, 567,
85 | ellimc3 23862 |
. 2
⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 limℂ 𝐵) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))) |
569 | 135, 565,
568 | mpbir2and 692 |
1
⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 limℂ 𝐵)) |