| Step | Hyp | Ref
| Expression |
| 1 | | rlimadd.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 2 | | rlimadd.5 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷) |
| 3 | 1, 2 | rlimmptrcl 15644 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 4 | | rlimadd.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
| 5 | | rlimadd.6 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸) |
| 6 | 4, 5 | rlimmptrcl 15644 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| 7 | | rlimdiv.8 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) |
| 8 | 6, 7 | reccld 12036 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐶) ∈ ℂ) |
| 9 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝐶 ∈ (ℂ ∖ {0})
↔ (𝐶 ∈ ℂ
∧ 𝐶 ≠
0)) |
| 10 | 6, 7, 9 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖
{0})) |
| 11 | 10 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶(ℂ ∖
{0})) |
| 12 | | rlimcl 15539 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ) |
| 13 | 5, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 14 | | rlimdiv.7 |
. . . . . 6
⊢ (𝜑 → 𝐸 ≠ 0) |
| 15 | | eldifsn 4786 |
. . . . . 6
⊢ (𝐸 ∈ (ℂ ∖ {0})
↔ (𝐸 ∈ ℂ
∧ 𝐸 ≠
0)) |
| 16 | 13, 14, 15 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (ℂ ∖
{0})) |
| 17 | | eldifsn 4786 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
| 18 | | reccl 11929 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / 𝑦) ∈
ℂ) |
| 19 | 17, 18 | sylbi 217 |
. . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
→ (1 / 𝑦) ∈
ℂ) |
| 20 | 19 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ {0})) → (1 /
𝑦) ∈
ℂ) |
| 21 | 20 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)):(ℂ ∖
{0})⟶ℂ) |
| 22 | | eqid 2737 |
. . . . . . . 8
⊢ (if(1
≤ ((abs‘𝐸)
· 𝑧), 1,
((abs‘𝐸) ·
𝑧)) ·
((abs‘𝐸) / 2)) =
(if(1 ≤ ((abs‘𝐸)
· 𝑧), 1,
((abs‘𝐸) ·
𝑧)) ·
((abs‘𝐸) /
2)) |
| 23 | 22 | reccn2 15633 |
. . . . . . 7
⊢ ((𝐸 ∈ (ℂ ∖ {0})
∧ 𝑧 ∈
ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
| 24 | 16, 23 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
| 25 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → (1 / 𝑦) = (1 / 𝑣)) |
| 26 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦)) = (𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦)) |
| 27 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ (1 /
𝑣) ∈
V |
| 28 | 25, 26, 27 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (ℂ ∖ {0})
→ ((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝑣) = (1 / 𝑣)) |
| 29 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐸 → (1 / 𝑦) = (1 / 𝐸)) |
| 30 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢ (1 /
𝐸) ∈
V |
| 31 | 29, 26, 30 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (ℂ ∖ {0})
→ ((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝐸) = (1 / 𝐸)) |
| 32 | 16, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸) = (1 / 𝐸)) |
| 33 | 28, 32 | oveqan12rd 7451 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(((𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸)) = ((1 / 𝑣) − (1 / 𝐸))) |
| 34 | 33 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(abs‘(((𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) = (abs‘((1 / 𝑣) − (1 / 𝐸)))) |
| 35 | 34 | breq1d 5153 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
((abs‘(((𝑦 ∈
(ℂ ∖ {0}) ↦ (1 / 𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧 ↔ (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) |
| 36 | 35 | imbi2d 340 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ (ℂ ∖ {0})) →
(((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ((abs‘(𝑣 − 𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
| 37 | 36 | ralbidva 3176 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
| 38 | 37 | rexbidv 3179 |
. . . . . . 7
⊢ (𝜑 → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧) ↔ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧))) |
| 39 | 38 | biimpar 477 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘((1 / 𝑣) − (1 / 𝐸))) < 𝑧)) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧)) |
| 40 | 24, 39 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ (ℂ ∖
{0})((abs‘(𝑣 −
𝐸)) < 𝑤 → (abs‘(((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝑣) − ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))‘𝐸))) < 𝑧)) |
| 41 | 11, 16, 5, 21, 40 | rlimcn1 15624 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) ∘ (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇝𝑟 ((𝑦 ∈ (ℂ ∖ {0})
↦ (1 / 𝑦))‘𝐸)) |
| 42 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
| 43 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) = (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))) |
| 44 | | oveq2 7439 |
. . . . 5
⊢ (𝑦 = 𝐶 → (1 / 𝑦) = (1 / 𝐶)) |
| 45 | 10, 42, 43, 44 | fmptco 7149 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦)) ∘ (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑥 ∈ 𝐴 ↦ (1 / 𝐶))) |
| 46 | 41, 45, 32 | 3brtr3d 5174 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐶)) ⇝𝑟 (1 / 𝐸)) |
| 47 | 3, 8, 2, 46 | rlimmul 15681 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 · (1 / 𝐶))) ⇝𝑟 (𝐷 · (1 / 𝐸))) |
| 48 | 3, 6, 7 | divrecd 12046 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶))) |
| 49 | 48 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵 · (1 / 𝐶)))) |
| 50 | | rlimcl 15539 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ) |
| 51 | 2, 50 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ ℂ) |
| 52 | 51, 13, 14 | divrecd 12046 |
. 2
⊢ (𝜑 → (𝐷 / 𝐸) = (𝐷 · (1 / 𝐸))) |
| 53 | 47, 49, 52 | 3brtr4d 5175 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶)) ⇝𝑟 (𝐷 / 𝐸)) |