Metamath Proof Explorer


Theorem 0ellimcdiv

Description: If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 0ellimcdiv.f 𝐹 = ( 𝑥𝐴𝐵 )
0ellimcdiv.g 𝐺 = ( 𝑥𝐴𝐶 )
0ellimcdiv.h 𝐻 = ( 𝑥𝐴 ↦ ( 𝐵 / 𝐶 ) )
0ellimcdiv.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
0ellimcdiv.c ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
0ellimcdiv.0limf ( 𝜑 → 0 ∈ ( 𝐹 lim 𝐸 ) )
0ellimcdiv.d ( 𝜑𝐷 ∈ ( 𝐺 lim 𝐸 ) )
0ellimcdiv.dne0 ( 𝜑𝐷 ≠ 0 )
Assertion 0ellimcdiv ( 𝜑 → 0 ∈ ( 𝐻 lim 𝐸 ) )

Proof

Step Hyp Ref Expression
1 0ellimcdiv.f 𝐹 = ( 𝑥𝐴𝐵 )
2 0ellimcdiv.g 𝐺 = ( 𝑥𝐴𝐶 )
3 0ellimcdiv.h 𝐻 = ( 𝑥𝐴 ↦ ( 𝐵 / 𝐶 ) )
4 0ellimcdiv.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
5 0ellimcdiv.c ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
6 0ellimcdiv.0limf ( 𝜑 → 0 ∈ ( 𝐹 lim 𝐸 ) )
7 0ellimcdiv.d ( 𝜑𝐷 ∈ ( 𝐺 lim 𝐸 ) )
8 0ellimcdiv.dne0 ( 𝜑𝐷 ≠ 0 )
9 0cnd ( 𝜑 → 0 ∈ ℂ )
10 5 eldifad ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
11 10 2 fmptd ( 𝜑𝐺 : 𝐴 ⟶ ℂ )
12 1 4 6 limcmptdm ( 𝜑𝐴 ⊆ ℂ )
13 limcrcl ( 𝐷 ∈ ( 𝐺 lim 𝐸 ) → ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ ) )
14 7 13 syl ( 𝜑 → ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ ) )
15 14 simp3d ( 𝜑𝐸 ∈ ℂ )
16 11 12 15 ellimc3 ( 𝜑 → ( 𝐷 ∈ ( 𝐺 lim 𝐸 ) ↔ ( 𝐷 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ) ) ) )
17 7 16 mpbid ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ) ) )
18 17 simprd ( 𝜑 → ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ) )
19 17 simpld ( 𝜑𝐷 ∈ ℂ )
20 19 8 absrpcld ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℝ+ )
21 20 rphalfcld ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ+ )
22 breq2 ( 𝑦 = ( ( abs ‘ 𝐷 ) / 2 ) → ( ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) )
23 22 imbi2d ( 𝑦 = ( ( abs ‘ 𝐷 ) / 2 ) → ( ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ) ↔ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
24 23 rexralbidv ( 𝑦 = ( ( abs ‘ 𝐷 ) / 2 ) → ( ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
25 24 rspccva ( ( ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < 𝑦 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) )
26 18 21 25 syl2anc ( 𝜑 → ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) )
27 simpl1l ( ( ( ( 𝜑𝑧 ∈ ℝ+ ) ∧ ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) ) → 𝜑 )
28 simpl3 ( ( ( ( 𝜑𝑧 ∈ ℝ+ ) ∧ ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) ) → 𝑣𝐴 )
29 simpr ( ( ( ( 𝜑𝑧 ∈ ℝ+ ) ∧ ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) ) → ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) )
30 simpl2 ( ( ( ( 𝜑𝑧 ∈ ℝ+ ) ∧ ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) ) → ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
31 28 29 30 mp2d ( ( ( ( 𝜑𝑧 ∈ ℝ+ ) ∧ ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) )
32 20 rpcnd ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℂ )
33 32 2halvesd ( 𝜑 → ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) = ( abs ‘ 𝐷 ) )
34 33 eqcomd ( 𝜑 → ( abs ‘ 𝐷 ) = ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) )
35 34 oveq1d ( 𝜑 → ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) = ( ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) − ( ( abs ‘ 𝐷 ) / 2 ) ) )
36 2cnd ( 𝜑 → 2 ∈ ℂ )
37 2ne0 2 ≠ 0
38 37 a1i ( 𝜑 → 2 ≠ 0 )
39 19 36 38 absdivd ( 𝜑 → ( abs ‘ ( 𝐷 / 2 ) ) = ( ( abs ‘ 𝐷 ) / ( abs ‘ 2 ) ) )
40 2re 2 ∈ ℝ
41 40 a1i ( 𝜑 → 2 ∈ ℝ )
42 0le2 0 ≤ 2
43 42 a1i ( 𝜑 → 0 ≤ 2 )
44 41 43 absidd ( 𝜑 → ( abs ‘ 2 ) = 2 )
45 44 oveq2d ( 𝜑 → ( ( abs ‘ 𝐷 ) / ( abs ‘ 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
46 39 45 eqtr2d ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) = ( abs ‘ ( 𝐷 / 2 ) ) )
47 46 oveq2d ( 𝜑 → ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) = ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) )
48 21 rpcnd ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℂ )
49 48 48 pncand ( 𝜑 → ( ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) − ( ( abs ‘ 𝐷 ) / 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
50 35 47 49 3eqtr3rd ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) = ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) )
51 50 3ad2ant1 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) = ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) )
52 46 eqcomd ( 𝜑 → ( abs ‘ ( 𝐷 / 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
53 52 3ad2ant1 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 / 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
54 53 oveq2d ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) = ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) )
55 19 adantr ( ( 𝜑𝑣𝐴 ) → 𝐷 ∈ ℂ )
56 55 abscld ( ( 𝜑𝑣𝐴 ) → ( abs ‘ 𝐷 ) ∈ ℝ )
57 56 3adant3 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ 𝐷 ) ∈ ℝ )
58 11 ffvelrnda ( ( 𝜑𝑣𝐴 ) → ( 𝐺𝑣 ) ∈ ℂ )
59 58 3adant3 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( 𝐺𝑣 ) ∈ ℂ )
60 59 abscld ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ )
61 19 3ad2ant1 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → 𝐷 ∈ ℂ )
62 61 59 subcld ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( 𝐷 − ( 𝐺𝑣 ) ) ∈ ℂ )
63 62 abscld ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) ∈ ℝ )
64 60 63 readdcld ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( 𝐺𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) ) ∈ ℝ )
65 57 rehalfcld ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
66 60 65 readdcld ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( 𝐺𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ )
67 58 55 pncan3d ( ( 𝜑𝑣𝐴 ) → ( ( 𝐺𝑣 ) + ( 𝐷 − ( 𝐺𝑣 ) ) ) = 𝐷 )
68 67 eqcomd ( ( 𝜑𝑣𝐴 ) → 𝐷 = ( ( 𝐺𝑣 ) + ( 𝐷 − ( 𝐺𝑣 ) ) ) )
69 68 fveq2d ( ( 𝜑𝑣𝐴 ) → ( abs ‘ 𝐷 ) = ( abs ‘ ( ( 𝐺𝑣 ) + ( 𝐷 − ( 𝐺𝑣 ) ) ) ) )
70 55 58 subcld ( ( 𝜑𝑣𝐴 ) → ( 𝐷 − ( 𝐺𝑣 ) ) ∈ ℂ )
71 58 70 abstrid ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( ( 𝐺𝑣 ) + ( 𝐷 − ( 𝐺𝑣 ) ) ) ) ≤ ( ( abs ‘ ( 𝐺𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) ) )
72 69 71 eqbrtrd ( ( 𝜑𝑣𝐴 ) → ( abs ‘ 𝐷 ) ≤ ( ( abs ‘ ( 𝐺𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) ) )
73 72 3adant3 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ 𝐷 ) ≤ ( ( abs ‘ ( 𝐺𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) ) )
74 61 59 abssubd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) = ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) )
75 simp3 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) )
76 74 75 eqbrtrd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) < ( ( abs ‘ 𝐷 ) / 2 ) )
77 63 65 60 76 ltadd2dd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( 𝐺𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺𝑣 ) ) ) ) < ( ( abs ‘ ( 𝐺𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) )
78 57 64 66 73 77 lelttrd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ 𝐷 ) < ( ( abs ‘ ( 𝐺𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) )
79 58 abscld ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ )
80 79 3adant3 ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ )
81 57 65 80 ltsubaddd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) < ( abs ‘ ( 𝐺𝑣 ) ) ↔ ( abs ‘ 𝐷 ) < ( ( abs ‘ ( 𝐺𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
82 78 81 mpbird ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) < ( abs ‘ ( 𝐺𝑣 ) ) )
83 54 82 eqbrtrd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) < ( abs ‘ ( 𝐺𝑣 ) ) )
84 51 83 eqbrtrd ( ( 𝜑𝑣𝐴 ∧ ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
85 27 28 31 84 syl3anc ( ( ( ( 𝜑𝑧 ∈ ℝ+ ) ∧ ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
86 85 3exp1 ( ( 𝜑𝑧 ∈ ℝ+ ) → ( ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ) )
87 86 ralimdv2 ( ( 𝜑𝑧 ∈ ℝ+ ) → ( ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) )
88 87 reximdva ( 𝜑 → ( ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) )
89 26 88 mpd ( 𝜑 → ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) )
90 89 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) )
91 simpr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
92 19 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
93 8 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐷 ≠ 0 )
94 92 93 absrpcld ( ( 𝜑𝑦 ∈ ℝ+ ) → ( abs ‘ 𝐷 ) ∈ ℝ+ )
95 94 rphalfcld ( ( 𝜑𝑦 ∈ ℝ+ ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ+ )
96 91 95 rpmulcld ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ )
97 96 ex ( 𝜑 → ( 𝑦 ∈ ℝ+ → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ ) )
98 97 imdistani ( ( 𝜑𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ ) )
99 eleq1 ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( 𝑤 ∈ ℝ+ ↔ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ ) )
100 99 anbi2d ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( 𝜑𝑤 ∈ ℝ+ ) ↔ ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ ) ) )
101 breq2 ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ↔ ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
102 101 imbi2d ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) ↔ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) )
103 102 rexralbidv ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) ↔ ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) )
104 100 103 imbi12d ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( ( 𝜑𝑤 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) ) ↔ ( ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ) )
105 4 1 fmptd ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
106 105 12 15 ellimc3 ( 𝜑 → ( 0 ∈ ( 𝐹 lim 𝐸 ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) ) ) )
107 6 106 mpbid ( 𝜑 → ( 0 ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) ) )
108 107 simprd ( 𝜑 → ∀ 𝑤 ∈ ℝ+𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) )
109 108 r19.21bi ( ( 𝜑𝑤 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < 𝑤 ) )
110 104 109 vtoclg ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ → ( ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) )
111 96 98 110 sylc ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
112 111 3ad2ant1 ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) → ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
113 simp12 ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝑧 ∈ ℝ+ )
114 simp2 ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝑢 ∈ ℝ+ )
115 113 114 ifcld ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ∈ ℝ+ )
116 nfv 𝑣 ( 𝜑𝑦 ∈ ℝ+ )
117 nfv 𝑣 𝑧 ∈ ℝ+
118 nfra1 𝑣𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
119 116 117 118 nf3an 𝑣 ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) )
120 nfv 𝑣 𝑢 ∈ ℝ+
121 nfra1 𝑣𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
122 119 120 121 nf3an 𝑣 ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
123 simp111 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( 𝜑𝑦 ∈ ℝ+ ) )
124 simp112 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑧 ∈ ℝ+ )
125 simp12 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑢 ∈ ℝ+ )
126 123 124 125 jca31 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) )
127 simp2 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑣𝐴 )
128 simp3l ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑣𝐸 )
129 126 127 128 jca31 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) )
130 12 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐴 ⊆ ℂ )
131 130 3ad2ant1 ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) → 𝐴 ⊆ ℂ )
132 131 3ad2ant1 ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝐴 ⊆ ℂ )
133 132 3ad2ant1 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝐴 ⊆ ℂ )
134 133 127 sseldd ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑣 ∈ ℂ )
135 15 adantr ( ( 𝜑𝑦 ∈ ℝ+ ) → 𝐸 ∈ ℂ )
136 135 3ad2ant1 ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) → 𝐸 ∈ ℂ )
137 136 3ad2ant1 ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝐸 ∈ ℂ )
138 137 3ad2ant1 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝐸 ∈ ℂ )
139 134 138 subcld ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( 𝑣𝐸 ) ∈ ℂ )
140 139 abscld ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣𝐸 ) ) ∈ ℝ )
141 124 rpred ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑧 ∈ ℝ )
142 125 rpred ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑢 ∈ ℝ )
143 141 142 ifcld ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ∈ ℝ )
144 simp3r ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) )
145 min1 ( ( 𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ ) → if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ≤ 𝑧 )
146 141 142 145 syl2anc ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ≤ 𝑧 )
147 140 143 141 144 146 ltletrd ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 )
148 simp113 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) )
149 rspa ( ( ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ 𝑣𝐴 ) → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) )
150 148 127 149 syl2anc ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) )
151 128 147 150 mp2and ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
152 simp13 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
153 rspa ( ( ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣𝐴 ) → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
154 152 127 153 syl2anc ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
155 min2 ( ( 𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ ) → if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ≤ 𝑢 )
156 141 142 155 syl2anc ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ≤ 𝑢 )
157 140 143 142 144 156 ltletrd ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 )
158 128 157 jca ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) )
159 123 simpld ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → 𝜑 )
160 159 3ad2ant1 ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → 𝜑 )
161 simp12 ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → 𝑣𝐴 )
162 nfv 𝑥 ( 𝜑𝑣𝐴 )
163 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
164 1 163 nfcxfr 𝑥 𝐹
165 nfcv 𝑥 𝑣
166 164 165 nffv 𝑥 ( 𝐹𝑣 )
167 166 nfel1 𝑥 ( 𝐹𝑣 ) ∈ ℂ
168 162 167 nfim 𝑥 ( ( 𝜑𝑣𝐴 ) → ( 𝐹𝑣 ) ∈ ℂ )
169 eleq1 ( 𝑥 = 𝑣 → ( 𝑥𝐴𝑣𝐴 ) )
170 169 anbi2d ( 𝑥 = 𝑣 → ( ( 𝜑𝑥𝐴 ) ↔ ( 𝜑𝑣𝐴 ) ) )
171 fveq2 ( 𝑥 = 𝑣 → ( 𝐹𝑥 ) = ( 𝐹𝑣 ) )
172 171 eleq1d ( 𝑥 = 𝑣 → ( ( 𝐹𝑥 ) ∈ ℂ ↔ ( 𝐹𝑣 ) ∈ ℂ ) )
173 170 172 imbi12d ( 𝑥 = 𝑣 → ( ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ℂ ) ↔ ( ( 𝜑𝑣𝐴 ) → ( 𝐹𝑣 ) ∈ ℂ ) ) )
174 simpr ( ( 𝜑𝑥𝐴 ) → 𝑥𝐴 )
175 1 fvmpt2 ( ( 𝑥𝐴𝐵 ∈ ℂ ) → ( 𝐹𝑥 ) = 𝐵 )
176 174 4 175 syl2anc ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = 𝐵 )
177 176 4 eqeltrd ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ℂ )
178 168 173 177 chvarfv ( ( 𝜑𝑣𝐴 ) → ( 𝐹𝑣 ) ∈ ℂ )
179 178 subid1d ( ( 𝜑𝑣𝐴 ) → ( ( 𝐹𝑣 ) − 0 ) = ( 𝐹𝑣 ) )
180 179 eqcomd ( ( 𝜑𝑣𝐴 ) → ( 𝐹𝑣 ) = ( ( 𝐹𝑣 ) − 0 ) )
181 180 fveq2d ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( 𝐹𝑣 ) ) = ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) )
182 160 161 181 syl2anc ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → ( abs ‘ ( 𝐹𝑣 ) ) = ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) )
183 simp3 ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) )
184 simp2 ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
185 183 184 mpd ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
186 182 185 eqbrtrd ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) ) → ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
187 154 158 186 mpd3an23 ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
188 simp-7l ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝜑 )
189 simp-4r ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝑣𝐴 )
190 eldifsni ( 𝐶 ∈ ( ℂ ∖ { 0 } ) → 𝐶 ≠ 0 )
191 5 190 syl ( ( 𝜑𝑥𝐴 ) → 𝐶 ≠ 0 )
192 4 10 191 divcld ( ( 𝜑𝑥𝐴 ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
193 192 3 fmptd ( 𝜑𝐻 : 𝐴 ⟶ ℂ )
194 193 ffvelrnda ( ( 𝜑𝑣𝐴 ) → ( 𝐻𝑣 ) ∈ ℂ )
195 194 subid1d ( ( 𝜑𝑣𝐴 ) → ( ( 𝐻𝑣 ) − 0 ) = ( 𝐻𝑣 ) )
196 nfmpt1 𝑥 ( 𝑥𝐴 ↦ ( 𝐵 / 𝐶 ) )
197 3 196 nfcxfr 𝑥 𝐻
198 197 165 nffv 𝑥 ( 𝐻𝑣 )
199 nfcv 𝑥 /
200 nfmpt1 𝑥 ( 𝑥𝐴𝐶 )
201 2 200 nfcxfr 𝑥 𝐺
202 201 165 nffv 𝑥 ( 𝐺𝑣 )
203 166 199 202 nfov 𝑥 ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) )
204 198 203 nfeq 𝑥 ( 𝐻𝑣 ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) )
205 162 204 nfim 𝑥 ( ( 𝜑𝑣𝐴 ) → ( 𝐻𝑣 ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) )
206 fveq2 ( 𝑥 = 𝑣 → ( 𝐻𝑥 ) = ( 𝐻𝑣 ) )
207 fveq2 ( 𝑥 = 𝑣 → ( 𝐺𝑥 ) = ( 𝐺𝑣 ) )
208 171 207 oveq12d ( 𝑥 = 𝑣 → ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) )
209 206 208 eqeq12d ( 𝑥 = 𝑣 → ( ( 𝐻𝑥 ) = ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) ↔ ( 𝐻𝑣 ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) )
210 170 209 imbi12d ( 𝑥 = 𝑣 → ( ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑥 ) = ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) ) ↔ ( ( 𝜑𝑣𝐴 ) → ( 𝐻𝑣 ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) ) )
211 3 fvmpt2 ( ( 𝑥𝐴 ∧ ( 𝐵 / 𝐶 ) ∈ ℂ ) → ( 𝐻𝑥 ) = ( 𝐵 / 𝐶 ) )
212 174 192 211 syl2anc ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑥 ) = ( 𝐵 / 𝐶 ) )
213 176 eqcomd ( ( 𝜑𝑥𝐴 ) → 𝐵 = ( 𝐹𝑥 ) )
214 2 fvmpt2 ( ( 𝑥𝐴𝐶 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐺𝑥 ) = 𝐶 )
215 174 5 214 syl2anc ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) = 𝐶 )
216 215 eqcomd ( ( 𝜑𝑥𝐴 ) → 𝐶 = ( 𝐺𝑥 ) )
217 213 216 oveq12d ( ( 𝜑𝑥𝐴 ) → ( 𝐵 / 𝐶 ) = ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) )
218 212 217 eqtrd ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑥 ) = ( ( 𝐹𝑥 ) / ( 𝐺𝑥 ) ) )
219 205 210 218 chvarfv ( ( 𝜑𝑣𝐴 ) → ( 𝐻𝑣 ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) )
220 195 219 eqtrd ( ( 𝜑𝑣𝐴 ) → ( ( 𝐻𝑣 ) − 0 ) = ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) )
221 220 fveq2d ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) = ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) )
222 188 189 221 syl2anc ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) = ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) )
223 simp-6l ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( 𝜑𝑦 ∈ ℝ+ ) )
224 223 189 jca ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) )
225 simplr ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
226 simpr ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
227 nfcv 𝑥 0
228 202 227 nfne 𝑥 ( 𝐺𝑣 ) ≠ 0
229 162 228 nfim 𝑥 ( ( 𝜑𝑣𝐴 ) → ( 𝐺𝑣 ) ≠ 0 )
230 207 neeq1d ( 𝑥 = 𝑣 → ( ( 𝐺𝑥 ) ≠ 0 ↔ ( 𝐺𝑣 ) ≠ 0 ) )
231 170 230 imbi12d ( 𝑥 = 𝑣 → ( ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) ≠ 0 ) ↔ ( ( 𝜑𝑣𝐴 ) → ( 𝐺𝑣 ) ≠ 0 ) ) )
232 215 191 eqnetrd ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) ≠ 0 )
233 229 231 232 chvarfv ( ( 𝜑𝑣𝐴 ) → ( 𝐺𝑣 ) ≠ 0 )
234 178 58 233 absdivd ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) = ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) )
235 234 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) = ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) )
236 235 ad2antrr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) = ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) )
237 178 abscld ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( 𝐹𝑣 ) ) ∈ ℝ )
238 58 233 absne0d ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( 𝐺𝑣 ) ) ≠ 0 )
239 237 79 238 redivcld ( ( 𝜑𝑣𝐴 ) → ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ∈ ℝ )
240 239 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ∈ ℝ )
241 240 ad2antrr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ∈ ℝ )
242 rpre ( 𝑦 ∈ ℝ+𝑦 ∈ ℝ )
243 242 ad2antlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → 𝑦 ∈ ℝ )
244 21 rpred ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
245 244 ad2antrr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
246 243 245 remulcld ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ )
247 246 ad2antrr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ )
248 58 233 absrpcld ( ( 𝜑𝑣𝐴 ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ+ )
249 248 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ+ )
250 249 ad2antrr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ+ )
251 247 250 rerpdivcld ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ∈ ℝ )
252 243 ad2antrr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝑦 ∈ ℝ )
253 simp-4l ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝜑 )
254 simpllr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝑣𝐴 )
255 253 254 237 syl2anc ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐹𝑣 ) ) ∈ ℝ )
256 simpr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
257 255 247 250 256 ltdiv1dd ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) )
258 243 recnd ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → 𝑦 ∈ ℂ )
259 48 ad2antrr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℂ )
260 249 rpcnd ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℂ )
261 238 adantlr ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( abs ‘ ( 𝐺𝑣 ) ) ≠ 0 )
262 258 259 260 261 divassd ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) = ( 𝑦 · ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ) )
263 262 adantr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) = ( 𝑦 · ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ) )
264 245 249 rerpdivcld ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ∈ ℝ )
265 264 adantr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ∈ ℝ )
266 1red ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → 1 ∈ ℝ )
267 simpllr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → 𝑦 ∈ ℝ+ )
268 244 ad2antrr ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
269 1rp 1 ∈ ℝ+
270 269 a1i ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → 1 ∈ ℝ+ )
271 248 adantr ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( abs ‘ ( 𝐺𝑣 ) ) ∈ ℝ+ )
272 48 div1d ( 𝜑 → ( ( ( abs ‘ 𝐷 ) / 2 ) / 1 ) = ( ( abs ‘ 𝐷 ) / 2 ) )
273 272 ad2antrr ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / 1 ) = ( ( abs ‘ 𝐷 ) / 2 ) )
274 simpr ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
275 273 274 eqbrtrd ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / 1 ) < ( abs ‘ ( 𝐺𝑣 ) ) )
276 268 270 271 275 ltdiv23d ( ( ( 𝜑𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < 1 )
277 276 adantllr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < 1 )
278 265 266 267 277 ltmul2dd ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( 𝑦 · ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺𝑣 ) ) ) ) < ( 𝑦 · 1 ) )
279 263 278 eqbrtrd ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < ( 𝑦 · 1 ) )
280 258 mulid1d ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) → ( 𝑦 · 1 ) = 𝑦 )
281 280 adantr ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( 𝑦 · 1 ) = 𝑦 )
282 279 281 breqtrd ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < 𝑦 )
283 282 adantr ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < 𝑦 )
284 241 251 252 257 283 lttrd ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ ( 𝐹𝑣 ) ) / ( abs ‘ ( 𝐺𝑣 ) ) ) < 𝑦 )
285 236 284 eqbrtrd ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) < 𝑦 )
286 224 225 226 285 syl21anc ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐹𝑣 ) / ( 𝐺𝑣 ) ) ) < 𝑦 )
287 222 286 eqbrtrd ( ( ( ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑢 ∈ ℝ+ ) ∧ 𝑣𝐴 ) ∧ 𝑣𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 )
288 129 151 187 287 syl21anc ( ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣𝐴 ∧ ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 )
289 288 3exp ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → ( 𝑣𝐴 → ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) ) )
290 122 289 ralrimi ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) )
291 brimralrspcev ( ( if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < if ( 𝑧𝑢 , 𝑧 , 𝑢 ) ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) ) → ∃ 𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) )
292 115 290 291 syl2anc ( ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → ∃ 𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) )
293 292 rexlimdv3a ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) → ( ∃ 𝑢 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ∃ 𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) ) )
294 112 293 mpd ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ∧ ∀ 𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) ) → ∃ 𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) )
295 294 rexlimdv3a ( ( 𝜑𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺𝑣 ) ) ) → ∃ 𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) ) )
296 90 295 mpd ( ( 𝜑𝑦 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) )
297 296 ralrimiva ( 𝜑 → ∀ 𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) )
298 193 12 15 ellimc3 ( 𝜑 → ( 0 ∈ ( 𝐻 lim 𝐸 ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+𝑤 ∈ ℝ+𝑣𝐴 ( ( 𝑣𝐸 ∧ ( abs ‘ ( 𝑣𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻𝑣 ) − 0 ) ) < 𝑦 ) ) ) )
299 9 297 298 mpbir2and ( 𝜑 → 0 ∈ ( 𝐻 lim 𝐸 ) )