This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mullimc

Description: Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mullimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
mullimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
mullimc.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) )
mullimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
mullimc.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
mullimc.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) )
mullimc.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 limℂ 𝐷 ) )
Assertion mullimc ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐻 limℂ 𝐷 ) )

Proof

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 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
10 limccl ⊢ ( 𝐺 limℂ 𝐷 ) ⊆ ℂ
11 10 7 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
159 30 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
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ℂ 𝐷 ) )