Metamath Proof Explorer

Theorem binomcxplemrat

Description: Lemma for binomcxp . As k increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a 
|- ( ph -> A e. RR+ )
binomcxp.b 
|- ( ph -> B e. RR )
binomcxp.lt 
|- ( ph -> ( abs ` B ) < ( abs ` A ) )
binomcxp.c 
|- ( ph -> C e. CC )
Assertion binomcxplemrat 
|- ( ph -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ~~> 1 )

Proof

Step Hyp Ref Expression
1 binomcxp.a 
 |-  ( ph -> A e. RR+ )
2 binomcxp.b 
 |-  ( ph -> B e. RR )
3 binomcxp.lt 
 |-  ( ph -> ( abs ` B ) < ( abs ` A ) )
4 binomcxp.c 
 |-  ( ph -> C e. CC )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 0zd 
 |-  ( ph -> 0 e. ZZ )
7 peano2cn 
 |-  ( C e. CC -> ( C + 1 ) e. CC )
8 4 7 syl 
 |-  ( ph -> ( C + 1 ) e. CC )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 nn0ex 
 |-  NN0 e. _V
11 10 mptex 
 |-  ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) e. _V
12 11 a1i 
 |-  ( ph -> ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) e. _V )
13 eqidd 
 |-  ( ( ph /\ x e. NN0 ) -> ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) )
14 simpr 
 |-  ( ( ( ph /\ x e. NN0 ) /\ k = x ) -> k = x )
15 14 oveq1d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ k = x ) -> ( k + 1 ) = ( x + 1 ) )
16 15 oveq2d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ k = x ) -> ( ( C + 1 ) / ( k + 1 ) ) = ( ( C + 1 ) / ( x + 1 ) ) )
17 simpr 
 |-  ( ( ph /\ x e. NN0 ) -> x e. NN0 )
18 ovexd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( C + 1 ) / ( x + 1 ) ) e. _V )
19 13 16 17 18 fvmptd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) ` x ) = ( ( C + 1 ) / ( x + 1 ) ) )
20 5 6 8 9 12 19 divcnvshft 
 |-  ( ph -> ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) ~~> 0 )
21 ovexd 
 |-  ( ph -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) oF - ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ) e. _V )
22 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
23 1cnd 
 |-  ( k e. NN0 -> 1 e. CC )
24 22 23 addcld 
 |-  ( k e. NN0 -> ( k + 1 ) e. CC )
25 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
26 25 nnne0d 
 |-  ( k e. NN0 -> ( k + 1 ) =/= 0 )
27 24 26 dividd 
 |-  ( k e. NN0 -> ( ( k + 1 ) / ( k + 1 ) ) = 1 )
28 27 mpteq2ia 
 |-  ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> 1 )
29 fconstmpt 
 |-  ( NN0 X. { 1 } ) = ( k e. NN0 |-> 1 )
30 28 29 eqtr4i 
 |-  ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) = ( NN0 X. { 1 } )
31 ax-1cn 
 |-  1 e. CC
32 0z 
 |-  0 e. ZZ
33 5 eqimss2i 
 |-  ( ZZ>= ` 0 ) C_ NN0
34 33 10 climconst2 
 |-  ( ( 1 e. CC /\ 0 e. ZZ ) -> ( NN0 X. { 1 } ) ~~> 1 )
35 31 32 34 mp2an 
 |-  ( NN0 X. { 1 } ) ~~> 1
36 30 35 eqbrtri 
 |-  ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ~~> 1
37 36 a1i 
 |-  ( ph -> ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ~~> 1 )
38 4 adantr 
 |-  ( ( ph /\ x e. NN0 ) -> C e. CC )
39 1cnd 
 |-  ( ( ph /\ x e. NN0 ) -> 1 e. CC )
40 38 39 addcld 
 |-  ( ( ph /\ x e. NN0 ) -> ( C + 1 ) e. CC )
41 17 nn0cnd 
 |-  ( ( ph /\ x e. NN0 ) -> x e. CC )
42 41 39 addcld 
 |-  ( ( ph /\ x e. NN0 ) -> ( x + 1 ) e. CC )
43 nn0p1nn 
 |-  ( x e. NN0 -> ( x + 1 ) e. NN )
44 43 nnne0d 
 |-  ( x e. NN0 -> ( x + 1 ) =/= 0 )
45 44 adantl 
 |-  ( ( ph /\ x e. NN0 ) -> ( x + 1 ) =/= 0 )
46 40 42 45 divcld 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( C + 1 ) / ( x + 1 ) ) e. CC )
47 19 46 eqeltrd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) ` x ) e. CC )
48 eqidd 
 |-  ( ( ph /\ x e. NN0 ) -> ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) )
49 15 15 oveq12d 
 |-  ( ( ( ph /\ x e. NN0 ) /\ k = x ) -> ( ( k + 1 ) / ( k + 1 ) ) = ( ( x + 1 ) / ( x + 1 ) ) )
50 ovexd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( x + 1 ) / ( x + 1 ) ) e. _V )
51 48 49 17 50 fvmptd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ` x ) = ( ( x + 1 ) / ( x + 1 ) ) )
52 42 42 45 divcld 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( x + 1 ) / ( x + 1 ) ) e. CC )
53 51 52 eqeltrd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ` x ) e. CC )
54 ovex 
 |-  ( ( C + 1 ) / ( k + 1 ) ) e. _V
55 eqid 
 |-  ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) )
56 54 55 fnmpti 
 |-  ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) Fn NN0
57 56 a1i 
 |-  ( ph -> ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) Fn NN0 )
58 ovex 
 |-  ( ( k + 1 ) / ( k + 1 ) ) e. _V
59 eqid 
 |-  ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) )
60 58 59 fnmpti 
 |-  ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) Fn NN0
61 60 a1i 
 |-  ( ph -> ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) Fn NN0 )
62 10 a1i 
 |-  ( ph -> NN0 e. _V )
63 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
64 eqidd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) ` x ) = ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) ` x ) )
65 eqidd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ` x ) = ( ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ` x ) )
66 57 61 62 62 63 64 65 ofval 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) oF - ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ) ` x ) = ( ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) ` x ) - ( ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ` x ) ) )
67 5 6 20 21 37 47 53 66 climsub 
 |-  ( ph -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) oF - ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ) ~~> ( 0 - 1 ) )
