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

Theorem ioodvbdlimc2lem 44165
Description: Limit at the upper 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
ioodvbdlimc2lem.a (𝜑𝐴 ∈ ℝ)
ioodvbdlimc2lem.b (𝜑𝐵 ∈ ℝ)
ioodvbdlimc2lem.altb (𝜑𝐴 < 𝐵)
ioodvbdlimc2lem.f (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
ioodvbdlimc2lem.dmdv (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
ioodvbdlimc2lem.dvbd (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
ioodvbdlimc2lem.y 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
ioodvbdlimc2lem.m 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
ioodvbdlimc2lem.s 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗))))
ioodvbdlimc2lem.r 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐵 − (1 / 𝑗)))
ioodvbdlimc2lem.n 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
ioodvbdlimc2lem.ch (𝜒 ↔ (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)))
Assertion
Ref Expression
ioodvbdlimc2lem (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐵))
Distinct variable groups:   𝐴,𝑗,𝑥,𝑧,𝑦   𝐵,𝑗,𝑥,𝑧,𝑦   𝑗,𝐹,𝑥,𝑧,𝑦   𝑗,𝑀,𝑥,𝑦   𝑗,𝑁,𝑧   𝑅,𝑗,𝑥,𝑦   𝑥,𝑆,𝑗,𝑦,𝑧   𝑥,𝑌   𝜑,𝑥,𝑗,𝑧,𝑦
Allowed substitution hints:   𝜒(𝑥,𝑦,𝑧,𝑗)   𝑅(𝑧)   𝑀(𝑧)   𝑁(𝑥,𝑦)   𝑌(𝑦,𝑧,𝑗)

Proof of Theorem ioodvbdlimc2lem
Dummy variables 𝑏 𝑘 𝑖 𝑙 𝑤 𝑚 𝑐 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 12784 . . . . . 6 (ℤ𝑀) ⊆ ℤ
2 zssre 12506 . . . . . 6 ℤ ⊆ ℝ
31, 2sstri 3953 . . . . 5 (ℤ𝑀) ⊆ ℝ
43a1i 11 . . . 4 (𝜑 → (ℤ𝑀) ⊆ ℝ)
5 ioodvbdlimc2lem.m . . . . . . 7 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
6 ioodvbdlimc2lem.b . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
7 ioodvbdlimc2lem.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
86, 7resubcld 11583 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
9 ioodvbdlimc2lem.altb . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
107, 6posdifd 11742 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
119, 10mpbid 231 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
1211gt0ne0d 11719 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ≠ 0)
138, 12rereccld 11982 . . . . . . . . 9 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ)
14 0red 11158 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
158, 11recgt0d 12089 . . . . . . . . . 10 (𝜑 → 0 < (1 / (𝐵𝐴)))
1614, 13, 15ltled 11303 . . . . . . . . 9 (𝜑 → 0 ≤ (1 / (𝐵𝐴)))
17 flge0nn0 13725 . . . . . . . . 9 (((1 / (𝐵𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵𝐴))) → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
1813, 16, 17syl2anc 584 . . . . . . . 8 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
19 peano2nn0 12453 . . . . . . . 8 ((⌊‘(1 / (𝐵𝐴))) ∈ ℕ0 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
2018, 19syl 17 . . . . . . 7 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
215, 20eqeltrid 2842 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
2221nn0zd 12525 . . . . 5 (𝜑𝑀 ∈ ℤ)
23 eqid 2736 . . . . . 6 (ℤ𝑀) = (ℤ𝑀)
2423uzsup 13768 . . . . 5 (𝑀 ∈ ℤ → sup((ℤ𝑀), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (𝜑 → sup((ℤ𝑀), ℝ*, < ) = +∞)
26 ioodvbdlimc2lem.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2726adantr 481 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
287rexrd 11205 . . . . . . . 8 (𝜑𝐴 ∈ ℝ*)
2928adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ*)
306rexrd 11205 . . . . . . . 8 (𝜑𝐵 ∈ ℝ*)
3130adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ*)
326adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
33 eluzelre 12774 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℝ)
3433adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ)
35 0red 11158 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
36 0red 11158 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 0 ∈ ℝ)
37 1red 11156 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 1 ∈ ℝ)
3836, 37readdcld 11184 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → (0 + 1) ∈ ℝ)
3938adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ∈ ℝ)
4036ltp1d 12085 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 0 < (0 + 1))
4140adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < (0 + 1))
42 eluzel2 12768 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
4342zred 12607 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℝ)
4443adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
4513flcld 13703 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℤ)
4645zred 12607 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℝ)
47 1red 11156 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℝ)
4818nn0ge0d 12476 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (⌊‘(1 / (𝐵𝐴))))
4914, 46, 47, 48leadd1dd 11769 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵𝐴))) + 1))
5049, 5breqtrrdi 5147 . . . . . . . . . . . . 13 (𝜑 → (0 + 1) ≤ 𝑀)
5150adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑀)
52 eluzle 12776 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀𝑗)
5352adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀𝑗)
5439, 44, 34, 51, 53letrd 11312 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑗)
5535, 39, 34, 41, 54ltletrd 11315 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < 𝑗)
5655gt0ne0d 11719 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ≠ 0)
5734, 56rereccld 11982 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ)
5832, 57resubcld 11583 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑗)) ∈ ℝ)
597adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
6021nn0red 12474 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
6114, 47readdcld 11184 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ∈ ℝ)
6246, 47readdcld 11184 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ)
6314ltp1d 12085 . . . . . . . . . . . . . 14 (𝜑 → 0 < (0 + 1))
6414, 61, 62, 63, 49ltletrd 11315 . . . . . . . . . . . . 13 (𝜑 → 0 < ((⌊‘(1 / (𝐵𝐴))) + 1))
6564, 5breqtrrdi 5147 . . . . . . . . . . . 12 (𝜑 → 0 < 𝑀)
6665gt0ne0d 11719 . . . . . . . . . . 11 (𝜑𝑀 ≠ 0)
6760, 66rereccld 11982 . . . . . . . . . 10 (𝜑 → (1 / 𝑀) ∈ ℝ)
6867adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑀) ∈ ℝ)
6932, 68resubcld 11583 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑀)) ∈ ℝ)
705eqcomi 2745 . . . . . . . . . . . . 13 ((⌊‘(1 / (𝐵𝐴))) + 1) = 𝑀
7170oveq2i 7368 . . . . . . . . . . . 12 (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) = (1 / 𝑀)
7271, 67eqeltrid 2842 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) ∈ ℝ)
7313, 15elrpd 12954 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ+)
7462, 64elrpd 12954 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ+)
75 1rp 12919 . . . . . . . . . . . . . 14 1 ∈ ℝ+
7675a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ+)
77 fllelt 13702 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
7813, 77syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
7978simprd 496 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1))
8073, 74, 76, 79ltdiv2dd 43518 . . . . . . . . . . . 12 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (1 / (1 / (𝐵𝐴))))
818recnd 11183 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℂ)
8281, 12recrecd 11928 . . . . . . . . . . . 12 (𝜑 → (1 / (1 / (𝐵𝐴))) = (𝐵𝐴))
8380, 82breqtrd 5131 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (𝐵𝐴))
8472, 8, 6, 83ltsub2dd 11768 . . . . . . . . . 10 (𝜑 → (𝐵 − (𝐵𝐴)) < (𝐵 − (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))))
856recnd 11183 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
867recnd 11183 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
8785, 86nncand 11517 . . . . . . . . . 10 (𝜑 → (𝐵 − (𝐵𝐴)) = 𝐴)
8871oveq2i 7368 . . . . . . . . . . 11 (𝐵 − (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))) = (𝐵 − (1 / 𝑀))
8988a1i 11 . . . . . . . . . 10 (𝜑 → (𝐵 − (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))) = (𝐵 − (1 / 𝑀)))
9084, 87, 893brtr3d 5136 . . . . . . . . 9 (𝜑𝐴 < (𝐵 − (1 / 𝑀)))
9190adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 < (𝐵 − (1 / 𝑀)))
9260, 65elrpd 12954 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
9392adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ+)
9434, 55elrpd 12954 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ+)
95 1red 11156 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
96 0le1 11678 . . . . . . . . . . 11 0 ≤ 1
9796a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ≤ 1)
9893, 94, 95, 97, 53lediv2ad 12979 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
9957, 68, 32, 98lesub2dd 11772 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑀)) ≤ (𝐵 − (1 / 𝑗)))
10059, 69, 58, 91, 99ltletrd 11315 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 < (𝐵 − (1 / 𝑗)))
10194rpreccld 12967 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ+)
10232, 101ltsubrpd 12989 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑗)) < 𝐵)
10329, 31, 58, 100, 102eliood 43726 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
10427, 103ffvelcdmd 7036 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ)
105 ioodvbdlimc2lem.s . . . . 5 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗))))
106104, 105fmptd 7062 . . . 4 (𝜑𝑆:(ℤ𝑀)⟶ℝ)
107 ioodvbdlimc2lem.dmdv . . . . . 6 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
108 ioodvbdlimc2lem.dvbd . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
1097, 6, 9, 26, 107, 108dvbdfbdioo 44161 . . . . 5 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
11060adantr 481 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
111 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ (ℤ𝑀))
112105fvmpt2 6959 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐹‘(𝐵 − (1 / 𝑗))) ∈ ℝ) → (𝑆𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
113111, 104, 112syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑆𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
114113fveq2d 6846 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
115114adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
116 simplr 767 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
117103adantlr 713 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
118 2fveq3 6847 . . . . . . . . . . . . . 14 (𝑥 = (𝐵 − (1 / 𝑗)) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))))
119118breq1d 5115 . . . . . . . . . . . . 13 (𝑥 = (𝐵 − (1 / 𝑗)) → ((abs‘(𝐹𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏))
120119rspccva 3580 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 ∧ (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)
121116, 117, 120syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝐵 − (1 / 𝑗)))) ≤ 𝑏)
122115, 121eqbrtrd 5127 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) ≤ 𝑏)
123122a1d 25 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
124123ralrimiva 3143 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
125 breq1 5108 . . . . . . . . . . 11 (𝑘 = 𝑀 → (𝑘𝑗𝑀𝑗))
126125imbi1d 341 . . . . . . . . . 10 (𝑘 = 𝑀 → ((𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
127126ralbidv 3174 . . . . . . . . 9 (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
128127rspcev 3581 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
129110, 124, 128syl2anc 584 . . . . . . 7 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
130129ex 413 . . . . . 6 (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
131130reximdv 3167 . . . . 5 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
132109, 131mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
1334, 25, 106, 132limsupre 43872 . . 3 (𝜑 → (lim sup‘𝑆) ∈ ℝ)
134133recnd 11183 . 2 (𝜑 → (lim sup‘𝑆) ∈ ℂ)
135 eluzelre 12774 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
136135adantl 482 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ)
137 0red 11158 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ∈ ℝ)
13845peano2zd 12610 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℤ)
1395, 138eqeltrid 2842 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
140139adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
141140zred 12607 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℝ)
142141adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀 ∈ ℝ)
14365ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑀)
144 ioodvbdlimc2lem.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
145 ioodvbdlimc2lem.y . . . . . . . . . . . . . . . . . . . 20 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
146 ioomidp 43742 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
1477, 6, 9, 146syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
148 ne0i 4294 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
149147, 148syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
150 ioossre 13325 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐵) ⊆ ℝ
151150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
152 dvfre 25315 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
15326, 151, 152syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
154107feq2d 6654 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
155153, 154mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
156155ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
157156recnd 11183 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
158157abscld 15321 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
159 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
160 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
161149, 158, 108, 159, 160suprnmpt 43381 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
162161simpld 495 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
163145, 162eqeltrid 2842 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ∈ ℝ)
164163adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑌 ∈ ℝ)
165 rpre 12923 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
166165rehalfcld 12400 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
167166adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ)
168165recnd 11183 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
169168adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
170 2cnd 12231 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
171 rpne0 12931 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ≠ 0)
172171adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
173 2ne0 12257 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
174173a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ≠ 0)
175169, 170, 172, 174divne0d 11947 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0)
176164, 167, 175redivcld 11983 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
177176flcld 13703 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
178177peano2zd 12610 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
179178, 140ifcld 4532 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
180144, 179eqeltrid 2842 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
181180zred 12607 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℝ)
182181adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
183178zred 12607 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
184 max1 13104 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
185141, 183, 184syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
186185, 144breqtrrdi 5147 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀𝑁)
187186adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑁)
188 eluzle 12776 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑁) → 𝑁𝑗)
189188adantl 482 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁𝑗)
190142, 182, 136, 187, 189letrd 11312 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑗)
191137, 142, 136, 143, 190ltletrd 11315 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑗)
192191gt0ne0d 11719 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ≠ 0)
193136, 192rereccld 11982 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ)
194136, 191recgt0d 12089 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < (1 / 𝑗))
195193, 194elrpd 12954 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ+)
196195adantr 481 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ+)
197 ioodvbdlimc2lem.ch . . . . . . . . 9 (𝜒 ↔ (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)))
198197biimpi 215 . . . . . . . . . . . . . . . . 17 (𝜒 → (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)))
199 simp-5l 783 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → 𝜑)
200198, 199syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝜑)
201200, 26syl 17 . . . . . . . . . . . . . . 15 (𝜒𝐹:(𝐴(,)𝐵)⟶ℝ)
202198simplrd 768 . . . . . . . . . . . . . . 15 (𝜒𝑧 ∈ (𝐴(,)𝐵))
203201, 202ffvelcdmd 7036 . . . . . . . . . . . . . 14 (𝜒 → (𝐹𝑧) ∈ ℝ)
204203recnd 11183 . . . . . . . . . . . . 13 (𝜒 → (𝐹𝑧) ∈ ℂ)
205200, 106syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑆:(ℤ𝑀)⟶ℝ)
206 simp-5r 784 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+)
207198, 206syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝑥 ∈ ℝ+)
208 eluz2 12769 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
209140, 180, 186, 208syl3anbrc 1343 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑀))
210200, 207, 209syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜒𝑁 ∈ (ℤ𝑀))
211 uzss 12786 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
212210, 211syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (ℤ𝑁) ⊆ (ℤ𝑀))
213 simp-4r 782 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ𝑁))
214198, 213syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ (ℤ𝑁))
215212, 214sseldd 3945 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (ℤ𝑀))
216205, 215ffvelcdmd 7036 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ ℝ)
217216recnd 11183 . . . . . . . . . . . . 13 (𝜒 → (𝑆𝑗) ∈ ℂ)
218200, 134syl 17 . . . . . . . . . . . . 13 (𝜒 → (lim sup‘𝑆) ∈ ℂ)
219204, 217, 218npncand 11536 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) = ((𝐹𝑧) − (lim sup‘𝑆)))
220219eqcomd 2742 . . . . . . . . . . 11 (𝜒 → ((𝐹𝑧) − (lim sup‘𝑆)) = (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))))
221220fveq2d 6846 . . . . . . . . . 10 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))))
222203, 216resubcld 11583 . . . . . . . . . . . . . 14 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℝ)
223200, 133syl 17 . . . . . . . . . . . . . . 15 (𝜒 → (lim sup‘𝑆) ∈ ℝ)
224216, 223resubcld 11583 . . . . . . . . . . . . . 14 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℝ)
225222, 224readdcld 11184 . . . . . . . . . . . . 13 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
226225recnd 11183 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℂ)
227226abscld 15321 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
228222recnd 11183 . . . . . . . . . . . . 13 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℂ)
229228abscld 15321 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ∈ ℝ)
230224recnd 11183 . . . . . . . . . . . . 13 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℂ)
231230abscld 15321 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
232229, 231readdcld 11184 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
233207rpred 12957 . . . . . . . . . . 11 (𝜒𝑥 ∈ ℝ)
234228, 230abstrid 15341 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))))
235233rehalfcld 12400 . . . . . . . . . . . . 13 (𝜒 → (𝑥 / 2) ∈ ℝ)
236200, 215, 113syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑆𝑗) = (𝐹‘(𝐵 − (1 / 𝑗))))
237236oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) = ((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗)))))
238237fveq2d 6846 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) = (abs‘((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))))
239238, 229eqeltrrd 2839 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ∈ ℝ)
240200, 163syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑌 ∈ ℝ)
241150, 202sselid 3942 . . . . . . . . . . . . . . . . 17 (𝜒𝑧 ∈ ℝ)
242200, 215, 58syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ)
243241, 242resubcld 11583 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ∈ ℝ)
244240, 243remulcld 11185 . . . . . . . . . . . . . . 15 (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∈ ℝ)
245200, 7syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝐴 ∈ ℝ)
246200, 6syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝐵 ∈ ℝ)
247200, 107syl 17 . . . . . . . . . . . . . . . . 17 (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
248161simprd 496 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
249145breq2i 5113 . . . . . . . . . . . . . . . . . . . . 21 ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
250249ralbii 3096 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
251248, 250sylibr 233 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
252200, 251syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
253 2fveq3 6847 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
254253breq1d 5115 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
255254cbvralvw 3225 . . . . . . . . . . . . . . . . . 18 (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
256252, 255sylibr 233 . . . . . . . . . . . . . . . . 17 (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
257200, 215, 103syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝐵 − (1 / 𝑗)) ∈ (𝐴(,)𝐵))
258242rexrd 11205 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐵 − (1 / 𝑗)) ∈ ℝ*)
259200, 30syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐵 ∈ ℝ*)
2603, 215sselid 3942 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑗 ∈ ℝ)
261200, 215, 56syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑗 ≠ 0)
262260, 261rereccld 11982 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (1 / 𝑗) ∈ ℝ)
263246, 241resubcld 11583 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝐵𝑧) ∈ ℝ)
264241, 246resubcld 11583 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑧𝐵) ∈ ℝ)
265264recnd 11183 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐵) ∈ ℂ)
266265abscld 15321 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (abs‘(𝑧𝐵)) ∈ ℝ)
267263leabsd 15299 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝐵𝑧) ≤ (abs‘(𝐵𝑧)))
268200, 85syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝐵 ∈ ℂ)
269241recnd 11183 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑧 ∈ ℂ)
270268, 269abssubd 15338 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝐵𝑧)) = (abs‘(𝑧𝐵)))
271267, 270breqtrd 5131 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝐵𝑧) ≤ (abs‘(𝑧𝐵)))
272198simprd 496 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (abs‘(𝑧𝐵)) < (1 / 𝑗))
273263, 266, 262, 271, 272lelttrd 11313 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐵𝑧) < (1 / 𝑗))
274246, 241, 262, 273ltsub23d 11760 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐵 − (1 / 𝑗)) < 𝑧)
275200, 28syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐴 ∈ ℝ*)
276 iooltub 43738 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑧 ∈ (𝐴(,)𝐵)) → 𝑧 < 𝐵)
277275, 259, 202, 276syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (𝜒𝑧 < 𝐵)
278258, 259, 241, 274, 277eliood 43726 . . . . . . . . . . . . . . . . 17 (𝜒𝑧 ∈ ((𝐵 − (1 / 𝑗))(,)𝐵))
279245, 246, 201, 247, 240, 256, 257, 278dvbdfbdioolem1 44159 . . . . . . . . . . . . . . . 16 (𝜒 → ((abs‘((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ∧ (abs‘((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝐵𝐴))))
280279simpld 495 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))))
281200, 215, 57syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜒 → (1 / 𝑗) ∈ ℝ)
282240, 281remulcld 11185 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
283155, 147ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
284283recnd 11183 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
285284abscld 15321 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
286284absge0d 15329 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
287 2fveq3 6847 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
288145eqcomi 2745 . . . . . . . . . . . . . . . . . . . . . . 23 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
289288a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
290287, 289breq12d 5118 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
291290rspcva 3579 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
292147, 248, 291syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
29314, 285, 163, 286, 292letrd 11312 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ 𝑌)
294200, 293syl 17 . . . . . . . . . . . . . . . . 17 (𝜒 → 0 ≤ 𝑌)
295281recnd 11183 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (1 / 𝑗) ∈ ℂ)
296 sub31 43514 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (1 / 𝑗) ∈ ℂ) → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵𝑧)))
297269, 268, 295, 296syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) = ((1 / 𝑗) − (𝐵𝑧)))
298241, 246posdifd 11742 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑧 < 𝐵 ↔ 0 < (𝐵𝑧)))
299277, 298mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → 0 < (𝐵𝑧))
300263, 299elrpd 12954 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝐵𝑧) ∈ ℝ+)
301281, 300ltsubrpd 12989 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ((1 / 𝑗) − (𝐵𝑧)) < (1 / 𝑗))
302297, 301eqbrtrd 5127 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) < (1 / 𝑗))
303243, 281, 302ltled 11303 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑧 − (𝐵 − (1 / 𝑗))) ≤ (1 / 𝑗))
304243, 281, 240, 294, 303lemul2ad 12095 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑌 · (1 / 𝑗)))
305282adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
306235adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
307 oveq1 7364 . . . . . . . . . . . . . . . . . . . 20 (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
308295mul02d 11353 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (0 · (1 / 𝑗)) = 0)
309307, 308sylan9eqr 2798 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
310207rphalfcld 12969 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑥 / 2) ∈ ℝ+)
311310rpgt0d 12960 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → 0 < (𝑥 / 2))
312311adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → 0 < (𝑥 / 2))
313309, 312eqbrtrd 5127 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
314305, 306, 313ltled 11303 . . . . . . . . . . . . . . . . 17 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
315240adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
316294adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
317 neqne 2951 . . . . . . . . . . . . . . . . . . . 20 𝑌 = 0 → 𝑌 ≠ 0)
318317adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
319315, 316, 318ne0gt0d 11292 . . . . . . . . . . . . . . . . . 18 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
320282adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
3213, 210sselid 3942 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑁 ∈ ℝ)
322 0red 11158 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → 0 ∈ ℝ)
323200, 207, 141syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒𝑀 ∈ ℝ)
324200, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → 0 < 𝑀)
325200, 207, 186syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒𝑀𝑁)
326322, 323, 321, 324, 325ltletrd 11315 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 0 < 𝑁)
327326gt0ne0d 11719 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑁 ≠ 0)
328321, 327rereccld 11982 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑁) ∈ ℝ)
329240, 328remulcld 11185 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
330329adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
331235adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
332281adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
333328adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
334240adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
335294adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
336321, 326elrpd 12954 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑁 ∈ ℝ+)
337200, 215, 94syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ∈ ℝ+)
338 1red 11156 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → 1 ∈ ℝ)
33996a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → 0 ≤ 1)
340214, 188syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑁𝑗)
341336, 337, 338, 339, 340lediv2ad 12979 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
342341adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
343332, 333, 334, 335, 342lemul2ad 12095 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
344233recnd 11183 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑥 ∈ ℂ)
345 2cnd 12231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → 2 ∈ ℂ)
346207rpne0d 12962 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑥 ≠ 0)
347173a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → 2 ≠ 0)
348344, 345, 346, 347divne0d 11947 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑥 / 2) ≠ 0)
349240, 235, 348redivcld 11983 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
350349adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
351 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
352311adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
353334, 331, 351, 352divgt0d 12090 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
354350, 353elrpd 12954 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ+)
355354rprecred 12968 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
356336adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ+)
357 1red 11156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
35896a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
359349flcld 13703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
360359peano2zd 12610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
361360zred 12607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
362200, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒𝑀 ∈ ℤ)
363360, 362ifcld 4532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
364144, 363eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑁 ∈ ℤ)
365364zred 12607 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑁 ∈ ℝ)
366 flltp1 13705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
367349, 366syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
368200, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑀 ∈ ℝ)
369 max2 13106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
370368, 361, 369syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
371370, 144breqtrrdi 5147 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
372349, 361, 365, 367, 371ltletrd 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
373349, 321, 372ltled 11303 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
374373adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
375354, 356, 357, 358, 374lediv2ad 12979 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
376333, 355, 334, 335, 375lemul2ad 12095 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
377334recnd 11183 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
378350recnd 11183 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
379353gt0ne0d 11719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
380377, 378, 379divrecd 11934 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
381331recnd 11183 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
382351gt0ne0d 11719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
383348adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
384377, 381, 382, 383ddcand 11951 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
385380, 384eqtr3d 2778 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
386376, 385breqtrd 5131 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
387320, 330, 331, 343, 386letrd 11312 . . . . . . . . . . . . . . . . . 18 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
388319, 387syldan 591 . . . . . . . . . . . . . . . . 17 ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
389314, 388pm2.61dan 811 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390244, 282, 235, 304, 389letrd 11312 . . . . . . . . . . . . . . 15 (𝜒 → (𝑌 · (𝑧 − (𝐵 − (1 / 𝑗)))) ≤ (𝑥 / 2))
391239, 244, 235, 280, 390letrd 11312 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝐹𝑧) − (𝐹‘(𝐵 − (1 / 𝑗))))) ≤ (𝑥 / 2))
392238, 391eqbrtrd 5127 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ≤ (𝑥 / 2))
393 simpllr 774 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
394198, 393syl 17 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
395229, 231, 235, 235, 392, 394leltaddd 11777 . . . . . . . . . . . 12 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
3963442halvesd 12399 . . . . . . . . . . . 12 (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
397395, 396breqtrd 5131 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
398227, 232, 233, 234, 397lelttrd 11313 . . . . . . . . . 10 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
399221, 398eqbrtrd 5127 . . . . . . . . 9 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
400197, 399sylbir 234 . . . . . . . 8 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
401400adantrl 714 . . . . . . 7 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗))) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
402401ex 413 . . . . . 6 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
403402ralrimiva 3143 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
404 brimralrspcev 5166 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
405196, 403, 404syl2anc 584 . . . 4 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
406 simpr 485 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑏𝑁)
407406iftrued 4494 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑁)
408 uzid 12778 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
409180, 408syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑁))
410409adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑁 ∈ (ℤ𝑁))
411407, 410eqeltrd 2838 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
412411adantlr 713 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
413 iffalse 4495 . . . . . . . . . 10 𝑏𝑁 → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
414413adantl 482 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
415180ad2antrr 724 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℤ)
416 simplr 767 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℤ)
417415zred 12607 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℝ)
418416zred 12607 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℝ)
419 simpr 485 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → ¬ 𝑏𝑁)
420417, 418ltnled 11302 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏𝑁))
421419, 420mpbird 256 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 < 𝑏)
422417, 418, 421ltled 11303 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁𝑏)
423 eluz2 12769 . . . . . . . . . 10 (𝑏 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁𝑏))
424415, 416, 422, 423syl3anbrc 1343 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ (ℤ𝑁))
425414, 424eqeltrd 2838 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
426412, 425pm2.61dan 811 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
427426adantr 481 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
428 simpr 485 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
429 simpr 485 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
430180adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
431430, 429ifcld 4532 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ)
432429zred 12607 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
433430zred 12607 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
434 max1 13104 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
435432, 433, 434syl2anc 584 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
436 eluz2 12769 . . . . . . . . . 10 (if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏)))
437429, 431, 435, 436syl3anbrc 1343 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
438437adantr 481 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
439 fveq2 6842 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑐) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
440439eleq1d 2822 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ))
441439fvoveq1d 7379 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
442441breq1d 5115 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
443440, 442anbi12d 631 . . . . . . . . 9 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
444443rspccva 3580 . . . . . . . 8 ((∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏)) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
445428, 438, 444syl2anc 584 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
446445simprd 496 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
447 fveq2 6842 . . . . . . . . 9 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑗) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
448447fvoveq1d 7379 . . . . . . . 8 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
449448breq1d 5115 . . . . . . 7 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
450449rspcev 3581 . . . . . 6 ((if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁) ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
451427, 446, 450syl2anc 584 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
452 ax-resscn 11108 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
453452a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℂ)
45426, 453fssd 6686 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
455 dvcn 25285 . . . . . . . . . . . . . 14 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
456453, 454, 151, 107, 455syl31anc 1373 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
457 cncfcdm 24261 . . . . . . . . . . . . 13 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
458453, 456, 457syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
45926, 458mpbird 256 . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
460 ioodvbdlimc2lem.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐵 − (1 / 𝑗)))
461103, 460fmptd 7062 . . . . . . . . . . 11 (𝜑𝑅:(ℤ𝑀)⟶(𝐴(,)𝐵))
462 eqid 2736 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))
463 climrel 15374 . . . . . . . . . . . . 13 Rel ⇝
464463a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ⇝ )
465 fvex 6855 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) ∈ V
466465mptex 7173 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ 𝐵) ∈ V
467466a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐵) ∈ V)
468 eqidd 2737 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐵))
469 eqidd 2737 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑚) → 𝐵 = 𝐵)
470 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝑚 ∈ (ℤ𝑀))
4716adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
472468, 469, 470, 471fvmptd 6955 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐵)‘𝑚) = 𝐵)
47323, 22, 467, 85, 472climconst 15425 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐵) ⇝ 𝐵)
474465mptex 7173 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ (𝐵 − (1 / 𝑗))) ∈ V
475460, 474eqeltri 2834 . . . . . . . . . . . . . . 15 𝑅 ∈ V
476475a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ V)
477 1cnd 11150 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
478 elnnnn0b 12457 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0 ∧ 0 < 𝑀))
47921, 65, 478sylanbrc 583 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
480 divcnvg 43858 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
481477, 479, 480syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
482 eqidd 2737 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐵) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐵))
483 eqidd 2737 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → 𝐵 = 𝐵)
484 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
4856adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
486482, 483, 484, 485fvmptd 6955 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐵)‘𝑖) = 𝐵)
487486, 485eqeltrd 2838 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐵)‘𝑖) ∈ ℝ)
488487recnd 11183 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐵)‘𝑖) ∈ ℂ)
489 eqidd 2737 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)))
490 oveq2 7365 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
491490adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
4923, 484sselid 3942 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
493 0red 11158 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
49460adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
49565adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑀)
496 eluzle 12776 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
497496adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
498493, 494, 492, 495, 497ltletrd 11315 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑖)
499498gt0ne0d 11719 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≠ 0)
500492, 499rereccld 11982 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℝ)
501489, 491, 484, 500fvmptd 6955 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
502492recnd 11183 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℂ)
503502, 499reccld 11924 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℂ)
504501, 503eqeltrd 2838 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
505490oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐵 − (1 / 𝑗)) = (𝐵 − (1 / 𝑖)))
506 ovex 7390 . . . . . . . . . . . . . . . . 17 (𝐵 − (1 / 𝑖)) ∈ V
507505, 460, 506fvmpt 6948 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (ℤ𝑀) → (𝑅𝑖) = (𝐵 − (1 / 𝑖)))
508507adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (𝐵 − (1 / 𝑖)))
509486, 501oveq12d 7375 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (((𝑗 ∈ (ℤ𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐵 − (1 / 𝑖)))
510508, 509eqtr4d 2779 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (((𝑗 ∈ (ℤ𝑀) ↦ 𝐵)‘𝑖) − ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)))
51123, 22, 473, 476, 481, 488, 504, 510climsub 15516 . . . . . . . . . . . . 13 (𝜑𝑅 ⇝ (𝐵 − 0))
51285subid1d 11501 . . . . . . . . . . . . 13 (𝜑 → (𝐵 − 0) = 𝐵)
513511, 512breqtrd 5131 . . . . . . . . . . . 12 (𝜑𝑅𝐵)
514 releldm 5899 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅𝐵) → 𝑅 ∈ dom ⇝ )
515464, 513, 514syl2anc 584 . . . . . . . . . . 11 (𝜑𝑅 ∈ dom ⇝ )
516 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → (ℤ𝑙) = (ℤ𝑘))
517 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → (𝑅𝑙) = (𝑅𝑘))
518517oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → ((𝑅) − (𝑅𝑙)) = ((𝑅) − (𝑅𝑘)))
519518fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑘 → (abs‘((𝑅) − (𝑅𝑙))) = (abs‘((𝑅) − (𝑅𝑘))))
520519breq1d 5115 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → ((abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
521516, 520raleqbidv 3319 . . . . . . . . . . . . . 14 (𝑙 = 𝑘 → (∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
522521cbvrabv 3417 . . . . . . . . . . . . 13 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
523 fveq2 6842 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (𝑅) = (𝑅𝑖))
524523fvoveq1d 7379 . . . . . . . . . . . . . . . . 17 ( = 𝑖 → (abs‘((𝑅) − (𝑅𝑘))) = (abs‘((𝑅𝑖) − (𝑅𝑘))))
525524breq1d 5115 . . . . . . . . . . . . . . . 16 ( = 𝑖 → ((abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
526525cbvralvw 3225 . . . . . . . . . . . . . . 15 (∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
527526rgenw 3068 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑀)(∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
528 rabbi 3432 . . . . . . . . . . . . . 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))})
529527, 528mpbi 229 . . . . . . . . . . . . 13 {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
530522, 529eqtri 2764 . . . . . . . . . . . 12 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
531530infeq1i 9414 . . . . . . . . . . 11 inf({𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
5327, 6, 9, 459, 107, 108, 22, 461, 462, 515, 531ioodvbdlimc1lem1 44162 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
533460fvmpt2 6959 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐵 − (1 / 𝑗)) ∈ ℝ) → (𝑅𝑗) = (𝐵 − (1 / 𝑗)))
534111, 58, 533syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑅𝑗) = (𝐵 − (1 / 𝑗)))
535534eqcomd 2742 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐵 − (1 / 𝑗)) = (𝑅𝑗))
536535fveq2d 6846 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐵 − (1 / 𝑗))) = (𝐹‘(𝑅𝑗)))
537536mpteq2dva 5205 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
538105, 537eqtrid 2788 . . . . . . . . . 10 (𝜑𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
539538fveq2d 6846 . . . . . . . . . 10 (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
540532, 538, 5393brtr4d 5137 . . . . . . . . 9 (𝜑𝑆 ⇝ (lim sup‘𝑆))
541465mptex 7173 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐵 − (1 / 𝑗)))) ∈ V
542105, 541eqeltri 2834 . . . . . . . . . . 11 𝑆 ∈ V
543542a1i 11 . . . . . . . . . 10 (𝜑𝑆 ∈ V)
544 eqidd 2737 . . . . . . . . . 10 ((𝜑𝑐 ∈ ℤ) → (𝑆𝑐) = (𝑆𝑐))
545543, 544clim 15376 . . . . . . . . 9 (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))))
546540, 545mpbid 231 . . . . . . . 8 (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎)))
547546simprd 496 . . . . . . 7 (𝜑 → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
548547adantr 481 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
549 simpr 485 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
550549rphalfcld 12969 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
551 breq2 5109 . . . . . . . . 9 (𝑎 = (𝑥 / 2) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
552551anbi2d 629 . . . . . . . 8 (𝑎 = (𝑥 / 2) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
553552rexralbidv 3214 . . . . . . 7 (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
554553rspccva 3580 . . . . . 6 ((∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
555548, 550, 554syl2anc 584 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
556451, 555r19.29a 3159 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
557405, 556r19.29a 3159 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
558557ralrimiva 3143 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
559 ioosscn 13326 . . . 4 (𝐴(,)𝐵) ⊆ ℂ
560559a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
561454, 560, 85ellimc3 25243 . 2 (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim 𝐵) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐵 ∧ (abs‘(𝑧𝐵)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))))
562134, 558, 561mpbir2and 711 1 (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  wss 3910  c0 4282  ifcif 4486   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  Rel wrel 5638  wf 6492  cfv 6496  (class class class)co 7357  supcsup 9376  infcinf 9377  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  +crp 12915  (,)cioo 13264  cfl 13695  abscabs 15119  lim supclsp 15352  cli 15366  cnccncf 24239   lim climc 25226   D cdv 25227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231
This theorem is referenced by:  ioodvbdlimc2  44166
  Copyright terms: Public domain W3C validator