| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | limccl 25910 | . . . 4
⊢ (𝐹 limℂ 𝐷) ⊆
ℂ | 
| 2 |  | mullimcf.b | . . . 4
⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐷)) | 
| 3 | 1, 2 | sselid 3981 | . . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 4 |  | limccl 25910 | . . . 4
⊢ (𝐺 limℂ 𝐷) ⊆
ℂ | 
| 5 |  | mullimcf.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) | 
| 6 | 4, 5 | sselid 3981 | . . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 7 | 3, 6 | mulcld 11281 | . 2
⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ) | 
| 8 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) | 
| 9 | 3 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐵 ∈
ℂ) | 
| 10 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐶 ∈
ℂ) | 
| 11 |  | mulcn2 15632 | . . . . 5
⊢ ((𝑤 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑎 ∈
ℝ+ ∃𝑏 ∈ ℝ+ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) | 
| 12 | 8, 9, 10, 11 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑎 ∈
ℝ+ ∃𝑏 ∈ ℝ+ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) | 
| 13 |  | mullimcf.f | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 14 | 13 | fdmd 6746 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐴) | 
| 15 |  | limcrcl 25909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ (𝐹 limℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) | 
| 16 | 2, 15 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) | 
| 17 | 16 | simp2d 1144 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 ⊆ ℂ) | 
| 18 | 14, 17 | eqsstrrd 4019 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 19 | 16 | simp3d 1145 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 20 | 13, 18, 19 | ellimc3 25914 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 ∈ (𝐹 limℂ 𝐷) ↔ (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))) | 
| 21 | 2, 20 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))) | 
| 22 | 21 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑒 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) | 
| 23 | 22 | r19.21bi 3251 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ+) →
∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) | 
| 24 | 23 | adantrr 717 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) | 
| 25 |  | mullimcf.g | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:𝐴⟶ℂ) | 
| 26 | 25, 18, 19 | ellimc3 25914 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 ∈ (𝐺 limℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ+
∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) | 
| 27 | 5, 26 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ+
∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 28 | 27 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∃𝑓 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 29 | 28 | r19.21bi 3251 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ+) →
∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 30 | 29 | adantrl 716 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 31 |  | reeanv 3229 | . . . . . . . . . . 11
⊢
(∃𝑒 ∈
ℝ+ ∃𝑓 ∈ ℝ+ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ (∃𝑒 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∃𝑓 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 32 | 24, 30, 31 | sylanbrc 583 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑒 ∈
ℝ+ ∃𝑓 ∈ ℝ+ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 33 |  | ifcl 4571 | . . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈
ℝ+) | 
| 34 | 33 | 3ad2ant2 1135 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈
ℝ+) | 
| 35 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈
ℝ+)) | 
| 36 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+) | 
| 37 |  | nfra1 3284 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) | 
| 38 |  | nfra1 3284 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) | 
| 39 | 37, 38 | nfan 1899 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 40 | 35, 36, 39 | nf3an 1901 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑧((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 41 |  | simp11l 1285 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑) | 
| 42 |  | simp1rl 1239 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝑎 ∈ ℝ+) | 
| 43 | 42 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑎 ∈ ℝ+) | 
| 44 | 41, 43 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝜑 ∧ 𝑎 ∈
ℝ+)) | 
| 45 |  | simp12 1205 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) | 
| 46 |  | simp13l 1289 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) | 
| 47 | 44, 45, 46 | jca31 514 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))) | 
| 48 |  | simp1r 1199 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) | 
| 49 |  | simp2 1138 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴) | 
| 50 |  | simp3l 1202 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷) | 
| 51 |  | simplll 775 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) → 𝜑) | 
| 52 | 51 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑) | 
| 53 |  | simp1lr 1238 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) | 
| 54 |  | simp3r 1203 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) | 
| 55 |  | simp1l 1198 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝜑) | 
| 56 |  | simp2 1138 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ 𝐴) | 
| 57 | 18 | sselda 3983 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ) | 
| 58 | 55, 56, 57 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ ℂ) | 
| 59 | 55, 19 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝐷 ∈ ℂ) | 
| 60 | 58, 59 | subcld 11620 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (𝑧 − 𝐷) ∈ ℂ) | 
| 61 | 60 | abscld 15475 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) ∈ ℝ) | 
| 62 |  | rpre 13043 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ) | 
| 63 | 62 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
→ 𝑒 ∈
ℝ) | 
| 64 | 63 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑒 ∈ ℝ) | 
| 65 |  | rpre 13043 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ ℝ+
→ 𝑓 ∈
ℝ) | 
| 66 | 65 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
→ 𝑓 ∈
ℝ) | 
| 67 | 66 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑓 ∈ ℝ) | 
| 68 | 64, 67 | ifcld 4572 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ) | 
| 69 |  | simp3 1139 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) | 
| 70 |  | min1 13231 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒) | 
| 71 | 64, 67, 70 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒) | 
| 72 | 61, 68, 64, 69, 71 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑒) | 
| 73 | 52, 53, 49, 54, 72 | syl211anc 1378 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑒) | 
| 74 | 50, 73 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒)) | 
| 75 |  | rsp 3247 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))) | 
| 76 | 48, 49, 74, 75 | syl3c 66 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) | 
| 77 | 47, 76 | syld3an1 1412 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) | 
| 78 |  | simp1l 1198 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑) | 
| 79 | 78, 42 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝜑 ∧ 𝑎 ∈
ℝ+)) | 
| 80 |  | simp2 1138 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) | 
| 81 |  | simp3r 1203 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 82 | 79, 80, 81 | jca31 514 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 83 |  | simp1r 1199 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 84 |  | simp2 1138 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴) | 
| 85 |  | simp3l 1202 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷) | 
| 86 |  | simplll 775 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → 𝜑) | 
| 87 | 86 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑) | 
| 88 |  | simp1lr 1238 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) | 
| 89 |  | simp3r 1203 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) | 
| 90 |  | min2 13232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓) | 
| 91 | 64, 67, 90 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓) | 
| 92 | 61, 68, 67, 69, 91 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑓) | 
| 93 | 87, 88, 84, 89, 92 | syl211anc 1378 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑓) | 
| 94 | 85, 93 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓)) | 
| 95 |  | rsp 3247 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 96 | 83, 84, 94, 95 | syl3c 66 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) | 
| 97 | 82, 96 | syl3an1 1164 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) | 
| 98 | 77, 97 | jca 511 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 99 | 98 | 3exp 1120 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) | 
| 100 | 40, 99 | ralrimi 3257 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 101 |  | brimralrspcev 5204 | . . . . . . . . . . . . 13
⊢
((if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 102 | 34, 100, 101 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 103 | 102 | 3exp 1120 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ((𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) → ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))) | 
| 104 | 103 | rexlimdvv 3212 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (∃𝑒 ∈
ℝ+ ∃𝑓 ∈ ℝ+ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) | 
| 105 | 32, 104 | mpd 15 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 106 | 105 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 107 | 106 | 3adant3 1133 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 108 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑧(((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) | 
| 109 |  | nfra1 3284 | . . . . . . . . . . 11
⊢
Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 110 | 108, 109 | nfan 1899 | . . . . . . . . . 10
⊢
Ⅎ𝑧((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 111 |  | simp1l 1198 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → 𝜑) | 
| 112 | 111 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑) | 
| 113 | 112 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝜑) | 
| 114 |  | simp2 1138 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝑧 ∈ 𝐴) | 
| 115 |  | mullimcf.h | . . . . . . . . . . . . . . 15
⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) | 
| 116 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 117 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) | 
| 118 | 116, 117 | oveq12d 7449 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) · (𝐺‘𝑥)) = ((𝐹‘𝑧) · (𝐺‘𝑧))) | 
| 119 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) | 
| 120 | 13 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) | 
| 121 | 25 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ) | 
| 122 | 120, 121 | mulcld 11281 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ) | 
| 123 | 115, 118,
119, 122 | fvmptd3 7039 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) | 
| 124 | 123 | fvoveq1d 7453 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶)))) | 
| 125 | 113, 114,
124 | syl2anc 584 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶)))) | 
| 126 | 120, 121 | jca 511 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ)) | 
| 127 | 113, 114,
126 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ)) | 
| 128 |  | simpll3 1215 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) | 
| 129 | 128 | 3ad2ant1 1134 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) | 
| 130 |  | rsp 3247 | . . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) | 
| 131 | 130 | 3imp 1111 | . . . . . . . . . . . . . 14
⊢
((∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 132 | 131 | 3adant1l 1177 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 133 |  | fvoveq1 7454 | . . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝐹‘𝑧) → (abs‘(𝑐 − 𝐵)) = (abs‘((𝐹‘𝑧) − 𝐵))) | 
| 134 | 133 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘(𝑐 − 𝐵)) < 𝑎 ↔ (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) | 
| 135 | 134 | anbi1d 631 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝐹‘𝑧) → (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏))) | 
| 136 |  | oveq1 7438 | . . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝐹‘𝑧) → (𝑐 · 𝑑) = ((𝐹‘𝑧) · 𝑑)) | 
| 137 | 136 | fvoveq1d 7453 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝐹‘𝑧) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶)))) | 
| 138 | 137 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) | 
| 139 | 135, 138 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑐 = (𝐹‘𝑧) → ((((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤))) | 
| 140 |  | fvoveq1 7454 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(𝑑 − 𝐶)) = (abs‘((𝐺‘𝑧) − 𝐶))) | 
| 141 | 140 | breq1d 5153 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(𝑑 − 𝐶)) < 𝑏 ↔ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) | 
| 142 | 141 | anbi2d 630 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝐺‘𝑧) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) | 
| 143 |  | oveq2 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝐺‘𝑧) → ((𝐹‘𝑧) · 𝑑) = ((𝐹‘𝑧) · (𝐺‘𝑧))) | 
| 144 | 143 | fvoveq1d 7453 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶)))) | 
| 145 | 144 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)) | 
| 146 | 142, 145 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑑 = (𝐺‘𝑧) → ((((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))) | 
| 147 | 139, 146 | rspc2v 3633 | . . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))) | 
| 148 | 127, 129,
132, 147 | syl3c 66 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤) | 
| 149 | 125, 148 | eqbrtrd 5165 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤) | 
| 150 | 149 | 3exp 1120 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) | 
| 151 | 110, 150 | ralrimi 3257 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) | 
| 152 | 151 | ex 412 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) →
(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) | 
| 153 | 152 | reximdva 3168 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) | 
| 154 | 107, 153 | mpd 15 | . . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) | 
| 155 | 154 | 3exp 1120 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))) | 
| 156 | 155 | rexlimdvv 3212 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(∃𝑎 ∈
ℝ+ ∃𝑏 ∈ ℝ+ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) | 
| 157 | 12, 156 | mpd 15 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) | 
| 158 | 157 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) | 
| 159 | 13 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) | 
| 160 | 25 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℂ) | 
| 161 | 159, 160 | mulcld 11281 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) | 
| 162 | 161, 115 | fmptd 7134 | . . 3
⊢ (𝜑 → 𝐻:𝐴⟶ℂ) | 
| 163 | 162, 18, 19 | ellimc3 25914 | . 2
⊢ (𝜑 → ((𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷) ↔ ((𝐵 · 𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))) | 
| 164 | 7, 158, 163 | mpbir2and 713 | 1
⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷)) |