Step | Hyp | Ref
| Expression |
1 | | climcn2.7 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) |
2 | | climcn2.1 |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | | climcn2.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | 3 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ 𝑀 ∈
ℤ) |
5 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ 𝑦 ∈
ℝ+) |
6 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
7 | | climcn2.5a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ⇝ 𝐴) |
8 | 7 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ 𝐺 ⇝ 𝐴) |
9 | 2, 4, 5, 6, 8 | climi2 15072 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦) |
10 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ 𝑧 ∈
ℝ+) |
11 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐻‘𝑘)) |
12 | | climcn2.5b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ⇝ 𝐵) |
13 | 12 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ 𝐻 ⇝ 𝐵) |
14 | 2, 4, 10, 11, 13 | climi2 15072 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) |
15 | 2 | rexanuz2 14913 |
. . . . . . . 8
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧)) |
16 | 9, 14, 15 | sylanbrc 586 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧)) |
17 | 2 | uztrn2 12457 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
18 | | climcn2.8a |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐶) |
19 | | climcn2.8b |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) ∈ 𝐷) |
20 | | fvoveq1 7236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝐺‘𝑘) → (abs‘(𝑢 − 𝐴)) = (abs‘((𝐺‘𝑘) − 𝐴))) |
21 | 20 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝐺‘𝑘) → ((abs‘(𝑢 − 𝐴)) < 𝑦 ↔ (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦)) |
22 | 21 | anbi1d 633 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝐺‘𝑘) → (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) ↔ ((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧))) |
23 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝐺‘𝑘) → (𝑢𝐹𝑣) = ((𝐺‘𝑘)𝐹𝑣)) |
24 | 23 | fvoveq1d 7235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝐺‘𝑘) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) = (abs‘(((𝐺‘𝑘)𝐹𝑣) − (𝐴𝐹𝐵)))) |
25 | 24 | breq1d 5063 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝐺‘𝑘) → ((abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥 ↔ (abs‘(((𝐺‘𝑘)𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) |
26 | 22, 25 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝐺‘𝑘) → ((((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) ↔ (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥))) |
27 | | fvoveq1 7236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐻‘𝑘) → (abs‘(𝑣 − 𝐵)) = (abs‘((𝐻‘𝑘) − 𝐵))) |
28 | 27 | breq1d 5063 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐻‘𝑘) → ((abs‘(𝑣 − 𝐵)) < 𝑧 ↔ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧)) |
29 | 28 | anbi2d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐻‘𝑘) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) ↔ ((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧))) |
30 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐻‘𝑘) → ((𝐺‘𝑘)𝐹𝑣) = ((𝐺‘𝑘)𝐹(𝐻‘𝑘))) |
31 | 30 | fvoveq1d 7235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐻‘𝑘) → (abs‘(((𝐺‘𝑘)𝐹𝑣) − (𝐴𝐹𝐵))) = (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵)))) |
32 | 31 | breq1d 5063 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐻‘𝑘) → ((abs‘(((𝐺‘𝑘)𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥 ↔ (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
33 | 29, 32 | imbi12d 348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝐻‘𝑘) → ((((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) ↔ (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥))) |
34 | 26, 33 | rspc2v 3547 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺‘𝑘) ∈ 𝐶 ∧ (𝐻‘𝑘) ∈ 𝐷) → (∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥))) |
35 | 18, 19, 34 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥))) |
36 | 35 | imp 410 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
37 | 36 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) ∧ 𝑘 ∈ 𝑍) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
38 | 17, 37 | sylan2 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
39 | 38 | anassrs 471 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → (abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
40 | 39 | ralimdva 3100 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
41 | 40 | reximdva 3193 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
42 | 41 | ex 416 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥))) |
43 | 42 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ (∀𝑢 ∈
𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦 ∧ (abs‘((𝐻‘𝑘) − 𝐵)) < 𝑧) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥))) |
44 | 16, 43 | mpid 44 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+))
→ (∀𝑢 ∈
𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
45 | 44 | rexlimdvva 3213 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
46 | 45 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (((abs‘(𝑢 − 𝐴)) < 𝑦 ∧ (abs‘(𝑣 − 𝐵)) < 𝑧) → (abs‘((𝑢𝐹𝑣) − (𝐴𝐹𝐵))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
47 | 1, 46 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥) |
48 | 47 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥) |
49 | | climcn2.6 |
. . 3
⊢ (𝜑 → 𝐾 ∈ 𝑊) |
50 | | climcn2.9 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐾‘𝑘) = ((𝐺‘𝑘)𝐹(𝐻‘𝑘))) |
51 | | climcn2.4 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷)) → (𝑢𝐹𝑣) ∈ ℂ) |
52 | | climcn2.3a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
53 | | climcn2.3b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
54 | 51, 52, 53 | caovcld 7401 |
. . 3
⊢ (𝜑 → (𝐴𝐹𝐵) ∈ ℂ) |
55 | 18, 19 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘) ∈ 𝐶 ∧ (𝐻‘𝑘) ∈ 𝐷)) |
56 | 51 | ralrimivva 3112 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (𝑢𝐹𝑣) ∈ ℂ) |
57 | 56 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (𝑢𝐹𝑣) ∈ ℂ) |
58 | 23 | eleq1d 2822 |
. . . . 5
⊢ (𝑢 = (𝐺‘𝑘) → ((𝑢𝐹𝑣) ∈ ℂ ↔ ((𝐺‘𝑘)𝐹𝑣) ∈ ℂ)) |
59 | 30 | eleq1d 2822 |
. . . . 5
⊢ (𝑣 = (𝐻‘𝑘) → (((𝐺‘𝑘)𝐹𝑣) ∈ ℂ ↔ ((𝐺‘𝑘)𝐹(𝐻‘𝑘)) ∈ ℂ)) |
60 | 58, 59 | rspc2v 3547 |
. . . 4
⊢ (((𝐺‘𝑘) ∈ 𝐶 ∧ (𝐻‘𝑘) ∈ 𝐷) → (∀𝑢 ∈ 𝐶 ∀𝑣 ∈ 𝐷 (𝑢𝐹𝑣) ∈ ℂ → ((𝐺‘𝑘)𝐹(𝐻‘𝑘)) ∈ ℂ)) |
61 | 55, 57, 60 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘)𝐹(𝐻‘𝑘)) ∈ ℂ) |
62 | 2, 3, 49, 50, 54, 61 | clim2c 15066 |
. 2
⊢ (𝜑 → (𝐾 ⇝ (𝐴𝐹𝐵) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐺‘𝑘)𝐹(𝐻‘𝑘)) − (𝐴𝐹𝐵))) < 𝑥)) |
63 | 48, 62 | mpbird 260 |
1
⊢ (𝜑 → 𝐾 ⇝ (𝐴𝐹𝐵)) |