Metamath Proof Explorer

Theorem binomcxp

Description: Generalize the binomial theorem binom to positive real summand A , real summand B , and complex exponent C . Proof in https://en.wikibooks.org/wiki/Advanced_Calculus ; see also https://en.wikipedia.org/wiki/Binomial_series , https://en.wikipedia.org/wiki/Binomial_theorem (sections "Newton's generalized binomial theorem" and "Future generalizations"), and proof "General Binomial Theorem" in https://proofwiki.org/wiki/Binomial_Theorem . (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 binomcxp 
|- ( ph -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )

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 1 2 3 4 binomcxplemnn0 
 |-  ( ( ph /\ C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
6 eqid 
 |-  ( j e. NN0 |-> ( C _Cc j ) ) = ( j e. NN0 |-> ( C _Cc j ) )
7 fveq2 
 |-  ( x = k -> ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) = ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) )
8 oveq2 
 |-  ( x = k -> ( b ^ x ) = ( b ^ k ) )
9 7 8 oveq12d 
 |-  ( x = k -> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) = ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) x. ( b ^ k ) ) )
10 9 cbvmptv 
 |-  ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) = ( k e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) x. ( b ^ k ) ) )
11 10 mpteq2i 
 |-  ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) = ( b e. CC |-> ( k e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) x. ( b ^ k ) ) ) )
12 eqid 
 |-  sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < )
13 id 
 |-  ( x = k -> x = k )
14 oveq2 
 |-  ( y = j -> ( C _Cc y ) = ( C _Cc j ) )
15 14 cbvmptv 
 |-  ( y e. NN0 |-> ( C _Cc y ) ) = ( j e. NN0 |-> ( C _Cc j ) )
16 15 a1i 
 |-  ( x = k -> ( y e. NN0 |-> ( C _Cc y ) ) = ( j e. NN0 |-> ( C _Cc j ) ) )
17 16 13 fveq12d 
 |-  ( x = k -> ( ( y e. NN0 |-> ( C _Cc y ) ) ` x ) = ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) )
18 13 17 oveq12d 
 |-  ( x = k -> ( x x. ( ( y e. NN0 |-> ( C _Cc y ) ) ` x ) ) = ( k x. ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) ) )
19 oveq1 
 |-  ( x = k -> ( x - 1 ) = ( k - 1 ) )
20 19 oveq2d 
 |-  ( x = k -> ( b ^ ( x - 1 ) ) = ( b ^ ( k - 1 ) ) )
21 18 20 oveq12d 
 |-  ( x = k -> ( ( x x. ( ( y e. NN0 |-> ( C _Cc y ) ) ` x ) ) x. ( b ^ ( x - 1 ) ) ) = ( ( k x. ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) ) x. ( b ^ ( k - 1 ) ) ) )
22 21 cbvmptv 
 |-  ( x e. NN |-> ( ( x x. ( ( y e. NN0 |-> ( C _Cc y ) ) ` x ) ) x. ( b ^ ( x - 1 ) ) ) ) = ( k e. NN |-> ( ( k x. ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) ) x. ( b ^ ( k - 1 ) ) ) )
23 22 mpteq2i 
 |-  ( b e. CC |-> ( x e. NN |-> ( ( x x. ( ( y e. NN0 |-> ( C _Cc y ) ) ` x ) ) x. ( b ^ ( x - 1 ) ) ) ) ) = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( ( j e. NN0 |-> ( C _Cc j ) ) ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
24 oveq2 
 |-  ( x = j -> ( C _Cc x ) = ( C _Cc j ) )
25 24 cbvmptv 
 |-  ( x e. NN0 |-> ( C _Cc x ) ) = ( j e. NN0 |-> ( C _Cc j ) )
26 25 fveq1i 
 |-  ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) = ( ( j e. NN0 |-> ( C _Cc j ) ) ` x )
27 26 oveq1i 
 |-  ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) = ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) )
28 27 mpteq2i 
 |-  ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) = ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) )
29 28 mpteq2i 
 |-  ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) = ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) )
30 29 fveq1i 
 |-  ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) = ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r )
31 seqeq3 
 |-  ( ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) = ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) -> seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) = seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) )
32 30 31 ax-mp 
 |-  seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) = seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) )
33 32 eleq1i 
 |-  ( seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> <-> seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> )
34 33 rabbii 
 |-  { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } = { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> }
35 34 supeq1i 
 |-  sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < )
36 35 oveq2i 
 |-  ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) = ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
37 36 imaeq2i 
 |-  ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) = ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) )
38 eqid 
 |-  ( b e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ k e. NN0 ( ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` b ) ` k ) ) = ( b e. ( `' abs " ( 0 [,) sup ( { r e. RR | seq 0 ( + , ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( x e. NN0 |-> ( C _Cc x ) ) ` x ) x. ( b ^ x ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) ) ) |-> sum_ k e. NN0 ( ( ( b e. CC |-> ( x e. NN0 |-> ( ( ( j e. NN0 |-> ( C _Cc j ) ) ` x ) x. ( b ^ x ) ) ) ) ` b ) ` k ) )
39 1 2 3 4 6 11 12 23 37 38 binomcxplemnotnn0 
 |-  ( ( ph /\ -. C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )
40 5 39 pm2.61dan 
 |-  ( ph -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )