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 40665
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 11908 . . . . . 6 (ℤ𝑀) ⊆ ℤ
2 zssre 11586 . . . . . 6 ℤ ⊆ ℝ
31, 2sstri 3761 . . . . 5 (ℤ𝑀) ⊆ ℝ
43a1i 11 . . . 4 (𝜑 → (ℤ𝑀) ⊆ ℝ)
5 ioodvbdlimc1lem2.m . . . . . . 7 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
6 ioodvbdlimc1lem2.b . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
7 ioodvbdlimc1lem2.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
86, 7resubcld 10660 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
9 ioodvbdlimc1lem2.altb . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
107, 6posdifd 10816 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
119, 10mpbid 222 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
1211gt0ne0d 10794 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ≠ 0)
138, 12rereccld 11054 . . . . . . . . 9 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ)
14 0red 10243 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
158, 11recgt0d 11160 . . . . . . . . . 10 (𝜑 → 0 < (1 / (𝐵𝐴)))
1614, 13, 15ltled 10387 . . . . . . . . 9 (𝜑 → 0 ≤ (1 / (𝐵𝐴)))
17 flge0nn0 12829 . . . . . . . . 9 (((1 / (𝐵𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵𝐴))) → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
1813, 16, 17syl2anc 573 . . . . . . . 8 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
19 peano2nn0 11535 . . . . . . . 8 ((⌊‘(1 / (𝐵𝐴))) ∈ ℕ0 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
2018, 19syl 17 . . . . . . 7 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
215, 20syl5eqel 2854 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
2221nn0zd 11682 . . . . 5 (𝜑𝑀 ∈ ℤ)
23 eqid 2771 . . . . . 6 (ℤ𝑀) = (ℤ𝑀)
2423uzsup 12870 . . . . 5 (𝑀 ∈ ℤ → sup((ℤ𝑀), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (𝜑 → sup((ℤ𝑀), ℝ*, < ) = +∞)
26 ioodvbdlimc1lem2.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2726adantr 466 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
287rexrd 10291 . . . . . . . 8 (𝜑𝐴 ∈ ℝ*)
2928adantr 466 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ*)
306rexrd 10291 . . . . . . . 8 (𝜑𝐵 ∈ ℝ*)
3130adantr 466 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ*)
327adantr 466 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
33 eluzelre 11899 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℝ)
3433adantl 467 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ)
35 0red 10243 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
36 0red 10243 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 0 ∈ ℝ)
37 1red 10257 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 1 ∈ ℝ)
3836, 37readdcld 10271 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → (0 + 1) ∈ ℝ)
3938adantl 467 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ∈ ℝ)
4036ltp1d 11156 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 0 < (0 + 1))
4140adantl 467 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < (0 + 1))
42 eluzel2 11893 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
4342zred 11684 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℝ)
4443adantl 467 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
4513flcld 12807 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℤ)
4645zred 11684 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℝ)
47 1red 10257 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℝ)
4818nn0ge0d 11556 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (⌊‘(1 / (𝐵𝐴))))
4914, 46, 47, 48leadd1dd 10843 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵𝐴))) + 1))
5049, 5syl6breqr 4828 . . . . . . . . . . . . 13 (𝜑 → (0 + 1) ≤ 𝑀)
5150adantr 466 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑀)
52 eluzle 11901 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀𝑗)
5352adantl 467 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀𝑗)
5439, 44, 34, 51, 53letrd 10396 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑗)
5535, 39, 34, 41, 54ltletrd 10399 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < 𝑗)
5655gt0ne0d 10794 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ≠ 0)
5734, 56rereccld 11054 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ)
5832, 57readdcld 10271 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
5934, 55elrpd 12072 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ+)
6059rpreccld 12085 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ+)
6132, 60ltaddrpd 12108 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
6221nn0red 11554 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
6314, 47readdcld 10271 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ∈ ℝ)
6446, 47readdcld 10271 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ)
6514ltp1d 11156 . . . . . . . . . . . . . 14 (𝜑 → 0 < (0 + 1))
6614, 63, 64, 65, 49ltletrd 10399 . . . . . . . . . . . . 13 (𝜑 → 0 < ((⌊‘(1 / (𝐵𝐴))) + 1))
6766, 5syl6breqr 4828 . . . . . . . . . . . 12 (𝜑 → 0 < 𝑀)
6867gt0ne0d 10794 . . . . . . . . . . 11 (𝜑𝑀 ≠ 0)
6962, 68rereccld 11054 . . . . . . . . . 10 (𝜑 → (1 / 𝑀) ∈ ℝ)
7069adantr 466 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑀) ∈ ℝ)
7132, 70readdcld 10271 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
726adantr 466 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
7362, 67elrpd 12072 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
7473adantr 466 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ+)
75 1red 10257 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
76 0le1 10753 . . . . . . . . . . 11 0 ≤ 1
7776a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ≤ 1)
7874, 59, 75, 77, 53lediv2ad 12097 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
7957, 70, 32, 78leadd2dd 10844 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
805eqcomi 2780 . . . . . . . . . . . . 13 ((⌊‘(1 / (𝐵𝐴))) + 1) = 𝑀
8180oveq2i 6804 . . . . . . . . . . . 12 (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) = (1 / 𝑀)
8281, 69syl5eqel 2854 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) ∈ ℝ)
8313, 15elrpd 12072 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ+)
8464, 66elrpd 12072 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ+)
85 1rp 12039 . . . . . . . . . . . . . 14 1 ∈ ℝ+
8685a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ+)
87 fllelt 12806 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8988simprd 483 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1))
9083, 84, 86, 89ltdiv2dd 40025 . . . . . . . . . . . 12 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (1 / (1 / (𝐵𝐴))))
918recnd 10270 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℂ)
9291, 12recrecd 11000 . . . . . . . . . . . 12 (𝜑 → (1 / (1 / (𝐵𝐴))) = (𝐵𝐴))
9390, 92breqtrd 4812 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (𝐵𝐴))
9482, 8, 7, 93ltadd2dd 10398 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))) < (𝐴 + (𝐵𝐴)))
955oveq2i 6804 . . . . . . . . . . . 12 (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))
9695oveq2i 6804 . . . . . . . . . . 11 (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)))
9796a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))))
987recnd 10270 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
996recnd 10270 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
10098, 99pncan3d 10597 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
101100eqcomd 2777 . . . . . . . . . 10 (𝜑𝐵 = (𝐴 + (𝐵𝐴)))
10294, 97, 1013brtr4d 4818 . . . . . . . . 9 (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103102adantr 466 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
10458, 71, 72, 79, 103lelttrd 10397 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
10529, 31, 58, 61, 104eliood 40241 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
10627, 105ffvelrnd 6503 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107 ioodvbdlimc1lem2.s . . . . 5 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108106, 107fmptd 6527 . . . 4 (𝜑𝑆:(ℤ𝑀)⟶ℝ)
109 ioodvbdlimc1lem2.dmdv . . . . . 6 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110 ioodvbdlimc1lem2.dvbd . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
1117, 6, 9, 26, 109, 110dvbdfbdioo 40663 . . . . 5 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
11262adantr 466 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113 simpr 471 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ (ℤ𝑀))
114107fvmpt2 6433 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115113, 106, 114syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116115fveq2d 6336 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117116adantlr 694 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118 simplr 752 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
119105adantlr 694 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑥 = (𝐴 + (1 / 𝑗)) → (𝐹𝑥) = (𝐹‘(𝐴 + (1 / 𝑗))))
121120fveq2d 6336 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
122121breq1d 4796 . . . . . . . . . . . . 13 (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
123122rspccva 3459 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124118, 119, 123syl2anc 573 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
125117, 124eqbrtrd 4808 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) ≤ 𝑏)
126125a1d 25 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
127126ralrimiva 3115 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
128 breq1 4789 . . . . . . . . . . 11 (𝑘 = 𝑀 → (𝑘𝑗𝑀𝑗))
129128imbi1d 330 . . . . . . . . . 10 (𝑘 = 𝑀 → ((𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
130129ralbidv 3135 . . . . . . . . 9 (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
131130rspcev 3460 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
132112, 127, 131syl2anc 573 . . . . . . 7 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
133132ex 397 . . . . . 6 (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
134133reximdv 3164 . . . . 5 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
135111, 134mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
1364, 25, 108, 135limsupre 40391 . . 3 (𝜑 → (lim sup‘𝑆) ∈ ℝ)
137136recnd 10270 . 2 (𝜑 → (lim sup‘𝑆) ∈ ℂ)
138 eluzelre 11899 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
139138adantl 467 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ)
140 0red 10243 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ∈ ℝ)
14145peano2zd 11687 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℤ)
1425, 141syl5eqel 2854 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
143142adantr 466 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
144143zred 11684 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℝ)
145144adantr 466 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀 ∈ ℝ)
14667ad2antrr 705 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑀)
147 ioodvbdlimc1lem2.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
148 ioodvbdlimc1lem2.y . . . . . . . . . . . . . . . . . . . 20 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
149 ioomidp 40259 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
1507, 6, 9, 149syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
151 ne0i 4069 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
153 ioossre 12440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐵) ⊆ ℝ
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
155 dvfre 23934 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
15626, 154, 155syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157109feq2d 6171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
158156, 157mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
159158ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
160159recnd 10270 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
161160abscld 14383 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
162 eqid 2771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
163 eqid 2771 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
164152, 161, 110, 162, 163suprnmpt 39875 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
165164simpld 482 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
166148, 165syl5eqel 2854 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ∈ ℝ)
167166adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑌 ∈ ℝ)
168 rpre 12042 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
169168rehalfcld 11481 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
170169adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ)
171168recnd 10270 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
172171adantl 467 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
173 2cnd 11295 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
174 rpne0 12051 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ≠ 0)
175174adantl 467 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
176 2ne0 11315 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
177176a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ≠ 0)
178172, 173, 175, 177divne0d 11019 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0)
179167, 170, 178redivcld 11055 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
180179flcld 12807 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
181180peano2zd 11687 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
182181, 143ifcld 4270 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
183147, 182syl5eqel 2854 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
184183zred 11684 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℝ)
185184adantr 466 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
186181zred 11684 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
187 max1 12221 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188144, 186, 187syl2anc 573 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
189188, 147syl6breqr 4828 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀𝑁)
190189adantr 466 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑁)
191 eluzle 11901 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑁) → 𝑁𝑗)
192191adantl 467 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁𝑗)
193145, 185, 139, 190, 192letrd 10396 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑗)
194140, 145, 139, 146, 193ltletrd 10399 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑗)
195194gt0ne0d 10794 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ≠ 0)
196139, 195rereccld 11054 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ)
197139, 194recgt0d 11160 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < (1 / 𝑗))
198196, 197elrpd 12072 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ+)
199198adantr 466 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → (1 / 𝑗) ∈ ℝ+)
200 ioodvbdlimc1lem2.ch . . . . . . . . 9 (𝜒 ↔ (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
201200biimpi 206 . . . . . . . . . . . . . . . . 17 (𝜒 → (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
202 simp-5l 772 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝜑)
203201, 202syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝜑)
204203, 26syl 17 . . . . . . . . . . . . . . 15 (𝜒𝐹:(𝐴(,)𝐵)⟶ℝ)
205201simplrd 753 . . . . . . . . . . . . . . 15 (𝜒𝑧 ∈ (𝐴(,)𝐵))
206204, 205ffvelrnd 6503 . . . . . . . . . . . . . 14 (𝜒 → (𝐹𝑧) ∈ ℝ)
207206recnd 10270 . . . . . . . . . . . . 13 (𝜒 → (𝐹𝑧) ∈ ℂ)
208203, 108syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑆:(ℤ𝑀)⟶ℝ)
209 simp-5r 774 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+)
210201, 209syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝑥 ∈ ℝ+)
211 eluz2 11894 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
212143, 183, 189, 211syl3anbrc 1428 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑀))
213203, 210, 212syl2anc 573 . . . . . . . . . . . . . . . . 17 (𝜒𝑁 ∈ (ℤ𝑀))
214 uzss 11909 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
215213, 214syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (ℤ𝑁) ⊆ (ℤ𝑀))
216 simp-4r 770 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ𝑁))
217201, 216syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ (ℤ𝑁))
218215, 217sseldd 3753 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (ℤ𝑀))
219208, 218ffvelrnd 6503 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ ℝ)
220219recnd 10270 . . . . . . . . . . . . 13 (𝜒 → (𝑆𝑗) ∈ ℂ)
221203, 137syl 17 . . . . . . . . . . . . 13 (𝜒 → (lim sup‘𝑆) ∈ ℂ)
222207, 220, 221npncand 10618 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) = ((𝐹𝑧) − (lim sup‘𝑆)))
223222eqcomd 2777 . . . . . . . . . . 11 (𝜒 → ((𝐹𝑧) − (lim sup‘𝑆)) = (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))))
224223fveq2d 6336 . . . . . . . . . 10 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))))
225206, 219resubcld 10660 . . . . . . . . . . . . . 14 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℝ)
226203, 136syl 17 . . . . . . . . . . . . . . 15 (𝜒 → (lim sup‘𝑆) ∈ ℝ)
227219, 226resubcld 10660 . . . . . . . . . . . . . 14 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℝ)
228225, 227readdcld 10271 . . . . . . . . . . . . 13 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
229228recnd 10270 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℂ)
230229abscld 14383 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
231225recnd 10270 . . . . . . . . . . . . 13 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℂ)
232231abscld 14383 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ∈ ℝ)
233227recnd 10270 . . . . . . . . . . . . 13 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℂ)
234233abscld 14383 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
235232, 234readdcld 10271 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
236210rpred 12075 . . . . . . . . . . 11 (𝜒𝑥 ∈ ℝ)
237231, 233abstrid 14403 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))))
238236rehalfcld 11481 . . . . . . . . . . . . 13 (𝜒 → (𝑥 / 2) ∈ ℝ)
239207, 220abssubd 14400 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) = (abs‘((𝑆𝑗) − (𝐹𝑧))))
240203, 218, 115syl2anc 573 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
241240fvoveq1d 6815 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))))
242203, 218, 106syl2anc 573 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
243242, 206resubcld 10660 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℝ)
244243recnd 10270 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℂ)
245244abscld 14383 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ∈ ℝ)
246203, 166syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑌 ∈ ℝ)
247203, 218, 58syl2anc 573 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
248153, 205sseldi 3750 . . . . . . . . . . . . . . . . . 18 (𝜒𝑧 ∈ ℝ)
249247, 248resubcld 10660 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
250246, 249remulcld 10272 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ)
251203, 7syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐴 ∈ ℝ)
252203, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐵 ∈ ℝ)
253203, 109syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
254164simprd 483 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
255148breq2i 4794 . . . . . . . . . . . . . . . . . . . . . 22 ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256255ralbii 3129 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
257254, 256sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
258203, 257syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
259 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑥 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑥))
260259fveq2d 6336 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
261260breq1d 4796 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
262261cbvralv 3320 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
263258, 262sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
264248rexrd 10291 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 ∈ ℝ*)
265203, 30syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐵 ∈ ℝ*)
266248, 251resubcld 10660 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ∈ ℝ)
267266recnd 10270 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑧𝐴) ∈ ℂ)
268267abscld 14383 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) ∈ ℝ)
2693, 218sseldi 3750 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ∈ ℝ)
270203, 218, 56syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ≠ 0)
271269, 270rereccld 11054 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℝ)
272266leabsd 14361 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ≤ (abs‘(𝑧𝐴)))
273201simprd 483 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) < (1 / 𝑗))
274266, 268, 271, 272, 273lelttrd 10397 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑧𝐴) < (1 / 𝑗))
275248, 251, 271ltsubadd2d 10827 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑧𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
276274, 275mpbid 222 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 < (𝐴 + (1 / 𝑗)))
277203, 218, 104syl2anc 573 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
278264, 265, 247, 276, 277eliood 40241 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
279251, 252, 204, 253, 246, 263, 205, 278dvbdfbdioolem1 40661 . . . . . . . . . . . . . . . . 17 (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · (𝐵𝐴))))
280279simpld 482 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
281203, 218, 57syl2anc 573 . . . . . . . . . . . . . . . . . 18 (𝜒 → (1 / 𝑗) ∈ ℝ)
282246, 281remulcld 10272 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
283158, 150ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
284283recnd 10270 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
285284abscld 14383 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
286284absge0d 14391 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
287 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝐴 + 𝐵) / 2) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))
288287fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
289148eqcomi 2780 . . . . . . . . . . . . . . . . . . . . . . . 24 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
290289a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
291288, 290breq12d 4799 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
292291rspcva 3458 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
293150, 254, 292syl2anc 573 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
29414, 285, 166, 286, 293letrd 10396 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑌)
295203, 294syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → 0 ≤ 𝑌)
296203, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝐴 ∈ ℝ*)
297 ioogtlb 40238 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
298296, 265, 205, 297syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 < 𝑧)
299251, 248, 247, 298ltsub2dd 10842 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
300203, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 ∈ ℂ)
301281recnd 10270 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℂ)
302300, 301pncan2d 10596 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
303299, 302breqtrd 4812 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
304249, 271, 303ltled 10387 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
305249, 271, 246, 295, 304lemul2ad 11166 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
306282adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
307238adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
308 oveq1 6800 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
309301mul02d 10436 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (0 · (1 / 𝑗)) = 0)
310308, 309sylan9eqr 2827 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
311210rphalfcld 12087 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑥 / 2) ∈ ℝ+)
312311rpgt0d 12078 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → 0 < (𝑥 / 2))
313312adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → 0 < (𝑥 / 2))
314310, 313eqbrtrd 4808 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
315306, 307, 314ltled 10387 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
316246adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
317295adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
318 neqne 2951 . . . . . . . . . . . . . . . . . . . . 21 𝑌 = 0 → 𝑌 ≠ 0)
319318adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
320316, 317, 319ne0gt0d 10376 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
321282adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
3223, 213sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ)
323 0red 10243 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 ∈ ℝ)
324203, 210, 144syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀 ∈ ℝ)
325203, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 < 𝑀)
326203, 210, 189syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀𝑁)
327323, 324, 322, 325, 326ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → 0 < 𝑁)
328327gt0ne0d 10794 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ≠ 0)
329322, 328rereccld 11054 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑁) ∈ ℝ)
330246, 329remulcld 10272 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
331330adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
332238adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
333281adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
334329adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
335246adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
336295adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
337322, 327elrpd 12072 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ+)
338203, 218, 59syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑗 ∈ ℝ+)
339 1red 10257 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 1 ∈ ℝ)
34076a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 0 ≤ 1)
341217, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁𝑗)
342337, 338, 339, 340, 341lediv2ad 12097 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
343342adantr 466 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
344333, 334, 335, 336, 343lemul2ad 11166 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
345236recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ∈ ℂ)
346 2cnd 11295 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ∈ ℂ)
347210rpne0d 12080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ≠ 0)
348176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ≠ 0)
349345, 346, 347, 348divne0d 11019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑥 / 2) ≠ 0)
350246, 238, 349redivcld 11055 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
351350adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
352 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
353312adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
354335, 332, 352, 353divgt0d 11161 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
355351, 354elrpd 12072 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ+)
356355rprecred 12086 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
357337adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ+)
358 1red 10257 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
35976a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
360350flcld 12807 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
361360peano2zd 11687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
362361zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
363203, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜒𝑀 ∈ ℤ)
364361, 363ifcld 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
365147, 364syl5eqel 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑁 ∈ ℤ)
366365zred 11684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑁 ∈ ℝ)
367 flltp1 12809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
368350, 367syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
369203, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒𝑀 ∈ ℝ)
370 max2 12223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
371369, 362, 370syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
372371, 147syl6breqr 4828 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
373350, 362, 366, 368, 372ltletrd 10399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
374350, 322, 373ltled 10387 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
375374adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
376355, 357, 358, 359, 375lediv2ad 12097 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
377334, 356, 335, 336, 376lemul2ad 11166 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
378335recnd 10270 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
379351recnd 10270 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
380354gt0ne0d 10794 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
381378, 379, 380divrecd 11006 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
382332recnd 10270 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
383352gt0ne0d 10794 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
384349adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
385378, 382, 383, 384ddcand 11023 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
386381, 385eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
387377, 386breqtrd 4812 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
388321, 331, 332, 344, 387letrd 10396 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
389320, 388syldan 579 . . . . . . . . . . . . . . . . . 18 ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390315, 389pm2.61dan 814 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
391250, 282, 238, 305, 390letrd 10396 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
392245, 250, 238, 280, 391letrd 10396 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑥 / 2))
393241, 392eqbrtrd 4808 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) ≤ (𝑥 / 2))
394239, 393eqbrtrd 4808 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ≤ (𝑥 / 2))
395 simpllr 760 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
396201, 395syl 17 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
397232, 234, 238, 238, 394, 396leltaddd 10851 . . . . . . . . . . . 12 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
3983452halvesd 11480 . . . . . . . . . . . 12 (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
399397, 398breqtrd 4812 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
400230, 235, 236, 237, 399lelttrd 10397 . . . . . . . . . 10 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
401224, 400eqbrtrd 4808 . . . . . . . . 9 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
402200, 401sylbir 225 . . . . . . . 8 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
403402adantrl 695 . . . . . . 7 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗))) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
404403ex 397 . . . . . 6 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
405404ralrimiva 3115 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
406 breq2 4790 . . . . . . . . 9 (𝑦 = (1 / 𝑗) → ((abs‘(𝑧𝐴)) < 𝑦 ↔ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
407406anbi2d 614 . . . . . . . 8 (𝑦 = (1 / 𝑗) → ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) ↔ (𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗))))
408407imbi1d 330 . . . . . . 7 (𝑦 = (1 / 𝑗) → (((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)))
409408ralbidv 3135 . . . . . 6 (𝑦 = (1 / 𝑗) → (∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)))
410409rspcev 3460 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
411199, 405, 410syl2anc 573 . . . 4 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
412 simpr 471 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑏𝑁)
413412iftrued 4233 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑁)
414 uzid 11903 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
415183, 414syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑁))
416415adantr 466 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑁 ∈ (ℤ𝑁))
417413, 416eqeltrd 2850 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
418417adantlr 694 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
419 iffalse 4234 . . . . . . . . . 10 𝑏𝑁 → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
420419adantl 467 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
421183ad2antrr 705 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℤ)
422 simplr 752 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℤ)
423421zred 11684 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℝ)
424422zred 11684 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℝ)
425 simpr 471 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → ¬ 𝑏𝑁)
426423, 424ltnled 10386 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏𝑁))
427425, 426mpbird 247 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 < 𝑏)
428423, 424, 427ltled 10387 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁𝑏)
429 eluz2 11894 . . . . . . . . . 10 (𝑏 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁𝑏))
430421, 422, 428, 429syl3anbrc 1428 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ (ℤ𝑁))
431420, 430eqeltrd 2850 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
432418, 431pm2.61dan 814 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
433432adantr 466 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
434 simpr 471 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
435 simpr 471 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
436183adantr 466 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
437436, 435ifcld 4270 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ)
438435zred 11684 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
439436zred 11684 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
440 max1 12221 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
441438, 439, 440syl2anc 573 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
442 eluz2 11894 . . . . . . . . . 10 (if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏)))
443435, 437, 441, 442syl3anbrc 1428 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
444443adantr 466 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
445 fveq2 6332 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑐) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
446445eleq1d 2835 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ))
447445fvoveq1d 6815 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
448447breq1d 4796 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
449446, 448anbi12d 616 . . . . . . . . 9 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
450449rspccva 3459 . . . . . . . 8 ((∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏)) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
451434, 444, 450syl2anc 573 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
452451simprd 483 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
453 fveq2 6332 . . . . . . . . 9 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑗) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
454453fvoveq1d 6815 . . . . . . . 8 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
455454breq1d 4796 . . . . . . 7 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
456455rspcev 3460 . . . . . 6 ((if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁) ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
457433, 452, 456syl2anc 573 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
458 ax-resscn 10195 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
459458a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℂ)
46026, 459fssd 6197 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
461 dvcn 23904 . . . . . . . . . . . . . 14 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
462459, 460, 154, 109, 461syl31anc 1479 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
463 cncffvrn 22921 . . . . . . . . . . . . 13 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
464459, 462, 463syl2anc 573 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
46526, 464mpbird 247 . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
466 ioodvbdlimc1lem2.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗)))
467105, 466fmptd 6527 . . . . . . . . . . 11 (𝜑𝑅:(ℤ𝑀)⟶(𝐴(,)𝐵))
468 eqid 2771 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))
469 climrel 14431 . . . . . . . . . . . . 13 Rel ⇝
470469a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ⇝ )
471 fvex 6342 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) ∈ V
472471mptex 6630 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V
473472a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V)
474 eqidd 2772 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
475 eqidd 2772 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
476 simpr 471 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝑚 ∈ (ℤ𝑀))
4777adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
478474, 475, 476, 477fvmptd 6430 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
47923, 142, 473, 98, 478climconst 14482 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ⇝ 𝐴)
480471mptex 6630 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
481466, 480eqeltri 2846 . . . . . . . . . . . . . . 15 𝑅 ∈ V
482481a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ V)
483 1cnd 10258 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
484 elnnnn0b 11539 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0 ∧ 0 < 𝑀))
48521, 67, 484sylanbrc 572 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
486 divcnvg 40377 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
487483, 485, 486syl2anc 573 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
488 eqidd 2772 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
489 eqidd 2772 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
490 simpr 471 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
4917adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
492488, 489, 490, 491fvmptd 6430 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
49398adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℂ)
494492, 493eqeltrd 2850 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
495 eqidd 2772 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)))
496 oveq2 6801 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
497496adantl 467 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
4983, 490sseldi 3750 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
499 0red 10243 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
50062adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
50167adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑀)
502 eluzle 11901 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
503502adantl 467 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
504499, 500, 498, 501, 503ltletrd 10399 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑖)
505504gt0ne0d 10794 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≠ 0)
506498, 505rereccld 11054 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℝ)
507495, 497, 490, 506fvmptd 6430 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
508498recnd 10270 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℂ)
509508, 505reccld 10996 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℂ)
510507, 509eqeltrd 2850 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
511466a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗))))
512496oveq2d 6809 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
513512adantl 467 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
514491, 506readdcld 10271 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
515511, 513, 490, 514fvmptd 6430 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (𝐴 + (1 / 𝑖)))
516492, 507oveq12d 6811 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
517515, 516eqtr4d 2808 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)))
51823, 142, 479, 482, 487, 494, 510, 517climadd 14570 . . . . . . . . . . . . 13 (𝜑𝑅 ⇝ (𝐴 + 0))
51998addid1d 10438 . . . . . . . . . . . . 13 (𝜑 → (𝐴 + 0) = 𝐴)
520518, 519breqtrd 4812 . . . . . . . . . . . 12 (𝜑𝑅𝐴)
521 releldm 5496 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅𝐴) → 𝑅 ∈ dom ⇝ )
522470, 520, 521syl2anc 573 . . . . . . . . . . 11 (𝜑𝑅 ∈ dom ⇝ )
523 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → (ℤ𝑙) = (ℤ𝑘))
524 fveq2 6332 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → (𝑅𝑙) = (𝑅𝑘))
525524oveq2d 6809 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → ((𝑅) − (𝑅𝑙)) = ((𝑅) − (𝑅𝑘)))
526525fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑘 → (abs‘((𝑅) − (𝑅𝑙))) = (abs‘((𝑅) − (𝑅𝑘))))
527526breq1d 4796 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → ((abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
528523, 527raleqbidv 3301 . . . . . . . . . . . . . 14 (𝑙 = 𝑘 → (∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
529528cbvrabv 3349 . . . . . . . . . . . . 13 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
530 fveq2 6332 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (𝑅) = (𝑅𝑖))
531530fvoveq1d 6815 . . . . . . . . . . . . . . . . 17 ( = 𝑖 → (abs‘((𝑅) − (𝑅𝑘))) = (abs‘((𝑅𝑖) − (𝑅𝑘))))
532531breq1d 4796 . . . . . . . . . . . . . . . 16 ( = 𝑖 → ((abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
533532cbvralv 3320 . . . . . . . . . . . . . . 15 (∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
534533rgenw 3073 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑀)(∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
535 rabbi 3269 . . . . . . . . . . . . . 14 (∀𝑘 ∈ (ℤ𝑀)(∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))) ↔ {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))})
536534, 535mpbi 220 . . . . . . . . . . . . 13 {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
537529, 536eqtri 2793 . . . . . . . . . . . 12 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
538537infeq1i 8540 . . . . . . . . . . 11 inf({𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
5397, 6, 9, 465, 109, 110, 22, 467, 468, 522, 538ioodvbdlimc1lem1 40664 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
540466fvmpt2 6433 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
541113, 58, 540syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
542541eqcomd 2777 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅𝑗))
543542fveq2d 6336 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅𝑗)))
544543mpteq2dva 4878 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
545107, 544syl5eq 2817 . . . . . . . . . 10 (𝜑𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
546545fveq2d 6336 . . . . . . . . . 10 (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
547539, 545, 5463brtr4d 4818 . . . . . . . . 9 (𝜑𝑆 ⇝ (lim sup‘𝑆))
548471mptex 6630 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
549107, 548eqeltri 2846 . . . . . . . . . . 11 𝑆 ∈ V
550549a1i 11 . . . . . . . . . 10 (𝜑𝑆 ∈ V)
551 eqidd 2772 . . . . . . . . . 10 ((𝜑𝑐 ∈ ℤ) → (𝑆𝑐) = (𝑆𝑐))
552550, 551clim 14433 . . . . . . . . 9 (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))))
553547, 552mpbid 222 . . . . . . . 8 (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎)))
554553simprd 483 . . . . . . 7 (𝜑 → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
555554adantr 466 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
556 simpr 471 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
557556rphalfcld 12087 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
558 breq2 4790 . . . . . . . . 9 (𝑎 = (𝑥 / 2) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
559558anbi2d 614 . . . . . . . 8 (𝑎 = (𝑥 / 2) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
560559rexralbidv 3206 . . . . . . 7 (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
561560rspccva 3459 . . . . . 6 ((∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
562555, 557, 561syl2anc 573 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
563457, 562r19.29a 3226 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
564411, 563r19.29a 3226 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
565564ralrimiva 3115 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
566 ioosscn 40237 . . . 4 (𝐴(,)𝐵) ⊆ ℂ
567566a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
568460, 567, 98ellimc3 23863 . 2 (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))))
569137, 565, 568mpbir2and 692 1 (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  wss 3723  c0 4063  ifcif 4225   class class class wbr 4786  cmpt 4863  dom cdm 5249  ran crn 5250  Rel wrel 5254  wf 6027  cfv 6031  (class class class)co 6793  supcsup 8502  infcinf 8503  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  +∞cpnf 10273  *cxr 10275   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  cn 11222  2c2 11272  0cn0 11494  cz 11579  cuz 11888  +crp 12035  (,)cioo 12380  cfl 12799  abscabs 14182  lim supclsp 14409  cli 14423  cnccncf 22899   lim climc 23846   D cdv 23847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17957  df-cmn 18402  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-cmp 21411  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-xms 22345  df-ms 22346  df-tms 22347  df-cncf 22901  df-limc 23850  df-dv 23851
This theorem is referenced by:  ioodvbdlimc1  40666
  Copyright terms: Public domain W3C validator