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 e. NN |-> ( ( ( A x. n ) + B ) / ( A x. n ) ) )
clim1fr1.2 
|- ( ph -> A e. CC )
clim1fr1.3 
|- ( ph -> A =/= 0 )
clim1fr1.4 
|- ( ph -> B e. CC )
Assertion clim1fr1 
|- ( ph -> F ~~> 1 )

Proof

Step Hyp Ref Expression
1 clim1fr1.1 
 |-  F = ( n e. NN |-> ( ( ( A x. n ) + B ) / ( A x. n ) ) )
2 clim1fr1.2 
 |-  ( ph -> A e. CC )
3 clim1fr1.3 
 |-  ( ph -> A =/= 0 )
4 clim1fr1.4 
 |-  ( ph -> B e. CC )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 1zzd 
 |-  ( ph -> 1 e. ZZ )
7 nnex 
 |-  NN e. _V
8 7 mptex 
 |-  ( n e. NN |-> 1 ) e. _V
9 8 a1i 
 |-  ( ph -> ( n e. NN |-> 1 ) e. _V )
10 1cnd 
 |-  ( ph -> 1 e. CC )
11 eqidd 
 |-  ( k e. NN -> ( n e. NN |-> 1 ) = ( n e. NN |-> 1 ) )
12 eqidd 
 |-  ( ( k e. NN /\ n = k ) -> 1 = 1 )
13 id 
 |-  ( k e. NN -> k e. NN )
14 1cnd 
 |-  ( k e. NN -> 1 e. CC )
15 11 12 13 14 fvmptd 
 |-  ( k e. NN -> ( ( n e. NN |-> 1 ) ` k ) = 1 )
16 15 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> 1 ) ` k ) = 1 )
17 5 6 9 10 16 climconst 
 |-  ( ph -> ( n e. NN |-> 1 ) ~~> 1 )
18 7 mptex 
 |-  ( n e. NN |-> ( ( ( A x. n ) + B ) / ( A x. n ) ) ) e. _V
19 1 18 eqeltri 
 |-  F e. _V
20 19 a1i 
 |-  ( ph -> F e. _V )
21 4 adantr 
 |-  ( ( ph /\ n e. NN ) -> B e. CC )
22 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. CC )
23 nncn 
 |-  ( n e. NN -> n e. CC )
24 23 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
25 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> A =/= 0 )
26 nnne0 
 |-  ( n e. NN -> n =/= 0 )
27 26 adantl 
 |-  ( ( ph /\ n e. NN ) -> n =/= 0 )
28 21 22 24 25 27 divdiv1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( B / A ) / n ) = ( B / ( A x. n ) ) )
29 28 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( ( B / A ) / n ) ) = ( n e. NN |-> ( B / ( A x. n ) ) ) )
30 4 2 3 divcld 
 |-  ( ph -> ( B / A ) e. CC )
31 divcnv 
 |-  ( ( B / A ) e. CC -> ( n e. NN |-> ( ( B / A ) / n ) ) ~~> 0 )
32 30 31 syl 
 |-  ( ph -> ( n e. NN |-> ( ( B / A ) / n ) ) ~~> 0 )
33 29 32 eqbrtrrd 
 |-  ( ph -> ( n e. NN |-> ( B / ( A x. n ) ) ) ~~> 0 )
34 eqid 
 |-  ( n e. NN |-> 1 ) = ( n e. NN |-> 1 )
35 1cnd 
 |-  ( n e. NN -> 1 e. CC )
36 34 35 fmpti 
 |-  ( n e. NN |-> 1 ) : NN --> CC
37 36 a1i 
 |-  ( ph -> ( n e. NN |-> 1 ) : NN --> CC )
38 37 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> 1 ) ` k ) e. CC )
39 22 24 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( A x. n ) e. CC )
40 22 24 25 27 mulne0d 
 |-  ( ( ph /\ n e. NN ) -> ( A x. n ) =/= 0 )
41 21 39 40 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( B / ( A x. n ) ) e. CC )
42 41 fmpttd 
 |-  ( ph -> ( n e. NN |-> ( B / ( A x. n ) ) ) : NN --> CC )
43 42 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( B / ( A x. n ) ) ) ` k ) e. CC )
44 oveq2 
 |-  ( n = k -> ( A x. n ) = ( A x. k ) )
