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ℂ 𝐸 ) ) |