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 44247
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 12791 . . . . . 6 (β„€β‰₯β€˜π‘€) βŠ† β„€
2 zssre 12513 . . . . . 6 β„€ βŠ† ℝ
31, 2sstri 3958 . . . . 5 (β„€β‰₯β€˜π‘€) βŠ† ℝ
43a1i 11 . . . 4 (πœ‘ β†’ (β„€β‰₯β€˜π‘€) βŠ† ℝ)
5 ioodvbdlimc1lem2.m . . . . . . 7 𝑀 = ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)
6 ioodvbdlimc1lem2.b . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ ℝ)
7 ioodvbdlimc1lem2.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
86, 7resubcld 11590 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
9 ioodvbdlimc1lem2.altb . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
107, 6posdifd 11749 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
119, 10mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
1211gt0ne0d 11726 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
138, 12rereccld 11989 . . . . . . . . 9 (πœ‘ β†’ (1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ)
14 0red 11165 . . . . . . . . . 10 (πœ‘ β†’ 0 ∈ ℝ)
158, 11recgt0d 12096 . . . . . . . . . 10 (πœ‘ β†’ 0 < (1 / (𝐡 βˆ’ 𝐴)))
1614, 13, 15ltled 11310 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (1 / (𝐡 βˆ’ 𝐴)))
17 flge0nn0 13732 . . . . . . . . 9 (((1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ ∧ 0 ≀ (1 / (𝐡 βˆ’ 𝐴))) β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„•0)
1813, 16, 17syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„•0)
19 peano2nn0 12460 . . . . . . . 8 ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„•0 β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ β„•0)
2018, 19syl 17 . . . . . . 7 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ β„•0)
215, 20eqeltrid 2842 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•0)
2221nn0zd 12532 . . . . 5 (πœ‘ β†’ 𝑀 ∈ β„€)
23 eqid 2737 . . . . . 6 (β„€β‰₯β€˜π‘€) = (β„€β‰₯β€˜π‘€)
2423uzsup 13775 . . . . 5 (𝑀 ∈ β„€ β†’ sup((β„€β‰₯β€˜π‘€), ℝ*, < ) = +∞)
2522, 24syl 17 . . . 4 (πœ‘ β†’ sup((β„€β‰₯β€˜π‘€), ℝ*, < ) = +∞)
26 ioodvbdlimc1lem2.f . . . . . . 7 (πœ‘ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
2726adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
287rexrd 11212 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ ℝ*)
2928adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ ℝ*)
306rexrd 11212 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ ℝ*)
3130adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐡 ∈ ℝ*)
327adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ ℝ)
33 eluzelre 12781 . . . . . . . . . 10 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑗 ∈ ℝ)
3433adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 ∈ ℝ)
35 0red 11165 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 ∈ ℝ)
36 0red 11165 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 0 ∈ ℝ)
37 1red 11163 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 1 ∈ ℝ)
3836, 37readdcld 11191 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ (0 + 1) ∈ ℝ)
3938adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (0 + 1) ∈ ℝ)
4036ltp1d 12092 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 0 < (0 + 1))
4140adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < (0 + 1))
42 eluzel2 12775 . . . . . . . . . . . . . 14 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ∈ β„€)
4342zred 12614 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ∈ ℝ)
4443adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ)
4513flcld 13710 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ β„€)
4645zred 12614 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
47 1red 11163 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ ℝ)
4818nn0ge0d 12483 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 0 ≀ (βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))))
4914, 46, 47, 48leadd1dd 11776 . . . . . . . . . . . . . 14 (πœ‘ β†’ (0 + 1) ≀ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
5049, 5breqtrrdi 5152 . . . . . . . . . . . . 13 (πœ‘ β†’ (0 + 1) ≀ 𝑀)
5150adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (0 + 1) ≀ 𝑀)
52 eluzle 12783 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝑗)
5352adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ≀ 𝑗)
5439, 44, 34, 51, 53letrd 11319 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (0 + 1) ≀ 𝑗)
5535, 39, 34, 41, 54ltletrd 11322 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < 𝑗)
5655gt0ne0d 11726 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 β‰  0)
5734, 56rereccld 11989 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑗) ∈ ℝ)
5832, 57readdcld 11191 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑗)) ∈ ℝ)
5934, 55elrpd 12961 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 ∈ ℝ+)
6059rpreccld 12974 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑗) ∈ ℝ+)
6132, 60ltaddrpd 12997 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 < (𝐴 + (1 / 𝑗)))
6221nn0red 12481 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ ℝ)
6314, 47readdcld 11191 . . . . . . . . . . . . . 14 (πœ‘ β†’ (0 + 1) ∈ ℝ)
6446, 47readdcld 11191 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ ℝ)
6514ltp1d 12092 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < (0 + 1))
6614, 63, 64, 65, 49ltletrd 11322 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
6766, 5breqtrrdi 5152 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 𝑀)
6867gt0ne0d 11726 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 β‰  0)
6962, 68rereccld 11989 . . . . . . . . . 10 (πœ‘ β†’ (1 / 𝑀) ∈ ℝ)
7069adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑀) ∈ ℝ)
7132, 70readdcld 11191 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑀)) ∈ ℝ)
726adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐡 ∈ ℝ)
7362, 67elrpd 12961 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ ℝ+)
7473adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ+)
75 1red 11163 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 1 ∈ ℝ)
76 0le1 11685 . . . . . . . . . . 11 0 ≀ 1
7776a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 ≀ 1)
7874, 59, 75, 77, 53lediv2ad 12986 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑗) ≀ (1 / 𝑀))
7957, 70, 32, 78leadd2dd 11777 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑗)) ≀ (𝐴 + (1 / 𝑀)))
805eqcomi 2746 . . . . . . . . . . . . 13 ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) = 𝑀
8180oveq2i 7373 . . . . . . . . . . . 12 (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) = (1 / 𝑀)
8281, 69eqeltrid 2842 . . . . . . . . . . 11 (πœ‘ β†’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) ∈ ℝ)
8313, 15elrpd 12961 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ+)
8464, 66elrpd 12961 . . . . . . . . . . . . 13 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ ℝ+)
85 1rp 12926 . . . . . . . . . . . . . 14 1 ∈ ℝ+
8685a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 ∈ ℝ+)
87 fllelt 13709 . . . . . . . . . . . . . . 15 ((1 / (𝐡 βˆ’ 𝐴)) ∈ ℝ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ≀ (1 / (𝐡 βˆ’ 𝐴)) ∧ (1 / (𝐡 βˆ’ 𝐴)) < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)))
8813, 87syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) ≀ (1 / (𝐡 βˆ’ 𝐴)) ∧ (1 / (𝐡 βˆ’ 𝐴)) < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)))
8988simprd 497 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 / (𝐡 βˆ’ 𝐴)) < ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
9083, 84, 86, 89ltdiv2dd 43602 . . . . . . . . . . . 12 (πœ‘ β†’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) < (1 / (1 / (𝐡 βˆ’ 𝐴))))
918recnd 11190 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ β„‚)
9291, 12recrecd 11935 . . . . . . . . . . . 12 (πœ‘ β†’ (1 / (1 / (𝐡 βˆ’ 𝐴))) = (𝐡 βˆ’ 𝐴))
9390, 92breqtrd 5136 . . . . . . . . . . 11 (πœ‘ β†’ (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)) < (𝐡 βˆ’ 𝐴))
9482, 8, 7, 93ltadd2dd 11321 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 + (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))) < (𝐴 + (𝐡 βˆ’ 𝐴)))
955oveq2i 7373 . . . . . . . . . . . 12 (1 / 𝑀) = (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))
9695oveq2i 7373 . . . . . . . . . . 11 (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1)))
9796a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 + (1 / 𝑀)) = (𝐴 + (1 / ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1))))
987recnd 11190 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ β„‚)
996recnd 11190 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ β„‚)
10098, 99pncan3d 11522 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 + (𝐡 βˆ’ 𝐴)) = 𝐡)
101100eqcomd 2743 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = (𝐴 + (𝐡 βˆ’ 𝐴)))
10294, 97, 1013brtr4d 5142 . . . . . . . . 9 (πœ‘ β†’ (𝐴 + (1 / 𝑀)) < 𝐡)
103102adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑀)) < 𝐡)
10458, 71, 72, 79, 103lelttrd 11320 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑗)) < 𝐡)
10529, 31, 58, 61, 104eliood 43810 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐡))
10627, 105ffvelcdmd 7041 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (πΉβ€˜(𝐴 + (1 / 𝑗))) ∈ ℝ)
107 ioodvbdlimc1lem2.s . . . . 5 𝑆 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐴 + (1 / 𝑗))))
108106, 107fmptd 7067 . . . 4 (πœ‘ β†’ 𝑆:(β„€β‰₯β€˜π‘€)βŸΆβ„)
109 ioodvbdlimc1lem2.dmdv . . . . . 6 (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
110 ioodvbdlimc1lem2.dvbd . . . . . 6 (πœ‘ β†’ βˆƒπ‘¦ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ 𝑦)
1117, 6, 9, 26, 109, 110dvbdfbdioo 44245 . . . . 5 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏)
11262adantr 482 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) β†’ 𝑀 ∈ ℝ)
113 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘€))
114107fvmpt2 6964 . . . . . . . . . . . . . 14 ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ∧ (πΉβ€˜(𝐴 + (1 / 𝑗))) ∈ ℝ) β†’ (π‘†β€˜π‘—) = (πΉβ€˜(𝐴 + (1 / 𝑗))))
115113, 106, 114syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘†β€˜π‘—) = (πΉβ€˜(𝐴 + (1 / 𝑗))))
116115fveq2d 6851 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(π‘†β€˜π‘—)) = (absβ€˜(πΉβ€˜(𝐴 + (1 / 𝑗)))))
117116adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(π‘†β€˜π‘—)) = (absβ€˜(πΉβ€˜(𝐴 + (1 / 𝑗)))))
118 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏)
119105adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐡))
120 2fveq3 6852 . . . . . . . . . . . . . 14 (π‘₯ = (𝐴 + (1 / 𝑗)) β†’ (absβ€˜(πΉβ€˜π‘₯)) = (absβ€˜(πΉβ€˜(𝐴 + (1 / 𝑗)))))
121120breq1d 5120 . . . . . . . . . . . . 13 (π‘₯ = (𝐴 + (1 / 𝑗)) β†’ ((absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 ↔ (absβ€˜(πΉβ€˜(𝐴 + (1 / 𝑗)))) ≀ 𝑏))
122121rspccva 3583 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 ∧ (𝐴 + (1 / 𝑗)) ∈ (𝐴(,)𝐡)) β†’ (absβ€˜(πΉβ€˜(𝐴 + (1 / 𝑗)))) ≀ 𝑏)
123118, 119, 122syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(πΉβ€˜(𝐴 + (1 / 𝑗)))) ≀ 𝑏)
124117, 123eqbrtrd 5132 . . . . . . . . . 10 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)
125124a1d 25 . . . . . . . . 9 (((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
126125ralrimiva 3144 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) β†’ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
127 breq1 5113 . . . . . . . . . . 11 (π‘˜ = 𝑀 β†’ (π‘˜ ≀ 𝑗 ↔ 𝑀 ≀ 𝑗))
128127imbi1d 342 . . . . . . . . . 10 (π‘˜ = 𝑀 β†’ ((π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏) ↔ (𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
129128ralbidv 3175 . . . . . . . . 9 (π‘˜ = 𝑀 β†’ (βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏) ↔ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
130129rspcev 3584 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(𝑀 ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
131112, 126, 130syl2anc 585 . . . . . . 7 ((πœ‘ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
132131ex 414 . . . . . 6 (πœ‘ β†’ (βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
133132reximdv 3168 . . . . 5 (πœ‘ β†’ (βˆƒπ‘ ∈ ℝ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜(πΉβ€˜π‘₯)) ≀ 𝑏 β†’ βˆƒπ‘ ∈ ℝ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏)))
134111, 133mpd 15 . . . 4 (πœ‘ β†’ βˆƒπ‘ ∈ ℝ βˆƒπ‘˜ ∈ ℝ βˆ€π‘— ∈ (β„€β‰₯β€˜π‘€)(π‘˜ ≀ 𝑗 β†’ (absβ€˜(π‘†β€˜π‘—)) ≀ 𝑏))
1354, 25, 108, 134limsupre 43956 . . 3 (πœ‘ β†’ (lim supβ€˜π‘†) ∈ ℝ)
136135recnd 11190 . 2 (πœ‘ β†’ (lim supβ€˜π‘†) ∈ β„‚)
137 eluzelre 12781 . . . . . . . . 9 (𝑗 ∈ (β„€β‰₯β€˜π‘) β†’ 𝑗 ∈ ℝ)
138137adantl 483 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑗 ∈ ℝ)
139 0red 11165 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 ∈ ℝ)
14045peano2zd 12617 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((βŒŠβ€˜(1 / (𝐡 βˆ’ 𝐴))) + 1) ∈ β„€)
1415, 140eqeltrid 2842 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„€)
142141adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ∈ β„€)
143142zred 12614 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ∈ ℝ)
144143adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑀 ∈ ℝ)
14567ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 < 𝑀)
146 ioodvbdlimc1lem2.n . . . . . . . . . . . . . 14 𝑁 = if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀)
147 ioodvbdlimc1lem2.y . . . . . . . . . . . . . . . . . . . 20 π‘Œ = sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )
148 ioomidp 43826 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡) β†’ ((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡))
1497, 6, 9, 148syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡))
150 ne0i 4299 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡) β†’ (𝐴(,)𝐡) β‰  βˆ…)
151149, 150syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐴(,)𝐡) β‰  βˆ…)
152 ioossre 13332 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝐡) βŠ† ℝ
153152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† ℝ)
154 dvfre 25331 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹:(𝐴(,)𝐡)βŸΆβ„ ∧ (𝐴(,)𝐡) βŠ† ℝ) β†’ (ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„)
15526, 153, 154syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„)
156109feq2d 6659 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„ ↔ (ℝ D 𝐹):(𝐴(,)𝐡)βŸΆβ„))
157155, 156mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (ℝ D 𝐹):(𝐴(,)𝐡)βŸΆβ„)
158157ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐹)β€˜π‘₯) ∈ ℝ)
159158recnd 11190 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐹)β€˜π‘₯) ∈ β„‚)
160159abscld 15328 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ∈ ℝ)
161 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))) = (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)))
162 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) = sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )
163151, 160, 110, 161, 162suprnmpt 43465 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) ∈ ℝ ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )))
164163simpld 496 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) ∈ ℝ)
165147, 164eqeltrid 2842 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ π‘Œ ∈ ℝ)
166165adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘Œ ∈ ℝ)
167 rpre 12930 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ ℝ)
168167rehalfcld 12407 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ+ β†’ (π‘₯ / 2) ∈ ℝ)
169168adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) ∈ ℝ)
170167recnd 11190 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ β„‚)
171170adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ β„‚)
172 2cnd 12238 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 2 ∈ β„‚)
173 rpne0 12938 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ β‰  0)
174173adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ β‰  0)
175 2ne0 12264 . . . . . . . . . . . . . . . . . . . 20 2 β‰  0
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 2 β‰  0)
177171, 172, 174, 176divne0d 11954 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) β‰  0)
178166, 169, 177redivcld 11990 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ)
179178flcld 13710 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) ∈ β„€)
180179peano2zd 12617 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ β„€)
181180, 142ifcld 4537 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀) ∈ β„€)
182146, 181eqeltrid 2842 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ β„€)
183182zred 12614 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ ℝ)
184183adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑁 ∈ ℝ)
185180zred 12614 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ)
186 max1 13111 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
187143, 185, 186syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
188187, 146breqtrrdi 5152 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑀 ≀ 𝑁)
189188adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑀 ≀ 𝑁)
190 eluzle 12783 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘) β†’ 𝑁 ≀ 𝑗)
191190adantl 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑁 ≀ 𝑗)
192144, 184, 138, 189, 191letrd 11319 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑀 ≀ 𝑗)
193139, 144, 138, 145, 192ltletrd 11322 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 < 𝑗)
194193gt0ne0d 11726 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 𝑗 β‰  0)
195138, 194rereccld 11989 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ (1 / 𝑗) ∈ ℝ)
196138, 193recgt0d 12096 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ 0 < (1 / 𝑗))
197195, 196elrpd 12961 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) β†’ (1 / 𝑗) ∈ ℝ+)
198197adantr 482 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ (1 / 𝑗) ∈ ℝ+)
199 ioodvbdlimc1lem2.ch . . . . . . . . 9 (πœ’ ↔ (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)))
200199biimpi 215 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)))
201 simp-5l 784 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ πœ‘)
202200, 201syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ πœ‘)
203202, 26syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„)
204200simplrd 769 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑧 ∈ (𝐴(,)𝐡))
205203, 204ffvelcdmd 7041 . . . . . . . . . . . . . 14 (πœ’ β†’ (πΉβ€˜π‘§) ∈ ℝ)
206205recnd 11190 . . . . . . . . . . . . 13 (πœ’ β†’ (πΉβ€˜π‘§) ∈ β„‚)
207202, 108syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑆:(β„€β‰₯β€˜π‘€)βŸΆβ„)
208 simp-5r 785 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ π‘₯ ∈ ℝ+)
209200, 208syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ π‘₯ ∈ ℝ+)
210 eluz2 12776 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (β„€β‰₯β€˜π‘€) ↔ (𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 𝑀 ≀ 𝑁))
211142, 182, 188, 210syl3anbrc 1344 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))
212202, 209, 211syl2anc 585 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘€))
213 uzss 12793 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (β„€β‰₯β€˜π‘€) β†’ (β„€β‰₯β€˜π‘) βŠ† (β„€β‰₯β€˜π‘€))
214212, 213syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (β„€β‰₯β€˜π‘) βŠ† (β„€β‰₯β€˜π‘€))
215 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘))
216200, 215syl 17 . . . . . . . . . . . . . . . 16 (πœ’ β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘))
217214, 216sseldd 3950 . . . . . . . . . . . . . . 15 (πœ’ β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘€))
218207, 217ffvelcdmd 7041 . . . . . . . . . . . . . 14 (πœ’ β†’ (π‘†β€˜π‘—) ∈ ℝ)
219218recnd 11190 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘†β€˜π‘—) ∈ β„‚)
220202, 136syl 17 . . . . . . . . . . . . 13 (πœ’ β†’ (lim supβ€˜π‘†) ∈ β„‚)
221206, 219, 220npncand 11543 . . . . . . . . . . . 12 (πœ’ β†’ (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) = ((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†)))
222221eqcomd 2743 . . . . . . . . . . 11 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†)) = (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))))
223222fveq2d 6851 . . . . . . . . . 10 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) = (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))))
224205, 218resubcld 11590 . . . . . . . . . . . . . 14 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) ∈ ℝ)
225202, 135syl 17 . . . . . . . . . . . . . . 15 (πœ’ β†’ (lim supβ€˜π‘†) ∈ ℝ)
226218, 225resubcld 11590 . . . . . . . . . . . . . 14 (πœ’ β†’ ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)) ∈ ℝ)
227224, 226readdcld 11191 . . . . . . . . . . . . 13 (πœ’ β†’ (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) ∈ ℝ)
228227recnd 11190 . . . . . . . . . . . 12 (πœ’ β†’ (((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) ∈ β„‚)
229228abscld 15328 . . . . . . . . . . 11 (πœ’ β†’ (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) ∈ ℝ)
230224recnd 11190 . . . . . . . . . . . . 13 (πœ’ β†’ ((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) ∈ β„‚)
231230abscld 15328 . . . . . . . . . . . 12 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) ∈ ℝ)
232226recnd 11190 . . . . . . . . . . . . 13 (πœ’ β†’ ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)) ∈ β„‚)
233232abscld 15328 . . . . . . . . . . . 12 (πœ’ β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) ∈ ℝ)
234231, 233readdcld 11191 . . . . . . . . . . 11 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) ∈ ℝ)
235209rpred 12964 . . . . . . . . . . 11 (πœ’ β†’ π‘₯ ∈ ℝ)
236230, 232abstrid 15348 . . . . . . . . . . 11 (πœ’ β†’ (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) ≀ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))))
237235rehalfcld 12407 . . . . . . . . . . . . 13 (πœ’ β†’ (π‘₯ / 2) ∈ ℝ)
238206, 219abssubd 15345 . . . . . . . . . . . . . 14 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) = (absβ€˜((π‘†β€˜π‘—) βˆ’ (πΉβ€˜π‘§))))
239202, 217, 115syl2anc 585 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘†β€˜π‘—) = (πΉβ€˜(𝐴 + (1 / 𝑗))))
240239fvoveq1d 7384 . . . . . . . . . . . . . . 15 (πœ’ β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (πΉβ€˜π‘§))) = (absβ€˜((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§))))
241202, 217, 106syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ (πΉβ€˜(𝐴 + (1 / 𝑗))) ∈ ℝ)
242241, 205resubcld 11590 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ ((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§)) ∈ ℝ)
243242recnd 11190 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ ((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§)) ∈ β„‚)
244243abscld 15328 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (absβ€˜((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§))) ∈ ℝ)
245202, 165syl 17 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ π‘Œ ∈ ℝ)
246202, 217, 58syl2anc 585 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (𝐴 + (1 / 𝑗)) ∈ ℝ)
247152, 204sselid 3947 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 𝑧 ∈ ℝ)
248246, 247resubcld 11590 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧) ∈ ℝ)
249245, 248remulcld 11192 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘Œ Β· ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧)) ∈ ℝ)
250202, 7syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 𝐴 ∈ ℝ)
251202, 6syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 𝐡 ∈ ℝ)
252202, 109syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
253163simprd 497 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ))
254147breq2i 5118 . . . . . . . . . . . . . . . . . . . . . 22 ((absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ ↔ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ))
255254ralbii 3097 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ ↔ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ))
256253, 255sylibr 233 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ)
257202, 256syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ)
258 2fveq3 6852 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘₯ β†’ (absβ€˜((ℝ D 𝐹)β€˜π‘€)) = (absβ€˜((ℝ D 𝐹)β€˜π‘₯)))
259258breq1d 5120 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = π‘₯ β†’ ((absβ€˜((ℝ D 𝐹)β€˜π‘€)) ≀ π‘Œ ↔ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ))
260259cbvralvw 3228 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘€ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘€)) ≀ π‘Œ ↔ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ π‘Œ)
261257, 260sylibr 233 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ βˆ€π‘€ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘€)) ≀ π‘Œ)
262247rexrd 11212 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ 𝑧 ∈ ℝ*)
263202, 30syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ 𝐡 ∈ ℝ*)
264247, 250resubcld 11590 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (𝑧 βˆ’ 𝐴) ∈ ℝ)
265264recnd 11190 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ (𝑧 βˆ’ 𝐴) ∈ β„‚)
266265abscld 15328 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (absβ€˜(𝑧 βˆ’ 𝐴)) ∈ ℝ)
2673, 217sselid 3947 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑗 ∈ ℝ)
268202, 217, 56syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝑗 β‰  0)
269267, 268rereccld 11989 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (1 / 𝑗) ∈ ℝ)
270264leabsd 15306 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (𝑧 βˆ’ 𝐴) ≀ (absβ€˜(𝑧 βˆ’ 𝐴)))
271200simprd 497 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗))
272264, 266, 269, 270, 271lelttrd 11320 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ (𝑧 βˆ’ 𝐴) < (1 / 𝑗))
273247, 250, 269ltsubadd2d 11760 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ ((𝑧 βˆ’ 𝐴) < (1 / 𝑗) ↔ 𝑧 < (𝐴 + (1 / 𝑗))))
274272, 273mpbid 231 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ 𝑧 < (𝐴 + (1 / 𝑗)))
275202, 217, 104syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ (𝐴 + (1 / 𝑗)) < 𝐡)
276262, 263, 246, 274, 275eliood 43810 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (𝐴 + (1 / 𝑗)) ∈ (𝑧(,)𝐡))
277250, 251, 203, 252, 245, 261, 204, 276dvbdfbdioolem1 44243 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ ((absβ€˜((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§))) ≀ (π‘Œ Β· ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧)) ∧ (absβ€˜((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§))) ≀ (π‘Œ Β· (𝐡 βˆ’ 𝐴))))
278277simpld 496 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (absβ€˜((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§))) ≀ (π‘Œ Β· ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧)))
279202, 217, 57syl2anc 585 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ (1 / 𝑗) ∈ ℝ)
280245, 279remulcld 11192 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (π‘Œ Β· (1 / 𝑗)) ∈ ℝ)
281157, 149ffvelcdmd 7041 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2)) ∈ ℝ)
282281recnd 11190 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2)) ∈ β„‚)
283282abscld 15328 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ∈ ℝ)
284282absge0d 15336 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 0 ≀ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))))
285 2fveq3 6852 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = ((𝐴 + 𝐡) / 2) β†’ (absβ€˜((ℝ D 𝐹)β€˜π‘₯)) = (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))))
286147eqcomi 2746 . . . . . . . . . . . . . . . . . . . . . . . 24 sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) = π‘Œ
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = ((𝐴 + 𝐡) / 2) β†’ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) = π‘Œ)
288285, 287breq12d 5123 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = ((𝐴 + 𝐡) / 2) β†’ ((absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < ) ↔ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ≀ π‘Œ))
289288rspcva 3582 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 + 𝐡) / 2) ∈ (𝐴(,)𝐡) ∧ βˆ€π‘₯ ∈ (𝐴(,)𝐡)(absβ€˜((ℝ D 𝐹)β€˜π‘₯)) ≀ sup(ran (π‘₯ ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘₯))), ℝ, < )) β†’ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ≀ π‘Œ)
290149, 253, 289syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (absβ€˜((ℝ D 𝐹)β€˜((𝐴 + 𝐡) / 2))) ≀ π‘Œ)
29114, 283, 165, 284, 290letrd 11319 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 0 ≀ π‘Œ)
292202, 291syl 17 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ 0 ≀ π‘Œ)
293202, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ 𝐴 ∈ ℝ*)
294 ioogtlb 43807 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑧)
295293, 263, 204, 294syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ 𝐴 < 𝑧)
296250, 247, 246, 295ltsub2dd 11775 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧) < ((𝐴 + (1 / 𝑗)) βˆ’ 𝐴))
297202, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ 𝐴 ∈ β„‚)
298279recnd 11190 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (1 / 𝑗) ∈ β„‚)
299297, 298pncan2d 11521 . . . . . . . . . . . . . . . . . . . 20 (πœ’ β†’ ((𝐴 + (1 / 𝑗)) βˆ’ 𝐴) = (1 / 𝑗))
300296, 299breqtrd 5136 . . . . . . . . . . . . . . . . . . 19 (πœ’ β†’ ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧) < (1 / 𝑗))
301248, 269, 300ltled 11310 . . . . . . . . . . . . . . . . . 18 (πœ’ β†’ ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧) ≀ (1 / 𝑗))
302248, 269, 245, 292, 301lemul2ad 12102 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (π‘Œ Β· ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧)) ≀ (π‘Œ Β· (1 / 𝑗)))
303280adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) ∈ ℝ)
304237adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘₯ / 2) ∈ ℝ)
305 oveq1 7369 . . . . . . . . . . . . . . . . . . . . 21 (π‘Œ = 0 β†’ (π‘Œ Β· (1 / 𝑗)) = (0 Β· (1 / 𝑗)))
306298mul02d 11360 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (0 Β· (1 / 𝑗)) = 0)
307305, 306sylan9eqr 2799 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) = 0)
308209rphalfcld 12976 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ (π‘₯ / 2) ∈ ℝ+)
309308rpgt0d 12967 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ 0 < (π‘₯ / 2))
310309adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ π‘Œ = 0) β†’ 0 < (π‘₯ / 2))
311307, 310eqbrtrd 5132 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) < (π‘₯ / 2))
312303, 304, 311ltled 11310 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
313245adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ π‘Œ ∈ ℝ)
314292adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ 0 ≀ π‘Œ)
315 neqne 2952 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ π‘Œ = 0 β†’ π‘Œ β‰  0)
316315adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ π‘Œ β‰  0)
317313, 314, 316ne0gt0d 11299 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ 0 < π‘Œ)
318280adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑗)) ∈ ℝ)
3193, 212sselid 3947 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 𝑁 ∈ ℝ)
320 0red 11165 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ 0 ∈ ℝ)
321202, 209, 143syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ 𝑀 ∈ ℝ)
322202, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ 0 < 𝑀)
323202, 209, 188syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ 𝑀 ≀ 𝑁)
324320, 321, 319, 322, 323ltletrd 11322 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ 0 < 𝑁)
325324gt0ne0d 11726 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 𝑁 β‰  0)
326319, 325rereccld 11989 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ (1 / 𝑁) ∈ ℝ)
327245, 326remulcld 11192 . . . . . . . . . . . . . . . . . . . . 21 (πœ’ β†’ (π‘Œ Β· (1 / 𝑁)) ∈ ℝ)
328327adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑁)) ∈ ℝ)
329237adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘₯ / 2) ∈ ℝ)
330279adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑗) ∈ ℝ)
331326adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑁) ∈ ℝ)
332245adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ π‘Œ ∈ ℝ)
333292adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 ≀ π‘Œ)
334319, 324elrpd 12961 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 𝑁 ∈ ℝ+)
335202, 217, 59syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 𝑗 ∈ ℝ+)
336 1red 11163 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 1 ∈ ℝ)
33776a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 0 ≀ 1)
338216, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ’ β†’ 𝑁 ≀ 𝑗)
339334, 335, 336, 337, 338lediv2ad 12986 . . . . . . . . . . . . . . . . . . . . . 22 (πœ’ β†’ (1 / 𝑗) ≀ (1 / 𝑁))
340339adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑗) ≀ (1 / 𝑁))
341330, 331, 332, 333, 340lemul2ad 12102 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘Œ Β· (1 / 𝑁)))
342235recnd 11190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ π‘₯ ∈ β„‚)
343 2cnd 12238 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ 2 ∈ β„‚)
344209rpne0d 12969 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ π‘₯ β‰  0)
345175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ 2 β‰  0)
346342, 343, 344, 345divne0d 11954 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ (π‘₯ / 2) β‰  0)
347245, 237, 346redivcld 11990 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ)
348347adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ)
349 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 < π‘Œ)
350309adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 < (π‘₯ / 2))
351332, 329, 349, 350divgt0d 12097 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 < (π‘Œ / (π‘₯ / 2)))
352348, 351elrpd 12961 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ∈ ℝ+)
353352rprecred 12975 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / (π‘Œ / (π‘₯ / 2))) ∈ ℝ)
354334adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ 𝑁 ∈ ℝ+)
355 1red 11163 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ 1 ∈ ℝ)
35676a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ 0 ≀ 1)
357347flcld 13710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ’ β†’ (βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) ∈ β„€)
358357peano2zd 12617 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ β„€)
359358zred 12614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ)
360202, 141syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ’ β†’ 𝑀 ∈ β„€)
361358, 360ifcld 4537 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ’ β†’ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀) ∈ β„€)
362146, 361eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ 𝑁 ∈ β„€)
363362zred 12614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ 𝑁 ∈ ℝ)
364 flltp1 13712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘Œ / (π‘₯ / 2)) ∈ ℝ β†’ (π‘Œ / (π‘₯ / 2)) < ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1))
365347, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) < ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1))
366202, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ’ β†’ 𝑀 ∈ ℝ)
367 max2 13113 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ∈ ℝ) β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
368366, 359, 367syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ≀ if(𝑀 ≀ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1), 𝑀))
369368, 146breqtrrdi 5152 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ’ β†’ ((βŒŠβ€˜(π‘Œ / (π‘₯ / 2))) + 1) ≀ 𝑁)
370347, 359, 363, 365, 369ltletrd 11322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) < 𝑁)
371347, 319, 370ltled 11310 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ’ β†’ (π‘Œ / (π‘₯ / 2)) ≀ 𝑁)
372371adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ≀ 𝑁)
373352, 354, 355, 356, 372lediv2ad 12986 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (1 / 𝑁) ≀ (1 / (π‘Œ / (π‘₯ / 2))))
374331, 353, 332, 333, 373lemul2ad 12102 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑁)) ≀ (π‘Œ Β· (1 / (π‘Œ / (π‘₯ / 2)))))
375332recnd 11190 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ π‘Œ ∈ β„‚)
376348recnd 11190 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) ∈ β„‚)
377351gt0ne0d 11726 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘₯ / 2)) β‰  0)
378375, 376, 377divrecd 11941 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘Œ / (π‘₯ / 2))) = (π‘Œ Β· (1 / (π‘Œ / (π‘₯ / 2)))))
379329recnd 11190 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘₯ / 2) ∈ β„‚)
380349gt0ne0d 11726 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ π‘Œ β‰  0)
381346adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘₯ / 2) β‰  0)
382375, 379, 380, 381ddcand 11958 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ / (π‘Œ / (π‘₯ / 2))) = (π‘₯ / 2))
383378, 382eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . 21 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / (π‘Œ / (π‘₯ / 2)))) = (π‘₯ / 2))
384374, 383breqtrd 5136 . . . . . . . . . . . . . . . . . . . 20 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑁)) ≀ (π‘₯ / 2))
385318, 328, 329, 341, 384letrd 11319 . . . . . . . . . . . . . . . . . . 19 ((πœ’ ∧ 0 < π‘Œ) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
386317, 385syldan 592 . . . . . . . . . . . . . . . . . 18 ((πœ’ ∧ Β¬ π‘Œ = 0) β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
387312, 386pm2.61dan 812 . . . . . . . . . . . . . . . . 17 (πœ’ β†’ (π‘Œ Β· (1 / 𝑗)) ≀ (π‘₯ / 2))
388249, 280, 237, 302, 387letrd 11319 . . . . . . . . . . . . . . . 16 (πœ’ β†’ (π‘Œ Β· ((𝐴 + (1 / 𝑗)) βˆ’ 𝑧)) ≀ (π‘₯ / 2))
389244, 249, 237, 278, 388letrd 11319 . . . . . . . . . . . . . . 15 (πœ’ β†’ (absβ€˜((πΉβ€˜(𝐴 + (1 / 𝑗))) βˆ’ (πΉβ€˜π‘§))) ≀ (π‘₯ / 2))
390240, 389eqbrtrd 5132 . . . . . . . . . . . . . 14 (πœ’ β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (πΉβ€˜π‘§))) ≀ (π‘₯ / 2))
391238, 390eqbrtrd 5132 . . . . . . . . . . . . 13 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) ≀ (π‘₯ / 2))
392 simpllr 775 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
393200, 392syl 17 . . . . . . . . . . . . 13 (πœ’ β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
394231, 233, 237, 237, 391, 393leltaddd 11784 . . . . . . . . . . . 12 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) < ((π‘₯ / 2) + (π‘₯ / 2)))
3953422halvesd 12406 . . . . . . . . . . . 12 (πœ’ β†’ ((π‘₯ / 2) + (π‘₯ / 2)) = π‘₯)
396394, 395breqtrd 5136 . . . . . . . . . . 11 (πœ’ β†’ ((absβ€˜((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—))) + (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) < π‘₯)
397229, 234, 235, 236, 396lelttrd 11320 . . . . . . . . . 10 (πœ’ β†’ (absβ€˜(((πΉβ€˜π‘§) βˆ’ (π‘†β€˜π‘—)) + ((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†)))) < π‘₯)
398223, 397eqbrtrd 5132 . . . . . . . . 9 (πœ’ β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)
399199, 398sylbir 234 . . . . . . . 8 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)
400399adantrl 715 . . . . . . 7 ((((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) ∧ (𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗))) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)
401400ex 414 . . . . . 6 (((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ ((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
402401ralrimiva 3144 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
403 brimralrspcev 5171 . . . . 5 (((1 / 𝑗) ∈ ℝ+ ∧ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < (1 / 𝑗)) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
404198, 402, 403syl2anc 585 . . . 4 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘)) ∧ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
405 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ 𝑏 ≀ 𝑁)
406405iftrued 4499 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) = 𝑁)
407 uzid 12785 . . . . . . . . . . . 12 (𝑁 ∈ β„€ β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘))
408182, 407syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘))
409408adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘))
410406, 409eqeltrd 2838 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
411410adantlr 714 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
412 iffalse 4500 . . . . . . . . . 10 (Β¬ 𝑏 ≀ 𝑁 β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) = 𝑏)
413412adantl 483 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) = 𝑏)
414182ad2antrr 725 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 ∈ β„€)
415 simplr 768 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑏 ∈ β„€)
416414zred 12614 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 ∈ ℝ)
417415zred 12614 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑏 ∈ ℝ)
418 simpr 486 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ Β¬ 𝑏 ≀ 𝑁)
419416, 417ltnled 11309 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ (𝑁 < 𝑏 ↔ Β¬ 𝑏 ≀ 𝑁))
420418, 419mpbird 257 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 < 𝑏)
421416, 417, 420ltled 11310 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑁 ≀ 𝑏)
422 eluz2 12776 . . . . . . . . . 10 (𝑏 ∈ (β„€β‰₯β€˜π‘) ↔ (𝑁 ∈ β„€ ∧ 𝑏 ∈ β„€ ∧ 𝑁 ≀ 𝑏))
423414, 415, 421, 422syl3anbrc 1344 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ 𝑏 ∈ (β„€β‰₯β€˜π‘))
424413, 423eqeltrd 2838 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ Β¬ 𝑏 ≀ 𝑁) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
425411, 424pm2.61dan 812 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
426425adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
427 simpr 486 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
428 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑏 ∈ β„€)
429182adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑁 ∈ β„€)
430429, 428ifcld 4537 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ β„€)
431428zred 12614 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑏 ∈ ℝ)
432429zred 12614 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑁 ∈ ℝ)
433 max1 13111 . . . . . . . . . . 11 ((𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ 𝑏 ≀ if(𝑏 ≀ 𝑁, 𝑁, 𝑏))
434431, 432, 433syl2anc 585 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ 𝑏 ≀ if(𝑏 ≀ 𝑁, 𝑁, 𝑏))
435 eluz2 12776 . . . . . . . . . 10 (if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘) ↔ (𝑏 ∈ β„€ ∧ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ β„€ ∧ 𝑏 ≀ if(𝑏 ≀ 𝑁, 𝑁, 𝑏)))
436428, 430, 434, 435syl3anbrc 1344 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
437436adantr 482 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘))
438 fveq2 6847 . . . . . . . . . . 11 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (π‘†β€˜π‘) = (π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)))
439438eleq1d 2823 . . . . . . . . . 10 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ ((π‘†β€˜π‘) ∈ β„‚ ↔ (π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚))
440438fvoveq1d 7384 . . . . . . . . . . 11 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) = (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))))
441440breq1d 5120 . . . . . . . . . 10 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ ((absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2) ↔ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
442439, 441anbi12d 632 . . . . . . . . 9 (𝑐 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ↔ ((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))))
443442rspccva 3583 . . . . . . . 8 ((βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) ∧ if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘)) β†’ ((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
444427, 437, 443syl2anc 585 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ ((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
445444simprd 497 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
446 fveq2 6847 . . . . . . . . 9 (𝑗 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (π‘†β€˜π‘—) = (π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)))
447446fvoveq1d 7384 . . . . . . . 8 (𝑗 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ (absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) = (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))))
448447breq1d 5120 . . . . . . 7 (𝑗 = if(𝑏 ≀ 𝑁, 𝑁, 𝑏) β†’ ((absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2) ↔ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
449448rspcev 3584 . . . . . 6 ((if(𝑏 ≀ 𝑁, 𝑁, 𝑏) ∈ (β„€β‰₯β€˜π‘) ∧ (absβ€˜((π‘†β€˜if(𝑏 ≀ 𝑁, 𝑁, 𝑏)) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)) β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘)(absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
450426, 445, 449syl2anc 585 . . . . 5 ((((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑏 ∈ β„€) ∧ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))) β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘)(absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
451 ax-resscn 11115 . . . . . . . . . . . . . 14 ℝ βŠ† β„‚
452451a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ℝ βŠ† β„‚)
45326, 452fssd 6691 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„‚)
454 dvcn 25301 . . . . . . . . . . . . . 14 (((ℝ βŠ† β„‚ ∧ 𝐹:(𝐴(,)𝐡)βŸΆβ„‚ ∧ (𝐴(,)𝐡) βŠ† ℝ) ∧ dom (ℝ D 𝐹) = (𝐴(,)𝐡)) β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
455452, 453, 153, 109, 454syl31anc 1374 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
456 cncfcdm 24277 . . . . . . . . . . . . 13 ((ℝ βŠ† β„‚ ∧ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚)) β†’ (𝐹 ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐡)βŸΆβ„))
457452, 455, 456syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ 𝐹:(𝐴(,)𝐡)βŸΆβ„))
45826, 457mpbird 257 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cn→ℝ))
459 ioodvbdlimc1lem2.r . . . . . . . . . . . 12 𝑅 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (𝐴 + (1 / 𝑗)))
460105, 459fmptd 7067 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅:(β„€β‰₯β€˜π‘€)⟢(𝐴(,)𝐡))
461 eqid 2737 . . . . . . . . . . 11 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—)))
462 climrel 15381 . . . . . . . . . . . . 13 Rel ⇝
463462a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ Rel ⇝ )
464 fvex 6860 . . . . . . . . . . . . . . . . 17 (β„€β‰₯β€˜π‘€) ∈ V
465464mptex 7178 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴) ∈ V
466465a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴) ∈ V)
467 eqidd 2738 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴))
468 eqidd 2738 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) ∧ 𝑗 = π‘š) β†’ 𝐴 = 𝐴)
469 simpr 486 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ π‘š ∈ (β„€β‰₯β€˜π‘€))
4707adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ ℝ)
471467, 468, 469, 470fvmptd 6960 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴)β€˜π‘š) = 𝐴)
47223, 141, 466, 98, 471climconst 15432 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴) ⇝ 𝐴)
473464mptex 7178 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (𝐴 + (1 / 𝑗))) ∈ V
474459, 473eqeltri 2834 . . . . . . . . . . . . . . 15 𝑅 ∈ V
475474a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 ∈ V)
476 1cnd 11157 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ β„‚)
477 elnnnn0b 12464 . . . . . . . . . . . . . . . 16 (𝑀 ∈ β„• ↔ (𝑀 ∈ β„•0 ∧ 0 < 𝑀))
47821, 67, 477sylanbrc 584 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑀 ∈ β„•)
479 divcnvg 43942 . . . . . . . . . . . . . . 15 ((1 ∈ β„‚ ∧ 𝑀 ∈ β„•) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)) ⇝ 0)
480476, 478, 479syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)) ⇝ 0)
481 eqidd 2738 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴))
482 eqidd 2738 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) ∧ 𝑗 = 𝑖) β†’ 𝐴 = 𝐴)
483 simpr 486 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
4847adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ ℝ)
485481, 482, 483, 484fvmptd 6960 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴)β€˜π‘–) = 𝐴)
48698adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝐴 ∈ β„‚)
487485, 486eqeltrd 2838 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴)β€˜π‘–) ∈ β„‚)
488 eqidd 2738 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗)))
489 oveq2 7370 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 β†’ (1 / 𝑗) = (1 / 𝑖))
490489adantl 483 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) ∧ 𝑗 = 𝑖) β†’ (1 / 𝑗) = (1 / 𝑖))
4913, 483sselid 3947 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ ℝ)
492 0red 11165 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 ∈ ℝ)
49362adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ)
49467adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < 𝑀)
495 eluzle 12783 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝑖)
496495adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ≀ 𝑖)
497492, 493, 491, 494, 496ltletrd 11322 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 0 < 𝑖)
498497gt0ne0d 11726 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 β‰  0)
499491, 498rereccld 11989 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑖) ∈ ℝ)
500488, 490, 483, 499fvmptd 6960 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–) = (1 / 𝑖))
501491recnd 11190 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ β„‚)
502501, 498reccld 11931 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (1 / 𝑖) ∈ β„‚)
503500, 502eqeltrd 2838 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–) ∈ β„‚)
504489oveq2d 7378 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 β†’ (𝐴 + (1 / 𝑗)) = (𝐴 + (1 / 𝑖)))
505484, 499readdcld 11191 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑖)) ∈ ℝ)
506459, 504, 483, 505fvmptd3 6976 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘…β€˜π‘–) = (𝐴 + (1 / 𝑖)))
507485, 500oveq12d 7380 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴)β€˜π‘–) + ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–)) = (𝐴 + (1 / 𝑖)))
508506, 507eqtr4d 2780 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘…β€˜π‘–) = (((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ 𝐴)β€˜π‘–) + ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (1 / 𝑗))β€˜π‘–)))
50923, 141, 472, 475, 480, 487, 503, 508climadd 15521 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 ⇝ (𝐴 + 0))
51098addid1d 11362 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴 + 0) = 𝐴)
511509, 510breqtrd 5136 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 ⇝ 𝐴)
512 releldm 5904 . . . . . . . . . . . 12 ((Rel ⇝ ∧ 𝑅 ⇝ 𝐴) β†’ 𝑅 ∈ dom ⇝ )
513463, 511, 512syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ 𝑅 ∈ dom ⇝ )
514 fveq2 6847 . . . . . . . . . . . . . . 15 (𝑙 = π‘˜ β†’ (β„€β‰₯β€˜π‘™) = (β„€β‰₯β€˜π‘˜))
515 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (𝑙 = π‘˜ β†’ (π‘…β€˜π‘™) = (π‘…β€˜π‘˜))
516515oveq2d 7378 . . . . . . . . . . . . . . . . 17 (𝑙 = π‘˜ β†’ ((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™)) = ((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜)))
517516fveq2d 6851 . . . . . . . . . . . . . . . 16 (𝑙 = π‘˜ β†’ (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) = (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))))
518517breq1d 5120 . . . . . . . . . . . . . . 15 (𝑙 = π‘˜ β†’ ((absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))))
519514, 518raleqbidv 3322 . . . . . . . . . . . . . 14 (𝑙 = π‘˜ β†’ (βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))))
520519cbvrabv 3420 . . . . . . . . . . . . 13 {𝑙 ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}
521 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (β„Ž = 𝑖 β†’ (π‘…β€˜β„Ž) = (π‘…β€˜π‘–))
522521fvoveq1d 7384 . . . . . . . . . . . . . . . . 17 (β„Ž = 𝑖 β†’ (absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) = (absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))))
523522breq1d 5120 . . . . . . . . . . . . . . . 16 (β„Ž = 𝑖 β†’ ((absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ (absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))))
524523cbvralvw 3228 . . . . . . . . . . . . . . 15 (βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)))
525524rgenw 3069 . . . . . . . . . . . . . 14 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘€)(βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)))
526 rabbi 3435 . . . . . . . . . . . . . 14 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘€)(βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1)) ↔ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))) ↔ {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))})
527525, 526mpbi 229 . . . . . . . . . . . . 13 {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}
528520, 527eqtri 2765 . . . . . . . . . . . 12 {𝑙 ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))} = {π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}
529528infeq1i 9421 . . . . . . . . . . 11 inf({𝑙 ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€β„Ž ∈ (β„€β‰₯β€˜π‘™)(absβ€˜((π‘…β€˜β„Ž) βˆ’ (π‘…β€˜π‘™))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}, ℝ, < ) = inf({π‘˜ ∈ (β„€β‰₯β€˜π‘€) ∣ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘˜)(absβ€˜((π‘…β€˜π‘–) βˆ’ (π‘…β€˜π‘˜))) < (π‘₯ / (sup(ran (𝑧 ∈ (𝐴(,)𝐡) ↦ (absβ€˜((ℝ D 𝐹)β€˜π‘§))), ℝ, < ) + 1))}, ℝ, < )
5307, 6, 9, 458, 109, 110, 22, 460, 461, 513, 529ioodvbdlimc1lem1 44246 . . . . . . . . . 10 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))) ⇝ (lim supβ€˜(𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—)))))
531459fvmpt2 6964 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (β„€β‰₯β€˜π‘€) ∧ (𝐴 + (1 / 𝑗)) ∈ ℝ) β†’ (π‘…β€˜π‘—) = (𝐴 + (1 / 𝑗)))
532113, 58, 531syl2anc 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (π‘…β€˜π‘—) = (𝐴 + (1 / 𝑗)))
533532eqcomd 2743 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐴 + (1 / 𝑗)) = (π‘…β€˜π‘—))
534533fveq2d 6851 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜π‘€)) β†’ (πΉβ€˜(𝐴 + (1 / 𝑗))) = (πΉβ€˜(π‘…β€˜π‘—)))
535534mpteq2dva 5210 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐴 + (1 / 𝑗)))) = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))))
536107, 535eqtrid 2789 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 = (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—))))
537536fveq2d 6851 . . . . . . . . . 10 (πœ‘ β†’ (lim supβ€˜π‘†) = (lim supβ€˜(𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(π‘…β€˜π‘—)))))
538530, 536, 5373brtr4d 5142 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ⇝ (lim supβ€˜π‘†))
539464mptex 7178 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜π‘€) ↦ (πΉβ€˜(𝐴 + (1 / 𝑗)))) ∈ V
540107, 539eqeltri 2834 . . . . . . . . . . 11 𝑆 ∈ V
541540a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ V)
542 eqidd 2738 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ β„€) β†’ (π‘†β€˜π‘) = (π‘†β€˜π‘))
543541, 542clim 15383 . . . . . . . . 9 (πœ‘ β†’ (𝑆 ⇝ (lim supβ€˜π‘†) ↔ ((lim supβ€˜π‘†) ∈ β„‚ ∧ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž))))
544538, 543mpbid 231 . . . . . . . 8 (πœ‘ β†’ ((lim supβ€˜π‘†) ∈ β„‚ ∧ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž)))
545544simprd 497 . . . . . . 7 (πœ‘ β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž))
546545adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž))
547 simpr 486 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ ℝ+)
548547rphalfcld 12976 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) ∈ ℝ+)
549 breq2 5114 . . . . . . . . 9 (π‘Ž = (π‘₯ / 2) β†’ ((absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž ↔ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
550549anbi2d 630 . . . . . . . 8 (π‘Ž = (π‘₯ / 2) β†’ (((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž) ↔ ((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))))
551550rexralbidv 3215 . . . . . . 7 (π‘Ž = (π‘₯ / 2) β†’ (βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž) ↔ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))))
552551rspccva 3583 . . . . . 6 ((βˆ€π‘Ž ∈ ℝ+ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < π‘Ž) ∧ (π‘₯ / 2) ∈ ℝ+) β†’ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
553546, 548, 552syl2anc 585 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘ ∈ β„€ βˆ€π‘ ∈ (β„€β‰₯β€˜π‘)((π‘†β€˜π‘) ∈ β„‚ ∧ (absβ€˜((π‘†β€˜π‘) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2)))
554450, 553r19.29a 3160 . . . 4 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘)(absβ€˜((π‘†β€˜π‘—) βˆ’ (lim supβ€˜π‘†))) < (π‘₯ / 2))
555404, 554r19.29a 3160 . . 3 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
556555ralrimiva 3144 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))
557 ioosscn 13333 . . . 4 (𝐴(,)𝐡) βŠ† β„‚
558557a1i 11 . . 3 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
559453, 558, 98ellimc3 25259 . 2 (πœ‘ β†’ ((lim supβ€˜π‘†) ∈ (𝐹 limβ„‚ 𝐴) ↔ ((lim supβ€˜π‘†) ∈ β„‚ ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘¦ ∈ ℝ+ βˆ€π‘§ ∈ (𝐴(,)𝐡)((𝑧 β‰  𝐴 ∧ (absβ€˜(𝑧 βˆ’ 𝐴)) < 𝑦) β†’ (absβ€˜((πΉβ€˜π‘§) βˆ’ (lim supβ€˜π‘†))) < π‘₯))))
560136, 556, 559mpbir2and 712 1 (πœ‘ β†’ (lim supβ€˜π‘†) ∈ (𝐹 limβ„‚ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  {crab 3410  Vcvv 3448   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638  ran crn 5639  Rel wrel 5643  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  supcsup 9383  infcinf 9384  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392   / cdiv 11819  β„•cn 12160  2c2 12215  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  (,)cioo 13271  βŒŠcfl 13702  abscabs 15126  lim supclsp 15359   ⇝ cli 15373  β€“cnβ†’ccncf 24255   limβ„‚ climc 25242   D cdv 25243
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247
This theorem is referenced by:  ioodvbdlimc1  44248
  Copyright terms: Public domain W3C validator