45 44 oveq1d 
 |-  ( n = k -> ( ( A x. n ) + B ) = ( ( A x. k ) + B ) )
46 45 44 oveq12d 
 |-  ( n = k -> ( ( ( A x. n ) + B ) / ( A x. n ) ) = ( ( ( A x. k ) + B ) / ( A x. k ) ) )
47 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
48 2 adantr 
 |-  ( ( ph /\ k e. NN ) -> A e. CC )
49 47 nncnd 
 |-  ( ( ph /\ k e. NN ) -> k e. CC )
50 48 49 mulcld 
 |-  ( ( ph /\ k e. NN ) -> ( A x. k ) e. CC )
51 4 adantr 
 |-  ( ( ph /\ k e. NN ) -> B e. CC )
52 50 51 addcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( A x. k ) + B ) e. CC )
53 3 adantr 
 |-  ( ( ph /\ k e. NN ) -> A =/= 0 )
54 47 nnne0d 
 |-  ( ( ph /\ k e. NN ) -> k =/= 0 )
55 48 49 53 54 mulne0d 
 |-  ( ( ph /\ k e. NN ) -> ( A x. k ) =/= 0 )
56 52 50 55 divcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A x. k ) + B ) / ( A x. k ) ) e. CC )
57 1 46 47 56 fvmptd3 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( ( ( A x. k ) + B ) / ( A x. k ) ) )
58 50 51 50 55 divdird 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A x. k ) + B ) / ( A x. k ) ) = ( ( ( A x. k ) / ( A x. k ) ) + ( B / ( A x. k ) ) ) )
59 50 55 dividd 
 |-  ( ( ph /\ k e. NN ) -> ( ( A x. k ) / ( A x. k ) ) = 1 )
60 59 oveq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A x. k ) / ( A x. k ) ) + ( B / ( A x. k ) ) ) = ( 1 + ( B / ( A x. k ) ) ) )
61 58 60 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A x. k ) + B ) / ( A x. k ) ) = ( 1 + ( B / ( A x. k ) ) ) )
62 16 eqcomd 
 |-  ( ( ph /\ k e. NN ) -> 1 = ( ( n e. NN |-> 1 ) ` k ) )
63 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( n e. NN |-> ( B / ( A x. n ) ) ) = ( n e. NN |-> ( B / ( A x. n ) ) ) )
64 simpr 
 |-  ( ( ( ph /\ k e. NN ) /\ n = k ) -> n = k )
65 64 oveq2d 
 |-  ( ( ( ph /\ k e. NN ) /\ n = k ) -> ( A x. n ) = ( A x. k ) )
66 65 oveq2d 
 |-  ( ( ( ph /\ k e. NN ) /\ n = k ) -> ( B / ( A x. n ) ) = ( B / ( A x. k ) ) )
67 51 50 55 divcld 
 |-  ( ( ph /\ k e. NN ) -> ( B / ( A x. k ) ) e. CC )
68 63 66 47 67 fvmptd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( B / ( A x. n ) ) ) ` k ) = ( B / ( A x. k ) ) )
69 68 eqcomd 
 |-  ( ( ph /\ k e. NN ) -> ( B / ( A x. k ) ) = ( ( n e. NN |-> ( B / ( A x. n ) ) ) ` k ) )
70 62 69 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( 1 + ( B / ( A x. k ) ) ) = ( ( ( n e. NN |-> 1 ) ` k ) + ( ( n e. NN |-> ( B / ( A x. n ) ) ) ` k ) ) )
71 57 61 70 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( ( ( n e. NN |-> 1 ) ` k ) + ( ( n e. NN |-> ( B / ( A x. n ) ) ) ` k ) ) )
72 5 6 17 20 33 38 43 71 climadd 
 |-  ( ph -> F ~~> ( 1 + 0 ) )
73 1p0e1 
 |-  ( 1 + 0 ) = 1
74 72 73 breqtrdi 
 |-  ( ph -> F ~~> 1 )