Metamath Proof Explorer

Theorem ioodvbdlimc1lem2

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)

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

Proof

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