Step | Hyp | Ref
| Expression |
1 | | rlimadd.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
2 | | rlimadd.5 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷) |
3 | 1, 2 | rlimmptrcl 14338 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
4 | | rlimadd.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
5 | | rlimadd.6 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸) |
6 | 4, 5 | rlimmptrcl 14338 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
7 | | rlimdiv.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) |
8 | 6, 7 | reccld 10794 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐶) ∈ ℂ) |
9 | | eldifsn 4317 |
. . . . . . 7
⊢ (𝐶 ∈ (ℂ ∖ {0})
↔ (𝐶 ∈ ℂ
∧ 𝐶 ≠
0)) |
10 | 6, 7, 9 | sylanbrc 698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖
{0})) |
11 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
12 | 10, 11 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶(ℂ ∖
{0})) |
13 | | rlimcl 14234 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ) |
14 | 5, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℂ) |
15 | | rlimdiv.7 |
. . . . . 6
⊢ (𝜑 → 𝐸 ≠ 0) |
16 | | eldifsn 4317 |
. . . . . 6
⊢ (𝐸 ∈ (ℂ ∖ {0})
↔ (𝐸 ∈ ℂ
∧ 𝐸 ≠
0)) |
17 | 14, 15, 16 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (ℂ ∖
{0})) |
18 | | eldifsn 4317 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
19 | | reccl 10692 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / 𝑦) ∈
ℂ) |
20 | 18, 19 | sylbi 207 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
21 | 20 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {0})) → (1 /
𝑦) ∈
ℂ) |
22 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦)) = (𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦)) |
23 | 21, 22 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)):(ℂ ∖
{0})⟶ℂ) |
24 | | eqid 2622 |
. . . . . . . 8
⊢ (if(1
≤ ((abs‘𝐸)
· 𝑧), 1,
((abs‘𝐸) ·
𝑧)) ·
((abs‘𝐸) / 2)) =
(if(1 ≤ ((abs‘𝐸)
· 𝑧), 1,
((abs‘𝐸) ·
𝑧)) ·
((abs‘𝐸) /
2)) |
25 | 24 | reccn2 14327 |
. . . . . . 7
⊢ ((𝐸 ∈ (ℂ ∖ {0})
∧ 𝑧 ∈
ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
26 | 17, 25 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
27 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (1 / 𝑦) = (1 / 𝑣)) |
28 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (1 /
𝑣) ∈
V |
29 | 27, 22, 28 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (ℂ ∖ {0})
→ ((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝑣) = (1 / 𝑣)) |
30 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐸 → (1 / 𝑦) = (1 / 𝐸)) |
31 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (1 /
𝐸) ∈
V |
32 | 30, 22, 31 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (ℂ ∖ {0})
→ ((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝐸) = (1 / 𝐸)) |
33 | 17, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸) = (1 / 𝐸)) |
34 | 29, 33 | oveqan12rd 6670 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸)) = ((1 / 𝑣) − (1 / 𝐸))) |
35 | 34 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(abs‘(((𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) = (abs‘((1 / 𝑣) − (1 / 𝐸)))) |
36 | 35 | breq1d 4663 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
((abs‘(((𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧 ↔ (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
37 | 36 | imbi2d 330 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ((abs‘(𝑣 − 𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
38 | 37 | ralbidva 2985 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
39 | 38 | rexbidv 3052 |
. . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
40 | 39 | biimpar 502 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧)) |
41 | 26, 40 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧)) |
42 | 12, 17, 5, 23, 41 | rlimcn1 14319 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) ∘ (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇝𝑟 ((𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦))‘𝐸)) |
43 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
44 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) = (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))) |
45 | | oveq2 6658 |
. . . . 5
⊢ (𝑦 = 𝐶 → (1 / 𝑦) = (1 / 𝐶)) |
46 | 10, 43, 44, 45 | fmptco 6396 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) ∘ (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑥 ∈ 𝐴 ↦ (1 / 𝐶))) |
47 | 42, 46, 33 | 3brtr3d 4684 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐶)) ⇝𝑟 (1 / 𝐸)) |
48 | 3, 8, 2, 47 | rlimmul 14375 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (1 / 𝐶))) ⇝𝑟 (𝐷 · (1 / 𝐸))) |
49 | 3, 6, 7 | divrecd 10804 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶))) |
50 | 49 | mpteq2dva 4744 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵 · (1 / 𝐶)))) |
51 | | rlimcl 14234 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ) |
52 | 2, 51 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ ℂ) |
53 | 52, 14, 15 | divrecd 10804 |
. 2
⊢ (𝜑 → (𝐷 / 𝐸) = (𝐷 · (1 / 𝐸))) |
54 | 48, 50, 53 | 3brtr4d 4685 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) ⇝𝑟 (𝐷 / 𝐸)) |