Proof of Theorem reclimc
Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) |
2 | | eqid 2739 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) |
3 | | eqid 2739 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) |
4 | | limccl 25020 |
. . . . . . 7
⊢ (𝐹 limℂ 𝐷) ⊆
ℂ |
5 | | reclimc.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) |
6 | 4, 5 | sselid 3923 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
8 | | reclimc.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖
{0})) |
9 | 8 | eldifad 3903 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 7, 9 | subcld 11315 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 − 𝐵) ∈ ℂ) |
11 | 9, 7 | mulcld 10979 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ ℂ) |
12 | | eldifsni 4728 |
. . . . . . . . 9
⊢ (𝐵 ∈ (ℂ ∖ {0})
→ 𝐵 ≠
0) |
13 | 8, 12 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0) |
14 | | reclimc.cne0 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≠ 0) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) |
16 | 9, 7, 13, 15 | mulne0d 11610 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ≠ 0) |
17 | 16 | neneqd 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ (𝐵 · 𝐶) = 0) |
18 | | elsng 4580 |
. . . . . . 7
⊢ ((𝐵 · 𝐶) ∈ ℂ → ((𝐵 · 𝐶) ∈ {0} ↔ (𝐵 · 𝐶) = 0)) |
19 | 11, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 · 𝐶) ∈ {0} ↔ (𝐵 · 𝐶) = 0)) |
20 | 17, 19 | mtbird 324 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ (𝐵 · 𝐶) ∈ {0}) |
21 | 11, 20 | eldifd 3902 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ (ℂ ∖
{0})) |
22 | | eqid 2739 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
23 | | eqid 2739 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ -𝐵) = (𝑥 ∈ 𝐴 ↦ -𝐵) |
24 | | eqid 2739 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) |
25 | 9 | negcld 11302 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
26 | | reclimc.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
27 | 26, 9, 5 | limcmptdm 43130 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
28 | | limcrcl 25019 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝐹 limℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
29 | 5, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
30 | 29 | simp3d 1142 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) |
31 | 22, 27, 6, 30 | constlimc 43119 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐶) limℂ 𝐷)) |
32 | 26, 23, 9, 5 | neglimc 43142 |
. . . . . 6
⊢ (𝜑 → -𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ -𝐵) limℂ 𝐷)) |
33 | 22, 23, 24, 7, 25, 31, 32 | addlimc 43143 |
. . . . 5
⊢ (𝜑 → (𝐶 + -𝐶) ∈ ((𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) limℂ 𝐷)) |
34 | 6 | negidd 11305 |
. . . . 5
⊢ (𝜑 → (𝐶 + -𝐶) = 0) |
35 | 7, 9 | negsubd 11321 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + -𝐵) = (𝐶 − 𝐵)) |
36 | 35 | mpteq2dva 5178 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵))) |
37 | 36 | oveq1d 7283 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) limℂ 𝐷) = ((𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) limℂ 𝐷)) |
38 | 33, 34, 37 | 3eltr3d 2854 |
. . . 4
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) limℂ 𝐷)) |
39 | 26, 22, 2, 9, 7, 5, 31 | mullimc 43111 |
. . . 4
⊢ (𝜑 → (𝐶 · 𝐶) ∈ ((𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) limℂ 𝐷)) |
40 | 6, 6, 14, 14 | mulne0d 11610 |
. . . 4
⊢ (𝜑 → (𝐶 · 𝐶) ≠ 0) |
41 | 1, 2, 3, 10, 21, 38, 39, 40 | 0ellimcdiv 43144 |
. . 3
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) limℂ 𝐷)) |
42 | | 1cnd 10954 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ) |
43 | 42, 9, 42, 7, 13, 15 | divsubdivd 11779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1 / 𝐵) − (1 / 𝐶)) = (((1 · 𝐶) − (1 · 𝐵)) / (𝐵 · 𝐶))) |
44 | 7 | mulid2d 10977 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · 𝐶) = 𝐶) |
45 | 9 | mulid2d 10977 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · 𝐵) = 𝐵) |
46 | 44, 45 | oveq12d 7286 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1 · 𝐶) − (1 · 𝐵)) = (𝐶 − 𝐵)) |
47 | 46 | oveq1d 7283 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((1 · 𝐶) − (1 · 𝐵)) / (𝐵 · 𝐶)) = ((𝐶 − 𝐵) / (𝐵 · 𝐶))) |
48 | 43, 47 | eqtr2d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 − 𝐵) / (𝐵 · 𝐶)) = ((1 / 𝐵) − (1 / 𝐶))) |
49 | 48 | mpteq2dva 5178 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶)))) |
50 | 49 | oveq1d 7283 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) limℂ 𝐷) = ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷)) |
51 | 41, 50 | eleqtrd 2842 |
. 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷)) |
52 | | reclimc.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) |
53 | | eqid 2739 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) |
54 | 9, 13 | reccld 11727 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐵) ∈ ℂ) |
55 | 6, 14 | reccld 11727 |
. . 3
⊢ (𝜑 → (1 / 𝐶) ∈ ℂ) |
56 | 52, 53, 27, 54, 30, 55 | ellimcabssub0 43112 |
. 2
⊢ (𝜑 → ((1 / 𝐶) ∈ (𝐺 limℂ 𝐷) ↔ 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷))) |
57 | 51, 56 | mpbird 256 |
1
⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷)) |