Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mullimcf Structured version   Visualization version   GIF version

Theorem mullimcf 42252
 Description: Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
mullimcf.f (𝜑𝐹:𝐴⟶ℂ)
mullimcf.g (𝜑𝐺:𝐴⟶ℂ)
mullimcf.h 𝐻 = (𝑥𝐴 ↦ ((𝐹𝑥) · (𝐺𝑥)))
mullimcf.b (𝜑𝐵 ∈ (𝐹 lim 𝐷))
mullimcf.c (𝜑𝐶 ∈ (𝐺 lim 𝐷))
Assertion
Ref Expression
mullimcf (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 lim 𝐷))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐷   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥
Allowed substitution hints:   𝐶(𝑥)   𝐻(𝑥)

Proof of Theorem mullimcf
Dummy variables 𝑎 𝑏 𝑒 𝑓 𝑦 𝑧 𝑤 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 24481 . . . 4 (𝐹 lim 𝐷) ⊆ ℂ
2 mullimcf.b . . . 4 (𝜑𝐵 ∈ (𝐹 lim 𝐷))
31, 2sseldi 3916 . . 3 (𝜑𝐵 ∈ ℂ)
4 limccl 24481 . . . 4 (𝐺 lim 𝐷) ⊆ ℂ
5 mullimcf.c . . . 4 (𝜑𝐶 ∈ (𝐺 lim 𝐷))
64, 5sseldi 3916 . . 3 (𝜑𝐶 ∈ ℂ)
73, 6mulcld 10654 . 2 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
8 simpr 488 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
93adantr 484 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → 𝐵 ∈ ℂ)
106adantr 484 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → 𝐶 ∈ ℂ)
11 mulcn2 14947 . . . . 5 ((𝑤 ∈ ℝ+𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑎 ∈ ℝ+𝑏 ∈ ℝ+𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
128, 9, 10, 11syl3anc 1368 . . . 4 ((𝜑𝑤 ∈ ℝ+) → ∃𝑎 ∈ ℝ+𝑏 ∈ ℝ+𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
13 mullimcf.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴⟶ℂ)
1413fdmd 6501 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐴)
15 limcrcl 24480 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (𝐹 lim 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
162, 15syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
1716simp2d 1140 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 ⊆ ℂ)
1814, 17eqsstrrd 3957 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℂ)
1916simp3d 1141 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
2013, 18, 19ellimc3 24485 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 ∈ (𝐹 lim 𝐷) ↔ (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑒 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))))
212, 20mpbid 235 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ+𝑒 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)))
2221simprd 499 . . . . . . . . . . . . 13 (𝜑 → ∀𝑎 ∈ ℝ+𝑒 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))
2322r19.21bi 3176 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ ℝ+) → ∃𝑒 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))
2423adantrr 716 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → ∃𝑒 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))
25 mullimcf.g . . . . . . . . . . . . . . . 16 (𝜑𝐺:𝐴⟶ℂ)
2625, 18, 19ellimc3 24485 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 ∈ (𝐺 lim 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ+𝑓 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))))
275, 26mpbid 235 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ+𝑓 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
2827simprd 499 . . . . . . . . . . . . 13 (𝜑 → ∀𝑏 ∈ ℝ+𝑓 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
2928r19.21bi 3176 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ ℝ+) → ∃𝑓 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
3029adantrl 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → ∃𝑓 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
31 reeanv 3323 . . . . . . . . . . 11 (∃𝑒 ∈ ℝ+𝑓 ∈ ℝ+ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ↔ (∃𝑒 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∃𝑓 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
3224, 30, 31sylanbrc 586 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → ∃𝑒 ∈ ℝ+𝑓 ∈ ℝ+ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
33 ifcl 4472 . . . . . . . . . . . . . 14 ((𝑒 ∈ ℝ+𝑓 ∈ ℝ+) → if(𝑒𝑓, 𝑒, 𝑓) ∈ ℝ+)
34333ad2ant2 1131 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → if(𝑒𝑓, 𝑒, 𝑓) ∈ ℝ+)
35 nfv 1915 . . . . . . . . . . . . . . 15 𝑧(𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+))
36 nfv 1915 . . . . . . . . . . . . . . 15 𝑧(𝑒 ∈ ℝ+𝑓 ∈ ℝ+)
37 nfra1 3186 . . . . . . . . . . . . . . . 16 𝑧𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)
38 nfra1 3186 . . . . . . . . . . . . . . . 16 𝑧𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)
3937, 38nfan 1900 . . . . . . . . . . . . . . 15 𝑧(∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
4035, 36, 39nf3an 1902 . . . . . . . . . . . . . 14 𝑧((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
41 simp11l 1281 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝜑)
42 simp1rl 1235 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → 𝑎 ∈ ℝ+)
43423ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝑎 ∈ ℝ+)
4441, 43jca 515 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (𝜑𝑎 ∈ ℝ+))
45 simp12 1201 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+𝑓 ∈ ℝ+))
46 simp13l 1285 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))
4744, 45, 46jca31 518 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)))
48 simp1r 1195 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))
49 simp2 1134 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝑧𝐴)
50 simp3l 1198 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝑧𝐷)
51 simplll 774 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) → 𝜑)
52513ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝜑)
53 simp1lr 1234 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+𝑓 ∈ ℝ+))
54 simp3r 1199 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))
55 simp1l 1194 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → 𝜑)
56 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → 𝑧𝐴)
5718sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧𝐴) → 𝑧 ∈ ℂ)
5855, 56, 57syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → 𝑧 ∈ ℂ)
5955, 19syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → 𝐷 ∈ ℂ)
6058, 59subcld 10990 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → (𝑧𝐷) ∈ ℂ)
6160abscld 14791 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → (abs‘(𝑧𝐷)) ∈ ℝ)
62 rpre 12389 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 ∈ ℝ+𝑒 ∈ ℝ)
6362ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) → 𝑒 ∈ ℝ)
64633ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → 𝑒 ∈ ℝ)
65 rpre 12389 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ∈ ℝ+𝑓 ∈ ℝ)
6665ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) → 𝑓 ∈ ℝ)
67663ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → 𝑓 ∈ ℝ)
6864, 67ifcld 4473 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → if(𝑒𝑓, 𝑒, 𝑓) ∈ ℝ)
69 simp3 1135 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))
70 min1 12574 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒𝑓, 𝑒, 𝑓) ≤ 𝑒)
7164, 67, 70syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → if(𝑒𝑓, 𝑒, 𝑓) ≤ 𝑒)
7261, 68, 64, 69, 71ltletrd 10793 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → (abs‘(𝑧𝐷)) < 𝑒)
7352, 53, 49, 54, 72syl211anc 1373 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘(𝑧𝐷)) < 𝑒)
7450, 73jca 515 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒))
75 rsp 3173 . . . . . . . . . . . . . . . . . 18 (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) → (𝑧𝐴 → ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)))
7648, 49, 74, 75syl3c 66 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)
7747, 76syld3an1 1407 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎)
78 simp1l 1194 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → 𝜑)
7978, 42jca 515 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → (𝜑𝑎 ∈ ℝ+))
80 simp2 1134 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → (𝑒 ∈ ℝ+𝑓 ∈ ℝ+))
81 simp3r 1199 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
8279, 80, 81jca31 518 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → (((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
83 simp1r 1195 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
84 simp2 1134 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝑧𝐴)
85 simp3l 1198 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝑧𝐷)
86 simplll 774 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) → 𝜑)
87863ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → 𝜑)
88 simp1lr 1234 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+𝑓 ∈ ℝ+))
89 simp3r 1199 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))
90 min2 12575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒𝑓, 𝑒, 𝑓) ≤ 𝑓)
9164, 67, 90syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → if(𝑒𝑓, 𝑒, 𝑓) ≤ 𝑓)
9261, 68, 67, 69, 91ltletrd 10793 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ 𝑧𝐴 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → (abs‘(𝑧𝐷)) < 𝑓)
9387, 88, 84, 89, 92syl211anc 1373 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘(𝑧𝐷)) < 𝑓)
9485, 93jca 515 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓))
95 rsp 3173 . . . . . . . . . . . . . . . . . 18 (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏) → (𝑧𝐴 → ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
9683, 84, 94, 95syl3c 66 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+)) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)
9782, 96syl3an1 1160 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)
9877, 97jca 515 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓))) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
99983exp 1116 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → (𝑧𝐴 → ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))))
10040, 99ralrimi 3183 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
101 brimralrspcev 5094 . . . . . . . . . . . . 13 ((if(𝑒𝑓, 𝑒, 𝑓) ∈ ℝ+ ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < if(𝑒𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
10234, 100, 101syl2anc 587 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) ∧ (𝑒 ∈ ℝ+𝑓 ∈ ℝ+) ∧ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
1031023exp 1116 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → ((𝑒 ∈ ℝ+𝑓 ∈ ℝ+) → ((∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))))
104103rexlimdvv 3255 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → (∃𝑒 ∈ ℝ+𝑓 ∈ ℝ+ (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑒) → (abs‘((𝐹𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑓) → (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))))
10532, 104mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
106105adantlr 714 . . . . . . . 8 (((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
1071063adant3 1129 . . . . . . 7 (((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
108 nfv 1915 . . . . . . . . . . 11 𝑧(((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+)
109 nfra1 3186 . . . . . . . . . . 11 𝑧𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
110108, 109nfan 1900 . . . . . . . . . 10 𝑧((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
111 simp1l 1194 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → 𝜑)
112111ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → 𝜑)
1131123ad2ant1 1130 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → 𝜑)
114 simp2 1134 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → 𝑧𝐴)
115 mullimcf.h . . . . . . . . . . . . . . 15 𝐻 = (𝑥𝐴 ↦ ((𝐹𝑥) · (𝐺𝑥)))
116 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
117 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
118116, 117oveq12d 7157 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((𝐹𝑥) · (𝐺𝑥)) = ((𝐹𝑧) · (𝐺𝑧)))
119 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐴) → 𝑧𝐴)
12013ffvelrnda 6832 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
12125ffvelrnda 6832 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝐴) → (𝐺𝑧) ∈ ℂ)
122120, 121mulcld 10654 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐴) → ((𝐹𝑧) · (𝐺𝑧)) ∈ ℂ)
123115, 118, 119, 122fvmptd3 6772 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐴) → (𝐻𝑧) = ((𝐹𝑧) · (𝐺𝑧)))
124123fvoveq1d 7161 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))))
125113, 114, 124syl2anc 587 . . . . . . . . . . . 12 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))))
126120, 121jca 515 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐴) → ((𝐹𝑧) ∈ ℂ ∧ (𝐺𝑧) ∈ ℂ))
127113, 114, 126syl2anc 587 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → ((𝐹𝑧) ∈ ℂ ∧ (𝐺𝑧) ∈ ℂ))
128 simpll3 1211 . . . . . . . . . . . . . 14 (((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
1291283ad2ant1 1130 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
130 rsp 3173 . . . . . . . . . . . . . . 15 (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) → (𝑧𝐴 → ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))))
1311303imp 1108 . . . . . . . . . . . . . 14 ((∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
1321313adant1l 1173 . . . . . . . . . . . . 13 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
133 fvoveq1 7162 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑧) → (abs‘(𝑐𝐵)) = (abs‘((𝐹𝑧) − 𝐵)))
134133breq1d 5043 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑧) → ((abs‘(𝑐𝐵)) < 𝑎 ↔ (abs‘((𝐹𝑧) − 𝐵)) < 𝑎))
135134anbi1d 632 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑧) → (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) ↔ ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏)))
136 oveq1 7146 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑧) → (𝑐 · 𝑑) = ((𝐹𝑧) · 𝑑))
137136fvoveq1d 7161 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑧) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹𝑧) · 𝑑) − (𝐵 · 𝐶))))
138137breq1d 5043 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑧) → ((abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
139135, 138imbi12d 348 . . . . . . . . . . . . . 14 (𝑐 = (𝐹𝑧) → ((((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘(((𝐹𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤)))
140 fvoveq1 7162 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝐺𝑧) → (abs‘(𝑑𝐶)) = (abs‘((𝐺𝑧) − 𝐶)))
141140breq1d 5043 . . . . . . . . . . . . . . . 16 (𝑑 = (𝐺𝑧) → ((abs‘(𝑑𝐶)) < 𝑏 ↔ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))
142141anbi2d 631 . . . . . . . . . . . . . . 15 (𝑑 = (𝐺𝑧) → (((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) ↔ ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)))
143 oveq2 7147 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝐺𝑧) → ((𝐹𝑧) · 𝑑) = ((𝐹𝑧) · (𝐺𝑧)))
144143fvoveq1d 7161 . . . . . . . . . . . . . . . 16 (𝑑 = (𝐺𝑧) → (abs‘(((𝐹𝑧) · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))))
145144breq1d 5043 . . . . . . . . . . . . . . 15 (𝑑 = (𝐺𝑧) → ((abs‘(((𝐹𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))) < 𝑤))
146142, 145imbi12d 348 . . . . . . . . . . . . . 14 (𝑑 = (𝐺𝑧) → ((((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘(((𝐹𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
147139, 146rspc2v 3584 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℂ ∧ (𝐺𝑧) ∈ ℂ) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → (((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
148127, 129, 132, 147syl3c 66 . . . . . . . . . . . 12 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → (abs‘(((𝐹𝑧) · (𝐺𝑧)) − (𝐵 · 𝐶))) < 𝑤)
149125, 148eqbrtrd 5055 . . . . . . . . . . 11 ((((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧𝐴 ∧ (𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦)) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤)
1501493exp 1116 . . . . . . . . . 10 (((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → (𝑧𝐴 → ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤)))
151110, 150ralrimi 3183 . . . . . . . . 9 (((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧ ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏))) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤))
152151ex 416 . . . . . . . 8 ((((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) → (∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) → ∀𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤)))
153152reximdva 3236 . . . . . . 7 (((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → (∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → ((abs‘((𝐹𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤)))
154107, 153mpd 15 . . . . . 6 (((𝜑𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤))
1551543exp 1116 . . . . 5 ((𝜑𝑤 ∈ ℝ+) → ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤))))
156155rexlimdvv 3255 . . . 4 ((𝜑𝑤 ∈ ℝ+) → (∃𝑎 ∈ ℝ+𝑏 ∈ ℝ+𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐𝐵)) < 𝑎 ∧ (abs‘(𝑑𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤)))
15712, 156mpd 15 . . 3 ((𝜑𝑤 ∈ ℝ+) → ∃𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤))
158157ralrimiva 3152 . 2 (𝜑 → ∀𝑤 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤))
15913ffvelrnda 6832 . . . . 5 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ ℂ)
16025ffvelrnda 6832 . . . . 5 ((𝜑𝑥𝐴) → (𝐺𝑥) ∈ ℂ)
161159, 160mulcld 10654 . . . 4 ((𝜑𝑥𝐴) → ((𝐹𝑥) · (𝐺𝑥)) ∈ ℂ)
162161, 115fmptd 6859 . . 3 (𝜑𝐻:𝐴⟶ℂ)
163162, 18, 19ellimc3 24485 . 2 (𝜑 → ((𝐵 · 𝐶) ∈ (𝐻 lim 𝐷) ↔ ((𝐵 · 𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+𝑦 ∈ ℝ+𝑧𝐴 ((𝑧𝐷 ∧ (abs‘(𝑧𝐷)) < 𝑦) → (abs‘((𝐻𝑧) − (𝐵 · 𝐶))) < 𝑤))))
1647, 158, 163mpbir2and 712 1 (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 lim 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ∀wral 3109  ∃wrex 3110   ⊆ wss 3884  ifcif 4428   class class class wbr 5033   ↦ cmpt 5113  dom cdm 5523  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139  ℂcc 10528  ℝcr 10529   · cmul 10535   < clt 10668   ≤ cle 10669   − cmin 10863  ℝ+crp 12381  abscabs 14588   limℂ climc 24468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-fz 12890  df-seq 13369  df-exp 13430  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-plusg 16573  df-mulr 16574  df-starv 16575  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-rest 16691  df-topn 16692  df-topgen 16712  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-cnfld 20095  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cnp 21836  df-xms 22930  df-ms 22931  df-limc 24472 This theorem is referenced by:  fourierdlem101  42836  fourierdlem111  42846
 Copyright terms: Public domain W3C validator