Step | Hyp | Ref
| Expression |
1 | | limccl 23639 |
. . . 4
⊢ (𝐹 limℂ 𝐷) ⊆
ℂ |
2 | | mullimcf.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐷)) |
3 | 1, 2 | sseldi 3601 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) |
4 | | limccl 23639 |
. . . 4
⊢ (𝐺 limℂ 𝐷) ⊆
ℂ |
5 | | mullimcf.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) |
6 | 4, 5 | sseldi 3601 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
7 | 3, 6 | mulcld 10060 |
. 2
⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ) |
8 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
9 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐵 ∈
ℂ) |
10 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝐶 ∈
ℂ) |
11 | | mulcn2 14326 |
. . . . 5
⊢ ((𝑤 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑎 ∈
ℝ+ ∃𝑏 ∈ ℝ+ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) |
12 | 8, 9, 10, 11 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑎 ∈
ℝ+ ∃𝑏 ∈ ℝ+ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) |
13 | | mullimcf.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
14 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐴) |
16 | | limcrcl 23638 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ (𝐹 limℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
18 | 17 | simp2d 1074 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 ⊆ ℂ) |
19 | 15, 18 | eqsstr3d 3640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
20 | 17 | simp3d 1075 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ ℂ) |
21 | 13, 19, 20 | ellimc3 23643 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 ∈ (𝐹 limℂ 𝐷) ↔ (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))) |
22 | 2, 21 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ+
∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))) |
23 | 22 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑎 ∈ ℝ+ ∃𝑒 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) |
24 | 23 | r19.21bi 2932 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ+) →
∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) |
25 | 24 | adantrr 753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑒 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) |
26 | | mullimcf.g |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:𝐴⟶ℂ) |
27 | 26, 19, 20 | ellimc3 23643 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 ∈ (𝐺 limℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ+
∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) |
28 | 5, 27 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ+
∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
29 | 28 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑏 ∈ ℝ+ ∃𝑓 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
30 | 29 | r19.21bi 2932 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ ℝ+) →
∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
31 | 30 | adantrl 752 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑓 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
32 | | reeanv 3107 |
. . . . . . . . . . 11
⊢
(∃𝑒 ∈
ℝ+ ∃𝑓 ∈ ℝ+ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ (∃𝑒 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∃𝑓 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
33 | 25, 31, 32 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑒 ∈
ℝ+ ∃𝑓 ∈ ℝ+ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
34 | | ifcl 4130 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈
ℝ+) |
35 | 34 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈
ℝ+) |
36 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈
ℝ+)) |
37 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+) |
38 | | nfra1 2941 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) |
39 | | nfra1 2941 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) |
40 | 38, 39 | nfan 1828 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
41 | 36, 37, 40 | nf3an 1831 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
42 | | simp11l 1172 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑) |
43 | | simp1rl 1126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝑎 ∈ ℝ+) |
44 | 43 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑎 ∈ ℝ+) |
45 | 42, 44 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝜑 ∧ 𝑎 ∈
ℝ+)) |
46 | | simp12 1092 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) |
47 | | simp13l 1176 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) |
48 | 45, 46, 47 | jca31 557 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))) |
49 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) |
50 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴) |
51 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷) |
52 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) → 𝜑) |
53 | 52 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑) |
54 | | simp1lr 1125 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) |
55 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) |
56 | | simp1l 1085 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝜑) |
57 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ 𝐴) |
58 | 19 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ) |
59 | 56, 57, 58 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ ℂ) |
60 | 56, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝐷 ∈ ℂ) |
61 | 59, 60 | subcld 10392 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (𝑧 − 𝐷) ∈ ℂ) |
62 | 61 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) ∈ ℝ) |
63 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ) |
64 | 63 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
→ 𝑒 ∈
ℝ) |
65 | 64 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑒 ∈ ℝ) |
66 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ ℝ+
→ 𝑓 ∈
ℝ) |
67 | 66 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
→ 𝑓 ∈
ℝ) |
68 | 67 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑓 ∈ ℝ) |
69 | 65, 68 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ) |
70 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) |
71 | | min1 12020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒) |
72 | 65, 68, 71 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒) |
73 | 62, 69, 65, 70, 72 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑒) |
74 | 53, 54, 50, 55, 73 | syl211anc 1332 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑒) |
75 | 51, 74 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒)) |
76 | | rsp 2929 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))) |
77 | 49, 50, 75, 76 | syl3c 66 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) |
78 | 48, 77 | syld3an1 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) |
79 | | simp1l 1085 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑) |
80 | 79, 43 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝜑 ∧ 𝑎 ∈
ℝ+)) |
81 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) |
82 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
83 | 80, 81, 82 | jca31 557 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
84 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
85 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴) |
86 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷) |
87 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ+) ∧ (𝑒 ∈ ℝ+
∧ 𝑓 ∈
ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → 𝜑) |
88 | 87 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑) |
89 | | simp1lr 1125 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ+ ∧ 𝑓 ∈
ℝ+)) |
90 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) |
91 | | min2 12021 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓) |
92 | 65, 68, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓) |
93 | 62, 69, 68, 70, 92 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑓) |
94 | 88, 89, 85, 90, 93 | syl211anc 1332 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑓) |
95 | 86, 94 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓)) |
96 | | rsp 2929 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
97 | 84, 85, 95, 96 | syl3c 66 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ+)
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) |
98 | 83, 97 | syl3an1 1359 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) |
99 | 78, 98 | jca 554 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
100 | 99 | 3exp 1264 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) |
101 | 41, 100 | ralrimi 2957 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
102 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = if(𝑒 ≤ 𝑓, 𝑒, 𝑓) → ((abs‘(𝑧 − 𝐷)) < 𝑦 ↔ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) |
103 | 102 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = if(𝑒 ≤ 𝑓, 𝑒, 𝑓) → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) ↔ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)))) |
104 | 103 | imbi1d 331 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(𝑒 ≤ 𝑓, 𝑒, 𝑓) → (((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) |
105 | 104 | ralbidv 2986 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = if(𝑒 ≤ 𝑓, 𝑒, 𝑓) → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) |
106 | 105 | rspcev 3309 |
. . . . . . . . . . . . 13
⊢
((if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ+ ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
107 | 35, 101, 106 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
∧ (𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
108 | 107 | 3exp 1264 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ((𝑒 ∈
ℝ+ ∧ 𝑓
∈ ℝ+) → ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))) |
109 | 108 | rexlimdvv 3037 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ (∃𝑒 ∈
ℝ+ ∃𝑓 ∈ ℝ+ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) |
110 | 33, 109 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+))
→ ∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
111 | 110 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
112 | 111 | 3adant3 1081 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
113 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧(((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) |
114 | | nfra1 2941 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
115 | 113, 114 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑧((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
116 | | simp1l 1085 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → 𝜑) |
117 | 116 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑) |
118 | 117 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝜑) |
119 | | simp2 1062 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝑧 ∈ 𝐴) |
120 | | mullimcf.h |
. . . . . . . . . . . . . . . . 17
⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))) |
122 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
123 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
124 | 122, 123 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) · (𝐺‘𝑥)) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
125 | 124 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑥 = 𝑧) → ((𝐹‘𝑥) · (𝐺‘𝑥)) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
126 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
127 | 13 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
128 | 26 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ) |
129 | 127, 128 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ) |
130 | 121, 125,
126, 129 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
131 | 130 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐻‘𝑧) − (𝐵 · 𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) |
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶)))) |
133 | 118, 119,
132 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶)))) |
134 | 127, 128 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ)) |
135 | 118, 119,
134 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ)) |
136 | | simpll3 1102 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) |
137 | 136 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) |
138 | | rsp 2929 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))) |
139 | 138 | 3imp 1256 |
. . . . . . . . . . . . . 14
⊢
((∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
140 | 139 | 3adant1l 1318 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
141 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝐹‘𝑧) → (𝑐 − 𝐵) = ((𝐹‘𝑧) − 𝐵)) |
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝐹‘𝑧) → (abs‘(𝑐 − 𝐵)) = (abs‘((𝐹‘𝑧) − 𝐵))) |
143 | 142 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘(𝑐 − 𝐵)) < 𝑎 ↔ (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) |
144 | 143 | anbi1d 741 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝐹‘𝑧) → (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏))) |
145 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = (𝐹‘𝑧) → (𝑐 · 𝑑) = ((𝐹‘𝑧) · 𝑑)) |
146 | 145 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝐹‘𝑧) → ((𝑐 · 𝑑) − (𝐵 · 𝐶)) = (((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) |
147 | 146 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝐹‘𝑧) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶)))) |
148 | 147 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) |
149 | 144, 148 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝐹‘𝑧) → ((((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤))) |
150 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝐺‘𝑧) → (𝑑 − 𝐶) = ((𝐺‘𝑧) − 𝐶)) |
151 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(𝑑 − 𝐶)) = (abs‘((𝐺‘𝑧) − 𝐶))) |
152 | 151 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(𝑑 − 𝐶)) < 𝑏 ↔ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) |
153 | 152 | anbi2d 740 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝐺‘𝑧) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) |
154 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝐺‘𝑧) → ((𝐹‘𝑧) · 𝑑) = ((𝐹‘𝑧) · (𝐺‘𝑧))) |
155 | 154 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝐺‘𝑧) → (((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶)) = (((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) |
156 | 155 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶)))) |
157 | 156 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)) |
158 | 153, 157 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝐺‘𝑧) → ((((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))) |
159 | 149, 158 | rspc2v 3322 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))) |
160 | 135, 137,
140, 159 | syl3c 66 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤) |
161 | 133, 160 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤) |
162 | 161 | 3exp 1264 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) |
163 | 115, 162 | ralrimi 2957 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) ∧
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) |
164 | 163 | ex 450 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ+) →
(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) |
165 | 164 | reximdva 3017 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) |
166 | 112, 165 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) |
167 | 166 | 3exp 1264 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))) |
168 | 167 | rexlimdvv 3037 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(∃𝑎 ∈
ℝ+ ∃𝑏 ∈ ℝ+ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ
(((abs‘(𝑐 −
𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))) |
169 | 12, 168 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) |
170 | 169 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)) |
171 | 13 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
172 | 26 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℂ) |
173 | 171, 172 | mulcld 10060 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
174 | 173, 120 | fmptd 6385 |
. . 3
⊢ (𝜑 → 𝐻:𝐴⟶ℂ) |
175 | 174, 19, 20 | ellimc3 23643 |
. 2
⊢ (𝜑 → ((𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷) ↔ ((𝐵 · 𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))) |
176 | 7, 170, 175 | mpbir2and 957 |
1
⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 limℂ 𝐷)) |