Metamath Proof Explorer

Theorem binomcxplemfrat

Description: Lemma for binomcxp . binomcxplemrat implies that when C is not a nonnegative integer, the absolute value of the ratio ( ( F( k + 1 ) ) / ( Fk ) ) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (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 )
binomcxplem.f 
|- F = ( j e. NN0 |-> ( C _Cc j ) )
Assertion binomcxplemfrat 
|- ( ( ph /\ -. C e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) ~~> 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 binomcxplem.f 
 |-  F = ( j e. NN0 |-> ( C _Cc j ) )
6 4 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> C e. CC )
7 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
8 6 7 bccp1k 
 |-  ( ( ph /\ k e. NN0 ) -> ( C _Cc ( k + 1 ) ) = ( ( C _Cc k ) x. ( ( C - k ) / ( k + 1 ) ) ) )
9 5 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> F = ( j e. NN0 |-> ( C _Cc j ) ) )
10 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( k + 1 ) ) -> j = ( k + 1 ) )
11 10 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = ( k + 1 ) ) -> ( C _Cc j ) = ( C _Cc ( k + 1 ) ) )
12 1nn0 
 |-  1 e. NN0
13 12 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> 1 e. NN0 )
14 7 13 nn0addcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. NN0 )
15 ovexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( C _Cc ( k + 1 ) ) e. _V )
16 9 11 14 15 fvmptd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) = ( C _Cc ( k + 1 ) ) )
17 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> j = k )
18 17 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ j = k ) -> ( C _Cc j ) = ( C _Cc k ) )
19 ovexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( C _Cc k ) e. _V )
20 9 18 7 19 fvmptd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( C _Cc k ) )
21 20 oveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( F ` k ) x. ( ( C - k ) / ( k + 1 ) ) ) = ( ( C _Cc k ) x. ( ( C - k ) / ( k + 1 ) ) ) )
22 8 16 21 3eqtr4d 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) = ( ( F ` k ) x. ( ( C - k ) / ( k + 1 ) ) ) )
23 22 adantlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) = ( ( F ` k ) x. ( ( C - k ) / ( k + 1 ) ) ) )
24 23 eqcomd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( F ` k ) x. ( ( C - k ) / ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
25 6 7 bcccl 
 |-  ( ( ph /\ k e. NN0 ) -> ( C _Cc k ) e. CC )
26 20 25 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
27 26 adantlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( F ` k ) e. CC )
28 6 adantlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> C e. CC )
29 simpr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> k e. NN0 )
30 29 nn0cnd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> k e. CC )
31 28 30 subcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( C - k ) e. CC )
32 1cnd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> 1 e. CC )
33 30 32 addcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( k + 1 ) e. CC )
34 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
35 34 nnne0d 
 |-  ( k e. NN0 -> ( k + 1 ) =/= 0 )
36 35 adantl 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( k + 1 ) =/= 0 )
37 31 33 36 divcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( C - k ) / ( k + 1 ) ) e. CC )
38 27 37 mulcld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( F ` k ) x. ( ( C - k ) / ( k + 1 ) ) ) e. CC )
39 23 38 eqeltrd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) e. CC )
40 20 adantlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( F ` k ) = ( C _Cc k ) )
41 elfznn0 
 |-  ( C e. ( 0 ... ( k - 1 ) ) -> C e. NN0 )
42 41 con3i 
 |-  ( -. C e. NN0 -> -. C e. ( 0 ... ( k - 1 ) ) )
43 42 ad2antlr 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> -. C e. ( 0 ... ( k - 1 ) ) )
44 28 29 bcc0 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( C _Cc k ) = 0 <-> C e. ( 0 ... ( k - 1 ) ) ) )
45 44 necon3abid 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( C _Cc k ) =/= 0 <-> -. C e. ( 0 ... ( k - 1 ) ) ) )
46 43 45 mpbird 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( C _Cc k ) =/= 0 )
47 40 46 eqnetrd 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( F ` k ) =/= 0 )
48 39 27 37 47 divmuld 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( ( F ` ( k + 1 ) ) / ( F ` k ) ) = ( ( C - k ) / ( k + 1 ) ) <-> ( ( F ` k ) x. ( ( C - k ) / ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) ) )
49 24 48 mpbird 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) = ( ( C - k ) / ( k + 1 ) ) )
50 49 fveq2d 
 |-  ( ( ( ph /\ -. C e. NN0 ) /\ k e. NN0 ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) = ( abs ` ( ( C - k ) / ( k + 1 ) ) ) )
51 50 mpteq2dva 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) = ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) )
52 1 2 3 4 binomcxplemrat 
 |-  ( ph -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ~~> 1 )
53 52 adantr 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( C - k ) / ( k + 1 ) ) ) ) ~~> 1 )
54 51 53 eqbrtrd 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( k e. NN0 |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) ~~> 1 )