Step | Hyp | Ref
| Expression |
1 | | rlimcn3.4 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑟 ∈
ℝ+ ∃𝑠 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) |
2 | | rlimcn3.1a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝑋) |
3 | 2 | ralrimiva 3103 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ 𝑋) |
4 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ ∀𝑧 ∈
𝐴 𝐵 ∈ 𝑋) |
5 | | simprl 768 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ 𝑟 ∈
ℝ+) |
6 | | rlimcn3.3a |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝑅) |
7 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝑅) |
8 | 4, 5, 7 | rlimi 15222 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ ∃𝑎 ∈
ℝ ∀𝑧 ∈
𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟)) |
9 | | rlimcn3.1b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝑌) |
10 | 9 | ralrimiva 3103 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐶 ∈ 𝑌) |
11 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ ∀𝑧 ∈
𝐴 𝐶 ∈ 𝑌) |
12 | | simprr 770 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ 𝑠 ∈
ℝ+) |
13 | | rlimcn3.3b |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝑆) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ (𝑧 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝑆) |
15 | 11, 12, 14 | rlimi 15222 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ ∃𝑏 ∈
ℝ ∀𝑧 ∈
𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) |
16 | | reeanv 3294 |
. . . . . . . 8
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ (∀𝑧 ∈
𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ ∀𝑧 ∈ 𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) ↔ (∃𝑎 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ ∃𝑏 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠))) |
17 | | r19.26 3095 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝐴 ((𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) ↔ (∀𝑧 ∈ 𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ ∀𝑧 ∈ 𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠))) |
18 | | anim12 806 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠))) |
19 | | simplrl 774 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ 𝑧 ∈ 𝐴) → 𝑎 ∈ ℝ) |
20 | | simplrr 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ 𝑧 ∈ 𝐴) → 𝑏 ∈ ℝ) |
21 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝐴 ↦ 𝐵) = (𝑧 ∈ 𝐴 ↦ 𝐵) |
22 | 21, 2 | dmmptd 6578 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom (𝑧 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
23 | | rlimss 15211 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝑅 → dom (𝑧 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
24 | 6, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom (𝑧 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
25 | 22, 24 | eqsstrrd 3960 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
26 | 25 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
→ 𝐴 ⊆
ℝ) |
27 | 26 | sselda 3921 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
28 | | maxle 12925 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
29 | 19, 20, 27, 28 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ 𝑧 ∈ 𝐴) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧))) |
30 | 29 | imbi1d 342 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ 𝑧 ∈ 𝐴) → ((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) ↔ ((𝑎 ≤ 𝑧 ∧ 𝑏 ≤ 𝑧) → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)))) |
31 | 18, 30 | syl5ibr 245 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ 𝑧 ∈ 𝐴) → (((𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)))) |
32 | 31 | ralimdva 3108 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
→ (∀𝑧 ∈
𝐴 ((𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → ∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)))) |
33 | | ifcl 4504 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
34 | 33 | ancoms 459 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
35 | 34 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ ∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ) |
36 | 2 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴) → 𝐵 ∈ 𝑋) |
37 | 9 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ 𝑌) |
38 | 36, 37 | jca 512 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴) → (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌)) |
39 | | fvoveq1 7298 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝐵 → (abs‘(𝑢 − 𝑅)) = (abs‘(𝐵 − 𝑅))) |
40 | 39 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝐵 → ((abs‘(𝑢 − 𝑅)) < 𝑟 ↔ (abs‘(𝐵 − 𝑅)) < 𝑟)) |
41 | 40 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝐵 → (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) ↔ ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠))) |
42 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝐵 → (𝑢𝐹𝑣) = (𝐵𝐹𝑣)) |
43 | 42 | fvoveq1d 7297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝐵 → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) = (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆)))) |
44 | 43 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝐵 → ((abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥 ↔ (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) |
45 | 41, 44 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝐵 → ((((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) ↔ (((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥))) |
46 | | fvoveq1 7298 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = 𝐶 → (abs‘(𝑣 − 𝑆)) = (abs‘(𝐶 − 𝑆))) |
47 | 46 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = 𝐶 → ((abs‘(𝑣 − 𝑆)) < 𝑠 ↔ (abs‘(𝐶 − 𝑆)) < 𝑠)) |
48 | 47 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝐶 → (((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) ↔ ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠))) |
49 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = 𝐶 → (𝐵𝐹𝑣) = (𝐵𝐹𝐶)) |
50 | 49 | fvoveq1d 7297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = 𝐶 → (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) = (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆)))) |
51 | 50 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 𝐶 → ((abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥 ↔ (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
52 | 48, 51 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝐶 → ((((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) ↔ (((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
53 | 45, 52 | rspc2va 3571 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌) ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
54 | 38, 53 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴) ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
55 | 54 | imim2d 57 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ 𝑧 ∈ 𝐴) ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → ((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
56 | 55 | an32s 649 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ ∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) ∧ 𝑧 ∈ 𝐴) → ((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
57 | 56 | ralimdva 3108 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ ∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → ∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
58 | 57 | adantlr 712 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ ∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → ∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
59 | | breq1 5077 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → (𝑐 ≤ 𝑧 ↔ if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧)) |
60 | 59 | rspceaimv 3565 |
. . . . . . . . . . . . . 14
⊢
((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
61 | 35, 58, 60 | syl6an 681 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
∧ ∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
62 | 61 | ex 413 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
→ (∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → (∀𝑧 ∈ 𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))) |
63 | 62 | com23 86 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
→ (∀𝑧 ∈
𝐴 (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵 − 𝑅)) < 𝑟 ∧ (abs‘(𝐶 − 𝑆)) < 𝑠)) → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))) |
64 | 32, 63 | syld 47 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
→ (∀𝑧 ∈
𝐴 ((𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))) |
65 | 17, 64 | syl5bir 242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
∧ (𝑎 ∈ ℝ
∧ 𝑏 ∈ ℝ))
→ ((∀𝑧 ∈
𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ ∀𝑧 ∈ 𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))) |
66 | 65 | rexlimdvva 3223 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ (∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ (∀𝑧 ∈
𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ ∀𝑧 ∈ 𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))) |
67 | 16, 66 | syl5bir 242 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ ((∃𝑎 ∈
ℝ ∀𝑧 ∈
𝐴 (𝑎 ≤ 𝑧 → (abs‘(𝐵 − 𝑅)) < 𝑟) ∧ ∃𝑏 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑏 ≤ 𝑧 → (abs‘(𝐶 − 𝑆)) < 𝑠)) → (∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))) |
68 | 8, 15, 67 | mp2and 696 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ 𝑠 ∈ ℝ+))
→ (∀𝑢 ∈
𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
69 | 68 | rexlimdvva 3223 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
70 | 69 | imp 407 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((abs‘(𝑢 − 𝑅)) < 𝑟 ∧ (abs‘(𝑣 − 𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
71 | 1, 70 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑐 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
72 | 71 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) |
73 | | rlimcn3.1c |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐵𝐹𝐶) ∈ ℂ) |
74 | 73 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 (𝐵𝐹𝐶) ∈ ℂ) |
75 | | rlimcn3.2 |
. . 3
⊢ (𝜑 → (𝑅𝐹𝑆) ∈ ℂ) |
76 | 74, 25, 75 | rlim2 15205 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑐 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑐 ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))) |
77 | 72, 76 | mpbird 256 |
1
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆)) |