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	$⊢ \underset{˙}{\times} = \cdot_{R}$
		crngbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		crngbinom.a	$⊢ \underset{˙}{+} = +_{R}$
		crngbinom.g	$⊢ G = {mulGrp}_{R}$
		crngbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	Assertion	crngbinom	$⊢ ((R \in CRing \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$

Proof

Step	Hyp	Ref	Expression
1		crngbinom.s	$⊢ S = {Base}_{R}$
2		crngbinom.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
3		crngbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		crngbinom.a	$⊢ \underset{˙}{+} = +_{R}$
5		crngbinom.g	$⊢ G = {mulGrp}_{R}$
6		crngbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		crngring	$⊢ R \in CRing \to R \in Ring$
8		ringsrg	$⊢ R \in Ring \to R \in SRing$
9	7 8	syl	$⊢ R \in CRing \to R \in SRing$
10	9	adantr	$⊢ (R \in CRing \land N \in ℕ_{0}) \to R \in SRing$
11	5	crngmgp	$⊢ R \in CRing \to G \in CMnd$
12	11	adantr	$⊢ (R \in CRing \land N \in ℕ_{0}) \to G \in CMnd$
13		simpr	$⊢ (R \in CRing \land N \in ℕ_{0}) \to N \in ℕ_{0}$
14	10 12 13	3jca	$⊢ (R \in CRing \land N \in ℕ_{0}) \to (R \in SRing \land G \in CMnd \land N \in ℕ_{0})$
15	1 2 3 4 5 6	csrgbinom	$⊢ ((R \in SRing \land G \in CMnd \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$
16	14 15	sylan	$⊢ ((R \in CRing \land N \in ℕ_{0}) \land (A \in S \land B \in S)) \to N \underset{˙}{\times} (A \underset{˙}{+} B) = {\sum_{R}}_{k = 0}^{N} ((\binom{N}{k}) \underset{˙}{\cdot} (((N - k) \underset{˙}{\times} A) \underset{˙}{\times} (k \underset{˙}{\times} B)))$