Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ioodvbdlimc1lem2 Structured version   Visualization version   GIF version

Theorem ioodvbdlimc1lem2 42201
Description: Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
Hypotheses
Ref Expression
ioodvbdlimc1lem2.a (𝜑𝐴 ∈ ℝ)
ioodvbdlimc1lem2.b (𝜑𝐵 ∈ ℝ)
ioodvbdlimc1lem2.altb (𝜑𝐴 < 𝐵)
ioodvbdlimc1lem2.f (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
ioodvbdlimc1lem2.dmdv (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
ioodvbdlimc1lem2.dvbd (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
ioodvbdlimc1lem2.y 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
ioodvbdlimc1lem2.m 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
ioodvbdlimc1lem2.s 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
ioodvbdlimc1lem2.r 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗)))
ioodvbdlimc1lem2.n 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
ioodvbdlimc1lem2.ch (𝜒 ↔ (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
Assertion
Ref Expression
ioodvbdlimc1lem2 (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐴))
Distinct variable groups:   𝐴,𝑗,𝑥,𝑧,𝑦   𝐵,𝑗,𝑥,𝑧,𝑦   𝑗,𝐹,𝑥,𝑧,𝑦   𝑗,𝑀,𝑥,𝑦   𝑗,𝑁,𝑧   𝑅,𝑗,𝑥,𝑦   𝑥,𝑆,𝑗,𝑦,𝑧   𝑥,𝑌   𝜑,𝑥,𝑗,𝑧,𝑦
Allowed substitution hints:   𝜒(𝑥,𝑦,𝑧,𝑗)   𝑅(𝑧)   𝑀(𝑧)   𝑁(𝑥,𝑦)   𝑌(𝑦,𝑧,𝑗)

Proof of Theorem ioodvbdlimc1lem2
Dummy variables 𝑏 𝑘 𝑖 𝑙 𝑚 𝑤 𝑐 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 12256 . . . . . 6 (ℤ𝑀) ⊆ ℤ
2 zssre 11980 . . . . . 6 ℤ ⊆ ℝ
31, 2sstri 3974 . . . . 5 (ℤ𝑀) ⊆ ℝ
43a1i 11 . . . 4 (𝜑 → (ℤ𝑀) ⊆ ℝ)
5 ioodvbdlimc1lem2.m . . . . . . 7 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
6 ioodvbdlimc1lem2.b . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
7 ioodvbdlimc1lem2.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
86, 7resubcld 11060 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
9 ioodvbdlimc1lem2.altb . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
107, 6posdifd 11219 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
119, 10mpbid 234 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
1211gt0ne0d 11196 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ≠ 0)
138, 12rereccld 11459 . . . . . . . . 9 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ)
14 0red 10636 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
158, 11recgt0d 11566 . . . . . . . . . 10 (𝜑 → 0 < (1 / (𝐵𝐴)))
1614, 13, 15ltled 10780 . . . . . . . . 9 (𝜑 → 0 ≤ (1 / (𝐵𝐴)))
17 flge0nn0 13182 . . . . . . . . 9 (((1 / (𝐵𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵𝐴))) → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
1813, 16, 17syl2anc 586 . . . . . . . 8 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
19 peano2nn0 11929 . . . . . . . 8 ((⌊‘(1 / (𝐵𝐴))) ∈ ℕ0 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
2018, 19syl 17 . . . . . . 7 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
215, 20eqeltrid 2915 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
2221nn0zd 12077 . . . . 5 (𝜑𝑀 ∈ ℤ)
23 eqid 2819 . . . . . 6 (ℤ𝑀) = (ℤ𝑀)
2423uzsup 13223 . . . . 5 (𝑀 ∈ ℤ → sup((ℤ𝑀), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (𝜑 → sup((ℤ𝑀), ℝ*, < ) = +∞)
26 ioodvbdlimc1lem2.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2726adantr 483 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
287rexrd 10683 . . . . . . . 8 (𝜑𝐴 ∈ ℝ*)
2928adantr 483 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ*)
306rexrd 10683 . . . . . . . 8 (𝜑𝐵 ∈ ℝ*)
3130adantr 483 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ*)
327adantr 483 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
33 eluzelre 12246 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℝ)
3433adantl 484 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ)
35 0red 10636 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
36 0red 10636 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 0 ∈ ℝ)
37 1red 10634 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 1 ∈ ℝ)
3836, 37readdcld 10662 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → (0 + 1) ∈ ℝ)
3938adantl 484 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ∈ ℝ)
4036ltp1d 11562 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 0 < (0 + 1))
4140adantl 484 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < (0 + 1))
42 eluzel2 12240 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
4342zred 12079 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℝ)
4443adantl 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
4513flcld 13160 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℤ)
4645zred 12079 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℝ)
47 1red 10634 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℝ)
4818nn0ge0d 11950 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (⌊‘(1 / (𝐵𝐴))))
4914, 46, 47, 48leadd1dd 11246 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵𝐴))) + 1))
5049, 5breqtrrdi 5099 . . . . . . . . . . . . 13 (𝜑 → (0 + 1) ≤ 𝑀)
5150adantr 483 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑀)
52 eluzle 12248 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀𝑗)
5352adantl 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀𝑗)
5439, 44, 34, 51, 53letrd 10789 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑗)
5535, 39, 34, 41, 54ltletrd 10792 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < 𝑗)
5655gt0ne0d 11196 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ≠ 0)
5734, 56rereccld 11459 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ)
5832, 57readdcld 10662 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
5934, 55elrpd 12420 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ+)
6059rpreccld 12433 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ+)
6132, 60ltaddrpd 12456 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
6221nn0red 11948 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
6314, 47readdcld 10662 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ∈ ℝ)
6446, 47readdcld 10662 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ)
6514ltp1d 11562 . . . . . . . . . . . . . 14 (𝜑 → 0 < (0 + 1))
6614, 63, 64, 65, 49ltletrd 10792 . . . . . . . . . . . . 13 (𝜑 → 0 < ((⌊‘(1 / (𝐵𝐴))) + 1))
6766, 5breqtrrdi 5099 . . . . . . . . . . . 12 (𝜑 → 0 < 𝑀)
6867gt0ne0d 11196 . . . . . . . . . . 11 (𝜑𝑀 ≠ 0)
6962, 68rereccld 11459 . . . . . . . . . 10 (𝜑 → (1 / 𝑀) ∈ ℝ)
7069adantr 483 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑀) ∈ ℝ)
7132, 70readdcld 10662 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
726adantr 483 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
7362, 67elrpd 12420 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
7473adantr 483 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ+)
75 1red 10634 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
76 0le1 11155 . . . . . . . . . . 11 0 ≤ 1
7776a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ≤ 1)
7874, 59, 75, 77, 53lediv2ad 12445 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
7957, 70, 32, 78leadd2dd 11247 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
805eqcomi 2828 . . . . . . . . . . . . 13 ((⌊‘(1 / (𝐵𝐴))) + 1) = 𝑀
8180oveq2i 7159 . . . . . . . . . . . 12 (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) = (1 / 𝑀)
8281, 69eqeltrid 2915 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) ∈ ℝ)
8313, 15elrpd 12420 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ+)
8464, 66elrpd 12420 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ+)
85 1rp 12385 . . . . . . . . . . . . . 14 1 ∈ ℝ+
8685a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ+)
87 fllelt 13159 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8988simprd 498 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1))
9083, 84, 86, 89ltdiv2dd 41545 . . . . . . . . . . . 12 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (1 / (1 / (𝐵𝐴))))
918recnd 10661 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℂ)
9291, 12recrecd 11405 . . . . . . . . . . . 12 (𝜑 → (1 / (1 / (𝐵𝐴))) = (𝐵𝐴))
9390, 92breqtrd 5083 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (𝐵𝐴))
9482, 8, 7, 93ltadd2dd 10791 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))) < (𝐴 + (𝐵𝐴)))
955oveq2i 7159 . . . . . . . . . . . 12 (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))
9695oveq2i 7159 . . . . . . . . . . 11 (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)))
9796a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))))
987recnd 10661 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
996recnd 10661 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
10098, 99pncan3d 10992 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
101100eqcomd 2825 . . . . . . . . . 10 (𝜑𝐵 = (𝐴 + (𝐵𝐴)))
10294, 97, 1013brtr4d 5089 . . . . . . . . 9 (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103102adantr 483 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
10458, 71, 72, 79, 103lelttrd 10790 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
10529, 31, 58, 61, 104eliood 41757 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
10627, 105ffvelrnd 6845 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107 ioodvbdlimc1lem2.s . . . . 5 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108106, 107fmptd 6871 . . . 4 (𝜑𝑆:(ℤ𝑀)⟶ℝ)
109 ioodvbdlimc1lem2.dmdv . . . . . 6 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110 ioodvbdlimc1lem2.dvbd . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
1117, 6, 9, 26, 109, 110dvbdfbdioo 42199 . . . . 5 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
11262adantr 483 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113 simpr 487 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ (ℤ𝑀))
114107fvmpt2 6772 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115113, 106, 114syl2anc 586 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116115fveq2d 6667 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117116adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118 simplr 767 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
119105adantlr 713 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120 2fveq3 6668 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
121120breq1d 5067 . . . . . . . . . . . . 13 (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
122121rspccva 3620 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
123118, 119, 122syl2anc 586 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124117, 123eqbrtrd 5079 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) ≤ 𝑏)
125124a1d 25 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
126125ralrimiva 3180 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
127 breq1 5060 . . . . . . . . . . 11 (𝑘 = 𝑀 → (𝑘𝑗𝑀𝑗))
128127imbi1d 344 . . . . . . . . . 10 (𝑘 = 𝑀 → ((𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
129128ralbidv 3195 . . . . . . . . 9 (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
130129rspcev 3621 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
131112, 126, 130syl2anc 586 . . . . . . 7 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
132131ex 415 . . . . . 6 (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
133132reximdv 3271 . . . . 5 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
134111, 133mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
1354, 25, 108, 134limsupre 41906 . . 3 (𝜑 → (lim sup‘𝑆) ∈ ℝ)
136135recnd 10661 . 2 (𝜑 → (lim sup‘𝑆) ∈ ℂ)
137 eluzelre 12246 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
138137adantl 484 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ)
139 0red 10636 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ∈ ℝ)
14045peano2zd 12082 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℤ)
1415, 140eqeltrid 2915 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
142141adantr 483 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
143142zred 12079 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℝ)
144143adantr 483 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀 ∈ ℝ)
14567ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑀)
146 ioodvbdlimc1lem2.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
147 ioodvbdlimc1lem2.y . . . . . . . . . . . . . . . . . . . 20 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
148 ioomidp 41774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
1497, 6, 9, 148syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
150 ne0i 4298 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
151149, 150syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
152 ioossre 12790 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐵) ⊆ ℝ
153152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
154 dvfre 24540 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
15526, 153, 154syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
156109feq2d 6493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
157155, 156mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
158157ffvelrnda 6844 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
159158recnd 10661 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
160159abscld 14788 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
161 eqid 2819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
162 eqid 2819 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
163151, 160, 110, 161, 162suprnmpt 41414 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
164163simpld 497 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
165147, 164eqeltrid 2915 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ∈ ℝ)
166165adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑌 ∈ ℝ)
167 rpre 12389 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
168167rehalfcld 11876 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
169168adantl 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ)
170167recnd 10661 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
171170adantl 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
172 2cnd 11707 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
173 rpne0 12397 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ≠ 0)
174173adantl 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
175 2ne0 11733 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ≠ 0)
177171, 172, 174, 176divne0d 11424 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0)
178166, 169, 177redivcld 11460 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
179178flcld 13160 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
180179peano2zd 12082 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
181180, 142ifcld 4510 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
182146, 181eqeltrid 2915 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
183182zred 12079 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℝ)
184183adantr 483 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
185180zred 12079 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
186 max1 12570 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
187143, 185, 186syl2anc 586 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188187, 146breqtrrdi 5099 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀𝑁)
189188adantr 483 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑁)
190 eluzle 12248 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑁) → 𝑁𝑗)
191190adantl 484 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁𝑗)
192144, 184, 138, 189, 191letrd 10789 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑗)
193139, 144, 138, 145, 192ltletrd 10792 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑗)
194193gt0ne0d 11196 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ≠ 0)
195138, 194rereccld 11459 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ)
196138, 193recgt0d 11566 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < (1 / 𝑗))
197195, 196elrpd 12420 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ+)
198197adantr 483 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ+)
199 ioodvbdlimc1lem2.ch . . . . . . . . 9 (𝜒 ↔ (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
200199biimpi 218 . . . . . . . . . . . . . . . . 17 (𝜒 → (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
201 simp-5l 783 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝜑)
202200, 201syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝜑)
203202, 26syl 17 . . . . . . . . . . . . . . 15 (𝜒𝐹:(𝐴(,)𝐵)⟶ℝ)
204200simplrd 768 . . . . . . . . . . . . . . 15 (𝜒𝑧 ∈ (𝐴(,)𝐵))
205203, 204ffvelrnd 6845 . . . . . . . . . . . . . 14 (𝜒 → (𝐹𝑧) ∈ ℝ)
206205recnd 10661 . . . . . . . . . . . . 13 (𝜒 → (𝐹𝑧) ∈ ℂ)
207202, 108syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑆:(ℤ𝑀)⟶ℝ)
208 simp-5r 784 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+)
209200, 208syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝑥 ∈ ℝ+)
210 eluz2 12241 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
211142, 182, 188, 210syl3anbrc 1337 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑀))
212202, 209, 211syl2anc 586 . . . . . . . . . . . . . . . . 17 (𝜒𝑁 ∈ (ℤ𝑀))
213 uzss 12257 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
214212, 213syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (ℤ𝑁) ⊆ (ℤ𝑀))
215 simp-4r 782 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ𝑁))
216200, 215syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ (ℤ𝑁))
217214, 216sseldd 3966 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (ℤ𝑀))
218207, 217ffvelrnd 6845 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ ℝ)
219218recnd 10661 . . . . . . . . . . . . 13 (𝜒 → (𝑆𝑗) ∈ ℂ)
220202, 136syl 17 . . . . . . . . . . . . 13 (𝜒 → (lim sup‘𝑆) ∈ ℂ)
221206, 219, 220npncand 11013 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) = ((𝐹𝑧) − (lim sup‘𝑆)))
222221eqcomd 2825 . . . . . . . . . . 11 (𝜒 → ((𝐹𝑧) − (lim sup‘𝑆)) = (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))))
223222fveq2d 6667 . . . . . . . . . 10 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))))
224205, 218resubcld 11060 . . . . . . . . . . . . . 14 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℝ)
225202, 135syl 17 . . . . . . . . . . . . . . 15 (𝜒 → (lim sup‘𝑆) ∈ ℝ)
226218, 225resubcld 11060 . . . . . . . . . . . . . 14 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℝ)
227224, 226readdcld 10662 . . . . . . . . . . . . 13 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
228227recnd 10661 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℂ)
229228abscld 14788 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
230224recnd 10661 . . . . . . . . . . . . 13 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℂ)
231230abscld 14788 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ∈ ℝ)
232226recnd 10661 . . . . . . . . . . . . 13 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℂ)
233232abscld 14788 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
234231, 233readdcld 10662 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
235209rpred 12423 . . . . . . . . . . 11 (𝜒𝑥 ∈ ℝ)
236230, 232abstrid 14808 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))))
237235rehalfcld 11876 . . . . . . . . . . . . 13 (𝜒 → (𝑥 / 2) ∈ ℝ)
238206, 219abssubd 14805 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) = (abs‘((𝑆𝑗) − (𝐹𝑧))))
239202, 217, 115syl2anc 586 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
240239fvoveq1d 7170 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))))
241202, 217, 106syl2anc 586 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
242241, 205resubcld 11060 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℝ)
243242recnd 10661 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℂ)
244243abscld 14788 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ∈ ℝ)
245202, 165syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑌 ∈ ℝ)
246202, 217, 58syl2anc 586 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
247152, 204sseldi 3963 . . . . . . . . . . . . . . . . . 18 (𝜒𝑧 ∈ ℝ)
248246, 247resubcld 11060 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
249245, 248remulcld 10663 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ)
250202, 7syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐴 ∈ ℝ)
251202, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐵 ∈ ℝ)
252202, 109syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
253163simprd 498 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
254147breq2i 5065 . . . . . . . . . . . . . . . . . . . . . 22 ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
255254ralbii 3163 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256253, 255sylibr 236 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
257202, 256syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
258 2fveq3 6668 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
259258breq1d 5067 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
260259cbvralvw 3448 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
261257, 260sylibr 236 . . . . . . . . . . . . . . . . . 18 (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
262247rexrd 10683 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 ∈ ℝ*)
263202, 30syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐵 ∈ ℝ*)
264247, 250resubcld 11060 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ∈ ℝ)
265264recnd 10661 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑧𝐴) ∈ ℂ)
266265abscld 14788 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) ∈ ℝ)
2673, 217sseldi 3963 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ∈ ℝ)
268202, 217, 56syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ≠ 0)
269267, 268rereccld 11459 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℝ)
270264leabsd 14766 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ≤ (abs‘(𝑧𝐴)))
271200simprd 498 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) < (1 / 𝑗))
272264, 266, 269, 270, 271lelttrd 10790 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑧𝐴) < (1 / 𝑗))
273247, 250, 269ltsubadd2d 11230 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑧𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
274272, 273mpbid 234 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 < (𝐴 + (1 / 𝑗)))
275202, 217, 104syl2anc 586 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
276262, 263, 246, 274, 275eliood 41757 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
277250, 251, 203, 252, 245, 261, 204, 276dvbdfbdioolem1 42197 . . . . . . . . . . . . . . . . 17 (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · (𝐵𝐴))))
278277simpld 497 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
279202, 217, 57syl2anc 586 . . . . . . . . . . . . . . . . . 18 (𝜒 → (1 / 𝑗) ∈ ℝ)
280245, 279remulcld 10663 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
281157, 149ffvelrnd 6845 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
282281recnd 10661 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
283282abscld 14788 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
284282absge0d 14796 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
285 2fveq3 6668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
286147eqcomi 2828 . . . . . . . . . . . . . . . . . . . . . . . 24 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
288285, 287breq12d 5070 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
289288rspcva 3619 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
290149, 253, 289syl2anc 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
29114, 283, 165, 284, 290letrd 10789 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑌)
292202, 291syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → 0 ≤ 𝑌)
293202, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝐴 ∈ ℝ*)
294 ioogtlb 41754 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
295293, 263, 204, 294syl3anc 1365 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 < 𝑧)
296250, 247, 246, 295ltsub2dd 11245 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
297202, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 ∈ ℂ)
298279recnd 10661 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℂ)
299297, 298pncan2d 10991 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
300296, 299breqtrd 5083 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
301248, 269, 300ltled 10780 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
302248, 269, 245, 292, 301lemul2ad 11572 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
303280adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
304237adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
305 oveq1 7155 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
306298mul02d 10830 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (0 · (1 / 𝑗)) = 0)
307305, 306sylan9eqr 2876 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
308209rphalfcld 12435 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑥 / 2) ∈ ℝ+)
309308rpgt0d 12426 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → 0 < (𝑥 / 2))
310309adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → 0 < (𝑥 / 2))
311307, 310eqbrtrd 5079 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
312303, 304, 311ltled 10780 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
313245adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
314292adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
315 neqne 3022 . . . . . . . . . . . . . . . . . . . . 21 𝑌 = 0 → 𝑌 ≠ 0)
316315adantl 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
317313, 314, 316ne0gt0d 10769 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
318280adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
3193, 212sseldi 3963 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ)
320 0red 10636 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 ∈ ℝ)
321202, 209, 143syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀 ∈ ℝ)
322202, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 < 𝑀)
323202, 209, 188syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀𝑁)
324320, 321, 319, 322, 323ltletrd 10792 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → 0 < 𝑁)
325324gt0ne0d 11196 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ≠ 0)
326319, 325rereccld 11459 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑁) ∈ ℝ)
327245, 326remulcld 10663 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
328327adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
329237adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
330279adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
331326adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
332245adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
333292adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
334319, 324elrpd 12420 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ+)
335202, 217, 59syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑗 ∈ ℝ+)
336 1red 10634 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 1 ∈ ℝ)
33776a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 0 ≤ 1)
338216, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁𝑗)
339334, 335, 336, 337, 338lediv2ad 12445 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
340339adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
341330, 331, 332, 333, 340lemul2ad 11572 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
342235recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ∈ ℂ)
343 2cnd 11707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ∈ ℂ)
344209rpne0d 12428 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ≠ 0)
345175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ≠ 0)
346342, 343, 344, 345divne0d 11424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑥 / 2) ≠ 0)
347245, 237, 346redivcld 11460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
348347adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
349 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
350309adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
351332, 329, 349, 350divgt0d 11567 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
352348, 351elrpd 12420 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ+)
353352rprecred 12434 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
354334adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ+)
355 1red 10634 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
35676a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
357347flcld 13160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
358357peano2zd 12082 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
359358zred 12079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
360202, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜒𝑀 ∈ ℤ)
361358, 360ifcld 4510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
362146, 361eqeltrid 2915 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑁 ∈ ℤ)
363362zred 12079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑁 ∈ ℝ)
364 flltp1 13162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
365347, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
366202, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒𝑀 ∈ ℝ)
367 max2 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
368366, 359, 367syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
369368, 146breqtrrdi 5099 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
370347, 359, 363, 365, 369ltletrd 10792 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
371347, 319, 370ltled 10780 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
372371adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
373352, 354, 355, 356, 372lediv2ad 12445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
374331, 353, 332, 333, 373lemul2ad 11572 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
375332recnd 10661 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
376348recnd 10661 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
377351gt0ne0d 11196 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
378375, 376, 377divrecd 11411 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
379329recnd 10661 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
380349gt0ne0d 11196 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
381346adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
382375, 379, 380, 381ddcand 11428 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
383378, 382eqtr3d 2856 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
384374, 383breqtrd 5083 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
385318, 328, 329, 341, 384letrd 10789 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
386317, 385syldan 593 . . . . . . . . . . . . . . . . . 18 ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
387312, 386pm2.61dan 811 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
388249, 280, 237, 302, 387letrd 10789 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
389244, 249, 237, 278, 388letrd 10789 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑥 / 2))
390240, 389eqbrtrd 5079 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) ≤ (𝑥 / 2))
391238, 390eqbrtrd 5079 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ≤ (𝑥 / 2))
392 simpllr 774 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
393200, 392syl 17 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
394231, 233, 237, 237, 391, 393leltaddd 11254 . . . . . . . . . . . 12 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
3953422halvesd 11875 . . . . . . . . . . . 12 (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
396394, 395breqtrd 5083 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
397229, 234, 235, 236, 396lelttrd 10790 . . . . . . . . . 10 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
398223, 397eqbrtrd 5079 . . . . . . . . 9 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
399199, 398sylbir 237 . . . . . . . 8 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
400399adantrl 714 . . . . . . 7 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗))) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
401400ex 415 . . . . . 6 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
402401ralrimiva 3180 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
403 brimralrspcev 5118 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
404198, 402, 403syl2anc 586 . . . 4 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
405 simpr 487 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑏𝑁)
406405iftrued 4473 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑁)
407 uzid 12250 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
408182, 407syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑁))
409408adantr 483 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑁 ∈ (ℤ𝑁))
410406, 409eqeltrd 2911 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
411410adantlr 713 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
412 iffalse 4474 . . . . . . . . . 10 𝑏𝑁 → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
413412adantl 484 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
414182ad2antrr 724 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℤ)
415 simplr 767 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℤ)
416414zred 12079 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℝ)
417415zred 12079 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℝ)
418 simpr 487 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → ¬ 𝑏𝑁)
419416, 417ltnled 10779 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏𝑁))
420418, 419mpbird 259 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 < 𝑏)
421416, 417, 420ltled 10780 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁𝑏)
422 eluz2 12241 . . . . . . . . . 10 (𝑏 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁𝑏))
423414, 415, 421, 422syl3anbrc 1337 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ (ℤ𝑁))
424413, 423eqeltrd 2911 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
425411, 424pm2.61dan 811 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
426425adantr 483 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
427 simpr 487 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
428 simpr 487 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
429182adantr 483 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
430429, 428ifcld 4510 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ)
431428zred 12079 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
432429zred 12079 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
433 max1 12570 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
434431, 432, 433syl2anc 586 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
435 eluz2 12241 . . . . . . . . . 10 (if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏)))
436428, 430, 434, 435syl3anbrc 1337 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
437436adantr 483 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
438 fveq2 6663 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑐) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
439438eleq1d 2895 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ))
440438fvoveq1d 7170 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
441440breq1d 5067 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
442439, 441anbi12d 632 . . . . . . . . 9 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
443442rspccva 3620 . . . . . . . 8 ((∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏)) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
444427, 437, 443syl2anc 586 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
445444simprd 498 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
446 fveq2 6663 . . . . . . . . 9 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑗) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
447446fvoveq1d 7170 . . . . . . . 8 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
448447breq1d 5067 . . . . . . 7 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
449448rspcev 3621 . . . . . 6 ((if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁) ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
450426, 445, 449syl2anc 586 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
451 ax-resscn 10586 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
452451a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℂ)
45326, 452fssd 6521 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
454 dvcn 24510 . . . . . . . . . . . . . 14 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
455452, 453, 153, 109, 454syl31anc 1367 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
456 cncffvrn 23498 . . . . . . . . . . . . 13 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
457452, 455, 456syl2anc 586 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
45826, 457mpbird 259 . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
459 ioodvbdlimc1lem2.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗)))
460105, 459fmptd 6871 . . . . . . . . . . 11 (𝜑𝑅:(ℤ𝑀)⟶(𝐴(,)𝐵))
461 eqid 2819 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))
462 climrel 14841 . . . . . . . . . . . . 13 Rel ⇝
463462a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ⇝ )
464 fvex 6676 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) ∈ V
465464mptex 6978 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V
466465a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V)
467 eqidd 2820 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
468 eqidd 2820 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
469 simpr 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝑚 ∈ (ℤ𝑀))
4707adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
471467, 468, 469, 470fvmptd 6768 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
47223, 141, 466, 98, 471climconst 14892 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ⇝ 𝐴)
473464mptex 6978 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
474459, 473eqeltri 2907 . . . . . . . . . . . . . . 15 𝑅 ∈ V
475474a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ V)
476 1cnd 10628 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
477 elnnnn0b 11933 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0 ∧ 0 < 𝑀))
47821, 67, 477sylanbrc 585 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
479 divcnvg 41892 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
480476, 478, 479syl2anc 586 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
481 eqidd 2820 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
482 eqidd 2820 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
483 simpr 487 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
4847adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
485481, 482, 483, 484fvmptd 6768 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
48698adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℂ)
487485, 486eqeltrd 2911 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
488 eqidd 2820 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)))
489 oveq2 7156 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
490489adantl 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
4913, 483sseldi 3963 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
492 0red 10636 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
49362adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
49467adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑀)
495 eluzle 12248 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
496495adantl 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
497492, 493, 491, 494, 496ltletrd 10792 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑖)
498497gt0ne0d 11196 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≠ 0)
499491, 498rereccld 11459 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℝ)
500488, 490, 483, 499fvmptd 6768 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
501491recnd 10661 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℂ)
502501, 498reccld 11401 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℂ)
503500, 502eqeltrd 2911 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
504489oveq2d 7164 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
505484, 499readdcld 10662 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
506459, 504, 483, 505fvmptd3 6784 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (𝐴 + (1 / 𝑖)))
507485, 500oveq12d 7166 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
508506, 507eqtr4d 2857 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)))
50923, 141, 472, 475, 480, 487, 503, 508climadd 14980 . . . . . . . . . . . . 13 (𝜑𝑅 ⇝ (𝐴 + 0))
51098addid1d 10832 . . . . . . . . . . . . 13 (𝜑 → (𝐴 + 0) = 𝐴)
511509, 510breqtrd 5083 . . . . . . . . . . . 12 (𝜑𝑅𝐴)
512 releldm 5807 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅𝐴) → 𝑅 ∈ dom ⇝ )
513463, 511, 512syl2anc 586 . . . . . . . . . . 11 (𝜑𝑅 ∈ dom ⇝ )
514 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → (ℤ𝑙) = (ℤ𝑘))
515 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → (𝑅𝑙) = (𝑅𝑘))
516515oveq2d 7164 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → ((𝑅) − (𝑅𝑙)) = ((𝑅) − (𝑅𝑘)))
517516fveq2d 6667 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑘 → (abs‘((𝑅) − (𝑅𝑙))) = (abs‘((𝑅) − (𝑅𝑘))))
518517breq1d 5067 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → ((abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
519514, 518raleqbidv 3400 . . . . . . . . . . . . . 14 (𝑙 = 𝑘 → (∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
520519cbvrabv 3490 . . . . . . . . . . . . 13 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
521 fveq2 6663 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (𝑅) = (𝑅𝑖))
522521fvoveq1d 7170 . . . . . . . . . . . . . . . . 17 ( = 𝑖 → (abs‘((𝑅) − (𝑅𝑘))) = (abs‘((𝑅𝑖) − (𝑅𝑘))))
523522breq1d 5067 . . . . . . . . . . . . . . . 16 ( = 𝑖 → ((abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
524523cbvralvw 3448 . . . . . . . . . . . . . . 15 (∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
525524rgenw 3148 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑀)(∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
526 rabbi 3382 . . . . . . . . . . . . . 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))})
527525, 526mpbi 232 . . . . . . . . . . . . 13 {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
528520, 527eqtri 2842 . . . . . . . . . . . 12 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
529528infeq1i 8934 . . . . . . . . . . 11 inf({𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
5307, 6, 9, 458, 109, 110, 22, 460, 461, 513, 529ioodvbdlimc1lem1 42200 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
531459fvmpt2 6772 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
532113, 58, 531syl2anc 586 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
533532eqcomd 2825 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅𝑗))
534533fveq2d 6667 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅𝑗)))
535534mpteq2dva 5152 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
536107, 535syl5eq 2866 . . . . . . . . . 10 (𝜑𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
537536fveq2d 6667 . . . . . . . . . 10 (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
538530, 536, 5373brtr4d 5089 . . . . . . . . 9 (𝜑𝑆 ⇝ (lim sup‘𝑆))
539464mptex 6978 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
540107, 539eqeltri 2907 . . . . . . . . . . 11 𝑆 ∈ V
541540a1i 11 . . . . . . . . . 10 (𝜑𝑆 ∈ V)
542 eqidd 2820 . . . . . . . . . 10 ((𝜑𝑐 ∈ ℤ) → (𝑆𝑐) = (𝑆𝑐))
543541, 542clim 14843 . . . . . . . . 9 (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))))
544538, 543mpbid 234 . . . . . . . 8 (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎)))
545544simprd 498 . . . . . . 7 (𝜑 → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
546545adantr 483 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
547 simpr 487 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
548547rphalfcld 12435 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
549 breq2 5061 . . . . . . . . 9 (𝑎 = (𝑥 / 2) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
550549anbi2d 630 . . . . . . . 8 (𝑎 = (𝑥 / 2) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
551550rexralbidv 3299 . . . . . . 7 (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
552551rspccva 3620 . . . . . 6 ((∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
553546, 548, 552syl2anc 586 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
554450, 553r19.29a 3287 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
555404, 554r19.29a 3287 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
556555ralrimiva 3180 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
557 ioosscn 41753 . . . 4 (𝐴(,)𝐵) ⊆ ℂ
558557a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
559453, 558, 98ellimc3 24469 . 2 (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))))
560136, 556, 559mpbir2and 711 1 (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398   = wceq 1530  wcel 2107  wne 3014  wral 3136  wrex 3137  {crab 3140  Vcvv 3493  wss 3934  c0 4289  ifcif 4465   class class class wbr 5057  cmpt 5137  dom cdm 5548  ran crn 5549  Rel wrel 5553  wf 6344  cfv 6348  (class class class)co 7148  supcsup 8896  infcinf 8897  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  +∞cpnf 10664  *cxr 10666   < clt 10667  cle 10668  cmin 10862   / cdiv 11289  cn 11630  2c2 11684  0cn0 11889  cz 11973  cuz 12235  +crp 12381  (,)cioo 12730  cfl 13152  abscabs 14585  lim supclsp 14819  cli 14833  cnccncf 23476   lim climc 24452   D cdv 24453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-supp 7823  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12885  df-fzo 13026  df-fl 13154  df-seq 13362  df-exp 13422  df-hash 13683  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20529  df-xmet 20530  df-met 20531  df-bl 20532  df-mopn 20533  df-fbas 20534  df-fg 20535  df-cnfld 20538  df-top 21494  df-topon 21511  df-topsp 21533  df-bases 21546  df-cld 21619  df-ntr 21620  df-cls 21621  df-nei 21698  df-lp 21736  df-perf 21737  df-cn 21827  df-cnp 21828  df-haus 21915  df-cmp 21987  df-tx 22162  df-hmeo 22355  df-fil 22446  df-fm 22538  df-flim 22539  df-flf 22540  df-xms 22922  df-ms 22923  df-tms 22924  df-cncf 23478  df-limc 24456  df-dv 24457
This theorem is referenced by:  ioodvbdlimc1  42202
  Copyright terms: Public domain W3C validator