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

Theorem ioodvbdlimc2lem 45245
Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
Hypotheses
Ref Expression
ioodvbdlimc2lem.a (πœ‘ β†’ 𝐴 ∈ ℝ)
ioodvbdlimc2lem.b (πœ‘ β†’ 𝐡 ∈ ℝ)
ioodvbdlimc2lem.altb (πœ‘ β†’ 𝐴 < 𝐡)
ioodvbdlimc2lem.f (πœ‘ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
ioodvbdlimc2lem.dmdv (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
ioodvbdlimc2lem.dvbd (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ 𝑦)
ioodvbdlimc2lem.y π‘Œ = sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )
ioodvbdlimc2lem.m 𝑀 = ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)
ioodvbdlimc2lem.s 𝑆 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))
ioodvbdlimc2lem.r 𝑅 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (𝐡 βˆ’ (1 / 𝑗)))
ioodvbdlimc2lem.n 𝑁 = if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀)
ioodvbdlimc2lem.ch (πœ’ ↔ (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)))
Assertion
Ref Expression
ioodvbdlimc2lem (πœ‘ β†’ (lim supβ€˜π‘†) ∈ (𝐹 limβ„‚ 𝐡))
Distinct variable groups:   𝐴,𝑗,π‘₯,𝑧,𝑦   𝐡,𝑗,π‘₯,𝑧,𝑦   𝑗,𝐹,π‘₯,𝑧,𝑦   𝑗,𝑀,π‘₯,𝑦   𝑗,𝑁,𝑧   𝑅,𝑗,π‘₯,𝑦   π‘₯,𝑆,𝑗,𝑦,𝑧   π‘₯,π‘Œ   πœ‘,π‘₯,𝑗,𝑧,𝑦
Allowed substitution hints:   πœ’(π‘₯,𝑦,𝑧,𝑗)   𝑅(𝑧)   𝑀(𝑧)   𝑁(π‘₯,𝑦)   π‘Œ(𝑦,𝑧,𝑗)

