Metamath Proof Explorer

Theorem ioodvbdlimc2lem

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)

Ref Expression
Hypotheses 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 ioodvbdlimc2lem ( 𝜑 → ( lim sup ‘ 𝑆 ) ∈ ( 𝐹 limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ioodvbdlimc2lem.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ioodvbdlimc2lem.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ioodvbdlimc2lem.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 ioodvbdlimc2lem.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
5 ioodvbdlimc2lem.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
6 ioodvbdlimc2lem.dvbd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑦 )
7 ioodvbdlimc2lem.y ⊢ 𝑌 = sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < )
8 ioodvbdlimc2lem.m ⊢ 𝑀 = ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 )
9 ioodvbdlimc2lem.s ⊢ 𝑆 = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) )
10 ioodvbdlimc2lem.r ⊢ 𝑅 = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐵 − ( 1 / 𝑗 ) ) )
11 ioodvbdlimc2lem.n ⊢ 𝑁 = if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 )
12 ioodvbdlimc2lem.ch ⊢ ( 𝜒 ↔ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) )
13 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
14 zssre ⊢ ℤ ⊆ ℝ
15 13 14 sstri ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
16 15 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ )
17 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
18 1 2 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
19 3 18 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
20 19 gt0ne0d ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
21 17 20 rereccld ⊢ ( 𝜑 → ( 1 / ( 𝐵 − 𝐴 ) ) ∈ ℝ )
22 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
23 17 19 recgt0d ⊢ ( 𝜑 → 0 < ( 1 / ( 𝐵 − 𝐴 ) ) )
24 22 21 23 ltled ⊢ ( 𝜑 → 0 ≤ ( 1 / ( 𝐵 − 𝐴 ) ) )
25 flge0nn0 ⊢ ( ( ( 1 / ( 𝐵 − 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝐵 − 𝐴 ) ) ) → ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ∈ ℕ0 )
26 21 24 25 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ∈ ℕ0 )
27 peano2nn0 ⊢ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ∈ ℕ0 )
28 26 27 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ∈ ℕ0 )
29 8 28 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
30 29 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
31 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
32 31 uzsup ⊢ ( 𝑀 ∈ ℤ → sup ( ( ℤ≥ ‘ 𝑀 ) , ℝ* , < ) = +∞ )
33 30 32 syl ⊢ ( 𝜑 → sup ( ( ℤ≥ ‘ 𝑀 ) , ℝ* , < ) = +∞ )
34 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
35 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℝ* )
37 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐵 ∈ ℝ* )
39 2 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐵 ∈ ℝ )
40 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℝ )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℝ )
42 0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 ∈ ℝ )
43 0red ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 0 ∈ ℝ )
44 1red ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 1 ∈ ℝ )
45 43 44 readdcld ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 + 1 ) ∈ ℝ )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 0 + 1 ) ∈ ℝ )
47 43 ltp1d ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 0 < ( 0 + 1 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < ( 0 + 1 ) )
49 eluzel2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
50 49 zred ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℝ )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ )
52 21 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ∈ ℤ )
53 52 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ∈ ℝ )
54 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
55 26 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) )
56 22 53 54 55 leadd1dd ⊢ ( 𝜑 → ( 0 + 1 ) ≤ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) )
57 56 8 breqtrrdi ⊢ ( 𝜑 → ( 0 + 1 ) ≤ 𝑀 )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 0 + 1 ) ≤ 𝑀 )
59 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑗 )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ≤ 𝑗 )
61 46 51 41 58 60 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 0 + 1 ) ≤ 𝑗 )
62 42 46 41 48 61 ltletrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < 𝑗 )
63 62 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ≠ 0 )
64 41 63 rereccld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 / 𝑗 ) ∈ ℝ )
65 39 64 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ℝ )
66 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℝ )
67 29 nn0red ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
68 22 54 readdcld ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℝ )
69 53 54 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ∈ ℝ )
70 22 ltp1d ⊢ ( 𝜑 → 0 < ( 0 + 1 ) )
71 22 68 69 70 56 ltletrd ⊢ ( 𝜑 → 0 < ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) )
72 71 8 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑀 )
73 72 gt0ne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
74 67 73 rereccld ⊢ ( 𝜑 → ( 1 / 𝑀 ) ∈ ℝ )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 / 𝑀 ) ∈ ℝ )
76 39 75 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑀 ) ) ∈ ℝ )
77 8 eqcomi ⊢ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) = 𝑀
78 77 oveq2i ⊢ ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) = ( 1 / 𝑀 )
79 78 74 eqeltrid ⊢ ( 𝜑 → ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ∈ ℝ )
80 21 23 elrpd ⊢ ( 𝜑 → ( 1 / ( 𝐵 − 𝐴 ) ) ∈ ℝ+ )
81 69 71 elrpd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ∈ ℝ+ )
82 1rp ⊢ 1 ∈ ℝ+
83 82 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
84 fllelt ⊢ ( ( 1 / ( 𝐵 − 𝐴 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ≤ ( 1 / ( 𝐵 − 𝐴 ) ) ∧ ( 1 / ( 𝐵 − 𝐴 ) ) < ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) )
85 21 84 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) ≤ ( 1 / ( 𝐵 − 𝐴 ) ) ∧ ( 1 / ( 𝐵 − 𝐴 ) ) < ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) )
86 85 simprd ⊢ ( 𝜑 → ( 1 / ( 𝐵 − 𝐴 ) ) < ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) )
87 80 81 83 86 ltdiv2dd ⊢ ( 𝜑 → ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) < ( 1 / ( 1 / ( 𝐵 − 𝐴 ) ) ) )
88 17 recnd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
89 88 20 recrecd ⊢ ( 𝜑 → ( 1 / ( 1 / ( 𝐵 − 𝐴 ) ) ) = ( 𝐵 − 𝐴 ) )
90 87 89 breqtrd ⊢ ( 𝜑 → ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) < ( 𝐵 − 𝐴 ) )
91 79 17 2 90 ltsub2dd ⊢ ( 𝜑 → ( 𝐵 − ( 𝐵 − 𝐴 ) ) < ( 𝐵 − ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ) )
92 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
93 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
94 92 93 nncand ⊢ ( 𝜑 → ( 𝐵 − ( 𝐵 − 𝐴 ) ) = 𝐴 )
95 78 oveq2i ⊢ ( 𝐵 − ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ) = ( 𝐵 − ( 1 / 𝑀 ) )
96 95 a1i ⊢ ( 𝜑 → ( 𝐵 − ( 1 / ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ) = ( 𝐵 − ( 1 / 𝑀 ) ) )
97 91 94 96 3brtr3d ⊢ ( 𝜑 → 𝐴 < ( 𝐵 − ( 1 / 𝑀 ) ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 < ( 𝐵 − ( 1 / 𝑀 ) ) )
99 67 72 elrpd ⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ+ )
101 41 62 elrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℝ+ )
102 1red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ∈ ℝ )
103 0le1 ⊢ 0 ≤ 1
104 103 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 ≤ 1 )
105 100 101 102 104 60 lediv2ad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 / 𝑗 ) ≤ ( 1 / 𝑀 ) )
106 64 75 39 105 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑀 ) ) ≤ ( 𝐵 − ( 1 / 𝑗 ) ) )
107 66 76 65 98 106 ltletrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 < ( 𝐵 − ( 1 / 𝑗 ) ) )
108 101 rpreccld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 / 𝑗 ) ∈ ℝ+ )
109 39 108 ltsubrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑗 ) ) < 𝐵 )
110 36 38 65 107 109 eliood ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ( 𝐴 (,) 𝐵 ) )
111 34 110 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ∈ ℝ )
112 111 9 fmptd ⊢ ( 𝜑 → 𝑆 : ( ℤ≥ ‘ 𝑀 ) ⟶ ℝ )
113 1 2 3 4 5 6 dvbdfbdioo ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
114 67 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) → 𝑀 ∈ ℝ )
115 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
116 9 fvmpt2 ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ∈ ℝ ) → ( 𝑆 ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) )
117 115 111 116 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑆 ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) )
118 117 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) )
119 118 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) )
120 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
121 110 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ( 𝐴 (,) 𝐵 ) )
122 2fveq3 ⊢ ( 𝑥 = ( 𝐵 − ( 1 / 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) )
123 122 breq1d ⊢ ( 𝑥 = ( 𝐵 − ( 1 / 𝑗 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ≤ 𝑏 ) )
124 123 rspccva ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ∧ ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ≤ 𝑏 )
125 120 121 124 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ≤ 𝑏 )
126 119 125 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 )
127 126 a1d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) )
128 127 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) → ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑀 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) )
129 breq1 ⊢ ( 𝑘 = 𝑀 → ( 𝑘 ≤ 𝑗 ↔ 𝑀 ≤ 𝑗 ) )
130 129 imbi1d ⊢ ( 𝑘 = 𝑀 → ( ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ↔ ( 𝑀 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ) )
131 130 ralbidv ⊢ ( 𝑘 = 𝑀 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑀 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ) )
132 131 rspcev ⊢ ( ( 𝑀 ∈ ℝ ∧ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑀 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) )
133 114 128 132 syl2anc ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) )
134 133 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ) )
135 134 reximdv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 → ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) ) )
136 113 135 mpd ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝑘 ≤ 𝑗 → ( abs ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝑏 ) )
137 16 33 112 136 limsupre ⊢ ( 𝜑 → ( lim sup ‘ 𝑆 ) ∈ ℝ )
138 137 recnd ⊢ ( 𝜑 → ( lim sup ‘ 𝑆 ) ∈ ℂ )
139 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑗 ∈ ℝ )
140 139 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ∈ ℝ )
141 0red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ∈ ℝ )
142 52 peano2zd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ∈ ℤ )
143 8 142 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
144 143 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
145 144 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℝ )
146 145 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℝ )
147 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < 𝑀 )
148 ioomidp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) )
149 1 2 3 148 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) )
150 ne0i ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
151 149 150 syl ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
152 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
153 152 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
154 dvfre ⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
155 4 153 154 syl2anc ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
156 5 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
157 155 156 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
158 157 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
159 158 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
160 159 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ℝ )
161 eqid ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
162 eqid ⊢ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < )
163 151 160 6 161 162 suprnmpt ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ∈ ℝ ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ) )
164 163 simpld ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ∈ ℝ )
165 7 164 eqeltrid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
166 165 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑌 ∈ ℝ )
167 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
168 167 rehalfcld ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ )
169 168 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ )
170 167 recnd ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
171 170 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
172 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
173 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
174 173 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
175 2ne0 ⊢ 2 ≠ 0
176 175 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ≠ 0 )
177 171 172 174 176 divne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ≠ 0 )
178 166 169 177 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑌 / ( 𝑥 / 2 ) ) ∈ ℝ )
179 178 flcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) ∈ ℤ )
180 179 peano2zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ∈ ℤ )
181 180 144 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 ) ∈ ℤ )
182 11 181 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℤ )
183 182 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℝ )
184 183 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
185 180 zred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ∈ ℝ )
186 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 ) )
187 145 185 186 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 ) )
188 187 11 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ≤ 𝑁 )
189 188 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ≤ 𝑁 )
190 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑗 )
191 190 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑗 )
192 146 184 140 189 191 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ≤ 𝑗 )
193 141 146 140 147 192 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < 𝑗 )
194 193 gt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑗 ≠ 0 )
195 140 194 rereccld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 1 / 𝑗 ) ∈ ℝ )
196 140 193 recgt0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 < ( 1 / 𝑗 ) )
197 195 196 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 1 / 𝑗 ) ∈ ℝ+ )
198 197 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) → ( 1 / 𝑗 ) ∈ ℝ+ )
199 12 biimpi ⊢ ( 𝜒 → ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) )
200 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → 𝜑 )
201 199 200 syl ⊢ ( 𝜒 → 𝜑 )
202 201 4 syl ⊢ ( 𝜒 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
203 199 simplrd ⊢ ( 𝜒 → 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
204 202 203 ffvelcdmd ⊢ ( 𝜒 → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
205 204 recnd ⊢ ( 𝜒 → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
206 201 112 syl ⊢ ( 𝜒 → 𝑆 : ( ℤ≥ ‘ 𝑀 ) ⟶ ℝ )
207 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → 𝑥 ∈ ℝ+ )
208 199 207 syl ⊢ ( 𝜒 → 𝑥 ∈ ℝ+ )
209 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
210 144 182 188 209 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
211 201 208 210 syl2anc ⊢ ( 𝜒 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
212 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
213 211 212 syl ⊢ ( 𝜒 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
214 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
215 199 214 syl ⊢ ( 𝜒 → 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
216 213 215 sseldd ⊢ ( 𝜒 → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
217 206 216 ffvelcdmd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
218 217 recnd ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
219 201 138 syl ⊢ ( 𝜒 → ( lim sup ‘ 𝑆 ) ∈ ℂ )
220 205 218 219 npncand ⊢ ( 𝜒 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) )
221 220 eqcomd ⊢ ( 𝜒 → ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) )
222 221 fveq2d ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) )
223 204 217 resubcld ⊢ ( 𝜒 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
224 201 137 syl ⊢ ( 𝜒 → ( lim sup ‘ 𝑆 ) ∈ ℝ )
225 217 224 resubcld ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ∈ ℝ )
226 223 225 readdcld ⊢ ( 𝜒 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ∈ ℝ )
227 226 recnd ⊢ ( 𝜒 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ∈ ℂ )
228 227 abscld ⊢ ( 𝜒 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) ∈ ℝ )
229 223 recnd ⊢ ( 𝜒 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
230 229 abscld ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
231 225 recnd ⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ∈ ℂ )
232 231 abscld ⊢ ( 𝜒 → ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ∈ ℝ )
233 230 232 readdcld ⊢ ( 𝜒 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) + ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) ∈ ℝ )
234 208 rpred ⊢ ( 𝜒 → 𝑥 ∈ ℝ )
235 229 231 abstrid ⊢ ( 𝜒 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) + ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) )
236 234 rehalfcld ⊢ ( 𝜒 → ( 𝑥 / 2 ) ∈ ℝ )
237 201 216 117 syl2anc ⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) = ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) )
238 237 oveq2d ⊢ ( 𝜒 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) )
239 238 fveq2d ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ) )
240 239 230 eqeltrrd ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ) ∈ ℝ )
241 201 165 syl ⊢ ( 𝜒 → 𝑌 ∈ ℝ )
242 152 203 sselid ⊢ ( 𝜒 → 𝑧 ∈ ℝ )
243 201 216 65 syl2anc ⊢ ( 𝜒 → ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ℝ )
244 242 243 resubcld ⊢ ( 𝜒 → ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ∈ ℝ )
245 241 244 remulcld ⊢ ( 𝜒 → ( 𝑌 · ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ∈ ℝ )
246 201 1 syl ⊢ ( 𝜒 → 𝐴 ∈ ℝ )
247 201 2 syl ⊢ ( 𝜒 → 𝐵 ∈ ℝ )
248 201 5 syl ⊢ ( 𝜒 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
249 163 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) )
250 7 breq2i ⊢ ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑌 ↔ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) )
251 250 ralbii ⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑌 ↔ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) )
252 249 251 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑌 )
253 201 252 syl ⊢ ( 𝜒 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑌 )
254 2fveq3 ⊢ ( 𝑤 = 𝑥 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
255 254 breq1d ⊢ ( 𝑤 = 𝑥 → ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ≤ 𝑌 ↔ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑌 ) )
256 255 cbvralvw ⊢ ( ∀ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ≤ 𝑌 ↔ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑌 )
257 253 256 sylibr ⊢ ( 𝜒 → ∀ 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑤 ) ) ≤ 𝑌 )
258 201 216 110 syl2anc ⊢ ( 𝜒 → ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ( 𝐴 (,) 𝐵 ) )
259 243 rexrd ⊢ ( 𝜒 → ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ℝ* )
260 201 37 syl ⊢ ( 𝜒 → 𝐵 ∈ ℝ* )
261 15 216 sselid ⊢ ( 𝜒 → 𝑗 ∈ ℝ )
262 201 216 63 syl2anc ⊢ ( 𝜒 → 𝑗 ≠ 0 )
263 261 262 rereccld ⊢ ( 𝜒 → ( 1 / 𝑗 ) ∈ ℝ )
264 247 242 resubcld ⊢ ( 𝜒 → ( 𝐵 − 𝑧 ) ∈ ℝ )
265 242 247 resubcld ⊢ ( 𝜒 → ( 𝑧 − 𝐵 ) ∈ ℝ )
266 265 recnd ⊢ ( 𝜒 → ( 𝑧 − 𝐵 ) ∈ ℂ )
267 266 abscld ⊢ ( 𝜒 → ( abs ‘ ( 𝑧 − 𝐵 ) ) ∈ ℝ )
268 264 leabsd ⊢ ( 𝜒 → ( 𝐵 − 𝑧 ) ≤ ( abs ‘ ( 𝐵 − 𝑧 ) ) )
269 201 92 syl ⊢ ( 𝜒 → 𝐵 ∈ ℂ )
270 242 recnd ⊢ ( 𝜒 → 𝑧 ∈ ℂ )
271 269 270 abssubd ⊢ ( 𝜒 → ( abs ‘ ( 𝐵 − 𝑧 ) ) = ( abs ‘ ( 𝑧 − 𝐵 ) ) )
272 268 271 breqtrd ⊢ ( 𝜒 → ( 𝐵 − 𝑧 ) ≤ ( abs ‘ ( 𝑧 − 𝐵 ) ) )
273 199 simprd ⊢ ( 𝜒 → ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) )
274 264 267 263 272 273 lelttrd ⊢ ( 𝜒 → ( 𝐵 − 𝑧 ) < ( 1 / 𝑗 ) )
275 247 242 263 274 ltsub23d ⊢ ( 𝜒 → ( 𝐵 − ( 1 / 𝑗 ) ) < 𝑧 )
276 201 35 syl ⊢ ( 𝜒 → 𝐴 ∈ ℝ* )
277 iooltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑧 < 𝐵 )
278 276 260 203 277 syl3anc ⊢ ( 𝜒 → 𝑧 < 𝐵 )
279 259 260 242 275 278 eliood ⊢ ( 𝜒 → 𝑧 ∈ ( ( 𝐵 − ( 1 / 𝑗 ) ) (,) 𝐵 ) )
280 246 247 202 248 241 257 258 279 dvbdfbdioolem1 ⊢ ( 𝜒 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ) ≤ ( 𝑌 · ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ) ≤ ( 𝑌 · ( 𝐵 − 𝐴 ) ) ) )
281 280 simpld ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ) ≤ ( 𝑌 · ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ) )
282 201 216 64 syl2anc ⊢ ( 𝜒 → ( 1 / 𝑗 ) ∈ ℝ )
283 241 282 remulcld ⊢ ( 𝜒 → ( 𝑌 · ( 1 / 𝑗 ) ) ∈ ℝ )
284 157 149 ffvelcdmd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℝ )
285 284 recnd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
286 285 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
287 285 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) )
288 2fveq3 ⊢ ( 𝑥 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) )
289 7 eqcomi ⊢ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) = 𝑌
290 289 a1i ⊢ ( 𝑥 = ( ( 𝐴 + 𝐵 ) / 2 ) → sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) = 𝑌 )
291 288 290 breq12d ⊢ ( 𝑥 = ( ( 𝐴 + 𝐵 ) / 2 ) → ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ↔ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ≤ 𝑌 ) )
292 291 rspcva ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ≤ 𝑌 )
293 149 249 292 syl2anc ⊢ ( 𝜑 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ≤ 𝑌 )
294 22 286 165 287 293 letrd ⊢ ( 𝜑 → 0 ≤ 𝑌 )
295 201 294 syl ⊢ ( 𝜒 → 0 ≤ 𝑌 )
296 282 recnd ⊢ ( 𝜒 → ( 1 / 𝑗 ) ∈ ℂ )
297 sub31 ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 1 / 𝑗 ) ∈ ℂ ) → ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) = ( ( 1 / 𝑗 ) − ( 𝐵 − 𝑧 ) ) )
298 270 269 296 297 syl3anc ⊢ ( 𝜒 → ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) = ( ( 1 / 𝑗 ) − ( 𝐵 − 𝑧 ) ) )
299 242 247 posdifd ⊢ ( 𝜒 → ( 𝑧 < 𝐵 ↔ 0 < ( 𝐵 − 𝑧 ) ) )
300 278 299 mpbid ⊢ ( 𝜒 → 0 < ( 𝐵 − 𝑧 ) )
301 264 300 elrpd ⊢ ( 𝜒 → ( 𝐵 − 𝑧 ) ∈ ℝ+ )
302 282 301 ltsubrpd ⊢ ( 𝜒 → ( ( 1 / 𝑗 ) − ( 𝐵 − 𝑧 ) ) < ( 1 / 𝑗 ) )
303 298 302 eqbrtrd ⊢ ( 𝜒 → ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) < ( 1 / 𝑗 ) )
304 244 282 303 ltled ⊢ ( 𝜒 → ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ≤ ( 1 / 𝑗 ) )
305 244 282 241 295 304 lemul2ad ⊢ ( 𝜒 → ( 𝑌 · ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ≤ ( 𝑌 · ( 1 / 𝑗 ) ) )
306 283 adantr ⊢ ( ( 𝜒 ∧ 𝑌 = 0 ) → ( 𝑌 · ( 1 / 𝑗 ) ) ∈ ℝ )
307 236 adantr ⊢ ( ( 𝜒 ∧ 𝑌 = 0 ) → ( 𝑥 / 2 ) ∈ ℝ )
308 oveq1 ⊢ ( 𝑌 = 0 → ( 𝑌 · ( 1 / 𝑗 ) ) = ( 0 · ( 1 / 𝑗 ) ) )
309 296 mul02d ⊢ ( 𝜒 → ( 0 · ( 1 / 𝑗 ) ) = 0 )
310 308 309 sylan9eqr ⊢ ( ( 𝜒 ∧ 𝑌 = 0 ) → ( 𝑌 · ( 1 / 𝑗 ) ) = 0 )
311 208 rphalfcld ⊢ ( 𝜒 → ( 𝑥 / 2 ) ∈ ℝ+ )
312 311 rpgt0d ⊢ ( 𝜒 → 0 < ( 𝑥 / 2 ) )
313 312 adantr ⊢ ( ( 𝜒 ∧ 𝑌 = 0 ) → 0 < ( 𝑥 / 2 ) )
314 310 313 eqbrtrd ⊢ ( ( 𝜒 ∧ 𝑌 = 0 ) → ( 𝑌 · ( 1 / 𝑗 ) ) < ( 𝑥 / 2 ) )
315 306 307 314 ltled ⊢ ( ( 𝜒 ∧ 𝑌 = 0 ) → ( 𝑌 · ( 1 / 𝑗 ) ) ≤ ( 𝑥 / 2 ) )
316 241 adantr ⊢ ( ( 𝜒 ∧ ¬ 𝑌 = 0 ) → 𝑌 ∈ ℝ )
317 295 adantr ⊢ ( ( 𝜒 ∧ ¬ 𝑌 = 0 ) → 0 ≤ 𝑌 )
318 neqne ⊢ ( ¬ 𝑌 = 0 → 𝑌 ≠ 0 )
319 318 adantl ⊢ ( ( 𝜒 ∧ ¬ 𝑌 = 0 ) → 𝑌 ≠ 0 )
320 316 317 319 ne0gt0d ⊢ ( ( 𝜒 ∧ ¬ 𝑌 = 0 ) → 0 < 𝑌 )
321 283 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / 𝑗 ) ) ∈ ℝ )
322 15 211 sselid ⊢ ( 𝜒 → 𝑁 ∈ ℝ )
323 0red ⊢ ( 𝜒 → 0 ∈ ℝ )
324 201 208 145 syl2anc ⊢ ( 𝜒 → 𝑀 ∈ ℝ )
325 201 72 syl ⊢ ( 𝜒 → 0 < 𝑀 )
326 201 208 188 syl2anc ⊢ ( 𝜒 → 𝑀 ≤ 𝑁 )
327 323 324 322 325 326 ltletrd ⊢ ( 𝜒 → 0 < 𝑁 )
328 327 gt0ne0d ⊢ ( 𝜒 → 𝑁 ≠ 0 )
329 322 328 rereccld ⊢ ( 𝜒 → ( 1 / 𝑁 ) ∈ ℝ )
330 241 329 remulcld ⊢ ( 𝜒 → ( 𝑌 · ( 1 / 𝑁 ) ) ∈ ℝ )
331 330 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / 𝑁 ) ) ∈ ℝ )
332 236 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑥 / 2 ) ∈ ℝ )
333 282 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 1 / 𝑗 ) ∈ ℝ )
334 329 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 1 / 𝑁 ) ∈ ℝ )
335 241 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 𝑌 ∈ ℝ )
336 295 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 0 ≤ 𝑌 )
337 322 327 elrpd ⊢ ( 𝜒 → 𝑁 ∈ ℝ+ )
338 201 216 101 syl2anc ⊢ ( 𝜒 → 𝑗 ∈ ℝ+ )
339 1red ⊢ ( 𝜒 → 1 ∈ ℝ )
340 103 a1i ⊢ ( 𝜒 → 0 ≤ 1 )
341 215 190 syl ⊢ ( 𝜒 → 𝑁 ≤ 𝑗 )
342 337 338 339 340 341 lediv2ad ⊢ ( 𝜒 → ( 1 / 𝑗 ) ≤ ( 1 / 𝑁 ) )
343 342 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 1 / 𝑗 ) ≤ ( 1 / 𝑁 ) )
344 333 334 335 336 343 lemul2ad ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / 𝑗 ) ) ≤ ( 𝑌 · ( 1 / 𝑁 ) ) )
345 234 recnd ⊢ ( 𝜒 → 𝑥 ∈ ℂ )
346 2cnd ⊢ ( 𝜒 → 2 ∈ ℂ )
347 208 rpne0d ⊢ ( 𝜒 → 𝑥 ≠ 0 )
348 175 a1i ⊢ ( 𝜒 → 2 ≠ 0 )
349 345 346 347 348 divne0d ⊢ ( 𝜒 → ( 𝑥 / 2 ) ≠ 0 )
350 241 236 349 redivcld ⊢ ( 𝜒 → ( 𝑌 / ( 𝑥 / 2 ) ) ∈ ℝ )
351 350 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑥 / 2 ) ) ∈ ℝ )
352 simpr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 0 < 𝑌 )
353 312 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 0 < ( 𝑥 / 2 ) )
354 335 332 352 353 divgt0d ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 0 < ( 𝑌 / ( 𝑥 / 2 ) ) )
355 351 354 elrpd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑥 / 2 ) ) ∈ ℝ+ )
356 355 rprecred ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 1 / ( 𝑌 / ( 𝑥 / 2 ) ) ) ∈ ℝ )
357 337 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 𝑁 ∈ ℝ+ )
358 1red ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 1 ∈ ℝ )
359 103 a1i ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 0 ≤ 1 )
360 350 flcld ⊢ ( 𝜒 → ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) ∈ ℤ )
361 360 peano2zd ⊢ ( 𝜒 → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ∈ ℤ )
362 361 zred ⊢ ( 𝜒 → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ∈ ℝ )
363 201 143 syl ⊢ ( 𝜒 → 𝑀 ∈ ℤ )
364 361 363 ifcld ⊢ ( 𝜒 → if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 ) ∈ ℤ )
365 11 364 eqeltrid ⊢ ( 𝜒 → 𝑁 ∈ ℤ )
366 365 zred ⊢ ( 𝜒 → 𝑁 ∈ ℝ )
367 flltp1 ⊢ ( ( 𝑌 / ( 𝑥 / 2 ) ) ∈ ℝ → ( 𝑌 / ( 𝑥 / 2 ) ) < ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) )
368 350 367 syl ⊢ ( 𝜒 → ( 𝑌 / ( 𝑥 / 2 ) ) < ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) )
369 201 67 syl ⊢ ( 𝜒 → 𝑀 ∈ ℝ )
370 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 ) )
371 369 362 370 syl2anc ⊢ ( 𝜒 → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) , 𝑀 ) )
372 371 11 breqtrrdi ⊢ ( 𝜒 → ( ( ⌊ ‘ ( 𝑌 / ( 𝑥 / 2 ) ) ) + 1 ) ≤ 𝑁 )
373 350 362 366 368 372 ltletrd ⊢ ( 𝜒 → ( 𝑌 / ( 𝑥 / 2 ) ) < 𝑁 )
374 350 322 373 ltled ⊢ ( 𝜒 → ( 𝑌 / ( 𝑥 / 2 ) ) ≤ 𝑁 )
375 374 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑥 / 2 ) ) ≤ 𝑁 )
376 355 357 358 359 375 lediv2ad ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 1 / 𝑁 ) ≤ ( 1 / ( 𝑌 / ( 𝑥 / 2 ) ) ) )
377 334 356 335 336 376 lemul2ad ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / 𝑁 ) ) ≤ ( 𝑌 · ( 1 / ( 𝑌 / ( 𝑥 / 2 ) ) ) ) )
378 335 recnd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 𝑌 ∈ ℂ )
379 351 recnd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑥 / 2 ) ) ∈ ℂ )
380 354 gt0ne0d ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑥 / 2 ) ) ≠ 0 )
381 378 379 380 divrecd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑌 / ( 𝑥 / 2 ) ) ) = ( 𝑌 · ( 1 / ( 𝑌 / ( 𝑥 / 2 ) ) ) ) )
382 332 recnd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑥 / 2 ) ∈ ℂ )
383 352 gt0ne0d ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → 𝑌 ≠ 0 )
384 349 adantr ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑥 / 2 ) ≠ 0 )
385 378 382 383 384 ddcand ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 / ( 𝑌 / ( 𝑥 / 2 ) ) ) = ( 𝑥 / 2 ) )
386 381 385 eqtr3d ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / ( 𝑌 / ( 𝑥 / 2 ) ) ) ) = ( 𝑥 / 2 ) )
387 377 386 breqtrd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / 𝑁 ) ) ≤ ( 𝑥 / 2 ) )
388 321 331 332 344 387 letrd ⊢ ( ( 𝜒 ∧ 0 < 𝑌 ) → ( 𝑌 · ( 1 / 𝑗 ) ) ≤ ( 𝑥 / 2 ) )
389 320 388 syldan ⊢ ( ( 𝜒 ∧ ¬ 𝑌 = 0 ) → ( 𝑌 · ( 1 / 𝑗 ) ) ≤ ( 𝑥 / 2 ) )
390 315 389 pm2.61dan ⊢ ( 𝜒 → ( 𝑌 · ( 1 / 𝑗 ) ) ≤ ( 𝑥 / 2 ) )
391 245 283 236 305 390 letrd ⊢ ( 𝜒 → ( 𝑌 · ( 𝑧 − ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ≤ ( 𝑥 / 2 ) )
392 240 245 236 281 391 letrd ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ) ≤ ( 𝑥 / 2 ) )
393 239 392 eqbrtrd ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) ≤ ( 𝑥 / 2 ) )
394 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) )
395 199 394 syl ⊢ ( 𝜒 → ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) )
396 230 232 236 236 393 395 leltaddd ⊢ ( 𝜒 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) + ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) < ( ( 𝑥 / 2 ) + ( 𝑥 / 2 ) ) )
397 345 2halvesd ⊢ ( 𝜒 → ( ( 𝑥 / 2 ) + ( 𝑥 / 2 ) ) = 𝑥 )
398 396 397 breqtrd ⊢ ( 𝜒 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) ) + ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) < 𝑥 )
399 228 233 234 235 398 lelttrd ⊢ ( 𝜒 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) ) < 𝑥 )
400 222 399 eqbrtrd ⊢ ( 𝜒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 )
401 12 400 sylbir ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 )
402 401 adantrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 )
403 402 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) )
404 403 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) )
405 brimralrspcev ⊢ ( ( ( 1 / 𝑗 ) ∈ ℝ+ ∧ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < ( 1 / 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) )
406 198 404 405 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) )
407 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ≤ 𝑁 ) → 𝑏 ≤ 𝑁 )
408 407 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ≤ 𝑁 ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) = 𝑁 )
409 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
410 182 409 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
411 410 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ≤ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
412 408 411 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ≤ 𝑁 ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
413 412 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑏 ≤ 𝑁 ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
414 iffalse ⊢ ( ¬ 𝑏 ≤ 𝑁 → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) = 𝑏 )
415 414 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) = 𝑏 )
416 182 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
417 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑏 ∈ ℤ )
418 416 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
419 417 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑏 ∈ ℝ )
420 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → ¬ 𝑏 ≤ 𝑁 )
421 418 419 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → ( 𝑁 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑁 ) )
422 420 421 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑁 < 𝑏 )
423 418 419 422 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑁 ≤ 𝑏 )
424 eluz2 ⊢ ( 𝑏 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ≤ 𝑏 ) )
425 416 417 423 424 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → 𝑏 ∈ ( ℤ≥ ‘ 𝑁 ) )
426 415 425 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ¬ 𝑏 ≤ 𝑁 ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
427 413 426 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
428 427 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
429 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) → ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
430 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
431 182 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → 𝑁 ∈ ℤ )
432 431 430 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ℤ )
433 430 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℝ )
434 431 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → 𝑁 ∈ ℝ )
435 max1 ⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑏 ≤ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) )
436 433 434 435 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → 𝑏 ≤ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) )
437 eluz2 ⊢ ( if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑏 ) ↔ ( 𝑏 ∈ ℤ ∧ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ℤ ∧ 𝑏 ≤ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) )
438 430 432 436 437 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑏 ) )
439 438 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) → if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑏 ) )
440 fveq2 ⊢ ( 𝑐 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) )
441 440 eleq1d ⊢ ( 𝑐 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ↔ ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) ∈ ℂ ) )
442 440 fvoveq1d ⊢ ( 𝑐 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) = ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) )
443 442 breq1d ⊢ ( 𝑐 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
444 441 443 anbi12d ⊢ ( 𝑐 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) )
445 444 rspccva ⊢ ( ( ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ∧ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑏 ) ) → ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
446 429 439 445 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
447 446 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) → ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) )
448 fveq2 ⊢ ( 𝑗 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) )
449 448 fvoveq1d ⊢ ( 𝑗 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) = ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) )
450 449 breq1d ⊢ ( 𝑗 = if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) → ( ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
451 450 rspcev ⊢ ( ( if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ∈ ( ℤ≥ ‘ 𝑁 ) ∧ ( abs ‘ ( ( 𝑆 ‘ if ( 𝑏 ≤ 𝑁 , 𝑁 , 𝑏 ) ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) )
452 428 447 451 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑏 ∈ ℤ ) ∧ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) )
453 ax-resscn ⊢ ℝ ⊆ ℂ
454 453 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
455 4 454 fssd ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
456 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ∧ dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) ) → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
457 454 455 153 5 456 syl31anc ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
458 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
459 454 457 458 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ↔ 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
460 4 459 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
461 110 10 fmptd ⊢ ( 𝜑 → 𝑅 : ( ℤ≥ ‘ 𝑀 ) ⟶ ( 𝐴 (,) 𝐵 ) )
462 eqid ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) )
463 climrel ⊢ Rel ⇝
464 463 a1i ⊢ ( 𝜑 → Rel ⇝ )
465 fvex ⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
466 465 mptex ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ∈ V
467 466 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ∈ V )
468 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) )
469 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑗 = 𝑚 ) → 𝐵 = 𝐵 )
470 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
471 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐵 ∈ ℝ )
472 468 469 470 471 fvmptd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ‘ 𝑚 ) = 𝐵 )
473 31 30 467 92 472 climconst ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ⇝ 𝐵 )
474 465 mptex ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐵 − ( 1 / 𝑗 ) ) ) ∈ V
475 10 474 eqeltri ⊢ 𝑅 ∈ V
476 475 a1i ⊢ ( 𝜑 → 𝑅 ∈ V )
477 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
478 elnnnn0b ⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℕ0 ∧ 0 < 𝑀 ) )
479 29 72 478 sylanbrc ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
480 divcnvg ⊢ ( ( 1 ∈ ℂ ∧ 𝑀 ∈ ℕ ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) ⇝ 0 )
481 477 479 480 syl2anc ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) ⇝ 0 )
482 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) )
483 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑗 = 𝑖 ) → 𝐵 = 𝐵 )
484 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
485 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐵 ∈ ℝ )
486 482 483 484 485 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ‘ 𝑖 ) = 𝐵 )
487 486 485 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ‘ 𝑖 ) ∈ ℝ )
488 487 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ‘ 𝑖 ) ∈ ℂ )
489 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) )
490 oveq2 ⊢ ( 𝑗 = 𝑖 → ( 1 / 𝑗 ) = ( 1 / 𝑖 ) )
491 490 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑗 = 𝑖 ) → ( 1 / 𝑗 ) = ( 1 / 𝑖 ) )
492 15 484 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℝ )
493 0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 ∈ ℝ )
494 67 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℝ )
495 72 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < 𝑀 )
496 eluzle ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑖 )
497 496 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ≤ 𝑖 )
498 493 494 492 495 497 ltletrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < 𝑖 )
499 498 gt0ne0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ≠ 0 )
500 492 499 rereccld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 / 𝑖 ) ∈ ℝ )
501 489 491 484 500 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) ‘ 𝑖 ) = ( 1 / 𝑖 ) )
502 492 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑖 ∈ ℂ )
503 502 499 reccld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 / 𝑖 ) ∈ ℂ )
504 501 503 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) ‘ 𝑖 ) ∈ ℂ )
505 490 oveq2d ⊢ ( 𝑗 = 𝑖 → ( 𝐵 − ( 1 / 𝑗 ) ) = ( 𝐵 − ( 1 / 𝑖 ) ) )
506 ovex ⊢ ( 𝐵 − ( 1 / 𝑖 ) ) ∈ V
507 505 10 506 fvmpt ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑅 ‘ 𝑖 ) = ( 𝐵 − ( 1 / 𝑖 ) ) )
508 507 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑅 ‘ 𝑖 ) = ( 𝐵 − ( 1 / 𝑖 ) ) )
509 486 501 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ‘ 𝑖 ) − ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) ‘ 𝑖 ) ) = ( 𝐵 − ( 1 / 𝑖 ) ) )
510 508 509 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑅 ‘ 𝑖 ) = ( ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ 𝐵 ) ‘ 𝑖 ) − ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 1 / 𝑗 ) ) ‘ 𝑖 ) ) )
511 31 30 473 476 481 488 504 510 climsub ⊢ ( 𝜑 → 𝑅 ⇝ ( 𝐵 − 0 ) )
512 92 subid1d ⊢ ( 𝜑 → ( 𝐵 − 0 ) = 𝐵 )
513 511 512 breqtrd ⊢ ( 𝜑 → 𝑅 ⇝ 𝐵 )
514 releldm ⊢ ( ( Rel ⇝ ∧ 𝑅 ⇝ 𝐵 ) → 𝑅 ∈ dom ⇝ )
515 464 513 514 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ dom ⇝ )
516 fveq2 ⊢ ( 𝑙 = 𝑘 → ( ℤ≥ ‘ 𝑙 ) = ( ℤ≥ ‘ 𝑘 ) )
517 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑅 ‘ 𝑙 ) = ( 𝑅 ‘ 𝑘 ) )
518 517 oveq2d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) = ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) )
519 518 fveq2d ⊢ ( 𝑙 = 𝑘 → ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) ) = ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) )
520 519 breq1d ⊢ ( 𝑙 = 𝑘 → ( ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
521 516 520 raleqbidv ⊢ ( 𝑙 = 𝑘 → ( ∀ ℎ ∈ ( ℤ≥ ‘ 𝑙 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
522 521 cbvrabv ⊢ { 𝑙 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑙 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } = { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) }
523 fveq2 ⊢ ( ℎ = 𝑖 → ( 𝑅 ‘ ℎ ) = ( 𝑅 ‘ 𝑖 ) )
524 523 fvoveq1d ⊢ ( ℎ = 𝑖 → ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) )
525 524 breq1d ⊢ ( ℎ = 𝑖 → ( ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) )
526 525 cbvralvw ⊢ ( ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
527 526 rgenw ⊢ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) )
528 rabbi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) ) ↔ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } = { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } )
529 527 528 mpbi ⊢ { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } = { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) }
530 522 529 eqtri ⊢ { 𝑙 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑙 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } = { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) }
531 530 infeq1i ⊢ inf ( { 𝑙 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ ℎ ∈ ( ℤ≥ ‘ 𝑙 ) ( abs ‘ ( ( 𝑅 ‘ ℎ ) − ( 𝑅 ‘ 𝑙 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } , ℝ , < ) = inf ( { 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∣ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( abs ‘ ( ( 𝑅 ‘ 𝑖 ) − ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝑥 / ( sup ( ran ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) , ℝ , < ) + 1 ) ) } , ℝ , < )
532 1 2 3 460 5 6 30 461 462 515 531 ioodvbdlimc1lem1 ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ) ⇝ ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ) ) )
533 10 fvmpt2 ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐵 − ( 1 / 𝑗 ) ) ∈ ℝ ) → ( 𝑅 ‘ 𝑗 ) = ( 𝐵 − ( 1 / 𝑗 ) ) )
534 115 65 533 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑅 ‘ 𝑗 ) = ( 𝐵 − ( 1 / 𝑗 ) ) )
535 534 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐵 − ( 1 / 𝑗 ) ) = ( 𝑅 ‘ 𝑗 ) )
536 535 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) )
537 536 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ) )
538 9 537 eqtrid ⊢ ( 𝜑 → 𝑆 = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ) )
539 538 fveq2d ⊢ ( 𝜑 → ( lim sup ‘ 𝑆 ) = ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝑅 ‘ 𝑗 ) ) ) ) )
540 532 538 539 3brtr4d ⊢ ( 𝜑 → 𝑆 ⇝ ( lim sup ‘ 𝑆 ) )
541 465 mptex ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ ( 𝐹 ‘ ( 𝐵 − ( 1 / 𝑗 ) ) ) ) ∈ V
542 9 541 eqeltri ⊢ 𝑆 ∈ V
543 542 a1i ⊢ ( 𝜑 → 𝑆 ∈ V )
544 eqidd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ℤ ) → ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑐 ) )
545 543 544 clim ⊢ ( 𝜑 → ( 𝑆 ⇝ ( lim sup ‘ 𝑆 ) ↔ ( ( lim sup ‘ 𝑆 ) ∈ ℂ ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) ) ) )
546 540 545 mpbid ⊢ ( 𝜑 → ( ( lim sup ‘ 𝑆 ) ∈ ℂ ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) ) )
547 546 simprd ⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) )
548 547 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) )
549 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
550 549 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
551 breq2 ⊢ ( 𝑎 = ( 𝑥 / 2 ) → ( ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ↔ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
552 551 anbi2d ⊢ ( 𝑎 = ( 𝑥 / 2 ) → ( ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) ↔ ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) )
553 552 rexralbidv ⊢ ( 𝑎 = ( 𝑥 / 2 ) → ( ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) ↔ ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) ) )
554 553 rspccva ⊢ ( ( ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑎 ) ∧ ( 𝑥 / 2 ) ∈ ℝ+ ) → ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
555 548 550 554 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑏 ∈ ℤ ∀ 𝑐 ∈ ( ℤ≥ ‘ 𝑏 ) ( ( 𝑆 ‘ 𝑐 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝑆 ‘ 𝑐 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) ) )
556 452 555 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( 𝑆 ‘ 𝑗 ) − ( lim sup ‘ 𝑆 ) ) ) < ( 𝑥 / 2 ) )
557 406 556 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) )
558 557 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) )
559 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
560 559 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
561 455 560 92 ellimc3 ⊢ ( 𝜑 → ( ( lim sup ‘ 𝑆 ) ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( ( lim sup ‘ 𝑆 ) ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( lim sup ‘ 𝑆 ) ) ) < 𝑥 ) ) ) )
562 138 558 561 mpbir2and ⊢ ( 𝜑 → ( lim sup ‘ 𝑆 ) ∈ ( 𝐹 limℂ 𝐵 ) )