Step | Hyp | Ref
| Expression |
1 | | rlimadd.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
2 | | rlimadd.5 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷) |
3 | 1, 2 | rlimmptrcl 15058 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
4 | | rlimadd.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
5 | | rlimadd.6 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸) |
6 | 4, 5 | rlimmptrcl 15058 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
7 | | rlimdiv.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) |
8 | 6, 7 | reccld 11490 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐶) ∈ ℂ) |
9 | | eldifsn 4676 |
. . . . . . 7
⊢ (𝐶 ∈ (ℂ ∖ {0})
↔ (𝐶 ∈ ℂ
∧ 𝐶 ≠
0)) |
10 | 6, 7, 9 | sylanbrc 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖
{0})) |
11 | 10 | fmpttd 6892 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶(ℂ ∖
{0})) |
12 | | rlimcl 14953 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ) |
13 | 5, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℂ) |
14 | | rlimdiv.7 |
. . . . . 6
⊢ (𝜑 → 𝐸 ≠ 0) |
15 | | eldifsn 4676 |
. . . . . 6
⊢ (𝐸 ∈ (ℂ ∖ {0})
↔ (𝐸 ∈ ℂ
∧ 𝐸 ≠
0)) |
16 | 13, 14, 15 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (ℂ ∖
{0})) |
17 | | eldifsn 4676 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
18 | | reccl 11386 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / 𝑦) ∈
ℂ) |
19 | 17, 18 | sylbi 220 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
20 | 19 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {0})) → (1 /
𝑦) ∈
ℂ) |
21 | 20 | fmpttd 6892 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)):(ℂ ∖
{0})⟶ℂ) |
22 | | eqid 2739 |
. . . . . . . 8
⊢ (if(1
≤ ((abs‘𝐸)
· 𝑧), 1,
((abs‘𝐸) ·
𝑧)) ·
((abs‘𝐸) / 2)) =
(if(1 ≤ ((abs‘𝐸)
· 𝑧), 1,
((abs‘𝐸) ·
𝑧)) ·
((abs‘𝐸) /
2)) |
23 | 22 | reccn2 15047 |
. . . . . . 7
⊢ ((𝐸 ∈ (ℂ ∖ {0})
∧ 𝑧 ∈
ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
24 | 16, 23 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
25 | | oveq2 7181 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (1 / 𝑦) = (1 / 𝑣)) |
26 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦)) = (𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦)) |
27 | | ovex 7206 |
. . . . . . . . . . . . . 14
⊢ (1 /
𝑣) ∈
V |
28 | 25, 26, 27 | fvmpt 6778 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (ℂ ∖ {0})
→ ((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝑣) = (1 / 𝑣)) |
29 | | oveq2 7181 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐸 → (1 / 𝑦) = (1 / 𝐸)) |
30 | | ovex 7206 |
. . . . . . . . . . . . . . 15
⊢ (1 /
𝐸) ∈
V |
31 | 29, 26, 30 | fvmpt 6778 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (ℂ ∖ {0})
→ ((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝐸) = (1 / 𝐸)) |
32 | 16, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸) = (1 / 𝐸)) |
33 | 28, 32 | oveqan12rd 7193 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸)) = ((1 / 𝑣) − (1 / 𝐸))) |
34 | 33 | fveq2d 6681 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(abs‘(((𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) = (abs‘((1 / 𝑣) − (1 / 𝐸)))) |
35 | 34 | breq1d 5041 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
((abs‘(((𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧 ↔ (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
36 | 35 | imbi2d 344 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ((abs‘(𝑣 − 𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
37 | 36 | ralbidva 3109 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
38 | 37 | rexbidv 3208 |
. . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
39 | 38 | biimpar 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧)) |
40 | 24, 39 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧)) |
41 | 11, 16, 5, 21, 40 | rlimcn1 15038 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) ∘ (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇝𝑟 ((𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦))‘𝐸)) |
42 | | eqidd 2740 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
43 | | eqidd 2740 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) = (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))) |
44 | | oveq2 7181 |
. . . . 5
⊢ (𝑦 = 𝐶 → (1 / 𝑦) = (1 / 𝐶)) |
45 | 10, 42, 43, 44 | fmptco 6904 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) ∘ (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑥 ∈ 𝐴 ↦ (1 / 𝐶))) |
46 | 41, 45, 32 | 3brtr3d 5062 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐶)) ⇝𝑟 (1 / 𝐸)) |
47 | 3, 8, 2, 46 | rlimmul 15096 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (1 / 𝐶))) ⇝𝑟 (𝐷 · (1 / 𝐸))) |
48 | 3, 6, 7 | divrecd 11500 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶))) |
49 | 48 | mpteq2dva 5126 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵 · (1 / 𝐶)))) |
50 | | rlimcl 14953 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ) |
51 | 2, 50 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ ℂ) |
52 | 51, 13, 14 | divrecd 11500 |
. 2
⊢ (𝜑 → (𝐷 / 𝐸) = (𝐷 · (1 / 𝐸))) |
53 | 47, 49, 52 | 3brtr4d 5063 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) ⇝𝑟 (𝐷 / 𝐸)) |