Proof of Theorem ioodvbdlimc2lem
Dummy variables 𝑏 π‘˜ β„Ž 𝑖 𝑙 𝑀 π‘š 𝑐 π‘Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 12865 . . . . . 6 (β„€β‰₯β€˜π‘€) βŠ† β„€
2 zssre 12587 . . . . . 6 β„€ βŠ† ℝ
31, 2sstri 3987 . . . . 5 (β„€β‰₯β€˜π‘€) βŠ† ℝ
43a1i 11 . . . 4 (πœ‘ β†’ (β„€β‰₯β€˜π‘€) βŠ† ℝ)
5 ioodvbdlimc2lem.m . . . . . . 7 𝑀 = ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)
6 ioodvbdlimc2lem.b . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ ℝ)
7 ioodvbdlimc2lem.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
86, 7resubcld 11664 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
9 ioodvbdlimc2lem.altb . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
107, 6posdifd 11823 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
119, 10mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
1211gt0ne0d 11800 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
138, 12rereccld 12063 . . . . . . . . 9 (πœ‘ β†’ (1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ)
14 0red 11239 . . . . . . . . . 10 (πœ‘ β†’ 0 ∈ ℝ)
158, 11recgt0d 12170 . . . . . . . . . 10 (πœ‘ β†’ 0 < (1 / (𝐡 βˆ’ 𝐴)))
1614, 13, 15ltled 11384 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (1 / (𝐡 βˆ’ 𝐴)))
17 flge0nn0 13809 . . . . . . . . 9 (((1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ ∧ 0 ≀ (1 / (𝐡 βˆ’ 𝐴))) β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„•0)
1813, 16, 17syl2anc 583 . . . . . . . 8 (πœ‘ β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„•0)
19 peano2nn0 12534 . . . . . . . 8 ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„•0 β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ β„•0)
2018, 19syl 17 . . . . . . 7 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ β„•0)
215, 20eqeltrid 2832 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•0)
2221nn0zd 12606 . . . . 5 (πœ‘ β†’ 𝑀 ∈ β„€)
23 eqid 2727 . . . . . 6 (β„€β‰₯β€˜π‘€) = (β„€β‰₯β€˜π‘€)
2423uzsup 13852 . . . . 5 (𝑀 ∈ β„€ β†’ sup((β„€β‰₯β€˜π‘€), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (πœ‘ β†’ sup((β„€β‰₯β€˜π‘€), ℝ*, < ) = +∞)
26 ioodvbdlimc2lem.f . . . . . . 7 (πœ‘ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
2726adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
287rexrd 11286 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ ℝ*)
2928adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ ℝ*)
306rexrd 11286 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ ℝ*)
3130adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐡 ∈ ℝ*)
326adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐡 ∈ ℝ)
33 eluzelre 12855 . . . . . . . . . 10 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑗 ∈ ℝ)
3433adantl 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 ∈ ℝ)
35 0red 11239 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 ∈ ℝ)
36 0red 11239 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 0 ∈ ℝ)
37 1red 11237 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 1 ∈ ℝ)
3836, 37readdcld 11265 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ (0 + 1) ∈ ℝ)
3938adantl 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (0 + 1) ∈ ℝ)
4036ltp1d 12166 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 0 < (0 + 1))
4140adantl 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < (0 + 1))
42 eluzel2 12849 . . . . . . . . . . . . . 14 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ∈ β„€)
4342zred 12688 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ∈ ℝ)
4443adantl 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ)
4513flcld 13787 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„€)
4645zred 12688 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
47 1red 11237 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ ℝ)
4818nn0ge0d 12557 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 0 ≀ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))))
4914, 46, 47, 48leadd1dd 11850 . . . . . . . . . . . . . 14 (πœ‘ β†’ (0 + 1) ≀ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
5049, 5breqtrrdi 5184 . . . . . . . . . . . . 13 (πœ‘ β†’ (0 + 1) ≀ 𝑀)
5150adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (0 + 1) ≀ 𝑀)
52 eluzle 12857 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝑗)
5352adantl 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ≀ 𝑗)
5439, 44, 34, 51, 53letrd 11393 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (0 + 1) ≀ 𝑗)
5535, 39, 34, 41, 54ltletrd 11396 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < 𝑗)
5655gt0ne0d 11800 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 β‰  0)
5734, 56rereccld 12063 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑗) ∈ ℝ)
5832, 57resubcld 11664 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑗)) ∈ ℝ)
597adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ ℝ)
6021nn0red 12555 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ ℝ)
6114, 47readdcld 11265 . . . . . . . . . . . . . 14 (πœ‘ β†’ (0 + 1) ∈ ℝ)
6246, 47readdcld 11265 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ ℝ)
6314ltp1d 12166 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < (0 + 1))
6414, 61, 62, 63, 49ltletrd 11396 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
6564, 5breqtrrdi 5184 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 𝑀)
6665gt0ne0d 11800 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 β‰  0)
6760, 66rereccld 12063 . . . . . . . . . 10 (πœ‘ β†’ (1 / 𝑀) ∈ ℝ)
6867adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑀) ∈ ℝ)
6932, 68resubcld 11664 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑀)) ∈ ℝ)
705eqcomi 2736 . . . . . . . . . . . . 13 ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) = 𝑀
7170oveq2i 7425 . . . . . . . . . . . 12 (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) = (1 / 𝑀)
7271, 67eqeltrid 2832 . . . . . . . . . . 11 (πœ‘ β†’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) ∈ ℝ)
7313, 15elrpd 13037 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ+)
7462, 64elrpd 13037 . . . . . . . . . . . . 13 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ ℝ+)
75 1rp 13002 . . . . . . . . . . . . . 14 1 ∈ ℝ+
7675a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 ∈ ℝ+)
77 fllelt 13786 . . . . . . . . . . . . . . 15 ((1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ≀ (1 / (𝐡 βˆ’ 𝐴)) ∧ (1 / (𝐡 βˆ’ 𝐴)) < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)))
7813, 77syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ≀ (1 / (𝐡 βˆ’ 𝐴)) ∧ (1 / (𝐡 βˆ’ 𝐴)) < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)))
7978simprd 495 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 / (𝐡 βˆ’ 𝐴)) < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
8073, 74, 76, 79ltdiv2dd 44599 . . . . . . . . . . . 12 (πœ‘ β†’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) < (1 / (1 / (𝐡 βˆ’ 𝐴))))
818recnd 11264 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ β„‚)
8281, 12recrecd 12009 . . . . . . . . . . . 12 (πœ‘ β†’ (1 / (1 / (𝐡 βˆ’ 𝐴))) = (𝐡 βˆ’ 𝐴))
8380, 82breqtrd 5168 . . . . . . . . . . 11 (πœ‘ β†’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) < (𝐡 βˆ’ 𝐴))
8472, 8, 6, 83ltsub2dd 11849 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ (𝐡 βˆ’ 𝐴)) < (𝐡 βˆ’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))))
856recnd 11264 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ β„‚)
867recnd 11264 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ β„‚)
8785, 86nncand 11598 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ (𝐡 βˆ’ 𝐴)) = 𝐴)
8871oveq2i 7425 . . . . . . . . . . 11 (𝐡 βˆ’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))) = (𝐡 βˆ’ (1 / 𝑀))
8988a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))) = (𝐡 βˆ’ (1 / 𝑀)))
9084, 87, 893brtr3d 5173 . . . . . . . . 9 (πœ‘ β†’ 𝐴 < (𝐡 βˆ’ (1 / 𝑀)))
9190adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 < (𝐡 βˆ’ (1 / 𝑀)))
9260, 65elrpd 13037 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ ℝ+)
9392adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ+)
9434, 55elrpd 13037 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 ∈ ℝ+)
95 1red 11237 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 1 ∈ ℝ)
96 0le1 11759 . . . . . . . . . . 11 0 ≀ 1
9796a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 ≀ 1)
9893, 94, 95, 97, 53lediv2ad 13062 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑗) ≀ (1 / 𝑀))
9957, 68, 32, 98lesub2dd 11853 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑀)) ≀ (𝐡 βˆ’ (1 / 𝑗)))
10059, 69, 58, 91, 99ltletrd 11396 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 < (𝐡 βˆ’ (1 / 𝑗)))
10194rpreccld 13050 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑗) ∈ ℝ+)
10232, 101ltsubrpd 13072 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑗)) < 𝐡)
10329, 31, 58, 100, 102eliood 44806 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑗)) ∈ (𝐴(,)𝐡))
10427, 103ffvelcdmd 7089 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))) ∈ ℝ)
105 ioodvbdlimc2lem.s . . . . 5 𝑆 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))
106104, 105fmptd 7118 . . . 4 (πœ‘ β†’ 𝑆:(β„€β‰₯β€˜π‘€)βŸΆβ„)
107 ioodvbdlimc2lem.dmdv . . . . . 6 (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
108 ioodvbdlimc2lem.dvbd . . . . . 6 (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ 𝑦)
1097, 6, 9, 26, 107, 108dvbdfbdioo 45241 . . . . 5 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏)
11060adantr 480 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) β†’ 𝑀 ∈ ℝ)
111 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘€))
112105fvmpt2 7010 . . . . . . . . . . . . . 14 ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ∧ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))) ∈ ℝ) β†’ (π‘†β€˜π‘—) = (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))
113111, 104, 112syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘†β€˜π‘—) = (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))
114113fveq2d 6895 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(π‘†β€˜π‘—)) = (absβ€˜(πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))))
115114adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(π‘†β€˜π‘—)) = (absβ€˜(πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))))
116 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏)
117103adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑗)) ∈ (𝐴(,)𝐡))
118 2fveq3 6896 . . . . . . . . . . . . . 14 (π‘₯ = (𝐡 βˆ’ (1 / 𝑗)) β†’ (absβ€˜(πΉβ€˜π‘₯)) = (absβ€˜(πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))))
119118breq1d 5152 . . . . . . . . . . . . 13 (π‘₯ = (𝐡 βˆ’ (1 / 𝑗)) β†’ ((absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 ↔ (absβ€˜(πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))) ≀ 𝑏))
120119rspccva 3606 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 ∧ (𝐡 βˆ’ (1 / 𝑗)) ∈ (𝐴(,)𝐡)) β†’ (absβ€˜(πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))) ≀ 𝑏)
121116, 117, 120syl2anc 583 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))) ≀ 𝑏)
122115, 121eqbrtrd 5164 . . . . . . . . . 10 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)
123122a1d 25 . . . . . . . . 9 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
124123ralrimiva 3141 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) β†’ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
125 breq1 5145 . . . . . . . . . . 11 (π‘˜ = 𝑀 β†’ (π‘˜ ≀ 𝑗 ↔ 𝑀 ≀ 𝑗))
126125imbi1d 341 . . . . . . . . . 10 (π‘˜ = 𝑀 β†’ ((π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏) ↔ (𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
127126ralbidv 3172 . . . . . . . . 9 (π‘˜ = 𝑀 β†’ (βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏) ↔ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
128127rspcev 3607 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
129110, 124, 128syl2anc 583 . . . . . . 7 ((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
130129ex 412 . . . . . 6 (πœ‘ β†’ (βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
131130reximdv 3165 . . . . 5 (πœ‘ β†’ (βˆƒπ‘ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 β†’ βˆƒπ‘ ∈ ℝ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
132109, 131mpd 15 . . . 4 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
1334, 25, 106, 132limsupre 44952 . . 3 (πœ‘ β†’ (lim supβ€˜π‘†) ∈ ℝ)
134133recnd 11264 . 2 (πœ‘ β†’ (lim supβ€˜π‘†) ∈ β„‚)
135 eluzelre 12855 . . . . . . . . 9 (𝑗 ∈ (β„€β‰₯β€˜π‘) β†’ 𝑗 ∈ ℝ)
136135adantl 481 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑗 ∈ ℝ)
137 0red 11239 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 ∈ ℝ)
13845peano2zd 12691 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ β„€)
1395, 138eqeltrid 2832 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„€)
140139adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ∈ β„€)
141140zred 12688 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ∈ ℝ)
142141adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑀 ∈ ℝ)
14365ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 < 𝑀)
144 ioodvbdlimc2lem.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀)
145 ioodvbdlimc2lem.y . . . . . . . . . . . . . . . . . . . 20 π‘Œ = sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )
146 ioomidp 44822 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡) β†’ ((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡))
1477, 6, 9, 146syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡))
148 ne0i 4330 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡) β†’ (𝐴(,)𝐡) β‰  βˆ…)
149147, 148syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐴(,)𝐡) β‰  βˆ…)
150 ioossre 13409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐡) βŠ† ℝ
151150a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† ℝ)
152 dvfre 25870 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐡)βŸΆβ„ ∧ (𝐴(,)𝐡) βŠ† ℝ) β†’ (ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„)
15326, 151, 152syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„)
154107feq2d 6702 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„ ↔ (ℝ D 𝐹):(𝐴(,)𝐡)βŸΆβ„))
155153, 154mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (ℝ D 𝐹):(𝐴(,)𝐡)βŸΆβ„)
156155ffvelcdmda 7088 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐹)β€˜π‘₯) ∈ ℝ)
157156recnd 11264 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐹)β€˜π‘₯) ∈ β„‚)
158157abscld 15407 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ∈ ℝ)
159 eqid 2727 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))) = (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)))
160 eqid 2727 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) = sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )
161149, 158, 108, 159, 160suprnmpt 44470 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) ∈ ℝ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )))
162161simpld 494 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) ∈ ℝ)
163145, 162eqeltrid 2832 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ π‘Œ ∈ ℝ)
164163adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘Œ ∈ ℝ)
165 rpre 13006 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ ℝ)
166165rehalfcld 12481 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ+ β†’ (π‘₯ / 2) ∈ ℝ)
167166adantl 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) ∈ ℝ)
168165recnd 11264 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ β„‚)
169168adantl 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ β„‚)
170 2cnd 12312 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 2 ∈ β„‚)
171 rpne0 13014 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ β‰  0)
172171adantl 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ β‰  0)
173 2ne0 12338 . . . . . . . . . . . . . . . . . . . 20 2 β‰  0
174173a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 2 β‰  0)
175169, 170, 172, 174divne0d 12028 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) β‰  0)
176164, 167, 175redivcld 12064 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ)
177176flcld 13787 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) ∈ β„€)
178177peano2zd 12691 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ β„€)
179178, 140ifcld 4570 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀) ∈ β„€)
180144, 179eqeltrid 2832 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ β„€)
181180zred 12688 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ ℝ)
182181adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑁 ∈ ℝ)
183178zred 12688 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ)
184 max1 13188 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
185141, 183, 184syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
186185, 144breqtrrdi 5184 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ≀ 𝑁)
187186adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑀 ≀ 𝑁)
188 eluzle 12857 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘) β†’ 𝑁 ≀ 𝑗)
189188adantl 481 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑁 ≀ 𝑗)
190142, 182, 136, 187, 189letrd 11393 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑀 ≀ 𝑗)
191137, 142, 136, 143, 190ltletrd 11396 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 < 𝑗)
192191gt0ne0d 11800 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑗 β‰  0)
193136, 192rereccld 12063 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ (1 / 𝑗) ∈ ℝ)
194136, 191recgt0d 12170 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 < (1 / 𝑗))
195193, 194elrpd 13037 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ (1 / 𝑗) ∈ ℝ+)
196195adantr 480 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ (1 / 𝑗) ∈ ℝ+)
197 ioodvbdlimc2lem.ch . . . . . . . . 9 (πœ’ ↔ (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)))
198197biimpi 215 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)))
199 simp-5l 784 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ πœ‘)
200198, 199syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ πœ‘)
201200, 26syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
202198simplrd 769 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑧 ∈ (𝐴(,)𝐡))
203201, 202ffvelcdmd 7089 . . . . . . . . . . . . . 14 (πœ’ β†’ (πΉβ€˜π‘§) ∈ ℝ)
204203recnd 11264 . . . . . . . . . . . . 13 (πœ’ β†’ (πΉβ€˜π‘§) ∈ β„‚)
205200, 106syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑆:(β„€β‰₯β€˜π‘€)βŸΆβ„)
206 simp-5r 785 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ π‘₯ ∈ ℝ+)
207198, 206syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ π‘₯ ∈ ℝ+)
208 eluz2 12850 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (β„€β‰₯β€˜π‘€) ↔ (𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 𝑀 ≀ 𝑁))
209140, 180, 186, 208syl3anbrc 1341 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))
210200, 207, 209syl2anc 583 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))
211 uzss 12867 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (β„€β‰₯β€˜π‘€) β†’ (β„€β‰₯β€˜π‘) βŠ† (β„€β‰₯β€˜π‘€))
212210, 211syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (β„€β‰₯β€˜π‘) βŠ† (β„€β‰₯β€˜π‘€))
213 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘))
214198, 213syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘))
215212, 214sseldd 3979 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘€))
216205, 215ffvelcdmd 7089 . . . . . . . . . . . . . 14 (πœ’ β†’ (π‘†β€˜π‘—) ∈ ℝ)
217216recnd 11264 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘†β€˜π‘—) ∈ β„‚)
218200, 134syl 17 . . . . . . . . . . . . 13 (πœ’ β†’ (lim supβ€˜π‘†) ∈ β„‚)
219204, 217, 218npncand 11617 . . . . . . . . . . . 12 (πœ’ β†’ (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) = ((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†)))
220219eqcomd 2733 . . . . . . . . . . 11 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†)) = (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))))
221220fveq2d 6895 . . . . . . . . . 10 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) = (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))))
222203, 216resubcld 11664 . . . . . . . . . . . . . 14 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) ∈ ℝ)
223200, 133syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ (lim supβ€˜π‘†) ∈ ℝ)
224216, 223resubcld 11664 . . . . . . . . . . . . . 14 (πœ’ β†’ ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)) ∈ ℝ)
225222, 224readdcld 11265 . . . . . . . . . . . . 13 (πœ’ β†’ (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) ∈ ℝ)
226225recnd 11264 . . . . . . . . . . . 12 (πœ’ β†’ (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) ∈ β„‚)
227226abscld 15407 . . . . . . . . . . 11 (πœ’ β†’ (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) ∈ ℝ)
228222recnd 11264 . . . . . . . . . . . . 13 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) ∈ β„‚)
229228abscld 15407 . . . . . . . . . . . 12 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) ∈ ℝ)
230224recnd 11264 . . . . . . . . . . . . 13 (πœ’ β†’ ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)) ∈ β„‚)
231230abscld 15407 . . . . . . . . . . . 12 (πœ’ β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) ∈ ℝ)
232229, 231readdcld 11265 . . . . . . . . . . 11 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) ∈ ℝ)
233207rpred 13040 . . . . . . . . . . 11 (πœ’ β†’ π‘₯ ∈ ℝ)
234228, 230abstrid 15427 . . . . . . . . . . 11 (πœ’ β†’ (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) ≀ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))))
235233rehalfcld 12481 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘₯ / 2) ∈ ℝ)
236200, 215, 113syl2anc 583 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘†β€˜π‘—) = (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))
237236oveq2d 7430 . . . . . . . . . . . . . . 15 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) = ((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))))
238237fveq2d 6895 . . . . . . . . . . . . . 14 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) = (absβ€˜((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))))
239238, 229eqeltrrd 2829 . . . . . . . . . . . . . . 15 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))) ∈ ℝ)
240200, 163syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ π‘Œ ∈ ℝ)
241150, 202sselid 3976 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝑧 ∈ ℝ)
242200, 215, 58syl2anc 583 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝐡 βˆ’ (1 / 𝑗)) ∈ ℝ)
243241, 242resubcld 11664 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗))) ∈ ℝ)
244240, 243remulcld 11266 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘Œ Β· (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗)))) ∈ ℝ)
245200, 7syl 17 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝐴 ∈ ℝ)
246200, 6syl 17 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝐡 ∈ ℝ)
247200, 107syl 17 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
248161simprd 495 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ))
249145breq2i 5150 . . . . . . . . . . . . . . . . . . . . 21 ((absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ ↔ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ))
250249ralbii 3088 . . . . . . . . . . . . . . . . . . . 20 (βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ ↔ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ))
251248, 250sylibr 233 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ)
252200, 251syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ)
253 2fveq3 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = π‘₯ β†’ (absβ€˜((ℝ D 𝐹)β€˜π‘€)) = (absβ€˜((ℝ D 𝐹)β€˜π‘₯)))
254253breq1d 5152 . . . . . . . . . . . . . . . . . . 19 (𝑀 = π‘₯ β†’ ((absβ€˜((ℝ D 𝐹)β€˜π‘€)) ≀ π‘Œ ↔ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ))
255254cbvralvw 3229 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘€ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘€)) ≀ π‘Œ ↔ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ)
256252, 255sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ βˆ€π‘€ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘€)) ≀ π‘Œ)
257200, 215, 103syl2anc 583 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝐡 βˆ’ (1 / 𝑗)) ∈ (𝐴(,)𝐡))
258242rexrd 11286 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (𝐡 βˆ’ (1 / 𝑗)) ∈ ℝ*)
259200, 30syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 𝐡 ∈ ℝ*)
2603, 215sselid 3976 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ 𝑗 ∈ ℝ)
261200, 215, 56syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ 𝑗 β‰  0)
262260, 261rereccld 12063 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ (1 / 𝑗) ∈ ℝ)
263246, 241resubcld 11664 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (𝐡 βˆ’ 𝑧) ∈ ℝ)
264241, 246resubcld 11664 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ (𝑧 βˆ’ 𝐡) ∈ ℝ)
265264recnd 11264 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (𝑧 βˆ’ 𝐡) ∈ β„‚)
266265abscld 15407 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (absβ€˜(𝑧 βˆ’ 𝐡)) ∈ ℝ)
267263leabsd 15385 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (𝐡 βˆ’ 𝑧) ≀ (absβ€˜(𝐡 βˆ’ 𝑧)))
268200, 85syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝐡 ∈ β„‚)
269241recnd 11264 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑧 ∈ β„‚)
270268, 269abssubd 15424 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (absβ€˜(𝐡 βˆ’ 𝑧)) = (absβ€˜(𝑧 βˆ’ 𝐡)))
271267, 270breqtrd 5168 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (𝐡 βˆ’ 𝑧) ≀ (absβ€˜(𝑧 βˆ’ 𝐡)))
272198simprd 495 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗))
273263, 266, 262, 271, 272lelttrd 11394 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ (𝐡 βˆ’ 𝑧) < (1 / 𝑗))
274246, 241, 262, 273ltsub23d 11841 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (𝐡 βˆ’ (1 / 𝑗)) < 𝑧)
275200, 28syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ 𝐴 ∈ ℝ*)
276 iooltub 44818 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ 𝑧 < 𝐡)
277275, 259, 202, 276syl3anc 1369 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 𝑧 < 𝐡)
278258, 259, 241, 274, 277eliood 44806 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝑧 ∈ ((𝐡 βˆ’ (1 / 𝑗))(,)𝐡))
279245, 246, 201, 247, 240, 256, 257, 278dvbdfbdioolem1 45239 . . . . . . . . . . . . . . . 16 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))) ≀ (π‘Œ Β· (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗)))) ∧ (absβ€˜((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))) ≀ (π‘Œ Β· (𝐡 βˆ’ 𝐴))))
280279simpld 494 . . . . . . . . . . . . . . 15 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))) ≀ (π‘Œ Β· (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗)))))
281200, 215, 57syl2anc 583 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (1 / 𝑗) ∈ ℝ)
282240, 281remulcld 11266 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘Œ Β· (1 / 𝑗)) ∈ ℝ)
283155, 147ffvelcdmd 7089 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2)) ∈ ℝ)
284283recnd 11264 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2)) ∈ β„‚)
285284abscld 15407 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ∈ ℝ)
286284absge0d 15415 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 0 ≀ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))))
287 2fveq3 6896 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ((𝐴 + 𝐡) / 2) β†’ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) = (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))))
288145eqcomi 2736 . . . . . . . . . . . . . . . . . . . . . . 23 sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) = π‘Œ
289288a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ((𝐴 + 𝐡) / 2) β†’ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) = π‘Œ)
290287, 289breq12d 5155 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = ((𝐴 + 𝐡) / 2) β†’ ((absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) ↔ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ≀ π‘Œ))
291290rspcva 3605 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡) ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )) β†’ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ≀ π‘Œ)
292147, 248, 291syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ≀ π‘Œ)
29314, 285, 163, 286, 292letrd 11393 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 0 ≀ π‘Œ)
294200, 293syl 17 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 0 ≀ π‘Œ)
295281recnd 11264 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (1 / 𝑗) ∈ β„‚)
296 sub31 44595 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ β„‚ ∧ 𝐡 ∈ β„‚ ∧ (1 / 𝑗) ∈ β„‚) β†’ (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗))) = ((1 / 𝑗) βˆ’ (𝐡 βˆ’ 𝑧)))
297269, 268, 295, 296syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗))) = ((1 / 𝑗) βˆ’ (𝐡 βˆ’ 𝑧)))
298241, 246posdifd 11823 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ (𝑧 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝑧)))
299277, 298mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ 0 < (𝐡 βˆ’ 𝑧))
300263, 299elrpd 13037 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (𝐡 βˆ’ 𝑧) ∈ ℝ+)
301281, 300ltsubrpd 13072 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ ((1 / 𝑗) βˆ’ (𝐡 βˆ’ 𝑧)) < (1 / 𝑗))
302297, 301eqbrtrd 5164 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗))) < (1 / 𝑗))
303243, 281, 302ltled 11384 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗))) ≀ (1 / 𝑗))
304243, 281, 240, 294, 303lemul2ad 12176 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘Œ Β· (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗)))) ≀ (π‘Œ Β· (1 / 𝑗)))
305282adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) ∈ ℝ)
306235adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘₯ / 2) ∈ ℝ)
307 oveq1 7421 . . . . . . . . . . . . . . . . . . . 20 (π‘Œ = 0 β†’ (π‘Œ Β· (1 / 𝑗)) = (0 Β· (1 / 𝑗)))
308295mul02d 11434 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (0 Β· (1 / 𝑗)) = 0)
309307, 308sylan9eqr 2789 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) = 0)
310207rphalfcld 13052 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (π‘₯ / 2) ∈ ℝ+)
311310rpgt0d 13043 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ 0 < (π‘₯ / 2))
312311adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ π‘Œ = 0) β†’ 0 < (π‘₯ / 2))
313309, 312eqbrtrd 5164 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) < (π‘₯ / 2))
314305, 306, 313ltled 11384 . . . . . . . . . . . . . . . . 17 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
315240adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ π‘Œ ∈ ℝ)
316294adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ 0 ≀ π‘Œ)
317 neqne 2943 . . . . . . . . . . . . . . . . . . . 20 (Β¬ π‘Œ = 0 β†’ π‘Œ β‰  0)
318317adantl 481 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ π‘Œ β‰  0)
319315, 316, 318ne0gt0d 11373 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ 0 < π‘Œ)
320282adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑗)) ∈ ℝ)
3213, 210sselid 3976 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑁 ∈ ℝ)
322 0red 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ 0 ∈ ℝ)
323200, 207, 141syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ 𝑀 ∈ ℝ)
324200, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ 0 < 𝑀)
325200, 207, 186syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ 𝑀 ≀ 𝑁)
326322, 323, 321, 324, 325ltletrd 11396 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 0 < 𝑁)
327326gt0ne0d 11800 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑁 β‰  0)
328321, 327rereccld 12063 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (1 / 𝑁) ∈ ℝ)
329240, 328remulcld 11266 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (π‘Œ Β· (1 / 𝑁)) ∈ ℝ)
330329adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑁)) ∈ ℝ)
331235adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘₯ / 2) ∈ ℝ)
332281adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑗) ∈ ℝ)
333328adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑁) ∈ ℝ)
334240adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ π‘Œ ∈ ℝ)
335294adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 ≀ π‘Œ)
336321, 326elrpd 13037 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑁 ∈ ℝ+)
337200, 215, 94syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑗 ∈ ℝ+)
338 1red 11237 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 1 ∈ ℝ)
33996a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 0 ≀ 1)
340214, 188syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑁 ≀ 𝑗)
341336, 337, 338, 339, 340lediv2ad 13062 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (1 / 𝑗) ≀ (1 / 𝑁))
342341adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑗) ≀ (1 / 𝑁))
343332, 333, 334, 335, 342lemul2ad 12176 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘Œ Β· (1 / 𝑁)))
344233recnd 11264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ π‘₯ ∈ β„‚)
345 2cnd 12312 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ 2 ∈ β„‚)
346207rpne0d 13045 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ π‘₯ β‰  0)
347173a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ 2 β‰  0)
348344, 345, 346, 347divne0d 12028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ (π‘₯ / 2) β‰  0)
349240, 235, 348redivcld 12064 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ)
350349adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ)
351 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 < π‘Œ)
352311adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 < (π‘₯ / 2))
353334, 331, 351, 352divgt0d 12171 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 < (π‘Œ / (π‘₯ / 2)))
354350, 353elrpd 13037 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ+)
355354rprecred 13051 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / (π‘Œ / (π‘₯ / 2))) ∈ ℝ)
356336adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ 𝑁 ∈ ℝ+)
357 1red 11237 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ 1 ∈ ℝ)
35896a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 ≀ 1)
359349flcld 13787 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ (βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) ∈ β„€)
360359peano2zd 12691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ β„€)
361360zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ)
362200, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ’ β†’ 𝑀 ∈ β„€)
363360, 362ifcld 4570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀) ∈ β„€)
364144, 363eqeltrid 2832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ 𝑁 ∈ β„€)
365364zred 12688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ 𝑁 ∈ ℝ)
366 flltp1 13789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Œ / (π‘₯ / 2)) ∈ ℝ β†’ (π‘Œ / (π‘₯ / 2)) < ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1))
367349, 366syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) < ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1))
368200, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ 𝑀 ∈ ℝ)
369 max2 13190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ ℝ ∧ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ) β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
370368, 361, 369syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
371370, 144breqtrrdi 5184 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ≀ 𝑁)
372349, 361, 365, 367, 371ltletrd 11396 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) < 𝑁)
373349, 321, 372ltled 11384 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) ≀ 𝑁)
374373adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ≀ 𝑁)
375354, 356, 357, 358, 374lediv2ad 13062 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑁) ≀ (1 / (π‘Œ / (π‘₯ / 2))))
376333, 355, 334, 335, 375lemul2ad 12176 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑁)) ≀ (π‘Œ Β· (1 / (π‘Œ / (π‘₯ / 2)))))
377334recnd 11264 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ π‘Œ ∈ β„‚)
378350recnd 11264 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ∈ β„‚)
379353gt0ne0d 11800 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) β‰  0)
380377, 378, 379divrecd 12015 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘Œ / (π‘₯ / 2))) = (π‘Œ Β· (1 / (π‘Œ / (π‘₯ / 2)))))
381331recnd 11264 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘₯ / 2) ∈ β„‚)
382351gt0ne0d 11800 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ π‘Œ β‰  0)
383348adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘₯ / 2) β‰  0)
384377, 381, 382, 383ddcand 12032 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘Œ / (π‘₯ / 2))) = (π‘₯ / 2))
385380, 384eqtr3d 2769 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / (π‘Œ / (π‘₯ / 2)))) = (π‘₯ / 2))
386376, 385breqtrd 5168 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑁)) ≀ (π‘₯ / 2))
387320, 330, 331, 343, 386letrd 11393 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
388319, 387syldan 590 . . . . . . . . . . . . . . . . 17 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
389314, 388pm2.61dan 812 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
390244, 282, 235, 304, 389letrd 11393 . . . . . . . . . . . . . . 15 (πœ’ β†’ (π‘Œ Β· (𝑧 βˆ’ (𝐡 βˆ’ (1 / 𝑗)))) ≀ (π‘₯ / 2))
391239, 244, 235, 280, 390letrd 11393 . . . . . . . . . . . . . 14 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))))) ≀ (π‘₯ / 2))
392238, 391eqbrtrd 5164 . . . . . . . . . . . . 13 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) ≀ (π‘₯ / 2))
393 simpllr 775 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
394198, 393syl 17 . . . . . . . . . . . . 13 (πœ’ β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
395229, 231, 235, 235, 392, 394leltaddd 11858 . . . . . . . . . . . 12 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) < ((π‘₯ / 2) + (π‘₯ / 2)))
3963442halvesd 12480 . . . . . . . . . . . 12 (πœ’ β†’ ((π‘₯ / 2) + (π‘₯ / 2)) = π‘₯)
397395, 396breqtrd 5168 . . . . . . . . . . 11 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) < π‘₯)
398227, 232, 233, 234, 397lelttrd 11394 . . . . . . . . . 10 (πœ’ β†’ (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) < π‘₯)
399221, 398eqbrtrd 5164 . . . . . . . . 9 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)
400197, 399sylbir 234 . . . . . . . 8 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)
401400adantrl 715 . . . . . . 7 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗))) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)
402401ex 412 . . . . . 6 (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ ((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
403402ralrimiva 3141 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
404 brimralrspcev 5203 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
405196, 403, 404syl2anc 583 . . . 4 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
406 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ 𝑏 ≀ 𝑁)
407406iftrued 4532 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) = 𝑁)
408 uzid 12859 . . . . . . . . . . . 12 (𝑁 ∈ β„€ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘))
409180, 408syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘))
410409adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘))
411407, 410eqeltrd 2828 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
412411adantlr 714 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
413 iffalse 4533 . . . . . . . . . 10 (Β¬ 𝑏 ≀ 𝑁 β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) = 𝑏)
414413adantl 481 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) = 𝑏)
415180ad2antrr 725 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 ∈ β„€)
416 simplr 768 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑏 ∈ β„€)
417415zred 12688 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 ∈ ℝ)
418416zred 12688 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑏 ∈ ℝ)
419 simpr 484 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ Β¬ 𝑏 ≀ 𝑁)
420417, 418ltnled 11383 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ (𝑁 < 𝑏 ↔ Β¬ 𝑏 ≀ 𝑁))
421419, 420mpbird 257 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 < 𝑏)
422417, 418, 421ltled 11384 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 ≀ 𝑏)
423 eluz2 12850 . . . . . . . . . 10 (𝑏 ∈ (β„€β‰₯β€˜π‘) ↔ (𝑁 ∈ β„€ ∧ 𝑏 ∈ β„€ ∧ 𝑁 ≀ 𝑏))
424415, 416, 422, 423syl3anbrc 1341 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑏 ∈ (β„€β‰₯β€˜π‘))
425414, 424eqeltrd 2828 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
426412, 425pm2.61dan 812 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
427426adantr 480 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
428 simpr 484 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
429 simpr 484 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑏 ∈ β„€)
430180adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑁 ∈ β„€)
431430, 429ifcld 4570 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ β„€)
432429zred 12688 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑏 ∈ ℝ)
433430zred 12688 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑁 ∈ ℝ)
434 max1 13188 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ 𝑏 ≀ if(𝑏 ≀ 𝑁, 𝑁, 𝑏))
435432, 433, 434syl2anc 583 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑏 ≀ if(𝑏 ≀ 𝑁, 𝑁, 𝑏))
436 eluz2 12850 . . . . . . . . . 10 (if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘) ↔ (𝑏 ∈ β„€ ∧ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ β„€ ∧ 𝑏 ≀ if(𝑏 ≀ 𝑁, 𝑁, 𝑏)))
437429, 431, 435, 436syl3anbrc 1341 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
438437adantr 480 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
439 fveq2 6891 . . . . . . . . . . 11 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (π‘†β€˜π‘) = (π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)))
440439eleq1d 2813 . . . . . . . . . 10 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ ((π‘†β€˜π‘) ∈ β„‚ ↔ (π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚))
441439fvoveq1d 7436 . . . . . . . . . . 11 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) = (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))))
442441breq1d 5152 . . . . . . . . . 10 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ ((absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2) ↔ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
443440, 442anbi12d 630 . . . . . . . . 9 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ↔ ((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))))
444443rspccva 3606 . . . . . . . 8 ((βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘)) β†’ ((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
445428, 438, 444syl2anc 583 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ ((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
446445simprd 495 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
447 fveq2 6891 . . . . . . . . 9 (𝑗 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (π‘†β€˜π‘—) = (π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)))
448447fvoveq1d 7436 . . . . . . . 8 (𝑗 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) = (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))))
449448breq1d 5152 . . . . . . 7 (𝑗 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ ((absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2) ↔ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
450449rspcev 3607 . . . . . 6 ((if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘) ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘)(absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
451427, 446, 450syl2anc 583 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘)(absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
452 ax-resscn 11187 . . . . . . . . . . . . . 14 ℝ βŠ† β„‚
453452a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ℝ βŠ† β„‚)
45426, 453fssd 6734 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„‚)
455 dvcn 25838 . . . . . . . . . . . . . 14 (((ℝ βŠ† β„‚ ∧ 𝐹:(𝐴(,)𝐡)βŸΆβ„‚ ∧ (𝐴(,)𝐡) βŠ† ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐡)) β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
456453, 454, 151, 107, 455syl31anc 1371 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
457 cncfcdm 24805 . . . . . . . . . . . . 13 ((ℝ βŠ† β„‚ ∧ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚)) β†’ (𝐹 ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐡)βŸΆβ„))
458453, 456, 457syl2anc 583 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐡)βŸΆβ„))
45926, 458mpbird 257 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cn→ℝ))
460 ioodvbdlimc2lem.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (𝐡 βˆ’ (1 / 𝑗)))
461103, 460fmptd 7118 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅:(β„€β‰₯β€˜π‘€)⟢(𝐴(,)𝐡))
462 eqid 2727 . . . . . . . . . . 11 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—)))
463 climrel 15460 . . . . . . . . . . . . 13 Rel ⇝
464463a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ Rel ⇝ )
465 fvex 6904 . . . . . . . . . . . . . . . . 17 (β„€β‰₯β€˜π‘€) ∈ V
466465mptex 7229 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡) ∈ V
467466a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡) ∈ V)
468 eqidd 2728 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡))
469 eqidd 2728 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) ∧ 𝑗 = π‘š) β†’ 𝐡 = 𝐡)
470 simpr 484 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ π‘š ∈ (β„€β‰₯β€˜π‘€))
4716adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐡 ∈ ℝ)
472468, 469, 470, 471fvmptd 7006 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡)β€˜π‘š) = 𝐡)
47323, 22, 467, 85, 472climconst 15511 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡) ⇝ 𝐡)
474465mptex 7229 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (𝐡 βˆ’ (1 / 𝑗))) ∈ V
475460, 474eqeltri 2824 . . . . . . . . . . . . . . 15 𝑅 ∈ V
476475a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 ∈ V)
477 1cnd 11231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ β„‚)
478 elnnnn0b 12538 . . . . . . . . . . . . . . . 16 (𝑀 ∈ β„• ↔ (𝑀 ∈ β„•0 ∧ 0 < 𝑀))
47921, 65, 478sylanbrc 582 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑀 ∈ β„•)
480 divcnvg 44938 . . . . . . . . . . . . . . 15 ((1 ∈ β„‚ ∧ 𝑀 ∈ β„•) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)) ⇝ 0)
481477, 479, 480syl2anc 583 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)) ⇝ 0)
482 eqidd 2728 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡))
483 eqidd 2728 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) ∧ 𝑗 = 𝑖) β†’ 𝐡 = 𝐡)
484 simpr 484 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
4856adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐡 ∈ ℝ)
486482, 483, 484, 485fvmptd 7006 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡)β€˜π‘–) = 𝐡)
487486, 485eqeltrd 2828 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡)β€˜π‘–) ∈ ℝ)
488487recnd 11264 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡)β€˜π‘–) ∈ β„‚)
489 eqidd 2728 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)))
490 oveq2 7422 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 β†’ (1 / 𝑗) = (1 / 𝑖))
491490adantl 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) ∧ 𝑗 = 𝑖) β†’ (1 / 𝑗) = (1 / 𝑖))
4923, 484sselid 3976 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ ℝ)
493 0red 11239 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 ∈ ℝ)
49460adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ)
49565adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < 𝑀)
496 eluzle 12857 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝑖)
497496adantl 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ≀ 𝑖)
498493, 494, 492, 495, 497ltletrd 11396 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < 𝑖)
499498gt0ne0d 11800 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 β‰  0)
500492, 499rereccld 12063 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑖) ∈ ℝ)
501489, 491, 484, 500fvmptd 7006 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–) = (1 / 𝑖))
502492recnd 11264 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ β„‚)
503502, 499reccld 12005 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑖) ∈ β„‚)
504501, 503eqeltrd 2828 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–) ∈ β„‚)
505490oveq2d 7430 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 β†’ (𝐡 βˆ’ (1 / 𝑗)) = (𝐡 βˆ’ (1 / 𝑖)))
506 ovex 7447 . . . . . . . . . . . . . . . . 17 (𝐡 βˆ’ (1 / 𝑖)) ∈ V
507505, 460, 506fvmpt 6999 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ (π‘…β€˜π‘–) = (𝐡 βˆ’ (1 / 𝑖)))
508507adantl 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘…β€˜π‘–) = (𝐡 βˆ’ (1 / 𝑖)))
509486, 501oveq12d 7432 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡)β€˜π‘–) βˆ’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–)) = (𝐡 βˆ’ (1 / 𝑖)))
510508, 509eqtr4d 2770 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘…β€˜π‘–) = (((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐡)β€˜π‘–) βˆ’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–)))
51123, 22, 473, 476, 481, 488, 504, 510climsub 15602 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 ⇝ (𝐡 βˆ’ 0))
51285subid1d 11582 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βˆ’ 0) = 𝐡)
513511, 512breqtrd 5168 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 ⇝ 𝐡)
514 releldm 5940 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅 ⇝ 𝐡) β†’ 𝑅 ∈ dom ⇝ )
515464, 513, 514syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅 ∈ dom ⇝ )
516 fveq2 6891 . . . . . . . . . . . . . . 15 (𝑙 = π‘˜ β†’ (β„€β‰₯β€˜π‘™) = (β„€β‰₯β€˜π‘˜))
517 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (𝑙 = π‘˜ β†’ (π‘…β€˜π‘™) = (π‘…β€˜π‘˜))
518517oveq2d 7430 . . . . . . . . . . . . . . . . 17 (𝑙 = π‘˜ β†’ ((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™)) = ((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜)))
519518fveq2d 6895 . . . . . . . . . . . . . . . 16 (𝑙 = π‘˜ β†’ (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) = (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))))
520519breq1d 5152 . . . . . . . . . . . . . . 15 (𝑙 = π‘˜ β†’ ((absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))))
521516, 520raleqbidv 3337 . . . . . . . . . . . . . 14 (𝑙 = π‘˜ β†’ (βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))))
522521cbvrabv 3437 . . . . . . . . . . . . 13 {𝑙 ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}
523 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (β„Ž = 𝑖 β†’ (π‘…β€˜β„Ž) = (π‘…β€˜π‘–))
524523fvoveq1d 7436 . . . . . . . . . . . . . . . . 17 (β„Ž = 𝑖 β†’ (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) = (absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))))
525524breq1d 5152 . . . . . . . . . . . . . . . 16 (β„Ž = 𝑖 β†’ ((absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ (absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))))
526525cbvralvw 3229 . . . . . . . . . . . . . . 15 (βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)))
527526rgenw 3060 . . . . . . . . . . . . . 14 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘€)(βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)))
528 rabbi 3457 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘€)(βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))) ↔ {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))})
529527, 528mpbi 229 . . . . . . . . . . . . 13 {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}
530522, 529eqtri 2755 . . . . . . . . . . . 12 {𝑙 ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}
531530infeq1i 9493 . . . . . . . . . . 11 inf({𝑙 ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}, ℝ, < ) = inf({π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}, ℝ, < )
5327, 6, 9, 459, 107, 108, 22, 461, 462, 515, 531ioodvbdlimc1lem1 45242 . . . . . . . . . 10 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))) ⇝ (lim supβ€˜(𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—)))))
533460fvmpt2 7010 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ∧ (𝐡 βˆ’ (1 / 𝑗)) ∈ ℝ) β†’ (π‘…β€˜π‘—) = (𝐡 βˆ’ (1 / 𝑗)))
534111, 58, 533syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘…β€˜π‘—) = (𝐡 βˆ’ (1 / 𝑗)))
535534eqcomd 2733 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐡 βˆ’ (1 / 𝑗)) = (π‘…β€˜π‘—))
536535fveq2d 6895 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗))) = (πΉβ€˜(π‘…β€˜π‘—)))
537536mpteq2dva 5242 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))))
538105, 537eqtrid 2779 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))))
539538fveq2d 6895 . . . . . . . . . 10 (πœ‘ β†’ (lim supβ€˜π‘†) = (lim supβ€˜(𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—)))))
540532, 538, 5393brtr4d 5174 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ⇝ (lim supβ€˜π‘†))
541465mptex 7229 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐡 βˆ’ (1 / 𝑗)))) ∈ V
542105, 541eqeltri 2824 . . . . . . . . . . 11 𝑆 ∈ V
543542a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ V)
544 eqidd 2728 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ β„€) β†’ (π‘†β€˜π‘) = (π‘†β€˜π‘))
545543, 544clim 15462 . . . . . . . . 9 (πœ‘ β†’ (𝑆 ⇝ (lim supβ€˜π‘†) ↔ ((lim supβ€˜π‘†) ∈ β„‚ ∧ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž))))
546540, 545mpbid 231 . . . . . . . 8 (πœ‘ β†’ ((lim supβ€˜π‘†) ∈ β„‚ ∧ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž)))
547546simprd 495 . . . . . . 7 (πœ‘ β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž))
548547adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž))
549 simpr 484 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ ℝ+)
550549rphalfcld 13052 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) ∈ ℝ+)
551 breq2 5146 . . . . . . . . 9 (π‘Ž = (π‘₯ / 2) β†’ ((absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž ↔ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
552551anbi2d 628 . . . . . . . 8 (π‘Ž = (π‘₯ / 2) β†’ (((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž) ↔ ((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))))
553552rexralbidv 3215 . . . . . . 7 (π‘Ž = (π‘₯ / 2) β†’ (βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž) ↔ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))))
554553rspccva 3606 . . . . . 6 ((βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž) ∧ (π‘₯ / 2) ∈ ℝ+) β†’ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
555548, 550, 554syl2anc 583 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
556451, 555r19.29a 3157 . . . 4 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘)(absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
557405, 556r19.29a 3157 . . 3 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
558557ralrimiva 3141 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
559 ioosscn 13410 . . . 4 (𝐴(,)𝐡) βŠ† β„‚
560559a1i 11 . . 3 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
561454, 560, 85ellimc3 25795 . 2 (πœ‘ β†’ ((lim supβ€˜π‘†) ∈ (𝐹 limβ„‚ 𝐡) ↔ ((lim supβ€˜π‘†) ∈ β„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐡 ∧ (absβ€˜(𝑧 βˆ’ 𝐡)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))))
562134, 558, 561mpbir2and 712 1 (πœ‘ β†’ (lim supβ€˜π‘†) ∈ (𝐹 limβ„‚ 𝐡))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427  Vcvv 3469   βŠ† wss 3944  βˆ…c0 4318  ifcif 4524   class class class wbr 5142   ↦ cmpt 5225  dom cdm 5672  ran crn 5673  Rel wrel 5677  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  supcsup 9455  infcinf 9456  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135  +∞cpnf 11267  β„*cxr 11269   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466   / cdiv 11893  β„•cn 12234  2c2 12289  β„•0cn0 12494  β„€cz 12580  β„€β‰₯cuz 12844  β„+crp 12998  (,)cioo 13348  βŒŠcfl 13779  abscabs 15205  lim supclsp 15438   ⇝ cli 15452  β€“cnβ†’ccncf 24783   limβ„‚ climc 25778   D cdv 25779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783
This theorem is referenced by:  ioodvbdlimc2  45246
  Copyright terms: Public domain W3C validator