Metamath Proof Explorer

Theorem clim1fr1

Description: A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses clim1fr1.1 ⊢F=n∈ℕ⟼A⁢n+BA⁢n
clim1fr1.2 ⊢φ→A∈ℂ
clim1fr1.3 ⊢φ→A≠0
clim1fr1.4 ⊢φ→B∈ℂ
Assertion clim1fr1 ⊢φ→F⇝1

Proof

Step Hyp Ref Expression
1 clim1fr1.1 ⊢F=n∈ℕ⟼A⁢n+BA⁢n
2 clim1fr1.2 ⊢φ→A∈ℂ
3 clim1fr1.3 ⊢φ→A≠0
4 clim1fr1.4 ⊢φ→B∈ℂ
5 nnuz ⊢ℕ=ℤ≥1
6 1zzd ⊢φ→1∈ℤ
7 nnex ⊢ℕ∈V
8 7 mptex ⊢n∈ℕ⟼1∈V
9 8 a1i ⊢φ→n∈ℕ⟼1∈V
10 1cnd ⊢φ→1∈ℂ
11 eqidd ⊢k∈ℕ→n∈ℕ⟼1=n∈ℕ⟼1
12 eqidd ⊢k∈ℕ∧n=k→1=1
13 id ⊢k∈ℕ→k∈ℕ
14 1cnd ⊢k∈ℕ→1∈ℂ
15 11 12 13 14 fvmptd ⊢k∈ℕ→n∈ℕ⟼1⁡k=1
16 15 adantl ⊢φ∧k∈ℕ→n∈ℕ⟼1⁡k=1
17 5 6 9 10 16 climconst ⊢φ→n∈ℕ⟼1⇝1
18 7 mptex ⊢n∈ℕ⟼A⁢n+BA⁢n∈V
19 1 18 eqeltri ⊢F∈V
20 19 a1i ⊢φ→F∈V
21 4 adantr ⊢φ∧n∈ℕ→B∈ℂ
22 2 adantr ⊢φ∧n∈ℕ→A∈ℂ
23 nncn ⊢n∈ℕ→n∈ℂ
24 23 adantl ⊢φ∧n∈ℕ→n∈ℂ
25 3 adantr ⊢φ∧n∈ℕ→A≠0
26 nnne0 ⊢n∈ℕ→n≠0
27 26 adantl ⊢φ∧n∈ℕ→n≠0
28 21 22 24 25 27 divdiv1d ⊢φ∧n∈ℕ→BAn=BA⁢n
29 28 mpteq2dva ⊢φ→n∈ℕ⟼BAn=n∈ℕ⟼BA⁢n
30 4 2 3 divcld ⊢φ→BA∈ℂ
31 divcnv ⊢BA∈ℂ→n∈ℕ⟼BAn⇝0
32 30 31 syl ⊢φ→n∈ℕ⟼BAn⇝0
33 29 32 eqbrtrrd ⊢φ→n∈ℕ⟼BA⁢n⇝0
34 eqid ⊢n∈ℕ⟼1=n∈ℕ⟼1
35 1cnd ⊢n∈ℕ→1∈ℂ
36 34 35 fmpti ⊢n∈ℕ⟼1:ℕ⟶ℂ
37 36 a1i ⊢φ→n∈ℕ⟼1:ℕ⟶ℂ
38 37 ffvelcdmda ⊢φ∧k∈ℕ→n∈ℕ⟼1⁡k∈ℂ
39 22 24 mulcld ⊢φ∧n∈ℕ→A⁢n∈ℂ
40 22 24 25 27 mulne0d ⊢φ∧n∈ℕ→A⁢n≠0
41 21 39 40 divcld ⊢φ∧n∈ℕ→BA⁢n∈ℂ
42 41 fmpttd ⊢φ→n∈ℕ⟼BA⁢n:ℕ⟶ℂ
43 42 ffvelcdmda ⊢φ∧k∈ℕ→n∈ℕ⟼BA⁢n⁡k∈ℂ
44 oveq2 ⊢n=k→A⁢n=A⁢k
45 44 oveq1d ⊢n=k→A⁢n+B=A⁢k+B
46 45 44 oveq12d ⊢n=k→A⁢n+BA⁢n=A⁢k+BA⁢k
47 simpr ⊢φ∧k∈ℕ→k∈ℕ
48 2 adantr ⊢φ∧k∈ℕ→A∈ℂ
49 47 nncnd ⊢φ∧k∈ℕ→k∈ℂ
50 48 49 mulcld ⊢φ∧k∈ℕ→A⁢k∈ℂ
51 4 adantr ⊢φ∧k∈ℕ→B∈ℂ
52 50 51 addcld ⊢φ∧k∈ℕ→A⁢k+B∈ℂ
53 3 adantr ⊢φ∧k∈ℕ→A≠0
54 47 nnne0d ⊢φ∧k∈ℕ→k≠0
55 48 49 53 54 mulne0d ⊢φ∧k∈ℕ→A⁢k≠0
56 52 50 55 divcld ⊢φ∧k∈ℕ→A⁢k+BA⁢k∈ℂ
57 1 46 47 56 fvmptd3 ⊢φ∧k∈ℕ→F⁡k=A⁢k+BA⁢k
58 50 51 50 55 divdird ⊢φ∧k∈ℕ→A⁢k+BA⁢k=A⁢kA⁢k+BA⁢k
59 50 55 dividd ⊢φ∧k∈ℕ→A⁢kA⁢k=1
60 59 oveq1d ⊢φ∧k∈ℕ→A⁢kA⁢k+BA⁢k=1+BA⁢k
61 58 60 eqtrd ⊢φ∧k∈ℕ→A⁢k+BA⁢k=1+BA⁢k
62 16 eqcomd ⊢φ∧k∈ℕ→1=n∈ℕ⟼1⁡k
63 eqidd ⊢φ∧k∈ℕ→n∈ℕ⟼BA⁢n=n∈ℕ⟼BA⁢n
64 simpr ⊢φ∧k∈ℕ∧n=k→n=k
65 64 oveq2d ⊢φ∧k∈ℕ∧n=k→A⁢n=A⁢k
66 65 oveq2d ⊢φ∧k∈ℕ∧n=k→BA⁢n=BA⁢k
67 51 50 55 divcld ⊢φ∧k∈ℕ→BA⁢k∈ℂ
68 63 66 47 67 fvmptd ⊢φ∧k∈ℕ→n∈ℕ⟼BA⁢n⁡k=BA⁢k
69 68 eqcomd ⊢φ∧k∈ℕ→BA⁢k=n∈ℕ⟼BA⁢n⁡k
70 62 69 oveq12d ⊢φ∧k∈ℕ→1+BA⁢k=n∈ℕ⟼1⁡k+n∈ℕ⟼BA⁢n⁡k
71 57 61 70 3eqtrd ⊢φ∧k∈ℕ→F⁡k=n∈ℕ⟼1⁡k+n∈ℕ⟼BA⁢n⁡k
72 5 6 17 20 33 38 43 71 climadd ⊢φ→F⇝1+0
73 1p0e1 ⊢1+0=1
74 72 73 breqtrdi ⊢φ→F⇝1