68 ovexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( C + 1 ) / ( k + 1 ) ) e. _V )
69 ovexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k + 1 ) / ( k + 1 ) ) e. _V )
70 eqidd 
 |-  ( ph -> ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) )
71 eqidd 
 |-  ( ph -> ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) )
72 62 68 69 70 71 offval2 
 |-  ( ph -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) oF - ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ) = ( k e. NN0 |-> ( ( ( C + 1 ) / ( k + 1 ) ) - ( ( k + 1 ) / ( k + 1 ) ) ) ) )
73 8 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( C + 1 ) e. CC )
74 24 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. CC )
75 26 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) =/= 0 )
76 73 74 74 75 divsubdird 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( C + 1 ) - ( k + 1 ) ) / ( k + 1 ) ) = ( ( ( C + 1 ) / ( k + 1 ) ) - ( ( k + 1 ) / ( k + 1 ) ) ) )
77 4 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> C e. CC )
78 22 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. CC )
79 1cnd 
 |-  ( ( ph /\ k e. NN0 ) -> 1 e. CC )
80 77 78 79 pnpcan2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( C + 1 ) - ( k + 1 ) ) = ( C - k ) )
81 80 oveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( C + 1 ) - ( k + 1 ) ) / ( k + 1 ) ) = ( ( C - k ) / ( k + 1 ) ) )
82 76 81 eqtr3d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( C + 1 ) / ( k + 1 ) ) - ( ( k + 1 ) / ( k + 1 ) ) ) = ( ( C - k ) / ( k + 1 ) ) )
83 82 mpteq2dva 
 |-  ( ph -> ( k e. NN0 |-> ( ( ( C + 1 ) / ( k + 1 ) ) - ( ( k + 1 ) / ( k + 1 ) ) ) ) = ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) )
84 72 83 eqtrd 
 |-  ( ph -> ( ( k e. NN0 |-> ( ( C + 1 ) / ( k + 1 ) ) ) oF - ( k e. NN0 |-> ( ( k + 1 ) / ( k + 1 ) ) ) ) = ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) )
85 df-neg 
 |-  -u 1 = ( 0 - 1 )
86 85 eqcomi 
 |-  ( 0 - 1 ) = -u 1
87 86 a1i 
 |-  ( ph -> ( 0 - 1 ) = -u 1 )
88 67 84 87 3brtr3d 
 |-  ( ph -> ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) ~~> -u 1 )
89 10 mptex 
 |-  ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) e. _V
90 89 a1i 
 |-  ( ph -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) e. _V )
91 eqidd 
 |-  ( ( ph /\ x e. NN0 ) -> ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) = ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) )
92 oveq2 
 |-  ( k = x -> ( C - k ) = ( C - x ) )
93 oveq1 
 |-  ( k = x -> ( k + 1 ) = ( x + 1 ) )
94 92 93 oveq12d 
 |-  ( k = x -> ( ( C - k ) / ( k + 1 ) ) = ( ( C - x ) / ( x + 1 ) ) )
95 94 adantl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ k = x ) -> ( ( C - k ) / ( k + 1 ) ) = ( ( C - x ) / ( x + 1 ) ) )
96 ovexd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( C - x ) / ( x + 1 ) ) e. _V )
97 91 95 17 96 fvmptd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) ` x ) = ( ( C - x ) / ( x + 1 ) ) )
98 38 41 subcld 
 |-  ( ( ph /\ x e. NN0 ) -> ( C - x ) e. CC )
99 98 42 45 divcld 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( C - x ) / ( x + 1 ) ) e. CC )
100 97 99 eqeltrd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) ` x ) e. CC )
101 eqidd 
 |-  ( ( ph /\ x e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) = ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) )
102 94 fveq2d 
 |-  ( k = x -> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) = ( abs ` ( ( C - x ) / ( x + 1 ) ) ) )
103 102 adantl 
 |-  ( ( ( ph /\ x e. NN0 ) /\ k = x ) -> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) = ( abs ` ( ( C - x ) / ( x + 1 ) ) ) )
104 fvexd 
 |-  ( ( ph /\ x e. NN0 ) -> ( abs ` ( ( C - x ) / ( x + 1 ) ) ) e. _V )
105 101 103 17 104 fvmptd 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ` x ) = ( abs ` ( ( C - x ) / ( x + 1 ) ) ) )
106 97 fveq2d 
 |-  ( ( ph /\ x e. NN0 ) -> ( abs ` ( ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) ` x ) ) = ( abs ` ( ( C - x ) / ( x + 1 ) ) ) )
107 105 106 eqtr4d 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ` x ) = ( abs ` ( ( k e. NN0 |-> ( ( C - k ) / ( k + 1 ) ) ) ` x ) ) )
108 5 88 90 6 100 107 climabs 
 |-  ( ph -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ~~> ( abs ` -u 1 ) )
109 31 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
110 abs1 
 |-  ( abs ` 1 ) = 1
111 109 110 eqtri 
 |-  ( abs ` -u 1 ) = 1
112 108 111 breqtrdi 
 |-  ( ph -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ~~> 1 )