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 ) ) ) ) ) )