This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crngbinom

Description: The binomial theorem for commutative rings (special case of csrgbinom ): ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) . (Contributed by AV, 24-Aug-2019)

Ref Expression
Hypotheses crngbinom.s 
|- S = ( Base ` R )
crngbinom.m 
|- .X. = ( .r ` R )
crngbinom.t 
|- .x. = ( .g ` R )
crngbinom.a 
|- .+ = ( +g ` R )
crngbinom.g 
|- G = ( mulGrp ` R )
crngbinom.e 
|- .^ = ( .g ` G )
Assertion crngbinom 
|- ( ( ( R e. CRing /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 crngbinom.s 
 |-  S = ( Base ` R )
2 crngbinom.m 
 |-  .X. = ( .r ` R )
3 crngbinom.t 
 |-  .x. = ( .g ` R )
4 crngbinom.a 
 |-  .+ = ( +g ` R )
5 crngbinom.g 
 |-  G = ( mulGrp ` R )
6 crngbinom.e 
 |-  .^ = ( .g ` G )
7 crngring 
 |-  ( R e. CRing -> R e. Ring )
8 ringsrg 
 |-  ( R e. Ring -> R e. SRing )
9 7 8 syl 
 |-  ( R e. CRing -> R e. SRing )
10 9 adantr 
 |-  ( ( R e. CRing /\ N e. NN0 ) -> R e. SRing )
11 5 crngmgp 
 |-  ( R e. CRing -> G e. CMnd )
12 11 adantr 
 |-  ( ( R e. CRing /\ N e. NN0 ) -> G e. CMnd )
13 simpr 
 |-  ( ( R e. CRing /\ N e. NN0 ) -> N e. NN0 )
14 10 12 13 3jca 
 |-  ( ( R e. CRing /\ N e. NN0 ) -> ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) )
15 1 2 3 4 5 6 csrgbinom 
 |-  ( ( ( R e. SRing /\ G e. CMnd /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )
16 14 15 sylan 
 |-  ( ( ( R e. CRing /\ N e. NN0 ) /\ ( A e. S /\ B e. S ) ) -> ( N .^ ( A .+ B ) ) = ( R gsum ( k e. ( 0 ... N ) |-> ( ( N _C k ) .x. ( ( ( N - k ) .^ A ) .X. ( k .^ B ) ) ) ) ) )