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}=\left({n}\in ℕ⟼\frac{{A}{n}+{B}}{{A}{n}}\right)$
clim1fr1.2 ${⊢}{\phi }\to {A}\in ℂ$
clim1fr1.3 ${⊢}{\phi }\to {A}\ne 0$
clim1fr1.4 ${⊢}{\phi }\to {B}\in ℂ$
Assertion clim1fr1 ${⊢}{\phi }\to {F}⇝1$

Proof

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