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 41057
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 12012 . . . . . 6 (ℤ𝑀) ⊆ ℤ
2 zssre 11735 . . . . . 6 ℤ ⊆ ℝ
31, 2sstri 3829 . . . . 5 (ℤ𝑀) ⊆ ℝ
43a1i 11 . . . 4 (𝜑 → (ℤ𝑀) ⊆ ℝ)
5 ioodvbdlimc1lem2.m . . . . . . 7 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
6 ioodvbdlimc1lem2.b . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
7 ioodvbdlimc1lem2.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
86, 7resubcld 10803 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
9 ioodvbdlimc1lem2.altb . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
107, 6posdifd 10962 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
119, 10mpbid 224 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
1211gt0ne0d 10939 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ≠ 0)
138, 12rereccld 11202 . . . . . . . . 9 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ)
14 0red 10380 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
158, 11recgt0d 11312 . . . . . . . . . 10 (𝜑 → 0 < (1 / (𝐵𝐴)))
1614, 13, 15ltled 10524 . . . . . . . . 9 (𝜑 → 0 ≤ (1 / (𝐵𝐴)))
17 flge0nn0 12940 . . . . . . . . 9 (((1 / (𝐵𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵𝐴))) → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
1813, 16, 17syl2anc 579 . . . . . . . 8 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
19 peano2nn0 11684 . . . . . . . 8 ((⌊‘(1 / (𝐵𝐴))) ∈ ℕ0 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
2018, 19syl 17 . . . . . . 7 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
215, 20syl5eqel 2862 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
2221nn0zd 11832 . . . . 5 (𝜑𝑀 ∈ ℤ)
23 eqid 2777 . . . . . 6 (ℤ𝑀) = (ℤ𝑀)
2423uzsup 12981 . . . . 5 (𝑀 ∈ ℤ → sup((ℤ𝑀), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (𝜑 → sup((ℤ𝑀), ℝ*, < ) = +∞)
26 ioodvbdlimc1lem2.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2726adantr 474 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
287rexrd 10426 . . . . . . . 8 (𝜑𝐴 ∈ ℝ*)
2928adantr 474 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ*)
306rexrd 10426 . . . . . . . 8 (𝜑𝐵 ∈ ℝ*)
3130adantr 474 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ*)
327adantr 474 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
33 eluzelre 12003 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℝ)
3433adantl 475 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ)
35 0red 10380 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
36 0red 10380 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 0 ∈ ℝ)
37 1red 10377 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 1 ∈ ℝ)
3836, 37readdcld 10406 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → (0 + 1) ∈ ℝ)
3938adantl 475 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ∈ ℝ)
4036ltp1d 11308 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 0 < (0 + 1))
4140adantl 475 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < (0 + 1))
42 eluzel2 11997 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
4342zred 11834 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℝ)
4443adantl 475 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
4513flcld 12918 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℤ)
4645zred 11834 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℝ)
47 1red 10377 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℝ)
4818nn0ge0d 11705 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (⌊‘(1 / (𝐵𝐴))))
4914, 46, 47, 48leadd1dd 10989 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵𝐴))) + 1))
5049, 5syl6breqr 4928 . . . . . . . . . . . . 13 (𝜑 → (0 + 1) ≤ 𝑀)
5150adantr 474 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑀)
52 eluzle 12005 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀𝑗)
5352adantl 475 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀𝑗)
5439, 44, 34, 51, 53letrd 10533 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑗)
5535, 39, 34, 41, 54ltletrd 10536 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < 𝑗)
5655gt0ne0d 10939 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ≠ 0)
5734, 56rereccld 11202 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ)
5832, 57readdcld 10406 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
5934, 55elrpd 12178 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ+)
6059rpreccld 12191 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ+)
6132, 60ltaddrpd 12214 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
6221nn0red 11703 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
6314, 47readdcld 10406 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ∈ ℝ)
6446, 47readdcld 10406 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ)
6514ltp1d 11308 . . . . . . . . . . . . . 14 (𝜑 → 0 < (0 + 1))
6614, 63, 64, 65, 49ltletrd 10536 . . . . . . . . . . . . 13 (𝜑 → 0 < ((⌊‘(1 / (𝐵𝐴))) + 1))
6766, 5syl6breqr 4928 . . . . . . . . . . . 12 (𝜑 → 0 < 𝑀)
6867gt0ne0d 10939 . . . . . . . . . . 11 (𝜑𝑀 ≠ 0)
6962, 68rereccld 11202 . . . . . . . . . 10 (𝜑 → (1 / 𝑀) ∈ ℝ)
7069adantr 474 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑀) ∈ ℝ)
7132, 70readdcld 10406 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
726adantr 474 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
7362, 67elrpd 12178 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
7473adantr 474 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ+)
75 1red 10377 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
76 0le1 10898 . . . . . . . . . . 11 0 ≤ 1
7776a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ≤ 1)
7874, 59, 75, 77, 53lediv2ad 12203 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
7957, 70, 32, 78leadd2dd 10990 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
805eqcomi 2786 . . . . . . . . . . . . 13 ((⌊‘(1 / (𝐵𝐴))) + 1) = 𝑀
8180oveq2i 6933 . . . . . . . . . . . 12 (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) = (1 / 𝑀)
8281, 69syl5eqel 2862 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) ∈ ℝ)
8313, 15elrpd 12178 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ+)
8464, 66elrpd 12178 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ+)
85 1rp 12141 . . . . . . . . . . . . . 14 1 ∈ ℝ+
8685a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ+)
87 fllelt 12917 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8988simprd 491 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1))
9083, 84, 86, 89ltdiv2dd 40399 . . . . . . . . . . . 12 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (1 / (1 / (𝐵𝐴))))
918recnd 10405 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℂ)
9291, 12recrecd 11148 . . . . . . . . . . . 12 (𝜑 → (1 / (1 / (𝐵𝐴))) = (𝐵𝐴))
9390, 92breqtrd 4912 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (𝐵𝐴))
9482, 8, 7, 93ltadd2dd 10535 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))) < (𝐴 + (𝐵𝐴)))
955oveq2i 6933 . . . . . . . . . . . 12 (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))
9695oveq2i 6933 . . . . . . . . . . 11 (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)))
9796a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))))
987recnd 10405 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
996recnd 10405 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
10098, 99pncan3d 10737 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
101100eqcomd 2783 . . . . . . . . . 10 (𝜑𝐵 = (𝐴 + (𝐵𝐴)))
10294, 97, 1013brtr4d 4918 . . . . . . . . 9 (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103102adantr 474 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
10458, 71, 72, 79, 103lelttrd 10534 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
10529, 31, 58, 61, 104eliood 40614 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
10627, 105ffvelrnd 6624 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107 ioodvbdlimc1lem2.s . . . . 5 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108106, 107fmptd 6648 . . . 4 (𝜑𝑆:(ℤ𝑀)⟶ℝ)
109 ioodvbdlimc1lem2.dmdv . . . . . 6 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110 ioodvbdlimc1lem2.dvbd . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
1117, 6, 9, 26, 109, 110dvbdfbdioo 41055 . . . . 5 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
11262adantr 474 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ (ℤ𝑀))
114107fvmpt2 6552 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115113, 106, 114syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116115fveq2d 6450 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117116adantlr 705 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118 simplr 759 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
119105adantlr 705 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120 2fveq3 6451 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
121120breq1d 4896 . . . . . . . . . . . . 13 (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
122121rspccva 3509 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
123118, 119, 122syl2anc 579 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124117, 123eqbrtrd 4908 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) ≤ 𝑏)
125124a1d 25 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
126125ralrimiva 3147 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
127 breq1 4889 . . . . . . . . . . 11 (𝑘 = 𝑀 → (𝑘𝑗𝑀𝑗))
128127imbi1d 333 . . . . . . . . . 10 (𝑘 = 𝑀 → ((𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
129128ralbidv 3167 . . . . . . . . 9 (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
130129rspcev 3510 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
131112, 126, 130syl2anc 579 . . . . . . 7 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
132131ex 403 . . . . . 6 (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
133132reximdv 3196 . . . . 5 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
134111, 133mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
1354, 25, 108, 134limsupre 40763 . . 3 (𝜑 → (lim sup‘𝑆) ∈ ℝ)
136135recnd 10405 . 2 (𝜑 → (lim sup‘𝑆) ∈ ℂ)
137 eluzelre 12003 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
138137adantl 475 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ)
139 0red 10380 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ∈ ℝ)
14045peano2zd 11837 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℤ)
1415, 140syl5eqel 2862 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
142141adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
143142zred 11834 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℝ)
144143adantr 474 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀 ∈ ℝ)
14567ad2antrr 716 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑀)
146 ioodvbdlimc1lem2.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
147 ioodvbdlimc1lem2.y . . . . . . . . . . . . . . . . . . . 20 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
148 ioomidp 40631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
1497, 6, 9, 148syl3anc 1439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
150 ne0i 4148 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
151149, 150syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
152 ioossre 12547 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐵) ⊆ ℝ
153152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
154 dvfre 24151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
15526, 153, 154syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
156109feq2d 6277 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
157155, 156mpbid 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
158157ffvelrnda 6623 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
159158recnd 10405 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
160159abscld 14583 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
161 eqid 2777 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
162 eqid 2777 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
163151, 160, 110, 161, 162suprnmpt 40261 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
164163simpld 490 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
165147, 164syl5eqel 2862 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ∈ ℝ)
166165adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑌 ∈ ℝ)
167 rpre 12145 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
168167rehalfcld 11629 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
169168adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ)
170167recnd 10405 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
171170adantl 475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
172 2cnd 11453 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
173 rpne0 12155 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ≠ 0)
174173adantl 475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
175 2ne0 11486 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ≠ 0)
177171, 172, 174, 176divne0d 11167 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0)
178166, 169, 177redivcld 11203 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
179178flcld 12918 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
180179peano2zd 11837 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
181180, 142ifcld 4351 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
182146, 181syl5eqel 2862 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
183182zred 11834 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℝ)
184183adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
185180zred 11834 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
186 max1 12328 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
187143, 185, 186syl2anc 579 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188187, 146syl6breqr 4928 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀𝑁)
189188adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑁)
190 eluzle 12005 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑁) → 𝑁𝑗)
191190adantl 475 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁𝑗)
192144, 184, 138, 189, 191letrd 10533 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑗)
193139, 144, 138, 145, 192ltletrd 10536 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑗)
194193gt0ne0d 10939 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ≠ 0)
195138, 194rereccld 11202 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ)
196138, 193recgt0d 11312 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < (1 / 𝑗))
197195, 196elrpd 12178 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ+)
198197adantr 474 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ+)
199 ioodvbdlimc1lem2.ch . . . . . . . . 9 (𝜒 ↔ (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
200199biimpi 208 . . . . . . . . . . . . . . . . 17 (𝜒 → (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
201 simp-5l 775 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝜑)
202200, 201syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝜑)
203202, 26syl 17 . . . . . . . . . . . . . . 15 (𝜒𝐹:(𝐴(,)𝐵)⟶ℝ)
204200simplrd 760 . . . . . . . . . . . . . . 15 (𝜒𝑧 ∈ (𝐴(,)𝐵))
205203, 204ffvelrnd 6624 . . . . . . . . . . . . . 14 (𝜒 → (𝐹𝑧) ∈ ℝ)
206205recnd 10405 . . . . . . . . . . . . 13 (𝜒 → (𝐹𝑧) ∈ ℂ)
207202, 108syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑆:(ℤ𝑀)⟶ℝ)
208 simp-5r 776 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+)
209200, 208syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝑥 ∈ ℝ+)
210 eluz2 11998 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
211142, 182, 188, 210syl3anbrc 1400 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑀))
212202, 209, 211syl2anc 579 . . . . . . . . . . . . . . . . 17 (𝜒𝑁 ∈ (ℤ𝑀))
213 uzss 12013 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
214212, 213syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (ℤ𝑁) ⊆ (ℤ𝑀))
215 simp-4r 774 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ𝑁))
216200, 215syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ (ℤ𝑁))
217214, 216sseldd 3821 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (ℤ𝑀))
218207, 217ffvelrnd 6624 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ ℝ)
219218recnd 10405 . . . . . . . . . . . . 13 (𝜒 → (𝑆𝑗) ∈ ℂ)
220202, 136syl 17 . . . . . . . . . . . . 13 (𝜒 → (lim sup‘𝑆) ∈ ℂ)
221206, 219, 220npncand 10758 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) = ((𝐹𝑧) − (lim sup‘𝑆)))
222221eqcomd 2783 . . . . . . . . . . 11 (𝜒 → ((𝐹𝑧) − (lim sup‘𝑆)) = (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))))
223222fveq2d 6450 . . . . . . . . . 10 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))))
224205, 218resubcld 10803 . . . . . . . . . . . . . 14 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℝ)
225202, 135syl 17 . . . . . . . . . . . . . . 15 (𝜒 → (lim sup‘𝑆) ∈ ℝ)
226218, 225resubcld 10803 . . . . . . . . . . . . . 14 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℝ)
227224, 226readdcld 10406 . . . . . . . . . . . . 13 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
228227recnd 10405 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℂ)
229228abscld 14583 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
230224recnd 10405 . . . . . . . . . . . . 13 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℂ)
231230abscld 14583 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ∈ ℝ)
232226recnd 10405 . . . . . . . . . . . . 13 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℂ)
233232abscld 14583 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
234231, 233readdcld 10406 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
235209rpred 12181 . . . . . . . . . . 11 (𝜒𝑥 ∈ ℝ)
236230, 232abstrid 14603 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))))
237235rehalfcld 11629 . . . . . . . . . . . . 13 (𝜒 → (𝑥 / 2) ∈ ℝ)
238206, 219abssubd 14600 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) = (abs‘((𝑆𝑗) − (𝐹𝑧))))
239202, 217, 115syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
240239fvoveq1d 6944 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))))
241202, 217, 106syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
242241, 205resubcld 10803 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℝ)
243242recnd 10405 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℂ)
244243abscld 14583 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ∈ ℝ)
245202, 165syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑌 ∈ ℝ)
246202, 217, 58syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
247152, 204sseldi 3818 . . . . . . . . . . . . . . . . . 18 (𝜒𝑧 ∈ ℝ)
248246, 247resubcld 10803 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
249245, 248remulcld 10407 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ)
250202, 7syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐴 ∈ ℝ)
251202, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐵 ∈ ℝ)
252202, 109syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
253163simprd 491 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
254147breq2i 4894 . . . . . . . . . . . . . . . . . . . . . 22 ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
255254ralbii 3161 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256253, 255sylibr 226 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
257202, 256syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
258 2fveq3 6451 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
259258breq1d 4896 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
260259cbvralv 3366 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
261257, 260sylibr 226 . . . . . . . . . . . . . . . . . 18 (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
262247rexrd 10426 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 ∈ ℝ*)
263202, 30syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐵 ∈ ℝ*)
264247, 250resubcld 10803 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ∈ ℝ)
265264recnd 10405 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑧𝐴) ∈ ℂ)
266265abscld 14583 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) ∈ ℝ)
2673, 217sseldi 3818 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ∈ ℝ)
268202, 217, 56syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ≠ 0)
269267, 268rereccld 11202 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℝ)
270264leabsd 14561 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ≤ (abs‘(𝑧𝐴)))
271200simprd 491 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) < (1 / 𝑗))
272264, 266, 269, 270, 271lelttrd 10534 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑧𝐴) < (1 / 𝑗))
273247, 250, 269ltsubadd2d 10973 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑧𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
274272, 273mpbid 224 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 < (𝐴 + (1 / 𝑗)))
275202, 217, 104syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
276262, 263, 246, 274, 275eliood 40614 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
277250, 251, 203, 252, 245, 261, 204, 276dvbdfbdioolem1 41053 . . . . . . . . . . . . . . . . 17 (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · (𝐵𝐴))))
278277simpld 490 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
279202, 217, 57syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜒 → (1 / 𝑗) ∈ ℝ)
280245, 279remulcld 10407 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
281157, 149ffvelrnd 6624 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
282281recnd 10405 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
283282abscld 14583 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
284282absge0d 14591 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
285 2fveq3 6451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
286147eqcomi 2786 . . . . . . . . . . . . . . . . . . . . . . . 24 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
288285, 287breq12d 4899 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
289288rspcva 3508 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
290149, 253, 289syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
29114, 283, 165, 284, 290letrd 10533 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑌)
292202, 291syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → 0 ≤ 𝑌)
293202, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝐴 ∈ ℝ*)
294 ioogtlb 40611 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
295293, 263, 204, 294syl3anc 1439 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 < 𝑧)
296250, 247, 246, 295ltsub2dd 10988 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
297202, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 ∈ ℂ)
298279recnd 10405 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℂ)
299297, 298pncan2d 10736 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
300296, 299breqtrd 4912 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
301248, 269, 300ltled 10524 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
302248, 269, 245, 292, 301lemul2ad 11318 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
303280adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
304237adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
305 oveq1 6929 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
306298mul02d 10574 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (0 · (1 / 𝑗)) = 0)
307305, 306sylan9eqr 2835 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
308209rphalfcld 12193 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑥 / 2) ∈ ℝ+)
309308rpgt0d 12184 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → 0 < (𝑥 / 2))
310309adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → 0 < (𝑥 / 2))
311307, 310eqbrtrd 4908 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
312303, 304, 311ltled 10524 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
313245adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
314292adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
315 neqne 2976 . . . . . . . . . . . . . . . . . . . . 21 𝑌 = 0 → 𝑌 ≠ 0)
316315adantl 475 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
317313, 314, 316ne0gt0d 10513 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
318280adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
3193, 212sseldi 3818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ)
320 0red 10380 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 ∈ ℝ)
321202, 209, 143syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀 ∈ ℝ)
322202, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 < 𝑀)
323202, 209, 188syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀𝑁)
324320, 321, 319, 322, 323ltletrd 10536 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → 0 < 𝑁)
325324gt0ne0d 10939 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ≠ 0)
326319, 325rereccld 11202 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑁) ∈ ℝ)
327245, 326remulcld 10407 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
328327adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
329237adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
330279adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
331326adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
332245adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
333292adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
334319, 324elrpd 12178 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ+)
335202, 217, 59syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑗 ∈ ℝ+)
336 1red 10377 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 1 ∈ ℝ)
33776a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 0 ≤ 1)
338216, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁𝑗)
339334, 335, 336, 337, 338lediv2ad 12203 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
340339adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
341330, 331, 332, 333, 340lemul2ad 11318 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
342235recnd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ∈ ℂ)
343 2cnd 11453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ∈ ℂ)
344209rpne0d 12186 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ≠ 0)
345175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ≠ 0)
346342, 343, 344, 345divne0d 11167 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑥 / 2) ≠ 0)
347245, 237, 346redivcld 11203 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
348347adantr 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
349 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
350309adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
351332, 329, 349, 350divgt0d 11313 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
352348, 351elrpd 12178 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ+)
353352rprecred 12192 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
354334adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ+)
355 1red 10377 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
35676a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
357347flcld 12918 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
358357peano2zd 11837 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
359358zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
360202, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜒𝑀 ∈ ℤ)
361358, 360ifcld 4351 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
362146, 361syl5eqel 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑁 ∈ ℤ)
363362zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑁 ∈ ℝ)
364 flltp1 12920 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
365347, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
366202, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒𝑀 ∈ ℝ)
367 max2 12330 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
368366, 359, 367syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
369368, 146syl6breqr 4928 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
370347, 359, 363, 365, 369ltletrd 10536 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
371347, 319, 370ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
372371adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
373352, 354, 355, 356, 372lediv2ad 12203 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
374331, 353, 332, 333, 373lemul2ad 11318 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
375332recnd 10405 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
376348recnd 10405 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
377351gt0ne0d 10939 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
378375, 376, 377divrecd 11154 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
379329recnd 10405 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
380349gt0ne0d 10939 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
381346adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
382375, 379, 380, 381ddcand 11171 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
383378, 382eqtr3d 2815 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
384374, 383breqtrd 4912 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
385318, 328, 329, 341, 384letrd 10533 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
386317, 385syldan 585 . . . . . . . . . . . . . . . . . 18 ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
387312, 386pm2.61dan 803 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
388249, 280, 237, 302, 387letrd 10533 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
389244, 249, 237, 278, 388letrd 10533 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑥 / 2))
390240, 389eqbrtrd 4908 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) ≤ (𝑥 / 2))
391238, 390eqbrtrd 4908 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ≤ (𝑥 / 2))
392 simpllr 766 . . . . . . . . . . . . . 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 10997 . . . . . . . . . . . 12 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
3953422halvesd 11628 . . . . . . . . . . . 12 (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
396394, 395breqtrd 4912 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
397229, 234, 235, 236, 396lelttrd 10534 . . . . . . . . . 10 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
398223, 397eqbrtrd 4908 . . . . . . . . 9 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
399199, 398sylbir 227 . . . . . . . 8 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
400399adantrl 706 . . . . . . 7 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗))) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
401400ex 403 . . . . . 6 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
402401ralrimiva 3147 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
403 brimralrspcev 4947 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
404198, 402, 403syl2anc 579 . . . 4 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
405 simpr 479 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑏𝑁)
406405iftrued 4314 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑁)
407 uzid 12007 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
408182, 407syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑁))
409408adantr 474 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑁 ∈ (ℤ𝑁))
410406, 409eqeltrd 2858 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
411410adantlr 705 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
412 iffalse 4315 . . . . . . . . . 10 𝑏𝑁 → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
413412adantl 475 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
414182ad2antrr 716 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℤ)
415 simplr 759 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℤ)
416414zred 11834 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℝ)
417415zred 11834 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℝ)
418 simpr 479 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → ¬ 𝑏𝑁)
419416, 417ltnled 10523 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏𝑁))
420418, 419mpbird 249 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 < 𝑏)
421416, 417, 420ltled 10524 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁𝑏)
422 eluz2 11998 . . . . . . . . . 10 (𝑏 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁𝑏))
423414, 415, 421, 422syl3anbrc 1400 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ (ℤ𝑁))
424413, 423eqeltrd 2858 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
425411, 424pm2.61dan 803 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
426425adantr 474 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
427 simpr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
428 simpr 479 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
429182adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
430429, 428ifcld 4351 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ)
431428zred 11834 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
432429zred 11834 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
433 max1 12328 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
434431, 432, 433syl2anc 579 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
435 eluz2 11998 . . . . . . . . . 10 (if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏)))
436428, 430, 434, 435syl3anbrc 1400 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
437436adantr 474 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
438 fveq2 6446 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑐) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
439438eleq1d 2843 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ))
440438fvoveq1d 6944 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
441440breq1d 4896 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
442439, 441anbi12d 624 . . . . . . . . 9 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
443442rspccva 3509 . . . . . . . 8 ((∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏)) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
444427, 437, 443syl2anc 579 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
445444simprd 491 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
446 fveq2 6446 . . . . . . . . 9 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑗) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
447446fvoveq1d 6944 . . . . . . . 8 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
448447breq1d 4896 . . . . . . 7 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
449448rspcev 3510 . . . . . 6 ((if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁) ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
450426, 445, 449syl2anc 579 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
451 ax-resscn 10329 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
452451a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℂ)
45326, 452fssd 6305 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
454 dvcn 24121 . . . . . . . . . . . . . 14 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
455452, 453, 153, 109, 454syl31anc 1441 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
456 cncffvrn 23109 . . . . . . . . . . . . 13 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
457452, 455, 456syl2anc 579 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
45826, 457mpbird 249 . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
459 ioodvbdlimc1lem2.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗)))
460105, 459fmptd 6648 . . . . . . . . . . 11 (𝜑𝑅:(ℤ𝑀)⟶(𝐴(,)𝐵))
461 eqid 2777 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))
462 climrel 14631 . . . . . . . . . . . . 13 Rel ⇝
463462a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ⇝ )
464 fvex 6459 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) ∈ V
465464mptex 6758 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V
466465a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V)
467 eqidd 2778 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
468 eqidd 2778 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
469 simpr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝑚 ∈ (ℤ𝑀))
4707adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
471467, 468, 469, 470fvmptd 6548 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
47223, 141, 466, 98, 471climconst 14682 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ⇝ 𝐴)
473464mptex 6758 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
474459, 473eqeltri 2854 . . . . . . . . . . . . . . 15 𝑅 ∈ V
475474a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ V)
476 1cnd 10371 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
477 elnnnn0b 11688 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0 ∧ 0 < 𝑀))
47821, 67, 477sylanbrc 578 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
479 divcnvg 40749 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
480476, 478, 479syl2anc 579 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
481 eqidd 2778 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
482 eqidd 2778 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
483 simpr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
4847adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
485481, 482, 483, 484fvmptd 6548 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
48698adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℂ)
487485, 486eqeltrd 2858 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
488 eqidd 2778 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)))
489 oveq2 6930 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
490489adantl 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
4913, 483sseldi 3818 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
492 0red 10380 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
49362adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
49467adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑀)
495 eluzle 12005 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
496495adantl 475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
497492, 493, 491, 494, 496ltletrd 10536 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑖)
498497gt0ne0d 10939 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≠ 0)
499491, 498rereccld 11202 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℝ)
500488, 490, 483, 499fvmptd 6548 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
501491recnd 10405 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℂ)
502501, 498reccld 11144 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℂ)
503500, 502eqeltrd 2858 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
504489oveq2d 6938 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
505484, 499readdcld 10406 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
506459, 504, 483, 505fvmptd3 6564 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (𝐴 + (1 / 𝑖)))
507485, 500oveq12d 6940 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
508506, 507eqtr4d 2816 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)))
50923, 141, 472, 475, 480, 487, 503, 508climadd 14770 . . . . . . . . . . . . 13 (𝜑𝑅 ⇝ (𝐴 + 0))
51098addid1d 10576 . . . . . . . . . . . . 13 (𝜑 → (𝐴 + 0) = 𝐴)
511509, 510breqtrd 4912 . . . . . . . . . . . 12 (𝜑𝑅𝐴)
512 releldm 5604 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅𝐴) → 𝑅 ∈ dom ⇝ )
513463, 511, 512syl2anc 579 . . . . . . . . . . 11 (𝜑𝑅 ∈ dom ⇝ )
514 fveq2 6446 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → (ℤ𝑙) = (ℤ𝑘))
515 fveq2 6446 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → (𝑅𝑙) = (𝑅𝑘))
516515oveq2d 6938 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → ((𝑅) − (𝑅𝑙)) = ((𝑅) − (𝑅𝑘)))
517516fveq2d 6450 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑘 → (abs‘((𝑅) − (𝑅𝑙))) = (abs‘((𝑅) − (𝑅𝑘))))
518517breq1d 4896 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → ((abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
519514, 518raleqbidv 3325 . . . . . . . . . . . . . 14 (𝑙 = 𝑘 → (∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
520519cbvrabv 3395 . . . . . . . . . . . . 13 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
521 fveq2 6446 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (𝑅) = (𝑅𝑖))
522521fvoveq1d 6944 . . . . . . . . . . . . . . . . 17 ( = 𝑖 → (abs‘((𝑅) − (𝑅𝑘))) = (abs‘((𝑅𝑖) − (𝑅𝑘))))
523522breq1d 4896 . . . . . . . . . . . . . . . 16 ( = 𝑖 → ((abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
524523cbvralv 3366 . . . . . . . . . . . . . . 15 (∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
525524rgenw 3105 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑀)(∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
526 rabbi 3306 . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . 13 {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
528520, 527eqtri 2801 . . . . . . . . . . . 12 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
529528infeq1i 8672 . . . . . . . . . . 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 41056 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
531459fvmpt2 6552 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
532113, 58, 531syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
533532eqcomd 2783 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅𝑗))
534533fveq2d 6450 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅𝑗)))
535534mpteq2dva 4979 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
536107, 535syl5eq 2825 . . . . . . . . . 10 (𝜑𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
537536fveq2d 6450 . . . . . . . . . 10 (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
538530, 536, 5373brtr4d 4918 . . . . . . . . 9 (𝜑𝑆 ⇝ (lim sup‘𝑆))
539464mptex 6758 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
540107, 539eqeltri 2854 . . . . . . . . . . 11 𝑆 ∈ V
541540a1i 11 . . . . . . . . . 10 (𝜑𝑆 ∈ V)
542 eqidd 2778 . . . . . . . . . 10 ((𝜑𝑐 ∈ ℤ) → (𝑆𝑐) = (𝑆𝑐))
543541, 542clim 14633 . . . . . . . . 9 (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))))
544538, 543mpbid 224 . . . . . . . 8 (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎)))
545544simprd 491 . . . . . . 7 (𝜑 → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
546545adantr 474 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
547 simpr 479 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
548547rphalfcld 12193 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
549 breq2 4890 . . . . . . . . 9 (𝑎 = (𝑥 / 2) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
550549anbi2d 622 . . . . . . . 8 (𝑎 = (𝑥 / 2) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
551550rexralbidv 3242 . . . . . . 7 (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
552551rspccva 3509 . . . . . 6 ((∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
553546, 548, 552syl2anc 579 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
554450, 553r19.29a 3263 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
555404, 554r19.29a 3263 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
556555ralrimiva 3147 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
557 ioosscn 40610 . . . 4 (𝐴(,)𝐵) ⊆ ℂ
558557a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
559453, 558, 98ellimc3 24080 . 2 (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))))
560136, 556, 559mpbir2and 703 1 (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1601  wcel 2106  wne 2968  wral 3089  wrex 3090  {crab 3093  Vcvv 3397  wss 3791  c0 4140  ifcif 4306   class class class wbr 4886  cmpt 4965  dom cdm 5355  ran crn 5356  Rel wrel 5360  wf 6131  cfv 6135  (class class class)co 6922  supcsup 8634  infcinf 8635  cc 10270  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  +∞cpnf 10408  *cxr 10410   < clt 10411  cle 10412  cmin 10606   / cdiv 11032  cn 11374  2c2 11430  0cn0 11642  cz 11728  cuz 11992  +crp 12137  (,)cioo 12487  cfl 12910  abscabs 14381  lim supclsp 14609  cli 14623  cnccncf 23087   lim climc 24063   D cdv 24064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-limsup 14610  df-clim 14627  df-rlim 14628  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-perf 21349  df-cn 21439  df-cnp 21440  df-haus 21527  df-cmp 21599  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cncf 23089  df-limc 24067  df-dv 24068
This theorem is referenced by:  ioodvbdlimc1  41058
  Copyright terms: Public domain W3C validator