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 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 𝐷 ) )