Metamath Proof Explorer

Theorem reclimc

Description: Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses reclimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
reclimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) )
reclimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
reclimc.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) )
reclimc.cne0 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion reclimc ( 𝜑 → ( 1 / 𝐶 ) ∈ ( 𝐺 limℂ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 reclimc.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 reclimc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐵 ) )
3 reclimc.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
4 reclimc.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) )
5 reclimc.cne0 ⊢ ( 𝜑 → 𝐶 ≠ 0 )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) )
7 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) )
8 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) )
9 limccl ⊢ ( 𝐹 limℂ 𝐷 ) ⊆ ℂ
10 9 4 sselid ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12 3 eldifad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
13 11 12 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
14 12 11 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
15 eldifsni ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 } ) → 𝐵 ≠ 0 )
16 3 15 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ 0 )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
18 12 11 16 17 mulne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ≠ 0 )
19 18 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝐵 · 𝐶 ) = 0 )
20 elsng ⊢ ( ( 𝐵 · 𝐶 ) ∈ ℂ → ( ( 𝐵 · 𝐶 ) ∈ { 0 } ↔ ( 𝐵 · 𝐶 ) = 0 ) )
21 14 20 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 · 𝐶 ) ∈ { 0 } ↔ ( 𝐵 · 𝐶 ) = 0 ) )
22 19 21 mtbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝐵 · 𝐶 ) ∈ { 0 } )
23 14 22 eldifd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ( ℂ ∖ { 0 } ) )
24 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
25 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
26 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + - 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + - 𝐵 ) )
27 12 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℂ )
28 1 12 4 limcmptdm ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
29 limcrcl ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
30 4 29 syl ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
31 30 simp3d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
32 24 28 10 31 constlimc ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) limℂ 𝐷 ) )
33 1 25 12 4 neglimc ⊢ ( 𝜑 → - 𝐶 ∈ ( ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) limℂ 𝐷 ) )
34 24 25 26 11 27 32 33 addlimc ⊢ ( 𝜑 → ( 𝐶 + - 𝐶 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + - 𝐵 ) ) limℂ 𝐷 ) )
35 10 negidd ⊢ ( 𝜑 → ( 𝐶 + - 𝐶 ) = 0 )
36 11 12 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 + - 𝐵 ) = ( 𝐶 − 𝐵 ) )
37 36 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + - 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) ) )
38 37 oveq1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 + - 𝐵 ) ) limℂ 𝐷 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) ) limℂ 𝐷 ) )
39 34 35 38 3eltr3d ⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) ) limℂ 𝐷 ) )
40 1 24 7 12 11 4 32 mullimc ⊢ ( 𝜑 → ( 𝐶 · 𝐶 ) ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) limℂ 𝐷 ) )
41 10 10 5 5 mulne0d ⊢ ( 𝜑 → ( 𝐶 · 𝐶 ) ≠ 0 )
42 6 7 8 13 23 39 40 41 0ellimcdiv ⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) ) limℂ 𝐷 ) )
43 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 1 ∈ ℂ )
44 43 12 43 11 16 17 divsubdivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) = ( ( ( 1 · 𝐶 ) − ( 1 · 𝐵 ) ) / ( 𝐵 · 𝐶 ) ) )
45 11 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 · 𝐶 ) = 𝐶 )
46 12 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 · 𝐵 ) = 𝐵 )
47 45 46 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1 · 𝐶 ) − ( 1 · 𝐵 ) ) = ( 𝐶 − 𝐵 ) )
48 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 1 · 𝐶 ) − ( 1 · 𝐵 ) ) / ( 𝐵 · 𝐶 ) ) = ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) )
49 44 48 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) = ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) )
50 49 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) ) )
51 50 oveq1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐶 − 𝐵 ) / ( 𝐵 · 𝐶 ) ) ) limℂ 𝐷 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) ) limℂ 𝐷 ) )
52 42 51 eleqtrd ⊢ ( 𝜑 → 0 ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) ) limℂ 𝐷 ) )
53 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) )
54 12 16 reccld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 / 𝐵 ) ∈ ℂ )
55 10 5 reccld ⊢ ( 𝜑 → ( 1 / 𝐶 ) ∈ ℂ )
56 2 53 28 54 31 55 ellimcabssub0 ⊢ ( 𝜑 → ( ( 1 / 𝐶 ) ∈ ( 𝐺 limℂ 𝐷 ) ↔ 0 ∈ ( ( 𝑥 ∈ 𝐴 ↦ ( ( 1 / 𝐵 ) − ( 1 / 𝐶 ) ) ) limℂ 𝐷 ) ) )
57 52 56 mpbird ⊢ ( 𝜑 → ( 1 / 𝐶 ) ∈ ( 𝐺 limℂ 𝐷 ) )