Step | Hyp | Ref
| Expression |
1 | | uzssz 12585 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
2 | | zssre 12309 |
. . . . . 6
⊢ ℤ
⊆ ℝ |
3 | 1, 2 | sstri 3934 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆ ℝ) |
5 | | ioodvbdlimc1lem2.m |
. . . . . . 7
⊢ 𝑀 = ((⌊‘(1 / (𝐵 − 𝐴))) + 1) |
6 | | ioodvbdlimc1lem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | ioodvbdlimc1lem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | 6, 7 | resubcld 11386 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
9 | | ioodvbdlimc1lem2.altb |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
10 | 7, 6 | posdifd 11545 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
11 | 9, 10 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
12 | 11 | gt0ne0d 11522 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
13 | 8, 12 | rereccld 11785 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈ ℝ) |
14 | | 0red 10962 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
15 | 8, 11 | recgt0d 11892 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (1 / (𝐵 − 𝐴))) |
16 | 14, 13, 15 | ltled 11106 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 / (𝐵 − 𝐴))) |
17 | | flge0nn0 13521 |
. . . . . . . . 9
⊢ (((1 /
(𝐵 − 𝐴)) ∈ ℝ ∧ 0 ≤
(1 / (𝐵 − 𝐴))) → (⌊‘(1 /
(𝐵 − 𝐴))) ∈
ℕ0) |
18 | 13, 16, 17 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈
ℕ0) |
19 | | peano2nn0 12256 |
. . . . . . . 8
⊢
((⌊‘(1 / (𝐵 − 𝐴))) ∈ ℕ0 →
((⌊‘(1 / (𝐵
− 𝐴))) + 1) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℕ0) |
21 | 5, 20 | eqeltrid 2844 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
22 | 21 | nn0zd 12406 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
23 | | eqid 2739 |
. . . . . 6
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
24 | 23 | uzsup 13564 |
. . . . 5
⊢ (𝑀 ∈ ℤ →
sup((ℤ≥‘𝑀), ℝ*, < ) =
+∞) |
25 | 22, 24 | syl 17 |
. . . 4
⊢ (𝜑 →
sup((ℤ≥‘𝑀), ℝ*, < ) =
+∞) |
26 | | ioodvbdlimc1lem2.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
28 | 7 | rexrd 11009 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈
ℝ*) |
30 | 6 | rexrd 11009 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈
ℝ*) |
32 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
33 | | eluzelre 12575 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℝ) |
34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ ℝ) |
35 | | 0red 10962 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 ∈
ℝ) |
36 | | 0red 10962 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 0 ∈ ℝ) |
37 | | 1red 10960 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 1 ∈ ℝ) |
38 | 36, 37 | readdcld 10988 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (0 + 1) ∈
ℝ) |
39 | 38 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ∈
ℝ) |
40 | 36 | ltp1d 11888 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 0 < (0 + 1)) |
41 | 40 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 < (0 +
1)) |
42 | | eluzel2 12569 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
43 | 42 | zred 12408 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) |
44 | 43 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
45 | 13 | flcld 13499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℤ) |
46 | 45 | zred 12408 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘(1 / (𝐵 − 𝐴))) ∈ ℝ) |
47 | | 1red 10960 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) |
48 | 18 | nn0ge0d 12279 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (⌊‘(1 /
(𝐵 − 𝐴)))) |
49 | 14, 46, 47, 48 | leadd1dd 11572 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + 1) ≤
((⌊‘(1 / (𝐵
− 𝐴))) +
1)) |
50 | 49, 5 | breqtrrdi 5120 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 + 1) ≤ 𝑀) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ≤ 𝑀) |
52 | | eluzle 12577 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
53 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑗) |
54 | 39, 44, 34, 51, 53 | letrd 11115 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (0 + 1) ≤ 𝑗) |
55 | 35, 39, 34, 41, 54 | ltletrd 11118 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 < 𝑗) |
56 | 55 | gt0ne0d 11522 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ≠ 0) |
57 | 34, 56 | rereccld 11785 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ∈
ℝ) |
58 | 32, 57 | readdcld 10988 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ) |
59 | 34, 55 | elrpd 12751 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ ℝ+) |
60 | 59 | rpreccld 12764 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ∈
ℝ+) |
61 | 32, 60 | ltaddrpd 12787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗))) |
62 | 21 | nn0red 12277 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
63 | 14, 47 | readdcld 10988 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + 1) ∈
ℝ) |
64 | 46, 47 | readdcld 10988 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℝ) |
65 | 14 | ltp1d 11888 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (0 +
1)) |
66 | 14, 63, 64, 65, 49 | ltletrd 11118 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((⌊‘(1
/ (𝐵 − 𝐴))) + 1)) |
67 | 66, 5 | breqtrrdi 5120 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑀) |
68 | 67 | gt0ne0d 11522 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≠ 0) |
69 | 62, 68 | rereccld 11785 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
70 | 69 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑀) ∈ ℝ) |
71 | 32, 70 | readdcld 10988 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ) |
72 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝐵 ∈ ℝ) |
73 | 62, 67 | elrpd 12751 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℝ+) |
74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈
ℝ+) |
75 | | 1red 10960 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 1 ∈
ℝ) |
76 | | 0le1 11481 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
77 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 0 ≤
1) |
78 | 74, 59, 75, 77, 53 | lediv2ad 12776 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀)) |
79 | 57, 70, 32, 78 | leadd2dd 11573 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀))) |
80 | 5 | eqcomi 2748 |
. . . . . . . . . . . . 13
⊢
((⌊‘(1 / (𝐵 − 𝐴))) + 1) = 𝑀 |
81 | 80 | oveq2i 7279 |
. . . . . . . . . . . 12
⊢ (1 /
((⌊‘(1 / (𝐵
− 𝐴))) + 1)) = (1 /
𝑀) |
82 | 81, 69 | eqeltrid 2844 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) ∈
ℝ) |
83 | 13, 15 | elrpd 12751 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) ∈
ℝ+) |
84 | 64, 66 | elrpd 12751 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℝ+) |
85 | | 1rp 12716 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
86 | 85 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ+) |
87 | | fllelt 13498 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
(𝐵 − 𝐴)) ∈ ℝ →
((⌊‘(1 / (𝐵
− 𝐴))) ≤ (1 /
(𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
88 | 13, 87 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) ≤ (1 / (𝐵 − 𝐴)) ∧ (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
89 | 88 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / (𝐵 − 𝐴)) < ((⌊‘(1 / (𝐵 − 𝐴))) + 1)) |
90 | 83, 84, 86, 89 | ltdiv2dd 42787 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) < (1 / (1 / (𝐵 − 𝐴)))) |
91 | 8 | recnd 10987 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
92 | 91, 12 | recrecd 11731 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / (1 / (𝐵 − 𝐴))) = (𝐵 − 𝐴)) |
93 | 90, 92 | breqtrd 5104 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / ((⌊‘(1 /
(𝐵 − 𝐴))) + 1)) < (𝐵 − 𝐴)) |
94 | 82, 8, 7, 93 | ltadd2dd 11117 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) < (𝐴 + (𝐵 − 𝐴))) |
95 | 5 | oveq2i 7279 |
. . . . . . . . . . . 12
⊢ (1 /
𝑀) = (1 /
((⌊‘(1 / (𝐵
− 𝐴))) +
1)) |
96 | 95 | oveq2i 7279 |
. . . . . . . . . . 11
⊢ (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1))) |
97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵 − 𝐴))) + 1)))) |
98 | 7 | recnd 10987 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
99 | 6 | recnd 10987 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) |
100 | 98, 99 | pncan3d 11318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵) |
101 | 100 | eqcomd 2745 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = (𝐴 + (𝐵 − 𝐴))) |
102 | 94, 97, 101 | 3brtr4d 5110 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵) |
103 | 102 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵) |
104 | 58, 71, 72, 79, 103 | lelttrd 11116 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵) |
105 | 29, 31, 58, 61, 104 | eliood 42990 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
106 | 27, 105 | ffvelrnd 6956 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) |
107 | | ioodvbdlimc1lem2.s |
. . . . 5
⊢ 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) |
108 | 106, 107 | fmptd 6982 |
. . . 4
⊢ (𝜑 → 𝑆:(ℤ≥‘𝑀)⟶ℝ) |
109 | | ioodvbdlimc1lem2.dmdv |
. . . . . 6
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
110 | | ioodvbdlimc1lem2.dvbd |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦) |
111 | 7, 6, 9, 26, 109, 110 | dvbdfbdioo 43425 |
. . . . 5
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) |
112 | 62 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ) |
113 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
114 | 107 | fvmpt2 6880 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈
(ℤ≥‘𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗)))) |
115 | 113, 106,
114 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗)))) |
116 | 115 | fveq2d 6772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗))))) |
117 | 116 | adantlr 711 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗))))) |
118 | | simplr 765 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) |
119 | 105 | adantlr 711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) |
120 | | 2fveq3 6773 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗))))) |
121 | 120 | breq1d 5088 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹‘𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)) |
122 | 121 | rspccva 3559 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
(𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏) |
123 | 118, 119,
122 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏) |
124 | 117, 123 | eqbrtrd 5100 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (abs‘(𝑆‘𝑗)) ≤ 𝑏) |
125 | 124 | a1d 25 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
126 | 125 | ralrimiva 3109 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
127 | | breq1 5081 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗)) |
128 | 127 | imbi1d 341 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ (𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
129 | 128 | ralbidv 3122 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
130 | 129 | rspcev 3560 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
∀𝑗 ∈
(ℤ≥‘𝑀)(𝑀 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
131 | 112, 126,
130 | syl2anc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
132 | 131 | ex 412 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
133 | 132 | reximdv 3203 |
. . . . 5
⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹‘𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏))) |
134 | 111, 133 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ≥‘𝑀)(𝑘 ≤ 𝑗 → (abs‘(𝑆‘𝑗)) ≤ 𝑏)) |
135 | 4, 25, 108, 134 | limsupre 43136 |
. . 3
⊢ (𝜑 → (lim sup‘𝑆) ∈
ℝ) |
136 | 135 | recnd 10987 |
. 2
⊢ (𝜑 → (lim sup‘𝑆) ∈
ℂ) |
137 | | eluzelre 12575 |
. . . . . . . . 9
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑗 ∈ ℝ) |
138 | 137 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ∈ ℝ) |
139 | | 0red 10962 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 ∈ ℝ) |
140 | 45 | peano2zd 12411 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘(1 /
(𝐵 − 𝐴))) + 1) ∈
ℤ) |
141 | 5, 140 | eqeltrid 2844 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
142 | 141 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
143 | 142 | zred 12408 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℝ) |
144 | 143 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ∈ ℝ) |
145 | 67 | ad2antrr 722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < 𝑀) |
146 | | ioodvbdlimc1lem2.n |
. . . . . . . . . . . . . 14
⊢ 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) |
147 | | ioodvbdlimc1lem2.y |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) |
148 | | ioomidp 43006 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
149 | 7, 6, 9, 148 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) |
150 | | ne0i 4273 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅) |
152 | | ioossre 13122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴(,)𝐵) ⊆ ℝ |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
154 | | dvfre 25096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
155 | 26, 153, 154 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
156 | 109 | feq2d 6582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
157 | 155, 156 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
158 | 157 | ffvelrnda 6955 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ) |
159 | 158 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
160 | 159 | abscld 15129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ) |
161 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) |
162 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ sup(ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) |
163 | 151, 160,
110, 161, 162 | suprnmpt 42663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧
∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))) |
164 | 163 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈
ℝ) |
165 | 147, 164 | eqeltrid 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑌 ∈ ℝ) |
166 | 165 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑌 ∈
ℝ) |
167 | | rpre 12720 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
168 | 167 | rehalfcld 12203 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ) |
169 | 168 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ) |
170 | 167 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
171 | 170 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
172 | | 2cnd 12034 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) |
173 | | rpne0 12728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
174 | 173 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
175 | | 2ne0 12060 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ≠
0) |
177 | 171, 172,
174, 176 | divne0d 11750 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0) |
178 | 166, 169,
177 | redivcld 11786 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
179 | 178 | flcld 13499 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘(𝑌 / (𝑥 / 2))) ∈
ℤ) |
180 | 179 | peano2zd 12411 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈
ℤ) |
181 | 180, 142 | ifcld 4510 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ) |
182 | 146, 181 | eqeltrid 2844 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℤ) |
183 | 182 | zred 12408 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℝ) |
184 | 183 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℝ) |
185 | 180 | zred 12408 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈
ℝ) |
186 | | max1 12901 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
→ 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
187 | 143, 185,
186 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
188 | 187, 146 | breqtrrdi 5120 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑀 ≤ 𝑁) |
189 | 188 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ≤ 𝑁) |
190 | | eluzle 12577 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑗) |
191 | 190 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ 𝑗) |
192 | 144, 184,
138, 189, 191 | letrd 11115 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑀 ≤ 𝑗) |
193 | 139, 144,
138, 145, 192 | ltletrd 11118 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < 𝑗) |
194 | 193 | gt0ne0d 11522 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 𝑗 ≠ 0) |
195 | 138, 194 | rereccld 11785 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / 𝑗) ∈ ℝ) |
196 | 138, 193 | recgt0d 11892 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → 0 < (1 / 𝑗)) |
197 | 195, 196 | elrpd 12751 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) → (1 / 𝑗) ∈
ℝ+) |
198 | 197 | adantr 480 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈
ℝ+) |
199 | | ioodvbdlimc1lem2.ch |
. . . . . . . . 9
⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) |
200 | 199 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) |
201 | | simp-5l 781 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝜑) |
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝜑) |
203 | 202, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝐹:(𝐴(,)𝐵)⟶ℝ) |
204 | 200 | simplrd 766 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑧 ∈ (𝐴(,)𝐵)) |
205 | 203, 204 | ffvelrnd 6956 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝐹‘𝑧) ∈ ℝ) |
206 | 205 | recnd 10987 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝐹‘𝑧) ∈ ℂ) |
207 | 202, 108 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑆:(ℤ≥‘𝑀)⟶ℝ) |
208 | | simp-5r 782 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+) |
209 | 200, 208 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑥 ∈ ℝ+) |
210 | | eluz2 12570 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
211 | 142, 182,
188, 210 | syl3anbrc 1341 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘𝑀)) |
212 | 202, 209,
211 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑁 ∈ (ℤ≥‘𝑀)) |
213 | | uzss 12587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 →
(ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
215 | | simp-4r 780 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ≥‘𝑁)) |
216 | 200, 215 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝑗 ∈ (ℤ≥‘𝑁)) |
217 | 214, 216 | sseldd 3926 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑗 ∈ (ℤ≥‘𝑀)) |
218 | 207, 217 | ffvelrnd 6956 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ) |
219 | 218 | recnd 10987 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ) |
220 | 202, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (lim sup‘𝑆) ∈
ℂ) |
221 | 206, 219,
220 | npncand 11339 |
. . . . . . . . . . . 12
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) = ((𝐹‘𝑧) − (lim sup‘𝑆))) |
222 | 221 | eqcomd 2745 |
. . . . . . . . . . 11
⊢ (𝜒 → ((𝐹‘𝑧) − (lim sup‘𝑆)) = (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) |
223 | 222 | fveq2d 6772 |
. . . . . . . . . 10
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))))) |
224 | 205, 218 | resubcld 11386 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℝ) |
225 | 202, 135 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (lim sup‘𝑆) ∈
ℝ) |
226 | 218, 225 | resubcld 11386 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℝ) |
227 | 224, 226 | readdcld 10988 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ) |
228 | 227 | recnd 10987 |
. . . . . . . . . . . 12
⊢ (𝜒 → (((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℂ) |
229 | 228 | abscld 15129 |
. . . . . . . . . . 11
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ) |
230 | 224 | recnd 10987 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ((𝐹‘𝑧) − (𝑆‘𝑗)) ∈ ℂ) |
231 | 230 | abscld 15129 |
. . . . . . . . . . . 12
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ∈ ℝ) |
232 | 226 | recnd 10987 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ((𝑆‘𝑗) − (lim sup‘𝑆)) ∈ ℂ) |
233 | 232 | abscld 15129 |
. . . . . . . . . . . 12
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) ∈ ℝ) |
234 | 231, 233 | readdcld 10988 |
. . . . . . . . . . 11
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) ∈ ℝ) |
235 | 209 | rpred 12754 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑥 ∈ ℝ) |
236 | 230, 232 | abstrid 15149 |
. . . . . . . . . . 11
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))))) |
237 | 235 | rehalfcld 12203 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (𝑥 / 2) ∈ ℝ) |
238 | 206, 219 | abssubd 15146 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) = (abs‘((𝑆‘𝑗) − (𝐹‘𝑧)))) |
239 | 202, 217,
115 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑆‘𝑗) = (𝐹‘(𝐴 + (1 / 𝑗)))) |
240 | 239 | fvoveq1d 7290 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)))) |
241 | 202, 217,
106 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) |
242 | 241, 205 | resubcld 11386 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℝ) |
243 | 242 | recnd 10987 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧)) ∈ ℂ) |
244 | 243 | abscld 15129 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ∈ ℝ) |
245 | 202, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑌 ∈ ℝ) |
246 | 202, 217,
58 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ) |
247 | 152, 204 | sselid 3923 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝑧 ∈ ℝ) |
248 | 246, 247 | resubcld 11386 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ) |
249 | 245, 248 | remulcld 10989 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ) |
250 | 202, 7 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝐴 ∈ ℝ) |
251 | 202, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 𝐵 ∈ ℝ) |
252 | 202, 109 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
253 | 163 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
254 | 147 | breq2i 5086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
255 | 254 | ralbii 3092 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑥 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) |
256 | 253, 255 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
257 | 202, 256 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
258 | | 2fveq3 6773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥))) |
259 | 258 | breq1d 5088 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)) |
260 | 259 | cbvralvw 3380 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑤 ∈
(𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌) |
261 | 257, 260 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌) |
262 | 247 | rexrd 11009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝑧 ∈ ℝ*) |
263 | 202, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝐵 ∈
ℝ*) |
264 | 247, 250 | resubcld 11386 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℝ) |
265 | 264 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑧 − 𝐴) ∈ ℂ) |
266 | 265 | abscld 15129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) ∈ ℝ) |
267 | 3, 217 | sselid 3923 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑗 ∈ ℝ) |
268 | 202, 217,
56 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑗 ≠ 0) |
269 | 267, 268 | rereccld 11785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (1 / 𝑗) ∈ ℝ) |
270 | 264 | leabsd 15107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑧 − 𝐴) ≤ (abs‘(𝑧 − 𝐴))) |
271 | 200 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) |
272 | 264, 266,
269, 270, 271 | lelttrd 11116 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑧 − 𝐴) < (1 / 𝑗)) |
273 | 247, 250,
269 | ltsubadd2d 11556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝑧 − 𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗)))) |
274 | 272, 273 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝑧 < (𝐴 + (1 / 𝑗))) |
275 | 202, 217,
104 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵) |
276 | 262, 263,
246, 274, 275 | eliood 42990 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵)) |
277 | 250, 251,
203, 252, 245, 261, 204, 276 | dvbdfbdioolem1 43423 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · (𝐵 − 𝐴)))) |
278 | 277 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧))) |
279 | 202, 217,
57 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (1 / 𝑗) ∈ ℝ) |
280 | 245, 279 | remulcld 10989 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
281 | 157, 149 | ffvelrnd 6956 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ) |
282 | 281 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ) |
283 | 282 | abscld 15129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ) |
284 | 282 | absge0d 15137 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
285 | | 2fveq3 6773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))) |
286 | 147 | eqcomi 2748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ sup(ran
(𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌 |
287 | 286 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌) |
288 | 285, 287 | breq12d 5091 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)) |
289 | 288 | rspcva 3558 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) →
(abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌) |
290 | 149, 253,
289 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (abs‘((ℝ D
𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌) |
291 | 14, 283, 165, 284, 290 | letrd 11115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 𝑌) |
292 | 202, 291 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → 0 ≤ 𝑌) |
293 | 202, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝐴 ∈
ℝ*) |
294 | | ioogtlb 42987 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑧
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧) |
295 | 293, 263,
204, 294 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 𝐴 < 𝑧) |
296 | 250, 247,
246, 295 | ltsub2dd 11571 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴)) |
297 | 202, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 𝐴 ∈ ℂ) |
298 | 279 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (1 / 𝑗) ∈ ℂ) |
299 | 297, 298 | pncan2d 11317 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗)) |
300 | 296, 299 | breqtrd 5104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗)) |
301 | 248, 269,
300 | ltled 11106 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗)) |
302 | 248, 269,
245, 292, 301 | lemul2ad 11898 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗))) |
303 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
304 | 237 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑥 / 2) ∈ ℝ) |
305 | | oveq1 7275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗))) |
306 | 298 | mul02d 11156 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (0 · (1 / 𝑗)) = 0) |
307 | 305, 306 | sylan9eqr 2801 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0) |
308 | 209 | rphalfcld 12766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑥 / 2) ∈
ℝ+) |
309 | 308 | rpgt0d 12757 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 0 < (𝑥 / 2)) |
310 | 309 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 𝑌 = 0) → 0 < (𝑥 / 2)) |
311 | 307, 310 | eqbrtrd 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2)) |
312 | 303, 304,
311 | ltled 11106 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
313 | 245 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ) |
314 | 292 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌) |
315 | | neqne 2952 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑌 = 0 → 𝑌 ≠ 0) |
316 | 315 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0) |
317 | 313, 314,
316 | ne0gt0d 11095 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌) |
318 | 280 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ) |
319 | 3, 212 | sselid 3923 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ∈ ℝ) |
320 | | 0red 10962 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 0 ∈
ℝ) |
321 | 202, 209,
143 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 𝑀 ∈ ℝ) |
322 | 202, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 0 < 𝑀) |
323 | 202, 209,
188 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → 𝑀 ≤ 𝑁) |
324 | 320, 321,
319, 322, 323 | ltletrd 11118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → 0 < 𝑁) |
325 | 324 | gt0ne0d 11522 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ≠ 0) |
326 | 319, 325 | rereccld 11785 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (1 / 𝑁) ∈ ℝ) |
327 | 245, 326 | remulcld 10989 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ) |
328 | 327 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ) |
329 | 237 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ) |
330 | 279 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ) |
331 | 326 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ) |
332 | 245 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ) |
333 | 292 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌) |
334 | 319, 324 | elrpd 12751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ∈
ℝ+) |
335 | 202, 217,
59 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑗 ∈ ℝ+) |
336 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 1 ∈
ℝ) |
337 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 0 ≤ 1) |
338 | 216, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑁 ≤ 𝑗) |
339 | 334, 335,
336, 337, 338 | lediv2ad 12776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁)) |
340 | 339 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁)) |
341 | 330, 331,
332, 333, 340 | lemul2ad 11898 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁))) |
342 | 235 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑥 ∈ ℂ) |
343 | | 2cnd 12034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 2 ∈
ℂ) |
344 | 209 | rpne0d 12759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑥 ≠ 0) |
345 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 2 ≠ 0) |
346 | 342, 343,
344, 345 | divne0d 11750 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → (𝑥 / 2) ≠ 0) |
347 | 245, 237,
346 | redivcld 11786 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
348 | 347 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ) |
349 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌) |
350 | 309 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2)) |
351 | 332, 329,
349, 350 | divgt0d 11893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2))) |
352 | 348, 351 | elrpd 12751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈
ℝ+) |
353 | 352 | rprecred 12765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ) |
354 | 334 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈
ℝ+) |
355 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ) |
356 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1) |
357 | 347 | flcld 13499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ) |
358 | 357 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ) |
359 | 358 | zred 12408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) |
360 | 202, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜒 → 𝑀 ∈ ℤ) |
361 | 358, 360 | ifcld 4510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ) |
362 | 146, 361 | eqeltrid 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → 𝑁 ∈ ℤ) |
363 | 362 | zred 12408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → 𝑁 ∈ ℝ) |
364 | | flltp1 13501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1)) |
365 | 347, 364 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1)) |
366 | 202, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜒 → 𝑀 ∈ ℝ) |
367 | | max2 12903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
→ ((⌊‘(𝑌 /
(𝑥 / 2))) + 1) ≤
if(𝑀 ≤
((⌊‘(𝑌 / (𝑥 / 2))) + 1),
((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
368 | 366, 359,
367 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)) |
369 | 368, 146 | breqtrrdi 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁) |
370 | 347, 359,
363, 365, 369 | ltletrd 11118 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁) |
371 | 347, 319,
370 | ltled 11106 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁) |
372 | 371 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁) |
373 | 352, 354,
355, 356, 372 | lediv2ad 12776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2)))) |
374 | 331, 353,
332, 333, 373 | lemul2ad 11898 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2))))) |
375 | 332 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ) |
376 | 348 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ) |
377 | 351 | gt0ne0d 11522 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0) |
378 | 375, 376,
377 | divrecd 11737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2))))) |
379 | 329 | recnd 10987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ) |
380 | 349 | gt0ne0d 11522 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0) |
381 | 346 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0) |
382 | 375, 379,
380, 381 | ddcand 11754 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2)) |
383 | 378, 382 | eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2)) |
384 | 374, 383 | breqtrd 5104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2)) |
385 | 318, 328,
329, 341, 384 | letrd 11115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
386 | 317, 385 | syldan 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
387 | 312, 386 | pm2.61dan 809 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2)) |
388 | 249, 280,
237, 302, 387 | letrd 11115 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2)) |
389 | 244, 249,
237, 278, 388 | letrd 11115 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹‘𝑧))) ≤ (𝑥 / 2)) |
390 | 240, 389 | eqbrtrd 5100 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (𝐹‘𝑧))) ≤ (𝑥 / 2)) |
391 | 238, 390 | eqbrtrd 5100 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) ≤ (𝑥 / 2)) |
392 | | simpllr 772 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
393 | 200, 392 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜒 → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
394 | 231, 233,
237, 237, 391, 393 | leltaddd 11580 |
. . . . . . . . . . . 12
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2))) |
395 | 342 | 2halvesd 12202 |
. . . . . . . . . . . 12
⊢ (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥) |
396 | 394, 395 | breqtrd 5104 |
. . . . . . . . . . 11
⊢ (𝜒 → ((abs‘((𝐹‘𝑧) − (𝑆‘𝑗))) + (abs‘((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥) |
397 | 229, 234,
235, 236, 396 | lelttrd 11116 |
. . . . . . . . . 10
⊢ (𝜒 → (abs‘(((𝐹‘𝑧) − (𝑆‘𝑗)) + ((𝑆‘𝑗) − (lim sup‘𝑆)))) < 𝑥) |
398 | 223, 397 | eqbrtrd 5100 |
. . . . . . . . 9
⊢ (𝜒 → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
399 | 199, 398 | sylbir 234 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
400 | 399 | adantrl 712 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗))) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥) |
401 | 400 | ex 412 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
402 | 401 | ralrimiva 3109 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
403 | | brimralrspcev 5139 |
. . . . 5
⊢ (((1 /
𝑗) ∈
ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < (1 / 𝑗)) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
404 | 198, 402,
403 | syl2anc 583 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈
(ℤ≥‘𝑁)) ∧ (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
405 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → 𝑏 ≤ 𝑁) |
406 | 405 | iftrued 4472 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑁) |
407 | | uzid 12579 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
408 | 182, 407 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘𝑁)) |
409 | 408 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → 𝑁 ∈ (ℤ≥‘𝑁)) |
410 | 406, 409 | eqeltrd 2840 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
411 | 410 | adantlr 711 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
412 | | iffalse 4473 |
. . . . . . . . . 10
⊢ (¬
𝑏 ≤ 𝑁 → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏) |
413 | 412 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) = 𝑏) |
414 | 182 | ad2antrr 722 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ∈ ℤ) |
415 | | simplr 765 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ ℤ) |
416 | 414 | zred 12408 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ∈ ℝ) |
417 | 415 | zred 12408 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ ℝ) |
418 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → ¬ 𝑏 ≤ 𝑁) |
419 | 416, 417 | ltnled 11105 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁)) |
420 | 418, 419 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 < 𝑏) |
421 | 416, 417,
420 | ltled 11106 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑁 ≤ 𝑏) |
422 | | eluz2 12570 |
. . . . . . . . . 10
⊢ (𝑏 ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏)) |
423 | 414, 415,
421, 422 | syl3anbrc 1341 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → 𝑏 ∈ (ℤ≥‘𝑁)) |
424 | 413, 423 | eqeltrd 2840 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬
𝑏 ≤ 𝑁) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
425 | 411, 424 | pm2.61dan 809 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
426 | 425 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁)) |
427 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
428 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
429 | 182 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈
ℤ) |
430 | 429, 428 | ifcld 4510 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ) |
431 | 428 | zred 12408 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℝ) |
432 | 429 | zred 12408 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈
ℝ) |
433 | | max1 12901 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) |
434 | 431, 432,
433 | syl2anc 583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) |
435 | | eluz2 12570 |
. . . . . . . . . 10
⊢ (if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
436 | 428, 430,
434, 435 | syl3anbrc 1341 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) |
437 | 436 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) |
438 | | fveq2 6768 |
. . . . . . . . . . 11
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑐) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
439 | 438 | eleq1d 2824 |
. . . . . . . . . 10
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((𝑆‘𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ)) |
440 | 438 | fvoveq1d 7290 |
. . . . . . . . . . 11
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))) |
441 | 440 | breq1d 5088 |
. . . . . . . . . 10
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
442 | 439, 441 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝑐 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
443 | 442 | rspccva 3559 |
. . . . . . . 8
⊢
((∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑏)) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
444 | 427, 437,
443 | syl2anc 583 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
445 | 444 | simprd 495 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) |
446 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (𝑆‘𝑗) = (𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏))) |
447 | 446 | fvoveq1d 7290 |
. . . . . . . 8
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → (abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))) |
448 | 447 | breq1d 5088 |
. . . . . . 7
⊢ (𝑗 = if(𝑏 ≤ 𝑁, 𝑁, 𝑏) → ((abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))) |
449 | 448 | rspcev 3560 |
. . . . . 6
⊢
((if(𝑏 ≤ 𝑁, 𝑁, 𝑏) ∈ (ℤ≥‘𝑁) ∧ (abs‘((𝑆‘if(𝑏 ≤ 𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
450 | 426, 445,
449 | syl2anc 583 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
451 | | ax-resscn 10912 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
452 | 451 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℂ) |
453 | 26, 452 | fssd 6614 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
454 | | dvcn 25066 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D
𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
455 | 452, 453,
153, 109, 454 | syl31anc 1371 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
456 | | cncffvrn 24042 |
. . . . . . . . . . . . 13
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
457 | 452, 455,
456 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ)) |
458 | 26, 457 | mpbird 256 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
459 | | ioodvbdlimc1lem2.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) |
460 | 105, 459 | fmptd 6982 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅:(ℤ≥‘𝑀)⟶(𝐴(,)𝐵)) |
461 | | eqid 2739 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) |
462 | | climrel 15182 |
. . . . . . . . . . . . 13
⊢ Rel
⇝ |
463 | 462 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → Rel ⇝
) |
464 | | fvex 6781 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) ∈ V |
465 | 464 | mptex 7093 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ 𝐴) ∈ V |
466 | 465 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) ∈ V) |
467 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)) |
468 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴) |
469 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
470 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
471 | 467, 468,
469, 470 | fvmptd 6876 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑚) = 𝐴) |
472 | 23, 141, 466, 98, 471 | climconst 15233 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) ⇝ 𝐴) |
473 | 464 | mptex 7093 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V |
474 | 459, 473 | eqeltri 2836 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 ∈ V |
475 | 474 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ V) |
476 | | 1cnd 10954 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
477 | | elnnnn0b 12260 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0
∧ 0 < 𝑀)) |
478 | 21, 67, 477 | sylanbrc 582 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
479 | | divcnvg 43122 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝑀
∈ ℕ) → (𝑗
∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0) |
480 | 476, 478,
479 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) ⇝ 0) |
481 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)) |
482 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴) |
483 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
484 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℝ) |
485 | 481, 482,
483, 484 | fvmptd 6876 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) = 𝐴) |
486 | 98 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
487 | 485, 486 | eqeltrd 2840 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ) |
488 | | eqidd 2740 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))) |
489 | | oveq2 7276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖)) |
490 | 489 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖)) |
491 | 3, 483 | sselid 3923 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℝ) |
492 | | 0red 10962 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 ∈
ℝ) |
493 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
494 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 < 𝑀) |
495 | | eluzle 12577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑖) |
496 | 495 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑖) |
497 | 492, 493,
491, 494, 496 | ltletrd 11118 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 0 < 𝑖) |
498 | 497 | gt0ne0d 11522 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ≠ 0) |
499 | 491, 498 | rereccld 11785 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (1 / 𝑖) ∈
ℝ) |
500 | 488, 490,
483, 499 | fvmptd 6876 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖)) |
501 | 491 | recnd 10987 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝑖 ∈ ℂ) |
502 | 501, 498 | reccld 11727 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (1 / 𝑖) ∈
ℂ) |
503 | 500, 502 | eqeltrd 2840 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ) |
504 | 489 | oveq2d 7284 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖))) |
505 | 484, 499 | readdcld 10988 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ) |
506 | 459, 504,
483, 505 | fvmptd3 6892 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑖) = (𝐴 + (1 / 𝑖))) |
507 | 485, 500 | oveq12d 7286 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖))) |
508 | 506, 507 | eqtr4d 2782 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑖) = (((𝑗 ∈ (ℤ≥‘𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ≥‘𝑀) ↦ (1 / 𝑗))‘𝑖))) |
509 | 23, 141, 472, 475, 480, 487, 503, 508 | climadd 15322 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ⇝ (𝐴 + 0)) |
510 | 98 | addid1d 11158 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
511 | 509, 510 | breqtrd 5104 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ⇝ 𝐴) |
512 | | releldm 5850 |
. . . . . . . . . . . 12
⊢ ((Rel
⇝ ∧ 𝑅 ⇝
𝐴) → 𝑅 ∈ dom ⇝ ) |
513 | 463, 511,
512 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ dom ⇝ ) |
514 | | fveq2 6768 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → (ℤ≥‘𝑙) =
(ℤ≥‘𝑘)) |
515 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑘 → (𝑅‘𝑙) = (𝑅‘𝑘)) |
516 | 515 | oveq2d 7284 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑘 → ((𝑅‘ℎ) − (𝑅‘𝑙)) = ((𝑅‘ℎ) − (𝑅‘𝑘))) |
517 | 516 | fveq2d 6772 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑘 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) = (abs‘((𝑅‘ℎ) − (𝑅‘𝑘)))) |
518 | 517 | breq1d 5088 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
519 | 514, 518 | raleqbidv 3334 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → (∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀ℎ ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
520 | 519 | cbvrabv 3424 |
. . . . . . . . . . . . 13
⊢ {𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
521 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑖 → (𝑅‘ℎ) = (𝑅‘𝑖)) |
522 | 521 | fvoveq1d 7290 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = 𝑖 → (abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) = (abs‘((𝑅‘𝑖) − (𝑅‘𝑘)))) |
523 | 522 | breq1d 5088 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝑖 → ((abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))) |
524 | 523 | cbvralvw 3380 |
. . . . . . . . . . . . . . 15
⊢
(∀ℎ ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) |
525 | 524 | rgenw 3077 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
(ℤ≥‘𝑀)(∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) |
526 | | rabbi 3314 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(ℤ≥‘𝑀)(∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔
∀𝑖 ∈
(ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) ↔ {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}) |
527 | 525, 526 | mpbi 229 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘ℎ) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
528 | 520, 527 | eqtri 2767 |
. . . . . . . . . . . 12
⊢ {𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} |
529 | 528 | infeq1i 9198 |
. . . . . . . . . . 11
⊢
inf({𝑙 ∈
(ℤ≥‘𝑀) ∣ ∀ℎ ∈ (ℤ≥‘𝑙)(abs‘((𝑅‘ℎ) − (𝑅‘𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
= inf({𝑘 ∈
(ℤ≥‘𝑀) ∣ ∀𝑖 ∈ (ℤ≥‘𝑘)(abs‘((𝑅‘𝑖) − (𝑅‘𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, <
) |
530 | 7, 6, 9, 458, 109, 110, 22, 460, 461, 513, 529 | ioodvbdlimc1lem1 43426 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))) ⇝ (lim sup‘(𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))) |
531 | 459 | fvmpt2 6880 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈
(ℤ≥‘𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗))) |
532 | 113, 58, 531 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝑅‘𝑗) = (𝐴 + (1 / 𝑗))) |
533 | 532 | eqcomd 2745 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅‘𝑗)) |
534 | 533 | fveq2d 6772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅‘𝑗))) |
535 | 534 | mpteq2dva 5178 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))) |
536 | 107, 535 | eqtrid 2791 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (𝑗 ∈ (ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗)))) |
537 | 536 | fveq2d 6772 |
. . . . . . . . . 10
⊢ (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝑅‘𝑗))))) |
538 | 530, 536,
537 | 3brtr4d 5110 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⇝ (lim sup‘𝑆)) |
539 | 464 | mptex 7093 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V |
540 | 107, 539 | eqeltri 2836 |
. . . . . . . . . . 11
⊢ 𝑆 ∈ V |
541 | 540 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ V) |
542 | | eqidd 2740 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ℤ) → (𝑆‘𝑐) = (𝑆‘𝑐)) |
543 | 541, 542 | clim 15184 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)))) |
544 | 538, 543 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧
∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎))) |
545 | 544 | simprd 495 |
. . . . . . 7
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)) |
546 | 545 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎)) |
547 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
548 | 547 | rphalfcld 12766 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
549 | | breq2 5082 |
. . . . . . . . 9
⊢ (𝑎 = (𝑥 / 2) → ((abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
550 | 549 | anbi2d 628 |
. . . . . . . 8
⊢ (𝑎 = (𝑥 / 2) → (((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
551 | 550 | rexralbidv 3231 |
. . . . . . 7
⊢ (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))) |
552 | 551 | rspccva 3559 |
. . . . . 6
⊢
((∀𝑎 ∈
ℝ+ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) →
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
553 | 546, 548,
552 | syl2anc 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑏 ∈ ℤ
∀𝑐 ∈
(ℤ≥‘𝑏)((𝑆‘𝑐) ∈ ℂ ∧ (abs‘((𝑆‘𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) |
554 | 450, 553 | r19.29a 3219 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈
(ℤ≥‘𝑁)(abs‘((𝑆‘𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) |
555 | 404, 554 | r19.29a 3219 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
556 | 555 | ralrimiva 3109 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)) |
557 | | ioosscn 13123 |
. . . 4
⊢ (𝐴(,)𝐵) ⊆ ℂ |
558 | 557 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
559 | 453, 558,
98 | ellimc3 25024 |
. 2
⊢ (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 limℂ 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧 ≠ 𝐴 ∧ (abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((𝐹‘𝑧) − (lim sup‘𝑆))) < 𝑥)))) |
560 | 136, 556,
559 | mpbir2and 709 |
1
⊢ (𝜑 → (lim sup‘𝑆) ∈ (𝐹 limℂ 𝐴)) |