Proof of Theorem reclimc
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) | 
| 2 |  | eqid 2736 | . . . 4
⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) | 
| 3 |  | eqid 2736 | . . . 4
⊢ (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) | 
| 4 |  | limccl 25911 | . . . . . . 7
⊢ (𝐹 limℂ 𝐷) ⊆
ℂ | 
| 5 |  | reclimc.c | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) | 
| 6 | 4, 5 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) | 
| 8 |  | reclimc.b | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (ℂ ∖
{0})) | 
| 9 | 8 | eldifad 3962 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 10 | 7, 9 | subcld 11621 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 − 𝐵) ∈ ℂ) | 
| 11 | 9, 7 | mulcld 11282 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ ℂ) | 
| 12 |  | eldifsni 4789 | . . . . . . . . 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 11916 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ≠ 0) | 
| 17 | 16 | neneqd 2944 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ (𝐵 · 𝐶) = 0) | 
| 18 |  | elsng 4639 | . . . . . . 7
⊢ ((𝐵 · 𝐶) ∈ ℂ → ((𝐵 · 𝐶) ∈ {0} ↔ (𝐵 · 𝐶) = 0)) | 
| 19 | 11, 18 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 · 𝐶) ∈ {0} ↔ (𝐵 · 𝐶) = 0)) | 
| 20 | 17, 19 | mtbird 325 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ (𝐵 · 𝐶) ∈ {0}) | 
| 21 | 11, 20 | eldifd 3961 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 · 𝐶) ∈ (ℂ ∖
{0})) | 
| 22 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶) | 
| 23 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ -𝐵) = (𝑥 ∈ 𝐴 ↦ -𝐵) | 
| 24 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) | 
| 25 | 9 | negcld 11608 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) | 
| 26 |  | reclimc.f | . . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | 
| 27 | 26, 9, 5 | limcmptdm 45655 | . . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 28 |  | limcrcl 25910 | . . . . . . . . 9
⊢ (𝐶 ∈ (𝐹 limℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) | 
| 29 | 5, 28 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) | 
| 30 | 29 | simp3d 1144 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 31 | 22, 27, 6, 30 | constlimc 45644 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐶) limℂ 𝐷)) | 
| 32 | 26, 23, 9, 5 | neglimc 45667 | . . . . . 6
⊢ (𝜑 → -𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ -𝐵) limℂ 𝐷)) | 
| 33 | 22, 23, 24, 7, 25, 31, 32 | addlimc 45668 | . . . . 5
⊢ (𝜑 → (𝐶 + -𝐶) ∈ ((𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) limℂ 𝐷)) | 
| 34 | 6 | negidd 11611 | . . . . 5
⊢ (𝜑 → (𝐶 + -𝐶) = 0) | 
| 35 | 7, 9 | negsubd 11627 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + -𝐵) = (𝐶 − 𝐵)) | 
| 36 | 35 | mpteq2dva 5241 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵))) | 
| 37 | 36 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 + -𝐵)) limℂ 𝐷) = ((𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) limℂ 𝐷)) | 
| 38 | 33, 34, 37 | 3eltr3d 2854 | . . . 4
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐵)) limℂ 𝐷)) | 
| 39 | 26, 22, 2, 9, 7, 5, 31 | mullimc 45636 | . . . 4
⊢ (𝜑 → (𝐶 · 𝐶) ∈ ((𝑥 ∈ 𝐴 ↦ (𝐵 · 𝐶)) limℂ 𝐷)) | 
| 40 | 6, 6, 14, 14 | mulne0d 11916 | . . . 4
⊢ (𝜑 → (𝐶 · 𝐶) ≠ 0) | 
| 41 | 1, 2, 3, 10, 21, 38, 39, 40 | 0ellimcdiv 45669 | . . 3
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) limℂ 𝐷)) | 
| 42 |  | 1cnd 11257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 1 ∈ ℂ) | 
| 43 | 42, 9, 42, 7, 13, 15 | divsubdivd 12089 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1 / 𝐵) − (1 / 𝐶)) = (((1 · 𝐶) − (1 · 𝐵)) / (𝐵 · 𝐶))) | 
| 44 | 7 | mullidd 11280 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · 𝐶) = 𝐶) | 
| 45 | 9 | mullidd 11280 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · 𝐵) = 𝐵) | 
| 46 | 44, 45 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((1 · 𝐶) − (1 · 𝐵)) = (𝐶 − 𝐵)) | 
| 47 | 46 | oveq1d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((1 · 𝐶) − (1 · 𝐵)) / (𝐵 · 𝐶)) = ((𝐶 − 𝐵) / (𝐵 · 𝐶))) | 
| 48 | 43, 47 | eqtr2d 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 − 𝐵) / (𝐵 · 𝐶)) = ((1 / 𝐵) − (1 / 𝐶))) | 
| 49 | 48 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶)))) | 
| 50 | 49 | oveq1d 7447 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝐶 − 𝐵) / (𝐵 · 𝐶))) limℂ 𝐷) = ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷)) | 
| 51 | 41, 50 | eleqtrd 2842 | . 2
⊢ (𝜑 → 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷)) | 
| 52 |  | reclimc.g | . . 3
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) | 
| 53 |  | eqid 2736 | . . 3
⊢ (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) = (𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) | 
| 54 | 9, 13 | reccld 12037 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐵) ∈ ℂ) | 
| 55 | 6, 14 | reccld 12037 | . . 3
⊢ (𝜑 → (1 / 𝐶) ∈ ℂ) | 
| 56 | 52, 53, 27, 54, 30, 55 | ellimcabssub0 45637 | . 2
⊢ (𝜑 → ((1 / 𝐶) ∈ (𝐺 limℂ 𝐷) ↔ 0 ∈ ((𝑥 ∈ 𝐴 ↦ ((1 / 𝐵) − (1 / 𝐶))) limℂ 𝐷))) | 
| 57 | 51, 56 | mpbird 257 | 1
⊢ (𝜑 → (1 / 𝐶) ∈ (𝐺 limℂ 𝐷)) |