Step |
Hyp |
Ref |
Expression |
1 |
|
mullimc.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
2 |
|
mullimc.g |
⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) |
3 |
|
mullimc.h |
⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) |
4 |
|
mullimc.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
5 |
|
mullimc.c |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ ) |
6 |
|
mullimc.x |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) ) |
7 |
|
mullimc.y |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 limℂ 𝐷 ) ) |
8 |
|
limccl |
⊢ ( 𝐹 limℂ 𝐷 ) ⊆ ℂ |
9 |
8 6
|
sseldi |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
10 |
|
limccl |
⊢ ( 𝐺 limℂ 𝐷 ) ⊆ ℂ |
11 |
10 7
|
sseldi |
⊢ ( 𝜑 → 𝑌 ∈ ℂ ) |
12 |
9 11
|
mulcld |
⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ℂ ) |
13 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ ) |
14 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑋 ∈ ℂ ) |
15 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑌 ∈ ℂ ) |
16 |
|
mulcn2 |
⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
17 |
13 14 15 16
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
18 |
4 1
|
fmptd |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ ) |
19 |
1 4
|
dmmptd |
⊢ ( 𝜑 → dom 𝐹 = 𝐴 ) |
20 |
|
limcrcl |
⊢ ( 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) ) |
21 |
6 20
|
syl |
⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) ) |
22 |
21
|
simp2d |
⊢ ( 𝜑 → dom 𝐹 ⊆ ℂ ) |
23 |
19 22
|
eqsstrrd |
⊢ ( 𝜑 → 𝐴 ⊆ ℂ ) |
24 |
21
|
simp3d |
⊢ ( 𝜑 → 𝐷 ∈ ℂ ) |
25 |
18 23 24
|
ellimc3 |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) ↔ ( 𝑋 ∈ ℂ ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ) ) |
26 |
6 25
|
mpbid |
⊢ ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ) |
27 |
26
|
simprd |
⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ+ ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) |
28 |
27
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) |
29 |
28
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) |
30 |
5 2
|
fmptd |
⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ ) |
31 |
30 23 24
|
ellimc3 |
⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐺 limℂ 𝐷 ) ↔ ( 𝑌 ∈ ℂ ∧ ∀ 𝑏 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ) |
32 |
7 31
|
mpbid |
⊢ ( 𝜑 → ( 𝑌 ∈ ℂ ∧ ∀ 𝑏 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
33 |
32
|
simprd |
⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
34 |
33
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ+ ) → ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
35 |
34
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
36 |
|
reeanv |
⊢ ( ∃ 𝑒 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ↔ ( ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
37 |
29 35 36
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑒 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
38 |
|
ifcl |
⊢ ( ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ+ ) |
39 |
38
|
3ad2ant2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ+ ) |
40 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) |
41 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) |
42 |
|
nfra1 |
⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) |
43 |
|
nfra1 |
⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) |
44 |
42 43
|
nfan |
⊢ Ⅎ 𝑧 ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
45 |
40 41 44
|
nf3an |
⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
46 |
|
simp11l |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝜑 ) |
47 |
|
simp1rl |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → 𝑎 ∈ ℝ+ ) |
48 |
47
|
3ad2ant1 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑎 ∈ ℝ+ ) |
49 |
46 48
|
jca |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ) |
50 |
|
simp12 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) |
51 |
|
simp13l |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) |
52 |
49 50 51
|
jca31 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ) |
53 |
|
simp1r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) |
54 |
|
simp2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ∈ 𝐴 ) |
55 |
|
simp3l |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ≠ 𝐷 ) |
56 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) → 𝜑 ) |
57 |
56
|
3ad2ant1 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝜑 ) |
58 |
|
simp1lr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) |
59 |
|
simp3r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) |
60 |
|
simp1l |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝜑 ) |
61 |
|
simp2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑧 ∈ 𝐴 ) |
62 |
23
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℂ ) |
63 |
60 61 62
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑧 ∈ ℂ ) |
64 |
60 24
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝐷 ∈ ℂ ) |
65 |
63 64
|
subcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( 𝑧 − 𝐷 ) ∈ ℂ ) |
66 |
65
|
abscld |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) ∈ ℝ ) |
67 |
|
rpre |
⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ ) |
68 |
67
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) → 𝑒 ∈ ℝ ) |
69 |
68
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑒 ∈ ℝ ) |
70 |
|
rpre |
⊢ ( 𝑓 ∈ ℝ+ → 𝑓 ∈ ℝ ) |
71 |
70
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) → 𝑓 ∈ ℝ ) |
72 |
71
|
3ad2ant1 |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑓 ∈ ℝ ) |
73 |
69 72
|
ifcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ ) |
74 |
|
simp3 |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) |
75 |
|
min1 |
⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑒 ) |
76 |
69 72 75
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑒 ) |
77 |
66 73 69 74 76
|
ltletrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) |
78 |
57 58 54 59 77
|
syl211anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) |
79 |
55 78
|
jca |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) ) |
80 |
|
rsp |
⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ) |
81 |
53 54 79 80
|
syl3c |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) |
82 |
52 81
|
syld3an1 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) |
83 |
|
simp1l |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → 𝜑 ) |
84 |
83 47
|
jca |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ) |
85 |
|
simp2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) |
86 |
|
simp3r |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
87 |
84 85 86
|
jca31 |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
88 |
|
simp1r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
89 |
|
simp2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ∈ 𝐴 ) |
90 |
|
simp3l |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ≠ 𝐷 ) |
91 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → 𝜑 ) |
92 |
91
|
3ad2ant1 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝜑 ) |
93 |
|
simp1lr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) |
94 |
|
simp3r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) |
95 |
|
min2 |
⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑓 ) |
96 |
69 72 95
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑓 ) |
97 |
66 73 72 74 96
|
ltletrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) |
98 |
92 93 89 94 97
|
syl211anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) |
99 |
90 98
|
jca |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) ) |
100 |
|
rsp |
⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
101 |
88 89 99 100
|
syl3c |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) |
102 |
87 101
|
syl3an1 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) |
103 |
82 102
|
jca |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
104 |
103
|
3exp |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ) |
105 |
45 104
|
ralrimi |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
106 |
|
brimralrspcev |
⊢ ( ( if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
107 |
39 105 106
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
108 |
107
|
3exp |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) → ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ) ) |
109 |
108
|
rexlimdvv |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ∃ 𝑒 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ) |
110 |
37 109
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
111 |
110
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
112 |
111
|
3adant3 |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
113 |
|
nfv |
⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) |
114 |
|
nfra1 |
⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
115 |
113 114
|
nfan |
⊢ Ⅎ 𝑧 ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
116 |
|
simp1l |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → 𝜑 ) |
117 |
116
|
ad2antrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → 𝜑 ) |
118 |
117
|
3ad2ant1 |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → 𝜑 ) |
119 |
|
simp2 |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → 𝑧 ∈ 𝐴 ) |
120 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) |
121 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) |
122 |
3 121
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐻 |
123 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑧 |
124 |
122 123
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 ) |
125 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
126 |
1 125
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐹 |
127 |
126 123
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) |
128 |
|
nfcv |
⊢ Ⅎ 𝑥 · |
129 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) |
130 |
2 129
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐺 |
131 |
130 123
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑧 ) |
132 |
127 128 131
|
nfov |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) |
133 |
124 132
|
nfeq |
⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) |
134 |
120 133
|
nfim |
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) |
135 |
|
eleq1w |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) ) |
136 |
135
|
anbi2d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ) ) |
137 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑧 ) ) |
138 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) ) |
139 |
|
fveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) ) |
140 |
138 139
|
oveq12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) |
141 |
137 140
|
eqeq12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) |
142 |
136 141
|
imbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) ) |
143 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) |
144 |
4 5
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ ) |
145 |
3
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 · 𝐶 ) ) |
146 |
143 144 145
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 · 𝐶 ) ) |
147 |
1
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) |
148 |
143 4 147
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) |
149 |
148
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( 𝐹 ‘ 𝑥 ) ) |
150 |
2
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 ) |
151 |
143 5 150
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 ) |
152 |
151
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐺 ‘ 𝑥 ) ) |
153 |
149 152
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) |
154 |
146 153
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) |
155 |
134 142 154
|
chvarfv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) |
156 |
155
|
fvoveq1d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) ) |
157 |
118 119 156
|
syl2anc |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) ) |
158 |
18
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
159 |
30
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) |
160 |
158 159
|
jca |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) ) |
161 |
118 119 160
|
syl2anc |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) ) |
162 |
|
simpll3 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
163 |
162
|
3ad2ant1 |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
164 |
|
rsp |
⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ) |
165 |
164
|
3imp |
⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
166 |
165
|
3adant1l |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
167 |
|
fvoveq1 |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ ( 𝑐 − 𝑋 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) ) |
168 |
167
|
breq1d |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) |
169 |
168
|
anbi1d |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) ) ) |
170 |
|
oveq1 |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( 𝑐 · 𝑑 ) = ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) ) |
171 |
170
|
fvoveq1d |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) ) |
172 |
171
|
breq1d |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
173 |
169 172
|
imbi12d |
⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ↔ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
174 |
|
fvoveq1 |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( abs ‘ ( 𝑑 − 𝑌 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) ) |
175 |
174
|
breq1d |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) |
176 |
175
|
anbi2d |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) |
177 |
|
oveq2 |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) |
178 |
177
|
fvoveq1d |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) ) |
179 |
178
|
breq1d |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
180 |
176 179
|
imbi12d |
⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ↔ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
181 |
173 180
|
rspc2v |
⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) → ( ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
182 |
161 163 166 181
|
syl3c |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) |
183 |
157 182
|
eqbrtrd |
⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) |
184 |
183
|
3exp |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
185 |
115 184
|
ralrimi |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
186 |
185
|
ex |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
187 |
186
|
reximdva |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
188 |
112 187
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
189 |
188
|
3exp |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) ) |
190 |
189
|
rexlimdvv |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) |
191 |
17 190
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
192 |
191
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) |
193 |
144 3
|
fmptd |
⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ ℂ ) |
194 |
193 23 24
|
ellimc3 |
⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ∈ ( 𝐻 limℂ 𝐷 ) ↔ ( ( 𝑋 · 𝑌 ) ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) ) |
195 |
12 192 194
|
mpbir2and |
⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐻 limℂ 𝐷 ) ) |