Proof of Theorem reclimc
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) |
2 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) |
3 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) |
4 | | limccl 25039 |
. . . . . . 7
⊢ (𝐹 limℂ 𝐷) ⊆
ℂ |
5 | | reclimc.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) |
6 | 4, 5 | sselid 3919 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
8 | | reclimc.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖
{0})) |
9 | 8 | eldifad 3899 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 7, 9 | subcld 11332 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 − 𝐵) ∈ ℂ) |
11 | 9, 7 | mulcld 10995 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ ℂ) |
12 | | eldifsni 4723 |
. . . . . . . . 9
⊢ (𝐵 ∈ (ℂ ∖ {0})
→ 𝐵 ≠
0) |
13 | 8, 12 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0) |
14 | | reclimc.cne0 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≠ 0) |
15 | 14 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0) |
16 | 9, 7, 13, 15 | mulne0d 11627 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ≠ 0) |
17 | 16 | neneqd 2948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ (𝐵 · 𝐶) = 0) |
18 | | elsng 4575 |
. . . . . . 7
⊢ ((𝐵 · 𝐶) ∈ ℂ → ((𝐵 · 𝐶) ∈ {0} ↔ (𝐵 · 𝐶) = 0)) |
19 | 11, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 · 𝐶) ∈ {0} ↔ (𝐵 · 𝐶) = 0)) |
20 | 17, 19 | mtbird 325 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ (𝐵 · 𝐶) ∈ {0}) |
21 | 11, 20 | eldifd 3898 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ (ℂ ∖
{0})) |
22 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) |
23 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ -𝐵) = (𝑥 ∈ 𝐴 ↦ -𝐵) |
24 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) |
25 | 9 | negcld 11319 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
26 | | reclimc.f |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
27 | 26, 9, 5 | limcmptdm 43176 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
28 | | limcrcl 25038 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝐹 limℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
29 | 5, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
30 | 29 | simp3d 1143 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) |
31 | 22, 27, 6, 30 | constlimc 43165 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐶) limℂ 𝐷)) |
32 | 26, 23, 9, 5 | neglimc 43188 |
. . . . . 6
⊢ (𝜑 → -𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ -𝐵) limℂ 𝐷)) |
33 | 22, 23, 24, 7, 25, 31, 32 | addlimc 43189 |
. . . . 5
⊢ (𝜑 → (𝐶 + -𝐶) ∈ ((𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) limℂ 𝐷)) |
34 | 6 | negidd 11322 |
. . . . 5
⊢ (𝜑 → (𝐶 + -𝐶) = 0) |
35 | 7, 9 | negsubd 11338 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + -𝐵) = (𝐶 − 𝐵)) |
36 | 35 | mpteq2dva 5174 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵))) |
37 | 36 | oveq1d 7290 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) limℂ 𝐷) = ((𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) limℂ 𝐷)) |
38 | 33, 34, 37 | 3eltr3d 2853 |
. . . 4
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) limℂ 𝐷)) |
39 | 26, 22, 2, 9, 7, 5, 31 | mullimc 43157 |
. . . 4
⊢ (𝜑 → (𝐶 · 𝐶) ∈ ((𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) limℂ 𝐷)) |
40 | 6, 6, 14, 14 | mulne0d 11627 |
. . . 4
⊢ (𝜑 → (𝐶 · 𝐶) ≠ 0) |
41 | 1, 2, 3, 10, 21, 38, 39, 40 | 0ellimcdiv 43190 |
. . 3
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) limℂ 𝐷)) |
42 | | 1cnd 10970 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ) |
43 | 42, 9, 42, 7, 13, 15 | divsubdivd 11796 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1 / 𝐵) − (1 / 𝐶)) = (((1 · 𝐶) − (1 · 𝐵)) / (𝐵 · 𝐶))) |
44 | 7 | mulid2d 10993 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · 𝐶) = 𝐶) |
45 | 9 | mulid2d 10993 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · 𝐵) = 𝐵) |
46 | 44, 45 | oveq12d 7293 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1 · 𝐶) − (1 · 𝐵)) = (𝐶 − 𝐵)) |
47 | 46 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((1 · 𝐶) − (1 · 𝐵)) / (𝐵 · 𝐶)) = ((𝐶 − 𝐵) / (𝐵 · 𝐶))) |
48 | 43, 47 | eqtr2d 2779 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 − 𝐵) / (𝐵 · 𝐶)) = ((1 / 𝐵) − (1 / 𝐶))) |
49 | 48 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶)))) |
50 | 49 | oveq1d 7290 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) limℂ 𝐷) = ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷)) |
51 | 41, 50 | eleqtrd 2841 |
. 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷)) |
52 | | reclimc.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) |
53 | | eqid 2738 |
. . 3
⊢ (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) |
54 | 9, 13 | reccld 11744 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐵) ∈ ℂ) |
55 | 6, 14 | reccld 11744 |
. . 3
⊢ (𝜑 → (1 / 𝐶) ∈ ℂ) |
56 | 52, 53, 27, 54, 30, 55 | ellimcabssub0 43158 |
. 2
⊢ (𝜑 → ((1 / 𝐶) ∈ (𝐺 limℂ 𝐷) ↔ 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷))) |
57 | 51, 56 | mpbird 256 |
1
⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷)) |