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 39475
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 11658 . . . . . 6 (ℤ𝑀) ⊆ ℤ
2 zssre 11335 . . . . . 6 ℤ ⊆ ℝ
31, 2sstri 3596 . . . . 5 (ℤ𝑀) ⊆ ℝ
43a1i 11 . . . 4 (𝜑 → (ℤ𝑀) ⊆ ℝ)
5 ioodvbdlimc1lem2.m . . . . . . 7 𝑀 = ((⌊‘(1 / (𝐵𝐴))) + 1)
6 ioodvbdlimc1lem2.b . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
7 ioodvbdlimc1lem2.a . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
86, 7resubcld 10409 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
9 ioodvbdlimc1lem2.altb . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
107, 6posdifd 10565 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
119, 10mpbid 222 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
1211gt0ne0d 10543 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ≠ 0)
138, 12rereccld 10803 . . . . . . . . 9 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ)
14 0red 9992 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
158, 11recgt0d 10909 . . . . . . . . . 10 (𝜑 → 0 < (1 / (𝐵𝐴)))
1614, 13, 15ltled 10136 . . . . . . . . 9 (𝜑 → 0 ≤ (1 / (𝐵𝐴)))
17 flge0nn0 12568 . . . . . . . . 9 (((1 / (𝐵𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (𝐵𝐴))) → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
1813, 16, 17syl2anc 692 . . . . . . . 8 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℕ0)
19 peano2nn0 11284 . . . . . . . 8 ((⌊‘(1 / (𝐵𝐴))) ∈ ℕ0 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
2018, 19syl 17 . . . . . . 7 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℕ0)
215, 20syl5eqel 2702 . . . . . 6 (𝜑𝑀 ∈ ℕ0)
2221nn0zd 11431 . . . . 5 (𝜑𝑀 ∈ ℤ)
23 eqid 2621 . . . . . 6 (ℤ𝑀) = (ℤ𝑀)
2423uzsup 12609 . . . . 5 (𝑀 ∈ ℤ → sup((ℤ𝑀), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (𝜑 → sup((ℤ𝑀), ℝ*, < ) = +∞)
26 ioodvbdlimc1lem2.f . . . . . . 7 (𝜑𝐹:(𝐴(,)𝐵)⟶ℝ)
2726adantr 481 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐹:(𝐴(,)𝐵)⟶ℝ)
287rexrd 10040 . . . . . . . 8 (𝜑𝐴 ∈ ℝ*)
2928adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ*)
306rexrd 10040 . . . . . . . 8 (𝜑𝐵 ∈ ℝ*)
3130adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ*)
327adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
33 eluzelre 11649 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℝ)
3433adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ)
35 0red 9992 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
36 0red 9992 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 0 ∈ ℝ)
37 1red 10006 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 1 ∈ ℝ)
3836, 37readdcld 10020 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → (0 + 1) ∈ ℝ)
3938adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ∈ ℝ)
4036ltp1d 10905 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 0 < (0 + 1))
4140adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < (0 + 1))
42 eluzel2 11643 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
4342zred 11433 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀 ∈ ℝ)
4443adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
4513flcld 12546 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℤ)
4645zred 11433 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘(1 / (𝐵𝐴))) ∈ ℝ)
47 1red 10006 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℝ)
4818nn0ge0d 11305 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (⌊‘(1 / (𝐵𝐴))))
4914, 46, 47, 48leadd1dd 10592 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ≤ ((⌊‘(1 / (𝐵𝐴))) + 1))
5049, 5syl6breqr 4660 . . . . . . . . . . . . 13 (𝜑 → (0 + 1) ≤ 𝑀)
5150adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑀)
52 eluzle 11651 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑀) → 𝑀𝑗)
5352adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀𝑗)
5439, 44, 34, 51, 53letrd 10145 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝑀)) → (0 + 1) ≤ 𝑗)
5535, 39, 34, 41, 54ltletrd 10148 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 < 𝑗)
5655gt0ne0d 10543 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ≠ 0)
5734, 56rereccld 10803 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ)
5832, 57readdcld 10020 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ ℝ)
5934, 55elrpd 11820 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ ℝ+)
6059rpreccld 11833 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ∈ ℝ+)
6132, 60ltaddrpd 11856 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐴 < (𝐴 + (1 / 𝑗)))
6221nn0red 11303 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
6314, 47readdcld 10020 . . . . . . . . . . . . . 14 (𝜑 → (0 + 1) ∈ ℝ)
6446, 47readdcld 10020 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ)
6514ltp1d 10905 . . . . . . . . . . . . . 14 (𝜑 → 0 < (0 + 1))
6614, 63, 64, 65, 49ltletrd 10148 . . . . . . . . . . . . 13 (𝜑 → 0 < ((⌊‘(1 / (𝐵𝐴))) + 1))
6766, 5syl6breqr 4660 . . . . . . . . . . . 12 (𝜑 → 0 < 𝑀)
6867gt0ne0d 10543 . . . . . . . . . . 11 (𝜑𝑀 ≠ 0)
6962, 68rereccld 10803 . . . . . . . . . 10 (𝜑 → (1 / 𝑀) ∈ ℝ)
7069adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑀) ∈ ℝ)
7132, 70readdcld 10020 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) ∈ ℝ)
726adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝐵 ∈ ℝ)
7362, 67elrpd 11820 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ+)
7473adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ+)
75 1red 10006 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
76 0le1 10502 . . . . . . . . . . 11 0 ≤ 1
7776a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝑀)) → 0 ≤ 1)
7874, 59, 75, 77, 53lediv2ad 11845 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝑀)) → (1 / 𝑗) ≤ (1 / 𝑀))
7957, 70, 32, 78leadd2dd 10593 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ≤ (𝐴 + (1 / 𝑀)))
805eqcomi 2630 . . . . . . . . . . . . 13 ((⌊‘(1 / (𝐵𝐴))) + 1) = 𝑀
8180oveq2i 6621 . . . . . . . . . . . 12 (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) = (1 / 𝑀)
8281, 69syl5eqel 2702 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) ∈ ℝ)
8313, 15elrpd 11820 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) ∈ ℝ+)
8464, 66elrpd 11820 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℝ+)
85 1rp 11787 . . . . . . . . . . . . . 14 1 ∈ ℝ+
8685a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℝ+)
87 fllelt 12545 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) ∈ ℝ → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8813, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) ≤ (1 / (𝐵𝐴)) ∧ (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1)))
8988simprd 479 . . . . . . . . . . . . 13 (𝜑 → (1 / (𝐵𝐴)) < ((⌊‘(1 / (𝐵𝐴))) + 1))
9083, 84, 86, 89ltdiv2dd 38994 . . . . . . . . . . . 12 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (1 / (1 / (𝐵𝐴))))
918recnd 10019 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℂ)
9291, 12recrecd 10749 . . . . . . . . . . . 12 (𝜑 → (1 / (1 / (𝐵𝐴))) = (𝐵𝐴))
9390, 92breqtrd 4644 . . . . . . . . . . 11 (𝜑 → (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)) < (𝐵𝐴))
9482, 8, 7, 93ltadd2dd 10147 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))) < (𝐴 + (𝐵𝐴)))
955oveq2i 6621 . . . . . . . . . . . 12 (1 / 𝑀) = (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))
9695oveq2i 6621 . . . . . . . . . . 11 (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1)))
9796a1i 11 . . . . . . . . . 10 (𝜑 → (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((⌊‘(1 / (𝐵𝐴))) + 1))))
987recnd 10019 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
996recnd 10019 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℂ)
10098, 99pncan3d 10346 . . . . . . . . . . 11 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
101100eqcomd 2627 . . . . . . . . . 10 (𝜑𝐵 = (𝐴 + (𝐵𝐴)))
10294, 97, 1013brtr4d 4650 . . . . . . . . 9 (𝜑 → (𝐴 + (1 / 𝑀)) < 𝐵)
103102adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑀)) < 𝐵)
10458, 71, 72, 79, 103lelttrd 10146 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) < 𝐵)
10529, 31, 58, 61, 104eliood 39154 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
10627, 105ffvelrnd 6321 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
107 ioodvbdlimc1lem2.s . . . . 5 𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗))))
108106, 107fmptd 6346 . . . 4 (𝜑𝑆:(ℤ𝑀)⟶ℝ)
109 ioodvbdlimc1lem2.dmdv . . . . . 6 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
110 ioodvbdlimc1lem2.dvbd . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑦)
1117, 6, 9, 26, 109, 110dvbdfbdioo 39473 . . . . 5 (𝜑 → ∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
11262adantr 481 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → 𝑀 ∈ ℝ)
113 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → 𝑗 ∈ (ℤ𝑀))
114107fvmpt2 6253 . . . . . . . . . . . . . 14 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
115113, 106, 114syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
116115fveq2d 6157 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
117116adantlr 750 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
118 simplr 791 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏)
119105adantlr 750 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵))
120 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑥 = (𝐴 + (1 / 𝑗)) → (𝐹𝑥) = (𝐹‘(𝐴 + (1 / 𝑗))))
121120fveq2d 6157 . . . . . . . . . . . . . 14 (𝑥 = (𝐴 + (1 / 𝑗)) → (abs‘(𝐹𝑥)) = (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))))
122121breq1d 4628 . . . . . . . . . . . . 13 (𝑥 = (𝐴 + (1 / 𝑗)) → ((abs‘(𝐹𝑥)) ≤ 𝑏 ↔ (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏))
123122rspccva 3297 . . . . . . . . . . . 12 ((∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
124118, 119, 123syl2anc 692 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝐴 + (1 / 𝑗)))) ≤ 𝑏)
125117, 124eqbrtrd 4640 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (abs‘(𝑆𝑗)) ≤ 𝑏)
126125a1d 25 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) ∧ 𝑗 ∈ (ℤ𝑀)) → (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
127126ralrimiva 2961 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
128 breq1 4621 . . . . . . . . . . 11 (𝑘 = 𝑀 → (𝑘𝑗𝑀𝑗))
129128imbi1d 331 . . . . . . . . . 10 (𝑘 = 𝑀 → ((𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ (𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
130129ralbidv 2981 . . . . . . . . 9 (𝑘 = 𝑀 → (∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏) ↔ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
131130rspcev 3298 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ (ℤ𝑀)(𝑀𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
132112, 127, 131syl2anc 692 . . . . . . 7 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏) → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
133132ex 450 . . . . . 6 (𝜑 → (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
134133reximdv 3011 . . . . 5 (𝜑 → (∃𝑏 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐹𝑥)) ≤ 𝑏 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏)))
135111, 134mpd 15 . . . 4 (𝜑 → ∃𝑏 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ (ℤ𝑀)(𝑘𝑗 → (abs‘(𝑆𝑗)) ≤ 𝑏))
1364, 25, 108, 135limsupre 39300 . . 3 (𝜑 → (lim sup‘𝑆) ∈ ℝ)
137136recnd 10019 . 2 (𝜑 → (lim sup‘𝑆) ∈ ℂ)
138 eluzelre 11649 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
139138adantl 482 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ∈ ℝ)
140 0red 9992 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 ∈ ℝ)
14145peano2zd 11436 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘(1 / (𝐵𝐴))) + 1) ∈ ℤ)
1425, 141syl5eqel 2702 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
143142adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
144143zred 11433 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ∈ ℝ)
145144adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀 ∈ ℝ)
14667ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑀)
147 ioodvbdlimc1lem2.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀)
148 ioodvbdlimc1lem2.y . . . . . . . . . . . . . . . . . . . 20 𝑌 = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
149 ioomidp 39174 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
1507, 6, 9, 149syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵))
151 ne0i 3902 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) → (𝐴(,)𝐵) ≠ ∅)
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
153 ioossre 12184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐵) ⊆ ℝ
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
155 dvfre 23633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
15626, 154, 155syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157109feq2d 5993 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ))
158156, 157mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ)
159158ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℝ)
160159recnd 10019 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
161160abscld 14116 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
162 eqid 2621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥)))
163 eqid 2621 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )
164152, 161, 110, 162, 163suprnmpt 38852 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )))
165164simpld 475 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ∈ ℝ)
166148, 165syl5eqel 2702 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑌 ∈ ℝ)
167166adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑌 ∈ ℝ)
168 rpre 11790 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
169168rehalfcld 11230 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ)
170169adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ)
171168recnd 10019 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
172171adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
173 2cnd 11044 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
174 rpne0 11799 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ≠ 0)
175174adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
176 2ne0 11064 . . . . . . . . . . . . . . . . . . . 20 2 ≠ 0
177176a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → 2 ≠ 0)
178172, 173, 175, 177divne0d 10768 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ≠ 0)
179167, 170, 178redivcld 10804 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
180179flcld 12546 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
181180peano2zd 11436 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
182181, 143ifcld 4108 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
183147, 182syl5eqel 2702 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℤ)
184183zred 11433 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℝ)
185184adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁 ∈ ℝ)
186181zred 11433 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
187 max1 11966 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
188144, 186, 187syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
189188, 147syl6breqr 4660 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → 𝑀𝑁)
190189adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑁)
191 eluzle 11651 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑁) → 𝑁𝑗)
192191adantl 482 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑁𝑗)
193145, 185, 139, 190, 192letrd 10145 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑀𝑗)
194140, 145, 139, 146, 193ltletrd 10148 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < 𝑗)
195194gt0ne0d 10543 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 𝑗 ≠ 0)
196139, 195rereccld 10803 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ)
197139, 194recgt0d 10909 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → 0 < (1 / 𝑗))
198196, 197elrpd 11820 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) → (1 / 𝑗) ∈ ℝ+)
199198adantr 481 . . . . 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 807 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝜑)
203201, 202syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝜑)
204203, 26syl 17 . . . . . . . . . . . . . . 15 (𝜒𝐹:(𝐴(,)𝐵)⟶ℝ)
205201simplrd 792 . . . . . . . . . . . . . . 15 (𝜒𝑧 ∈ (𝐴(,)𝐵))
206204, 205ffvelrnd 6321 . . . . . . . . . . . . . 14 (𝜒 → (𝐹𝑧) ∈ ℝ)
207206recnd 10019 . . . . . . . . . . . . 13 (𝜒 → (𝐹𝑧) ∈ ℂ)
208203, 108syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑆:(ℤ𝑀)⟶ℝ)
209 simp-5r 808 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑥 ∈ ℝ+)
210201, 209syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝑥 ∈ ℝ+)
211 eluz2 11644 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁))
212143, 183, 189, 211syl3anbrc 1244 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑀))
213203, 210, 212syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜒𝑁 ∈ (ℤ𝑀))
214 uzss 11659 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
215213, 214syl 17 . . . . . . . . . . . . . . . 16 (𝜒 → (ℤ𝑁) ⊆ (ℤ𝑀))
216 simp-4r 806 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → 𝑗 ∈ (ℤ𝑁))
217201, 216syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑗 ∈ (ℤ𝑁))
218215, 217sseldd 3588 . . . . . . . . . . . . . . 15 (𝜒𝑗 ∈ (ℤ𝑀))
219208, 218ffvelrnd 6321 . . . . . . . . . . . . . 14 (𝜒 → (𝑆𝑗) ∈ ℝ)
220219recnd 10019 . . . . . . . . . . . . 13 (𝜒 → (𝑆𝑗) ∈ ℂ)
221203, 137syl 17 . . . . . . . . . . . . 13 (𝜒 → (lim sup‘𝑆) ∈ ℂ)
222207, 220, 221npncand 10367 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) = ((𝐹𝑧) − (lim sup‘𝑆)))
223222eqcomd 2627 . . . . . . . . . . 11 (𝜒 → ((𝐹𝑧) − (lim sup‘𝑆)) = (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))))
224223fveq2d 6157 . . . . . . . . . 10 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) = (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))))
225206, 219resubcld 10409 . . . . . . . . . . . . . 14 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℝ)
226203, 136syl 17 . . . . . . . . . . . . . . 15 (𝜒 → (lim sup‘𝑆) ∈ ℝ)
227219, 226resubcld 10409 . . . . . . . . . . . . . 14 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℝ)
228225, 227readdcld 10020 . . . . . . . . . . . . 13 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
229228recnd 10019 . . . . . . . . . . . 12 (𝜒 → (((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℂ)
230229abscld 14116 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
231225recnd 10019 . . . . . . . . . . . . 13 (𝜒 → ((𝐹𝑧) − (𝑆𝑗)) ∈ ℂ)
232231abscld 14116 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ∈ ℝ)
233227recnd 10019 . . . . . . . . . . . . 13 (𝜒 → ((𝑆𝑗) − (lim sup‘𝑆)) ∈ ℂ)
234233abscld 14116 . . . . . . . . . . . 12 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) ∈ ℝ)
235232, 234readdcld 10020 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) ∈ ℝ)
236210rpred 11823 . . . . . . . . . . 11 (𝜒𝑥 ∈ ℝ)
237231, 233abstrid 14136 . . . . . . . . . . 11 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) ≤ ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))))
238236rehalfcld 11230 . . . . . . . . . . . . 13 (𝜒 → (𝑥 / 2) ∈ ℝ)
239207, 220abssubd 14133 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) = (abs‘((𝑆𝑗) − (𝐹𝑧))))
240203, 218, 115syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑆𝑗) = (𝐹‘(𝐴 + (1 / 𝑗))))
241240oveq1d 6625 . . . . . . . . . . . . . . . 16 (𝜒 → ((𝑆𝑗) − (𝐹𝑧)) = ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)))
242241fveq2d 6157 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) = (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))))
243203, 218, 106syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐹‘(𝐴 + (1 / 𝑗))) ∈ ℝ)
244243, 206resubcld 10409 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℝ)
245244recnd 10019 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧)) ∈ ℂ)
246245abscld 14116 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ∈ ℝ)
247203, 166syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑌 ∈ ℝ)
248203, 218, 58syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ ℝ)
249153, 205sseldi 3585 . . . . . . . . . . . . . . . . . 18 (𝜒𝑧 ∈ ℝ)
250248, 249resubcld 10409 . . . . . . . . . . . . . . . . 17 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ∈ ℝ)
251247, 250remulcld 10021 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∈ ℝ)
252203, 7syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐴 ∈ ℝ)
253203, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒𝐵 ∈ ℝ)
254203, 109syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
255164simprd 479 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
256148breq2i 4626 . . . . . . . . . . . . . . . . . . . . . 22 ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
257256ralbii 2975 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ))
258255, 257sylibr 224 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
259203, 258syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
260 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑥 → ((ℝ D 𝐹)‘𝑤) = ((ℝ D 𝐹)‘𝑥))
261260fveq2d 6157 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑥 → (abs‘((ℝ D 𝐹)‘𝑤)) = (abs‘((ℝ D 𝐹)‘𝑥)))
262261breq1d 4628 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑥 → ((abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌))
263262cbvralv 3162 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌 ↔ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑌)
264259, 263sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝜒 → ∀𝑤 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑤)) ≤ 𝑌)
265249rexrd 10040 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 ∈ ℝ*)
266203, 30syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝐵 ∈ ℝ*)
267249, 252resubcld 10409 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ∈ ℝ)
268267recnd 10019 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑧𝐴) ∈ ℂ)
269268abscld 14116 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) ∈ ℝ)
2703, 218sseldi 3585 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ∈ ℝ)
271203, 218, 56syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑗 ≠ 0)
272270, 271rereccld 10803 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℝ)
273267leabsd 14094 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑧𝐴) ≤ (abs‘(𝑧𝐴)))
274201simprd 479 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (abs‘(𝑧𝐴)) < (1 / 𝑗))
275267, 269, 272, 273, 274lelttrd 10146 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑧𝐴) < (1 / 𝑗))
276249, 252, 272ltsubadd2d 10576 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑧𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
277275, 276mpbid 222 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑧 < (𝐴 + (1 / 𝑗)))
278203, 218, 104syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝐴 + (1 / 𝑗)) < 𝐵)
279265, 266, 248, 277, 278eliood 39154 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐵))
280252, 253, 204, 254, 247, 264, 205, 279dvbdfbdioolem1 39471 . . . . . . . . . . . . . . . . 17 (𝜒 → ((abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ∧ (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · (𝐵𝐴))))
281280simpld 475 . . . . . . . . . . . . . . . 16 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)))
282203, 218, 57syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (1 / 𝑗) ∈ ℝ)
283247, 282remulcld 10021 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ∈ ℝ)
284158, 150ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℝ)
285284recnd 10019 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)) ∈ ℂ)
286285abscld 14116 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ∈ ℝ)
287285absge0d 14124 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
288 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝐴 + 𝐵) / 2) → ((ℝ D 𝐹)‘𝑥) = ((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2)))
289288fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → (abs‘((ℝ D 𝐹)‘𝑥)) = (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))))
290148eqcomi 2630 . . . . . . . . . . . . . . . . . . . . . . . 24 sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌
291290a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ((𝐴 + 𝐵) / 2) → sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) = 𝑌)
292289, 291breq12d 4631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = ((𝐴 + 𝐵) / 2) → ((abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < ) ↔ (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌))
293292rspcva 3296 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵) ∧ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘((ℝ D 𝐹)‘𝑥)) ≤ sup(ran (𝑥 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑥))), ℝ, < )) → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
294150, 255, 293syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (abs‘((ℝ D 𝐹)‘((𝐴 + 𝐵) / 2))) ≤ 𝑌)
29514, 286, 166, 287, 294letrd 10145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑌)
296203, 295syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → 0 ≤ 𝑌)
297203, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝐴 ∈ ℝ*)
298 ioogtlb 39151 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑧 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑧)
299297, 266, 205, 298syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 < 𝑧)
300252, 249, 248, 299ltsub2dd 10591 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < ((𝐴 + (1 / 𝑗)) − 𝐴))
301203, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝐴 ∈ ℂ)
302282recnd 10019 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (1 / 𝑗) ∈ ℂ)
303301, 302pncan2d 10345 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝐴) = (1 / 𝑗))
304300, 303breqtrd 4644 . . . . . . . . . . . . . . . . . . 19 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) < (1 / 𝑗))
305250, 272, 304ltled 10136 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((𝐴 + (1 / 𝑗)) − 𝑧) ≤ (1 / 𝑗))
306250, 272, 247, 296, 305lemul2ad 10915 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑌 · (1 / 𝑗)))
307283adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
308238adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑥 / 2) ∈ ℝ)
309 oveq1 6617 . . . . . . . . . . . . . . . . . . . . 21 (𝑌 = 0 → (𝑌 · (1 / 𝑗)) = (0 · (1 / 𝑗)))
310302mul02d 10185 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (0 · (1 / 𝑗)) = 0)
311309, 310sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) = 0)
312210rphalfcld 11835 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑥 / 2) ∈ ℝ+)
313312rpgt0d 11826 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → 0 < (𝑥 / 2))
314313adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒𝑌 = 0) → 0 < (𝑥 / 2))
315311, 314eqbrtrd 4640 . . . . . . . . . . . . . . . . . . 19 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) < (𝑥 / 2))
316307, 308, 315ltled 10136 . . . . . . . . . . . . . . . . . 18 ((𝜒𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
317247adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ∈ ℝ)
318296adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 ≤ 𝑌)
319 neqne 2798 . . . . . . . . . . . . . . . . . . . . 21 𝑌 = 0 → 𝑌 ≠ 0)
320319adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ ¬ 𝑌 = 0) → 𝑌 ≠ 0)
321317, 318, 320ne0gt0d 10125 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ ¬ 𝑌 = 0) → 0 < 𝑌)
322283adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ∈ ℝ)
3233, 213sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ)
324 0red 9992 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 ∈ ℝ)
325203, 210, 144syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀 ∈ ℝ)
326203, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → 0 < 𝑀)
327203, 210, 189syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒𝑀𝑁)
328324, 325, 323, 326, 327ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → 0 < 𝑁)
329328gt0ne0d 10543 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ≠ 0)
330323, 329rereccld 10803 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑁) ∈ ℝ)
331247, 330remulcld 10021 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑌 · (1 / 𝑁)) ∈ ℝ)
332331adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ∈ ℝ)
333238adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℝ)
334282adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ∈ ℝ)
335330adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ∈ ℝ)
336247adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℝ)
337296adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 𝑌)
338323, 328elrpd 11820 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁 ∈ ℝ+)
339203, 218, 59syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑗 ∈ ℝ+)
340 1red 10006 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 1 ∈ ℝ)
34176a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → 0 ≤ 1)
342217, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑁𝑗)
343338, 339, 340, 341, 342lediv2ad 11845 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (1 / 𝑗) ≤ (1 / 𝑁))
344343adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑗) ≤ (1 / 𝑁))
345334, 335, 336, 337, 344lemul2ad 10915 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑌 · (1 / 𝑁)))
346236recnd 10019 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ∈ ℂ)
347 2cnd 11044 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ∈ ℂ)
348210rpne0d 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑥 ≠ 0)
349176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → 2 ≠ 0)
350346, 347, 348, 349divne0d 10768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑥 / 2) ≠ 0)
351247, 238, 350redivcld 10804 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) ∈ ℝ)
352351adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ)
353 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < 𝑌)
354313adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑥 / 2))
355336, 333, 353, 354divgt0d 10910 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜒 ∧ 0 < 𝑌) → 0 < (𝑌 / (𝑥 / 2)))
356352, 355elrpd 11820 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℝ+)
357356rprecred 11834 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / (𝑌 / (𝑥 / 2))) ∈ ℝ)
358338adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑁 ∈ ℝ+)
359 1red 10006 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 1 ∈ ℝ)
36076a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 0 ≤ 1)
361351flcld 12546 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → (⌊‘(𝑌 / (𝑥 / 2))) ∈ ℤ)
362361peano2zd 11436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℤ)
363362zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ)
364203, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜒𝑀 ∈ ℤ)
365362, 364ifcld 4108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒 → if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀) ∈ ℤ)
366147, 365syl5eqel 2702 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒𝑁 ∈ ℤ)
367366zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒𝑁 ∈ ℝ)
368 flltp1 12548 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 / (𝑥 / 2)) ∈ ℝ → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
369351, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → (𝑌 / (𝑥 / 2)) < ((⌊‘(𝑌 / (𝑥 / 2))) + 1))
370203, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜒𝑀 ∈ ℝ)
371 max2 11968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ∈ ℝ) → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
372370, 363, 371syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ if(𝑀 ≤ ((⌊‘(𝑌 / (𝑥 / 2))) + 1), ((⌊‘(𝑌 / (𝑥 / 2))) + 1), 𝑀))
373372, 147syl6breqr 4660 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜒 → ((⌊‘(𝑌 / (𝑥 / 2))) + 1) ≤ 𝑁)
374351, 363, 367, 369, 373ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜒 → (𝑌 / (𝑥 / 2)) < 𝑁)
375351, 323, 374ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜒 → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
376375adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≤ 𝑁)
377356, 358, 359, 360, 376lediv2ad 11845 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (1 / 𝑁) ≤ (1 / (𝑌 / (𝑥 / 2))))
378335, 357, 336, 337, 377lemul2ad 10915 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
379336recnd 10019 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ∈ ℂ)
380352recnd 10019 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ∈ ℂ)
381355gt0ne0d 10543 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑥 / 2)) ≠ 0)
382379, 380, 381divrecd 10755 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑌 · (1 / (𝑌 / (𝑥 / 2)))))
383333recnd 10019 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ∈ ℂ)
384353gt0ne0d 10543 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → 𝑌 ≠ 0)
385350adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜒 ∧ 0 < 𝑌) → (𝑥 / 2) ≠ 0)
386379, 383, 384, 385ddcand 10772 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜒 ∧ 0 < 𝑌) → (𝑌 / (𝑌 / (𝑥 / 2))) = (𝑥 / 2))
387382, 386eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . 21 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / (𝑌 / (𝑥 / 2)))) = (𝑥 / 2))
388378, 387breqtrd 4644 . . . . . . . . . . . . . . . . . . . 20 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑁)) ≤ (𝑥 / 2))
389322, 332, 333, 345, 388letrd 10145 . . . . . . . . . . . . . . . . . . 19 ((𝜒 ∧ 0 < 𝑌) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
390321, 389syldan 487 . . . . . . . . . . . . . . . . . 18 ((𝜒 ∧ ¬ 𝑌 = 0) → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
391316, 390pm2.61dan 831 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑌 · (1 / 𝑗)) ≤ (𝑥 / 2))
392251, 283, 238, 306, 391letrd 10145 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑌 · ((𝐴 + (1 / 𝑗)) − 𝑧)) ≤ (𝑥 / 2))
393246, 251, 238, 281, 392letrd 10145 . . . . . . . . . . . . . . 15 (𝜒 → (abs‘((𝐹‘(𝐴 + (1 / 𝑗))) − (𝐹𝑧))) ≤ (𝑥 / 2))
394242, 393eqbrtrd 4640 . . . . . . . . . . . . . 14 (𝜒 → (abs‘((𝑆𝑗) − (𝐹𝑧))) ≤ (𝑥 / 2))
395239, 394eqbrtrd 4640 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝐹𝑧) − (𝑆𝑗))) ≤ (𝑥 / 2))
396 simpllr 798 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
397201, 396syl 17 . . . . . . . . . . . . 13 (𝜒 → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
398232, 234, 238, 238, 395, 397leltaddd 10600 . . . . . . . . . . . 12 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < ((𝑥 / 2) + (𝑥 / 2)))
3993462halvesd 11229 . . . . . . . . . . . 12 (𝜒 → ((𝑥 / 2) + (𝑥 / 2)) = 𝑥)
400398, 399breqtrd 4644 . . . . . . . . . . 11 (𝜒 → ((abs‘((𝐹𝑧) − (𝑆𝑗))) + (abs‘((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
401230, 235, 236, 237, 400lelttrd 10146 . . . . . . . . . 10 (𝜒 → (abs‘(((𝐹𝑧) − (𝑆𝑗)) + ((𝑆𝑗) − (lim sup‘𝑆)))) < 𝑥)
402224, 401eqbrtrd 4640 . . . . . . . . 9 (𝜒 → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
403200, 402sylbir 225 . . . . . . . 8 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
404403adantrl 751 . . . . . . 7 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) ∧ (𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗))) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)
405404ex 450 . . . . . 6 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
406405ralrimiva 2961 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
407 breq2 4622 . . . . . . . . 9 (𝑦 = (1 / 𝑗) → ((abs‘(𝑧𝐴)) < 𝑦 ↔ (abs‘(𝑧𝐴)) < (1 / 𝑗)))
408407anbi2d 739 . . . . . . . 8 (𝑦 = (1 / 𝑗) → ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) ↔ (𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗))))
409408imbi1d 331 . . . . . . 7 (𝑦 = (1 / 𝑗) → (((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)))
410409ralbidv 2981 . . . . . 6 (𝑦 = (1 / 𝑗) → (∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥) ↔ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)))
411410rspcev 3298 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < (1 / 𝑗)) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
412199, 406, 411syl2anc 692 . . . 4 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (ℤ𝑁)) ∧ (abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
413 simpr 477 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑏𝑁)
414413iftrued 4071 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑁)
415 uzid 11653 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
416183, 415syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ (ℤ𝑁))
417416adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → 𝑁 ∈ (ℤ𝑁))
418414, 417eqeltrd 2698 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
419418adantlr 750 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
420 iffalse 4072 . . . . . . . . . 10 𝑏𝑁 → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
421420adantl 482 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) = 𝑏)
422183ad2antrr 761 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℤ)
423 simplr 791 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℤ)
424422zred 11433 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 ∈ ℝ)
425423zred 11433 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ ℝ)
426 simpr 477 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → ¬ 𝑏𝑁)
427424, 425ltnled 10135 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → (𝑁 < 𝑏 ↔ ¬ 𝑏𝑁))
428426, 427mpbird 247 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁 < 𝑏)
429424, 425, 428ltled 10136 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑁𝑏)
430 eluz2 11644 . . . . . . . . . 10 (𝑏 ∈ (ℤ𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁𝑏))
431422, 423, 429, 430syl3anbrc 1244 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → 𝑏 ∈ (ℤ𝑁))
432421, 431eqeltrd 2698 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ¬ 𝑏𝑁) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
433419, 432pm2.61dan 831 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
434433adantr 481 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁))
435 simpr 477 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
436 simpr 477 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℤ)
437183adantr 481 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℤ)
438437, 436ifcld 4108 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ)
439436zred 11433 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
440437zred 11433 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑁 ∈ ℝ)
441 max1 11966 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
442439, 440, 441syl2anc 692 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏))
443 eluz2 11644 . . . . . . . . . 10 (if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏) ↔ (𝑏 ∈ ℤ ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ ℤ ∧ 𝑏 ≤ if(𝑏𝑁, 𝑁, 𝑏)))
444436, 438, 442, 443syl3anbrc 1244 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
445444adantr 481 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏))
446 fveq2 6153 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑐) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
447446eleq1d 2683 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑐) ∈ ℂ ↔ (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ))
448446oveq1d 6625 . . . . . . . . . . . 12 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑐) − (lim sup‘𝑆)) = ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))
449448fveq2d 6157 . . . . . . . . . . 11 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑐) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
450449breq1d 4628 . . . . . . . . . 10 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
451447, 450anbi12d 746 . . . . . . . . 9 (𝑐 = if(𝑏𝑁, 𝑁, 𝑏) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ↔ ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))))
452451rspccva 3297 . . . . . . . 8 ((∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)) ∧ if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑏)) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
453435, 445, 452syl2anc 692 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) ∈ ℂ ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
454453simprd 479 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2))
455 fveq2 6153 . . . . . . . . . 10 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (𝑆𝑗) = (𝑆‘if(𝑏𝑁, 𝑁, 𝑏)))
456455oveq1d 6625 . . . . . . . . 9 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → ((𝑆𝑗) − (lim sup‘𝑆)) = ((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆)))
457456fveq2d 6157 . . . . . . . 8 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → (abs‘((𝑆𝑗) − (lim sup‘𝑆))) = (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))))
458457breq1d 4628 . . . . . . 7 (𝑗 = if(𝑏𝑁, 𝑁, 𝑏) → ((abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2) ↔ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)))
459458rspcev 3298 . . . . . 6 ((if(𝑏𝑁, 𝑁, 𝑏) ∈ (ℤ𝑁) ∧ (abs‘((𝑆‘if(𝑏𝑁, 𝑁, 𝑏)) − (lim sup‘𝑆))) < (𝑥 / 2)) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
460434, 454, 459syl2anc 692 . . . . 5 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑏 ∈ ℤ) ∧ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
461 ax-resscn 9944 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
462461a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℂ)
46326, 462fssd 6019 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴(,)𝐵)⟶ℂ)
464 dvcn 23603 . . . . . . . . . . . . . 14 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴(,)𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐵)) → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
465462, 463, 154, 109, 464syl31anc 1326 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
466 cncffvrn 22620 . . . . . . . . . . . . 13 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
467462, 465, 466syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐵)⟶ℝ))
46826, 467mpbird 247 . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴(,)𝐵)–cn→ℝ))
469 ioodvbdlimc1lem2.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗)))
470105, 469fmptd 6346 . . . . . . . . . . 11 (𝜑𝑅:(ℤ𝑀)⟶(𝐴(,)𝐵))
471 eqid 2621 . . . . . . . . . . 11 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))
472 climrel 14164 . . . . . . . . . . . . 13 Rel ⇝
473472a1i 11 . . . . . . . . . . . 12 (𝜑 → Rel ⇝ )
474 fvex 6163 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) ∈ V
475474mptex 6446 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V
476475a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ∈ V)
477 eqidd 2622 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
478 eqidd 2622 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑚) → 𝐴 = 𝐴)
479 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝑚 ∈ (ℤ𝑀))
4807adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
481477, 478, 479, 480fvmptd 6250 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑚) = 𝐴)
48223, 142, 476, 98, 481climconst 14215 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) ⇝ 𝐴)
483474mptex 6446 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗))) ∈ V
484469, 483eqeltri 2694 . . . . . . . . . . . . . . 15 𝑅 ∈ V
485484a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ V)
486 1cnd 10007 . . . . . . . . . . . . . . 15 (𝜑 → 1 ∈ ℂ)
487 elnnnn0b 11288 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℕ0 ∧ 0 < 𝑀))
48821, 67, 487sylanbrc 697 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
489 divcnvg 39286 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑀 ∈ ℕ) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
490486, 488, 489syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) ⇝ 0)
491 eqidd 2622 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ 𝐴) = (𝑗 ∈ (ℤ𝑀) ↦ 𝐴))
492 eqidd 2622 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → 𝐴 = 𝐴)
493 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ (ℤ𝑀))
4947adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℝ)
495491, 492, 493, 494fvmptd 6250 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) = 𝐴)
49698adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝐴 ∈ ℂ)
497495, 496eqeltrd 2698 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) ∈ ℂ)
498 eqidd 2622 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)) = (𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗)))
499 oveq2 6618 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (1 / 𝑗) = (1 / 𝑖))
500499adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (1 / 𝑗) = (1 / 𝑖))
5013, 493sseldi 3585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℝ)
502 0red 9992 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 ∈ ℝ)
50362adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
50467adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑀)
505 eluzle 11651 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (ℤ𝑀) → 𝑀𝑖)
506505adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑀𝑖)
507502, 503, 501, 504, 506ltletrd 10148 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (ℤ𝑀)) → 0 < 𝑖)
508507gt0ne0d 10543 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ≠ 0)
509501, 508rereccld 10803 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℝ)
510498, 500, 493, 509fvmptd 6250 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) = (1 / 𝑖))
511501recnd 10019 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑖 ∈ ℂ)
512511, 508reccld 10745 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (1 / 𝑖) ∈ ℂ)
513510, 512eqeltrd 2698 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖) ∈ ℂ)
514469a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → 𝑅 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐴 + (1 / 𝑗))))
515499oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
516515adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (ℤ𝑀)) ∧ 𝑗 = 𝑖) → (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
517494, 509readdcld 10020 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑖)) ∈ ℝ)
518514, 516, 493, 517fvmptd 6250 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (𝐴 + (1 / 𝑖)))
519495, 510oveq12d 6628 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (ℤ𝑀)) → (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)) = (𝐴 + (1 / 𝑖)))
520518, 519eqtr4d 2658 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (ℤ𝑀)) → (𝑅𝑖) = (((𝑗 ∈ (ℤ𝑀) ↦ 𝐴)‘𝑖) + ((𝑗 ∈ (ℤ𝑀) ↦ (1 / 𝑗))‘𝑖)))
52123, 142, 482, 485, 490, 497, 513, 520climadd 14303 . . . . . . . . . . . . 13 (𝜑𝑅 ⇝ (𝐴 + 0))
52298addid1d 10187 . . . . . . . . . . . . 13 (𝜑 → (𝐴 + 0) = 𝐴)
523521, 522breqtrd 4644 . . . . . . . . . . . 12 (𝜑𝑅𝐴)
524 releldm 5323 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅𝐴) → 𝑅 ∈ dom ⇝ )
525473, 523, 524syl2anc 692 . . . . . . . . . . 11 (𝜑𝑅 ∈ dom ⇝ )
526 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → (ℤ𝑙) = (ℤ𝑘))
527 fveq2 6153 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → (𝑅𝑙) = (𝑅𝑘))
528527oveq2d 6626 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → ((𝑅) − (𝑅𝑙)) = ((𝑅) − (𝑅𝑘)))
529528fveq2d 6157 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑘 → (abs‘((𝑅) − (𝑅𝑙))) = (abs‘((𝑅) − (𝑅𝑘))))
530529breq1d 4628 . . . . . . . . . . . . . . 15 (𝑙 = 𝑘 → ((abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
531526, 530raleqbidv 3144 . . . . . . . . . . . . . 14 (𝑙 = 𝑘 → (∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
532531cbvrabv 3188 . . . . . . . . . . . . 13 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
533 fveq2 6153 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → (𝑅) = (𝑅𝑖))
534533oveq1d 6625 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → ((𝑅) − (𝑅𝑘)) = ((𝑅𝑖) − (𝑅𝑘)))
535534fveq2d 6157 . . . . . . . . . . . . . . . . 17 ( = 𝑖 → (abs‘((𝑅) − (𝑅𝑘))) = (abs‘((𝑅𝑖) − (𝑅𝑘))))
536535breq1d 4628 . . . . . . . . . . . . . . . 16 ( = 𝑖 → ((abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ (abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))))
537536cbvralv 3162 . . . . . . . . . . . . . . 15 (∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
538537rgenw 2919 . . . . . . . . . . . . . 14 𝑘 ∈ (ℤ𝑀)(∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)) ↔ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1)))
539 rabbi 3112 . . . . . . . . . . . . . 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))})
540538, 539mpbi 220 . . . . . . . . . . . . 13 {𝑘 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑘)(abs‘((𝑅) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
541532, 540eqtri 2643 . . . . . . . . . . . 12 {𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))} = {𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}
542541infeq1i 8335 . . . . . . . . . . 11 inf({𝑙 ∈ (ℤ𝑀) ∣ ∀ ∈ (ℤ𝑙)(abs‘((𝑅) − (𝑅𝑙))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < ) = inf({𝑘 ∈ (ℤ𝑀) ∣ ∀𝑖 ∈ (ℤ𝑘)(abs‘((𝑅𝑖) − (𝑅𝑘))) < (𝑥 / (sup(ran (𝑧 ∈ (𝐴(,)𝐵) ↦ (abs‘((ℝ D 𝐹)‘𝑧))), ℝ, < ) + 1))}, ℝ, < )
5437, 6, 9, 468, 109, 110, 22, 470, 471, 525, 542ioodvbdlimc1lem1 39474 . . . . . . . . . 10 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))) ⇝ (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
544469fvmpt2 6253 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (ℤ𝑀) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
545113, 58, 544syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝑅𝑗) = (𝐴 + (1 / 𝑗)))
546545eqcomd 2627 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐴 + (1 / 𝑗)) = (𝑅𝑗))
547546fveq2d 6157 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝑀)) → (𝐹‘(𝐴 + (1 / 𝑗))) = (𝐹‘(𝑅𝑗)))
548547mpteq2dva 4709 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
549107, 548syl5eq 2667 . . . . . . . . . 10 (𝜑𝑆 = (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗))))
550549fveq2d 6157 . . . . . . . . . 10 (𝜑 → (lim sup‘𝑆) = (lim sup‘(𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝑅𝑗)))))
551543, 549, 5503brtr4d 4650 . . . . . . . . 9 (𝜑𝑆 ⇝ (lim sup‘𝑆))
552474mptex 6446 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) ↦ (𝐹‘(𝐴 + (1 / 𝑗)))) ∈ V
553107, 552eqeltri 2694 . . . . . . . . . . 11 𝑆 ∈ V
554553a1i 11 . . . . . . . . . 10 (𝜑𝑆 ∈ V)
555 eqidd 2622 . . . . . . . . . 10 ((𝜑𝑐 ∈ ℤ) → (𝑆𝑐) = (𝑆𝑐))
556554, 555clim 14166 . . . . . . . . 9 (𝜑 → (𝑆 ⇝ (lim sup‘𝑆) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))))
557551, 556mpbid 222 . . . . . . . 8 (𝜑 → ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎)))
558557simprd 479 . . . . . . 7 (𝜑 → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
559558adantr 481 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎))
560 simpr 477 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
561560rphalfcld 11835 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
562 breq2 4622 . . . . . . . . 9 (𝑎 = (𝑥 / 2) → ((abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎 ↔ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
563562anbi2d 739 . . . . . . . 8 (𝑎 = (𝑥 / 2) → (((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
564563rexralbidv 3052 . . . . . . 7 (𝑎 = (𝑥 / 2) → (∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ↔ ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2))))
565564rspccva 3297 . . . . . 6 ((∀𝑎 ∈ ℝ+𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < 𝑎) ∧ (𝑥 / 2) ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
566559, 561, 565syl2anc 692 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ∃𝑏 ∈ ℤ ∀𝑐 ∈ (ℤ𝑏)((𝑆𝑐) ∈ ℂ ∧ (abs‘((𝑆𝑐) − (lim sup‘𝑆))) < (𝑥 / 2)))
567460, 566r19.29a 3072 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗 ∈ (ℤ𝑁)(abs‘((𝑆𝑗) − (lim sup‘𝑆))) < (𝑥 / 2))
568412, 567r19.29a 3072 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
569568ralrimiva 2961 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))
570 ioosscn 39150 . . . 4 (𝐴(,)𝐵) ⊆ ℂ
571570a1i 11 . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
572463, 571, 98ellimc3 23562 . 2 (𝜑 → ((lim sup‘𝑆) ∈ (𝐹 lim 𝐴) ↔ ((lim sup‘𝑆) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑧 ∈ (𝐴(,)𝐵)((𝑧𝐴 ∧ (abs‘(𝑧𝐴)) < 𝑦) → (abs‘((𝐹𝑧) − (lim sup‘𝑆))) < 𝑥))))
573137, 569, 572mpbir2and 956 1 (𝜑 → (lim sup‘𝑆) ∈ (𝐹 lim 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  wss 3559  c0 3896  ifcif 4063   class class class wbr 4618  cmpt 4678  dom cdm 5079  ran crn 5080  Rel wrel 5084  wf 5848  cfv 5852  (class class class)co 6610  supcsup 8297  infcinf 8298  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892  +∞cpnf 10022  *cxr 10024   < clt 10025  cle 10026  cmin 10217   / cdiv 10635  cn 10971  2c2 11021  0cn0 11243  cz 11328  cuz 11638  +crp 11783  (,)cioo 12124  cfl 12538  abscabs 13915  lim supclsp 14142  cli 14156  cnccncf 22598   lim climc 23545   D cdv 23546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-limsup 14143  df-clim 14160  df-rlim 14161  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-sca 15885  df-vsca 15886  df-ip 15887  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-hom 15894  df-cco 15895  df-rest 16011  df-topn 16012  df-0g 16030  df-gsum 16031  df-topgen 16032  df-pt 16033  df-prds 16036  df-xrs 16090  df-qtop 16095  df-imas 16096  df-xps 16098  df-mre 16174  df-mrc 16175  df-acs 16177  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-submnd 17264  df-mulg 17469  df-cntz 17678  df-cmn 18123  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-fbas 19671  df-fg 19672  df-cnfld 19675  df-top 20627  df-topon 20644  df-topsp 20657  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-perf 20860  df-cn 20950  df-cnp 20951  df-haus 21038  df-cmp 21109  df-tx 21284  df-hmeo 21477  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663  df-xms 22044  df-ms 22045  df-tms 22046  df-cncf 22600  df-limc 23549  df-dv 23550
This theorem is referenced by:  ioodvbdlimc1  39476
  Copyright terms: Public domain W3C validator