# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Ring_Binomial_ZF imports Monoid_ZF_1 Ring_ZF
begin

This theory aims at formalizing sufficient background to be able to state and prove the binomial theorem.

### Sums of multiplicities of powers of ring elements and binomial theorem

The binomial theorem asserts that for any two elements of a commutative ring the n-th power of the sum $$x+y$$ can be written as a sum of certain multiplicities of terms $$x^{n-k}y^k$$, where $$k \in 0..n$$. In this section we setup the notation and prove basic properties of such multiplicities and powers of ring elements. We show the binomial theorem as an application.

The next locale (context) extends the ring0 locale with notation for powers, multiplicities and sums and products of finite lists of ring elements.

locale ring3 = ring0 +

defines $$\sum s \equiv \text{Fold}(A, 0 ,s)$$

defines $$\prod s \equiv \text{Fold}(M,1 ,s)$$

defines $$n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\}$$

defines $$x^{n} \equiv \prod \{\langle k,x\rangle .\ k\in n\}$$

A ring with addition forms a monoid, hence all propositions proven in the monoid1 locale (defined in the Monoid_ZF_1 theory) can be used in the ring3 locale, applied to the additive operation.

using ringAssum unfolding IsAring_def, IsAgroup_def, monoid1_def, monoid0_def

A ring with multiplication forms a monoid, hence all propositions proven in the monoid1 locale (defined in the Monoid_ZF_1 theory) can be used in the ring3 locale, applied to the multiplicative operation.

sublocale ring3 < mul_monoid: monoid1

using ringAssum unfolding IsAring_def, IsAgroup_def, monoid1_def, monoid0_def

$$0\cdot x = 0$$ and $$x^0=1$$. It is a bit surprising that we do not need to assume that $$x\in R$$ (i.e. $$x$$ is an element of the ring). These properties are really proven in the Monoid_ZF_1 theory where there is no assumption that $$x$$ is an element of the monoid.

lemma (in ring3) mult_pow_zero:

shows $$0\cdot x = 0$$ and $$x^{0} = 1$$ using nat_mult_zero, nat_mult_zero

Natural multiple and power of a ring element is a ring element.

lemma (in ring3) mult_pow_type:

assumes $$n\in nat$$, $$x\in R$$

shows $$n\cdot x \in R$$ and $$x^{n} \in R$$ using assms, nat_mult_type, nat_mult_type

The usual properties of multiples and powers: $$(n+1)x = nx+x$$ and $$x^n+1=x^n x$$. These are just versions of nat_mult_add_one from Monoid_ZF_1 writtent in the notation defined in the ring3 locale.

assumes $$n\in nat$$, $$x\in R$$

shows $$(n + 1)\cdot x = (n\cdot x) + x$$ and $$x^{n + 1} = x^{n}\cdot x$$ using assms, nat_mult_add_one, nat_mult_add_one

Associativity for the multiplication by natural number and the ring multiplication:

lemma (in ring3) nat_mult_assoc:

assumes $$n\in nat$$, $$x\in R$$, $$y\in R$$

shows $$n\cdot x\cdot y = n\cdot (x\cdot y)$$proof
from assms(1,3) have $$n\in nat$$ and $$0\cdot x\cdot y = 0\cdot (x\cdot y)$$ using mult_pow_zero(1), Ring_ZF_1_L6
moreover
from assms(2,3) have $$\forall k\in nat.\$$ $$k\cdot x\cdot y = k\cdot (x\cdot y) \longrightarrow (k + 1)\cdot x\cdot y = (k + 1)\cdot (x\cdot y)$$ using nat_mult_pow_add_one(1), mult_pow_type, ring_oper_distr(2), Ring_ZF_1_L4(3)
ultimately show $$thesis$$ by (rule ind_on_nat1 )
qed

Addition of natural numbers is distributive with respect to natural multiple. This is essentially lemma nat_mult_add from Monoid_ZF_1.thy, just transferred to the ring3 locale.

assumes $$n\in nat$$, $$m\in nat$$, $$x\in R$$

shows $$(n + m)\cdot x = n\cdot x + m\cdot x$$ using assms, nat_mult_add

Associativity for the multiplication by natural number and the ring multiplication extended to three elements of the ring:

lemma (in ring3) nat_mult_assoc1:

assumes $$n\in nat$$, $$x\in R$$, $$y\in R$$, $$z\in R$$

shows $$n\cdot x\cdot y\cdot z = n\cdot (x\cdot y\cdot z)$$ using assms, Ring_ZF_1_L4(3), nat_mult_assoc

When we multiply an expression whose value belongs to a ring by a ring element and we get an expression whose value belongs to a ring.

lemma (in ring3) mult_elem_ring_type:

assumes $$n\in nat$$, $$x\in R$$ and $$\forall k\in n.\ q(k) \in R$$

shows $$\forall k\in n.\ q(k)\cdot x \in R$$ and $$(\sum \{\langle k,q(k)\cdot x\rangle .\ k\in n\}) \in R$$ using assms, Ring_ZF_1_L4(3), sum_in_mono

The sum of expressions whose values belong to a ring is an expression whose value belongs to a ring.

lemma (in ring3) sum_expr_ring_type:

assumes $$n\in nat$$, $$\forall k\in n.\ q(k) \in R$$, $$\forall k\in n.\ p(k) \in R$$

shows $$\forall k\in n.\ q(k) + p(k) \in R$$ and $$(\sum \{\langle k,q(k) + p(k)\rangle .\ k\in n\}) \in R$$ using assms, Ring_ZF_1_L4(1), sum_in_mono

Combining mult_elem_ring_type and sum_expr_ring_type we obtain that a (kind of) linear combination of expressions whose values belong to a ring belongs to the ring.

lemma (in ring3) lin_comb_expr_ring_type:

assumes $$n\in nat$$, $$x\in R$$, $$y\in R$$, $$\forall k\in n.\ q(k) \in R$$, $$\forall k\in n.\ p(k) \in R$$

shows $$\forall k\in n.\ q(k)\cdot x + p(k)\cdot y \in R$$ and $$(\sum \{\langle k,q(k)\cdot x + p(k)\cdot y\rangle .\ k\in n\}) \in R$$proof
from assms have $$\forall k\in n.\ q(k)\cdot x \in R$$ and $$\forall k\in n.\ p(k)\cdot y \in R$$ using mult_elem_ring_type(1)
with assms(1) show $$\forall k\in n.\ q(k)\cdot x + p(k)\cdot y \in R$$ using sum_expr_ring_type(1)
with assms(1) show $$(\sum \{\langle k,q(k)\cdot x + p(k)\cdot y\rangle .\ k\in n\}) \in R$$ using sum_in_mono
qed

A ring3 version of seq_sum_pull_one_elem from Monoid_ZF_1:

lemma (in ring3) rng_seq_sum_pull_one_elem:

assumes $$j \in nat$$, $$\forall k\in j + 1.\ q(k) \in R$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = q(0) + (\sum \{\langle k,q(k + 1)\rangle .\ k\in j\})$$, $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j)$$ using assms, seq_sum_pull_one_elem

Distributive laws for finite sums in a ring: $$(\sum_{k=0}^{n-1}q(k))\cdot x = \sum_{k=0}^{n-1}q(k)\cdot x$$ and $$x\cdot (\sum_{k=0}^{n-1}q(k)) = \sum_{k=0}^{n-1}x\cdot q(k)$$.

theorem (in ring3) fin_sum_distrib:

assumes $$x\in R$$, $$n\in nat$$, $$\forall k\in n.\ q(k) \in R$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in n\})\cdot x = \sum \{\langle k,q(k)\cdot x\rangle .\ k\in n\}$$, $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in n\}) = \sum \{\langle k,x\cdot q(k)\rangle .\ k\in n\}$$proof
from assms(1,2) have $$n\in nat$$ and $$(\sum \{\langle k,q(k)\rangle .\ k\in 0\})\cdot x = \sum \{\langle k,q(k)\cdot x\rangle .\ k\in 0\}$$ using sum_empty, Ring_ZF_1_L6(1)
moreover
have $$\forall j\in n.\ (\sum \{\langle k,q(k)\rangle .\ k\in j\})\cdot x = (\sum \{\langle k,q(k)\cdot x\rangle .\ k\in j\})$$ $$\longrightarrow (\sum \{\langle k,q(k)\rangle .\ k\in j + 1\})\cdot x = \sum \{\langle k,q(k)\cdot x\rangle .\ k\in j + 1\}$$proof
{
fix $$j$$
assume $$j\in n$$ and I: $$(\sum \{\langle k,q(k)\rangle .\ k\in j\})\cdot x = (\sum \{\langle k,q(k)\cdot x\rangle .\ k\in j\})$$
from assms(2), $$j\in n$$ have $$j\in nat$$ using elem_nat_is_nat(2)
moreover
from assms(2,3), $$j\in n$$ have II: $$\forall k\in j + 1.\ q(k) \in R$$ using mem_add_one_subset
ultimately have $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j)$$ using seq_sum_pull_one_elem(2)
hence $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\})\cdot x = ((\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j))\cdot x$$
moreover
from assms(1), $$j\in nat$$, II have $$(\sum \{\langle k,q(k)\rangle .\ k\in j\}) \in R$$, $$q(j) \in R$$ and $$x\in R$$ using sum_in_mono
ultimately have $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\})\cdot x = (\sum \{\langle k,q(k)\rangle .\ k\in j\})\cdot x + q(j)\cdot x$$ using ring_oper_distr(2)
with I have $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\})\cdot x = (\sum \{\langle k,q(k)\cdot x\rangle .\ k\in j\}) + q(j)\cdot x$$
moreover
from assms(1), II have $$\forall k\in j + 1.\ q(k)\cdot x \in R$$ using Ring_ZF_1_L4(3)
with $$j\in nat$$ have $$(\sum \{\langle k,q(k)\cdot x\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\cdot x\rangle .\ k\in j\}) + q(j)\cdot x$$ using seq_sum_pull_one_elem(2)
ultimately have $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\})\cdot x = (\sum \{\langle k,q(k)\cdot x\rangle .\ k\in j + 1\})$$
}
thus $$thesis$$
qed
ultimately show $$(\sum \{\langle k,q(k)\rangle .\ k\in n\})\cdot x = \sum \{\langle k,q(k)\cdot x\rangle .\ k\in n\}$$ by (rule fin_nat_ind1 )
from assms(1,2) have $$n\in nat$$ and $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in 0\}) = \sum \{\langle k,x\cdot q(k)\rangle .\ k\in 0\}$$ using sum_empty, Ring_ZF_1_L6(2)
moreover
have $$\forall j\in n.\ x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j\}) = (\sum \{\langle k,x\cdot q(k)\rangle .\ k\in j\})$$ $$\longrightarrow x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = \sum \{\langle k,x\cdot q(k)\rangle .\ k\in j + 1\}$$proof
{
fix $$j$$
assume $$j\in n$$ and I: $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j\}) = (\sum \{\langle k,x\cdot q(k)\rangle .\ k\in j\})$$
from assms(2), $$j\in n$$ have $$j\in nat$$ using elem_nat_is_nat(2)
moreover
from assms(2,3), $$j\in n$$ have II: $$\forall k\in j + 1.\ q(k) \in R$$ using mem_add_one_subset
ultimately have $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j)$$ using seq_sum_pull_one_elem(2)
hence $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = x\cdot ((\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j))$$
moreover
from assms(1), $$j\in nat$$, II have $$(\sum \{\langle k,q(k)\rangle .\ k\in j\}) \in R$$, $$q(j) \in R$$ and $$x\in R$$ using sum_in_mono
ultimately have $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + x\cdot q(j)$$ using ring_oper_distr(1)
with I have $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,x\cdot q(k)\rangle .\ k\in j\}) + x\cdot q(j)$$
moreover
from assms(1), II have $$\forall k\in j + 1.\ x\cdot q(k) \in R$$ using Ring_ZF_1_L4(3)
with $$j\in nat$$ have $$(\sum \{\langle k,x\cdot q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,x\cdot q(k)\rangle .\ k\in j\}) + x\cdot q(j)$$ using seq_sum_pull_one_elem(2)
ultimately have $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,x\cdot q(k)\rangle .\ k\in j + 1\})$$
}
thus $$thesis$$
qed
ultimately show $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in n\}) = \sum \{\langle k,x\cdot q(k)\rangle .\ k\in n\}$$ by (rule fin_nat_ind1 )
qed

In rings we have $$\sum_{k=0}^{n-1}q(k) + p(k) = (\sum_{k=0}^{n-1} p(k)) + (\sum_{k=0}^{n-1} q(k))$$. This is the same as theorem sum_comm_distrib in Monoid_ZF_1.thy, except that we do not need the assumption about commutativity of the operation as addition in rings is always commutative.

lemma (in ring3) sum_ring_distrib:

assumes $$n\in nat$$ and $$\forall k\in n.\ p(k) \in R$$, $$\forall k\in n.\ q(k) \in R$$

shows $$(\sum \{\langle k,p(k) + q(k)\rangle .\ k\in n\}) = (\sum \{\langle k,p(k)\rangle .\ k\in n\}) + (\sum \{\langle k,q(k)\rangle .\ k\in n\})$$ using assms, Ring_ZF_1_L1(3), sum_comm_distrib

To shorten the notation in the proof of the binomial theorem we give a name to the binomial term $${n \choose k} x^{n-k} y^k$$.

definition (in ring3)

$$\text{BT}(n,k,x,y) \equiv {{n}\choose {k}}\cdot x^{n - k}\cdot y^{k}$$

If $$n,k$$ are natural numbers and $$x,y$$ are ring elements then the binomial term is an element of the ring.

lemma (in ring3) bt_type:

assumes $$n\in nat$$, $$k\in nat$$, $$x\in R$$, $$y\in R$$

shows $$\text{BT}(n,k,x,y) \in R$$ using assms, mult_pow_type, binom_in_nat, Ring_ZF_1_L4(3) unfolding BT_def

The binomial term is $$1$$ when the $$n=0$$ and $$k=0$$. Somehow we do not need the assumption that $$x,y$$ are ring elements.

lemma (in ring3) bt_at_zero:

shows $$\text{BT}(0,0,x,y) = 1$$ using binom_zero_zero, mult_pow_zero(2), nat_mult_one, Ring_ZF_1_L2(2), Ring_ZF_1_L3(5) unfolding BT_def

The binomial term is $$x^n$$ when $$k=0$$.

lemma (in ring3) bt_at_zero1:

assumes $$n\in nat$$, $$x\in R$$

shows $$\text{BT}(n,0,x,y) = x^{n}$$ unfolding BT_def using assms, mult_pow_zero(2), binom_left_boundary, mult_pow_type(2), nat_mult_one, Ring_ZF_1_L3(5)

When $$k=0$$ multiplying the binomial term by $$x$$ is the same as adding one to $$n$$.

lemma (in ring3) bt_at_zero2:

assumes $$n\in nat$$, $$x\in R$$

shows $$\text{BT}(n,0,x,y)\cdot x = \text{BT}(n + 1,0,x,y)$$ using assms, bt_at_zero1, nat_mult_pow_add_one(2)

The binomial term is $$y^n$$ when $$k=n$$.

lemma (in ring3) bt_at_right:

assumes $$n\in nat$$, $$y\in R$$

shows $$\text{BT}(n,n,x,y) = y^{n}$$ unfolding BT_def using assms, binom_right_boundary, mult_pow_zero(2), nat_mult_one, Ring_ZF_1_L2(2), mult_pow_type(2), Ring_ZF_1_L3(6)

When $$k=n$$ multiplying the binomial term by $$x$$ is the same as adding one to $$n$$.

lemma (in ring3) bt_at_right1:

assumes $$n\in nat$$, $$y\in R$$

shows $$\text{BT}(n,n,x,y)\cdot y = \text{BT}(n + 1,n + 1,x,y)$$ using assms, bt_at_right, nat_mult_pow_add_one(2)

A key identity for binomial terms needed for the proof of the binomial theorem:

lemma (in ring3) bt_rec_identity:

assumes $$M \text{ is commutative on } R$$, $$j\in nat$$, $$k\in j$$, $$x\in R$$, $$y\in R$$

shows $$\text{BT}(j,k + 1,x,y)\cdot x + \text{BT}(j,k,x,y)\cdot y = \text{BT}(j + 1,k + 1,x,y)$$proof
from assms(2,3,4) have $$k\in nat$$, $${{j}\choose {k + 1}} \in nat$$ and $${{j}\choose {k}} \in nat$$, $${{j + 1}\choose {k + 1}} \in nat$$ and I: $$x^{j - (k + 1)} \in R$$ and II: $$x^{j - k} \in R$$ using elem_nat_is_nat(2), binom_in_nat, mult_pow_type(2)
with assms(5) have III: $$y^{k + 1} \in R$$ using mult_pow_type(2)
let $$L = \text{BT}(j,k + 1,x,y)\cdot x + \text{BT}(j,k,x,y)\cdot y$$
let $$p = x^{j - k}\cdot y^{k + 1}$$
from assms(2,4), $$k\in nat$$, II, III have $$p \in R$$ using mult_pow_type(2), Ring_ZF_1_L4(3)
from assms(2,3,4,5) have $$\text{BT}(j,k,x,y)\cdot y = {{j}\choose {k}}\cdot p$$ using elem_nat_is_nat(2), binom_in_nat, mult_pow_type(2), nat_mult_assoc1, Ring_ZF_1_L11(2), nat_mult_pow_add_one(2) unfolding BT_def
moreover
have $$\text{BT}(j,k + 1,x,y)\cdot x = {{j}\choose {k + 1}}\cdot p$$proof
from assms(1,4), $${{j}\choose {k + 1}} \in nat$$, I, III have $${{j}\choose {k + 1}}\cdot x^{j - (k + 1)}\cdot y^{k + 1}\cdot x =$$ $${{j}\choose {k + 1}}\cdot (x^{j - (k + 1) + 1}\cdot y^{k + 1})$$ using nat_mult_assoc1, Ring_ZF_2_L4(2), nat_mult_pow_add_one(2)
with assms(2,3) have $${{j}\choose {k + 1}}\cdot x^{j - (k + 1)}\cdot y^{k + 1}\cdot x =$$ $${{j}\choose {k + 1}}\cdot (x^{j - (k + 1) + 1}\cdot y^{k + 1})$$ using nat_subtr_simpl0
moreover
from assms(2,3) have $$x^{j - (k + 1) + 1} = x^{j - k}$$ using nat_subtr_simpl0
ultimately show $$thesis$$ unfolding BT_def
qed
ultimately have $$L = {{j}\choose {k + 1}}\cdot p + {{j}\choose {k}}\cdot p$$
with assms(2,3), $${{j}\choose {k + 1}} \in nat$$, $${{j}\choose {k}} \in nat$$, $$p \in R$$ have $$L = {{j + 1}\choose {k + 1}}\cdot p$$ using nat_add_mult_distrib, binom_prop2, succ_ineq1(3)
with assms(2,3), $${{j + 1}\choose {k + 1}} \in nat$$, II, III show $$thesis$$ using nat_mult_assoc, nat_subtr_simpl0 unfolding BT_def
qed

The binomial theorem: if $$x,y$$ are elements of a commutative ring, $$n\in \mathbb{N}$$ then $$(x+y)^n = \sum_{k=0}^{n} {n \choose k} x^{n-k} y^k$$.

theorem (in ring3) binomial_theorem:

assumes $$M \text{ is commutative on } R$$, $$n\in nat$$, $$x\in R$$, $$y\in R$$

shows $$(x + y)^{n} = \sum \{\langle k,{{n}\choose {k}}\cdot x^{n - k} \cdot y^{k}\rangle .\ k\in n + 1\}$$proof
from assms(2) have $$n\in nat$$
moreover
have $$(x + y)^{0} = \sum \{\langle k, \text{BT}(0,k,x,y)\rangle .\ k\in 0 + 1\}$$proof
from assms(3,4) have $$(\sum \{\langle k, \text{BT}(0,k,x,y)\rangle .\ k\in 0 + 1\}) = 1$$ using bt_at_zero, Ring_ZF_1_L2(2), seq_sum_singleton
then show $$thesis$$ using mult_pow_zero(2)
qed
moreover
have $$\forall j\in nat.\$$ $$(x + y)^{j} = (\sum \{\langle k, \text{BT}(j,k,x,y)\rangle .\ k\in j + 1\}) \longrightarrow$$ $$(x + y)^{j + 1} = (\sum \{\langle k, \text{BT}(j + 1,k,x,y)\rangle .\ k\in j + 1 + 1\})$$proof
{
fix $$j$$
let $$s_0 = \sum \{\langle k, \text{BT}(j,k,x,y)\rangle .\ k\in j + 1\}$$
let $$s_1 = \sum \{\langle k, \text{BT}(j,k,x,y)\cdot x\rangle .\ k\in j + 1\}$$
let $$s_2 = \sum \{\langle k, \text{BT}(j,k,x,y)\cdot y\rangle .\ k\in j + 1\}$$
let $$s_3 = \sum \{\langle k, \text{BT}(j,k + 1,x,y)\cdot x\rangle .\ k\in j\}$$
let $$s_4 = \sum \{\langle k, \text{BT}(j,k,x,y)\cdot y\rangle .\ k\in j\}$$
let $$s_5 = \sum \{\langle k, \text{BT}(j,k + 1,x,y)\cdot x + \text{BT}(j,k,x,y)\cdot y\rangle .\ k\in j\}$$
let $$s_6 = \sum \{\langle k, \text{BT}(j + 1,k + 1,x,y)\rangle .\ k\in j\}$$
let $$s_7 = \sum \{\langle k, \text{BT}(j + 1,k,x,y)\rangle .\ k\in j + 1\}$$
let $$s_8 = \sum \{\langle k, \text{BT}(j + 1,k,x,y)\rangle .\ k\in j + 1 + 1\}$$
assume $$j\in nat$$ and $$(x + y)^{j} = s_0$$
then have $$j + 1 \in nat$$ and $$j + 1 + 1 \in nat$$
have I: $$\forall k\in j + 1.\ \text{BT}(j,k,x,y) \in R$$ and II: $$\forall k\in j + 1.\ \text{BT}(j,k,x,y)\cdot x \in R$$ and III: $$\forall k\in j + 1.\ \text{BT}(j,k,x,y)\cdot y \in R$$ and IV: $$\forall k\in j.\ \text{BT}(j,k + 1,x,y)\cdot x \in R$$ and V: $$\forall k\in j.\ \text{BT}(j,k,x,y)\cdot y \in R$$ and VI: $$\forall k\in j + 1.\ \text{BT}(j + 1,k,x,y) \in R$$ and VII: $$\forall k\in j + 1 + 1.\ \text{BT}(j + 1,k,x,y) \in R$$proof
from assms(3,4), $$j\in nat$$ show $$\forall k\in j + 1.\ \text{BT}(j,k,x,y) \in R$$ using elem_nat_is_nat(2), bt_type
with assms(3,4), $$j\in nat$$ show $$\forall k\in j + 1.\ \text{BT}(j,k,x,y)\cdot x \in R$$ and $$\forall k\in j + 1.\ \text{BT}(j,k,x,y)\cdot y \in R$$ and $$\forall k\in j.\ \text{BT}(j,k,x,y)\cdot y \in R$$ using Ring_ZF_1_L4(3)
from assms(3,4), $$j\in nat$$ have $$\forall k\in j.\ \text{BT}(j,k + 1,x,y) \in R$$ using elem_nat_is_nat(2), bt_type
with $$j\in nat$$, assms(3) show $$\forall k\in j.\ \text{BT}(j,k + 1,x,y)\cdot x \in R$$ using mult_elem_ring_type(1)
from assms(3,4), $$j + 1 \in nat$$ show $$\forall k\in j + 1.\ \text{BT}(j + 1,k,x,y) \in R$$ using elem_nat_is_nat(2), bt_type
from assms(3,4), $$j + 1 + 1 \in nat$$ show $$\forall k\in j + 1 + 1.\ \text{BT}(j + 1,k,x,y) \in R$$ using elem_nat_is_nat(2), bt_type
qed
have $$(x + y)^{j + 1} = s_0\cdot x + s_0\cdot y$$proof
from assms(3,4), $$j\in nat$$ have $$(x + y)^{j + 1} = (x + y)^{j}\cdot x + (x + y)^{j}\cdot y$$ using Ring_ZF_1_L4(1), mult_pow_type, nat_mult_pow_add_one(2), ring_oper_distr(1)
with $$(x + y)^{j} = s_0$$ show $$thesis$$
qed
also
have $$s_0\cdot x + s_0\cdot y = s_1 + s_2$$proof
from assms(3), $$j + 1 \in nat$$, I have $$s_0\cdot x = s_1$$ by (rule fin_sum_distrib )
moreover
from assms(4), $$j + 1 \in nat$$, I have $$s_0\cdot y = s_2$$ by (rule fin_sum_distrib )
ultimately show $$thesis$$
qed
also
have $$s_1 + s_2 =$$ $$( \text{BT}(j,0,x,y)\cdot x + s_3) + (s_4 + \text{BT}(j,j,x,y)\cdot y)$$proof
from $$j\in nat$$, II have $$s_1 = \text{BT}(j,0,x,y)\cdot x + s_3$$ using rng_seq_sum_pull_one_elem(1)
moreover
from $$j\in nat$$, III have $$s_2 = s_4 + \text{BT}(j,j,x,y)\cdot y$$ using rng_seq_sum_pull_one_elem(2)
ultimately show $$thesis$$
qed
also
from assms(3,4), IV, V, $$j\in nat$$ have $$( \text{BT}(j,0,x,y)\cdot x + s_3) + (s_4 + \text{BT}(j,j,x,y)\cdot y) =$$ $$\text{BT}(j,0,x,y)\cdot x + (s_3 + s_4) + \text{BT}(j,j,x,y)\cdot y$$ using bt_type, Ring_ZF_1_L4(3), sum_in_mono, Ring_ZF_2_L2(3)
also
have $$\text{BT}(j,0,x,y)\cdot x + (s_3 + s_4) + \text{BT}(j,j,x,y)\cdot y =$$ $$\text{BT}(j,0,x,y)\cdot x + s_5 + \text{BT}(j,j,x,y)\cdot y$$proof
from $$j\in nat$$, IV, V have $$s_3 + s_4 = s_5$$ using sum_ring_distrib
thus $$thesis$$
qed
also
from assms(1,3,4), $$j\in nat$$ have $$\text{BT}(j,0,x,y)\cdot x + s_5 + \text{BT}(j,j,x,y)\cdot y =$$ $$\text{BT}(j,0,x,y)\cdot x + s_6 + \text{BT}(j,j,x,y)\cdot y$$ using bt_rec_identity
also
have $$\text{BT}(j,0,x,y)\cdot x + s_6 + \text{BT}(j,j,x,y)\cdot y =$$ $$s_7 + \text{BT}(j,j,x,y)\cdot y$$proof
from $$j\in nat$$, VI have $$s_7 = \text{BT}(j + 1,0,x,y) + s_6$$ by (rule rng_seq_sum_pull_one_elem )
with assms(3), $$j\in nat$$ show $$thesis$$ using bt_at_zero2
qed
also
have $$s_7 + \text{BT}(j,j,x,y)\cdot y = s_8$$proof
from $$j + 1 \in nat$$, VII have $$s_8 = s_7 + \text{BT}(j + 1,j + 1,x,y)$$ by (rule rng_seq_sum_pull_one_elem )
with assms(4), $$j\in nat$$ show $$thesis$$ using bt_at_right1
qed
finally have $$(x + y)^{j + 1} = s_8$$
}
thus $$thesis$$
qed
ultimately have $$(x + y)^{n} = \sum \{\langle k, \text{BT}(n,k,x,y)\rangle .\ k\in n + 1\}$$ by (rule ind_on_nat1 )
then show $$thesis$$ unfolding BT_def
qed
end
Definition of IsAring: $$\text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge$$ $$\text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M)$$
Definition of IsAgroup: $$\text{IsAgroup}(G,f) \equiv$$ $$( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f)))$$
lemma (in monoid1) nat_mult_zero: shows $$0\cdot x = 0$$
lemma (in monoid1) nat_mult_type:

assumes $$n\in nat$$, $$x\in G$$

shows $$n\cdot x \in G$$

assumes $$n\in nat$$, $$x\in G$$

shows $$(n + 1)\cdot x = n\cdot x \oplus x$$ and $$(n + 1)\cdot x = x \oplus n\cdot x$$
lemma (in ring3) mult_pow_zero: shows $$0\cdot x = 0$$ and $$x^{0} = 1$$
lemma (in ring0) Ring_ZF_1_L6:

assumes $$x\in R$$

shows $$0 \cdot x = 0$$, $$x\cdot 0 = 0$$

assumes $$n\in nat$$, $$x\in R$$

shows $$(n + 1)\cdot x = (n\cdot x) + x$$ and $$x^{n + 1} = x^{n}\cdot x$$
lemma (in ring3) mult_pow_type:

assumes $$n\in nat$$, $$x\in R$$

shows $$n\cdot x \in R$$ and $$x^{n} \in R$$
lemma (in ring0) ring_oper_distr:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b + c) = a\cdot b + a\cdot c$$, $$(b + c)\cdot a = b\cdot a + c\cdot a$$
lemma (in ring0) Ring_ZF_1_L4:

assumes $$a\in R$$, $$b\in R$$

shows $$a + b \in R$$, $$a - b \in R$$, $$a\cdot b \in R$$, $$a + b = b + a$$
lemma ind_on_nat1:

assumes $$n\in nat$$ and $$P(0)$$ and $$\forall k\in nat.\ P(k)\longrightarrow P(k + 1)$$

shows $$P(n)$$

assumes $$n\in nat$$, $$m\in nat$$, $$x\in G$$

shows $$(n + m)\cdot x = n\cdot x \oplus m\cdot x$$
lemma (in ring3) nat_mult_assoc:

assumes $$n\in nat$$, $$x\in R$$, $$y\in R$$

shows $$n\cdot x\cdot y = n\cdot (x\cdot y)$$
lemma (in monoid1) sum_in_mono:

assumes $$n\in nat$$, $$\forall k\in n.\ q(k)\in G$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in n\}) \in G$$
lemma (in ring0) Ring_ZF_1_L4:

assumes $$a\in R$$, $$b\in R$$

shows $$a + b \in R$$, $$a - b \in R$$, $$a\cdot b \in R$$, $$a + b = b + a$$
lemma (in ring3) mult_elem_ring_type:

assumes $$n\in nat$$, $$x\in R$$ and $$\forall k\in n.\ q(k) \in R$$

shows $$\forall k\in n.\ q(k)\cdot x \in R$$ and $$(\sum \{\langle k,q(k)\cdot x\rangle .\ k\in n\}) \in R$$
lemma (in ring3) sum_expr_ring_type:

assumes $$n\in nat$$, $$\forall k\in n.\ q(k) \in R$$, $$\forall k\in n.\ p(k) \in R$$

shows $$\forall k\in n.\ q(k) + p(k) \in R$$ and $$(\sum \{\langle k,q(k) + p(k)\rangle .\ k\in n\}) \in R$$
theorem (in monoid1) seq_sum_pull_one_elem:

assumes $$n \in nat$$, $$\forall k\in n + 1.\ q(k) \in G$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\})$$, $$(\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n)$$
lemma (in monoid1) sum_empty:

assumes $$s:0\rightarrow G$$

shows $$(\sum s) = 0$$
lemma (in ring0) Ring_ZF_1_L6:

assumes $$x\in R$$

shows $$0 \cdot x = 0$$, $$x\cdot 0 = 0$$
lemma elem_nat_is_nat:

assumes $$n \in nat$$ and $$k\in n$$

shows $$k \lt n$$, $$k \in nat$$, $$k \leq n$$, $$\langle k,n\rangle \in Le$$

assumes $$n \in nat$$, $$k\in n$$

shows $$k + 1 \subseteq n$$
theorem (in monoid1) seq_sum_pull_one_elem:

assumes $$n \in nat$$, $$\forall k\in n + 1.\ q(k) \in G$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\})$$, $$(\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n)$$
lemma fin_nat_ind1:

assumes $$n\in nat$$ and $$P(0)$$ and $$\forall j\in n.\ P(j)\longrightarrow P(j + 1)$$

shows $$\forall k\in n + 1.\ P(k)$$ and $$P(n)$$
lemma (in ring0) Ring_ZF_1_L6:

assumes $$x\in R$$

shows $$0 \cdot x = 0$$, $$x\cdot 0 = 0$$
lemma (in ring0) ring_oper_distr:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b + c) = a\cdot b + a\cdot c$$, $$(b + c)\cdot a = b\cdot a + c\cdot a$$
lemma (in ring0) Ring_ZF_1_L1: shows $$monoid0(R,M)$$, $$group0(R,A)$$, $$A \text{ is commutative on } R$$
theorem (in monoid1) sum_comm_distrib:

assumes $$f \text{ is commutative on } G$$, $$n\in nat$$ and $$\forall k\in n.\ p(k) \in G$$, $$\forall k\in n.\ q(k) \in G$$

shows $$(\sum \{\langle k,p(k)\oplus q(k)\rangle .\ k\in n\}) = (\sum \{\langle k,p(k)\rangle .\ k\in n\}) \oplus (\sum \{\langle k,q(k)\rangle .\ k\in n\})$$
lemma binom_in_nat:

assumes $$n\in nat$$

shows $${{n}\choose {k}} \in nat$$
Definition of BT: $$\text{BT}(n,k,x,y) \equiv {{n}\choose {k}}\cdot x^{n - k}\cdot y^{k}$$
lemma binom_zero_zero: shows $${{0}\choose {0}} = 1$$
lemma (in ring3) mult_pow_zero: shows $$0\cdot x = 0$$ and $$x^{0} = 1$$
lemma (in monoid1) nat_mult_one:

assumes $$x\in G$$

shows $$1\cdot x = x$$
lemma (in ring0) Ring_ZF_1_L2: shows $$0 \in R$$, $$1 \in R$$, $$( - 0 ) = 0$$
lemma (in ring0) Ring_ZF_1_L3:

assumes $$a\in R$$

shows $$( - a) \in R$$, $$( - ( - a)) = a$$, $$a + 0 = a$$, $$0 + a = a$$, $$a\cdot 1 = a$$, $$1 \cdot a = a$$, $$a - a = 0$$, $$a - 0 = a$$, $$2 \cdot a = a + a$$, $$( - a) + a = 0$$
theorem binom_left_boundary:

assumes $$n\in nat$$

shows $${{n}\choose {0}} = 1$$
lemma (in ring3) mult_pow_type:

assumes $$n\in nat$$, $$x\in R$$

shows $$n\cdot x \in R$$ and $$x^{n} \in R$$
lemma (in ring3) bt_at_zero1:

assumes $$n\in nat$$, $$x\in R$$

shows $$\text{BT}(n,0,x,y) = x^{n}$$

assumes $$n\in nat$$, $$x\in R$$

shows $$(n + 1)\cdot x = (n\cdot x) + x$$ and $$x^{n + 1} = x^{n}\cdot x$$
theorem binom_right_boundary:

assumes $$n\in nat$$

shows $${{n}\choose {n}} = 1$$
lemma (in ring0) Ring_ZF_1_L3:

assumes $$a\in R$$

shows $$( - a) \in R$$, $$( - ( - a)) = a$$, $$a + 0 = a$$, $$0 + a = a$$, $$a\cdot 1 = a$$, $$1 \cdot a = a$$, $$a - a = 0$$, $$a - 0 = a$$, $$2 \cdot a = a + a$$, $$( - a) + a = 0$$
lemma (in ring3) bt_at_right:

assumes $$n\in nat$$, $$y\in R$$

shows $$\text{BT}(n,n,x,y) = y^{n}$$
lemma (in ring3) nat_mult_assoc1:

assumes $$n\in nat$$, $$x\in R$$, $$y\in R$$, $$z\in R$$

shows $$n\cdot x\cdot y\cdot z = n\cdot (x\cdot y\cdot z)$$
lemma (in ring0) Ring_ZF_1_L11:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a + b + c = a + (b + c)$$, $$a\cdot b\cdot c = a\cdot (b\cdot c)$$
lemma (in ring0) Ring_ZF_2_L4:

assumes $$M \text{ is commutative on } R$$ and $$a\in R$$, $$b\in R$$, $$c\in R$$

shows $$a\cdot (b\cdot c) = a\cdot c\cdot b$$ and $$a\cdot b\cdot c = a\cdot c\cdot b$$
lemma nat_subtr_simpl0:

assumes $$n\in nat$$, $$k\in n$$

shows $$n - (k + 1) + 1 = n - k$$

assumes $$n\in nat$$, $$m\in nat$$, $$x\in R$$

shows $$(n + m)\cdot x = n\cdot x + m\cdot x$$
lemma binom_prop2:

assumes $$n\in nat$$, $$k \in n + 1$$

shows $${{n + 1}\choose {k + 1}} = {{n}\choose {k + 1}} + {{n}\choose {k}}$$
lemma succ_ineq1:

assumes $$n \in nat$$, $$i\in n$$

shows $$succ(i) \in succ(n)$$, $$i + 1 \in n + 1$$, $$i \in n + 1$$
lemma (in ring3) bt_at_zero: shows $$\text{BT}(0,0,x,y) = 1$$
lemma (in monoid1) seq_sum_singleton:

assumes $$q(0) \in G$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in 1\}) = q(0)$$
lemma (in ring3) bt_type:

assumes $$n\in nat$$, $$k\in nat$$, $$x\in R$$, $$y\in R$$

shows $$\text{BT}(n,k,x,y) \in R$$
theorem (in ring3) fin_sum_distrib:

assumes $$x\in R$$, $$n\in nat$$, $$\forall k\in n.\ q(k) \in R$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in n\})\cdot x = \sum \{\langle k,q(k)\cdot x\rangle .\ k\in n\}$$, $$x\cdot (\sum \{\langle k,q(k)\rangle .\ k\in n\}) = \sum \{\langle k,x\cdot q(k)\rangle .\ k\in n\}$$
lemma (in ring3) rng_seq_sum_pull_one_elem:

assumes $$j \in nat$$, $$\forall k\in j + 1.\ q(k) \in R$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = q(0) + (\sum \{\langle k,q(k + 1)\rangle .\ k\in j\})$$, $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j)$$
lemma (in ring3) rng_seq_sum_pull_one_elem:

assumes $$j \in nat$$, $$\forall k\in j + 1.\ q(k) \in R$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = q(0) + (\sum \{\langle k,q(k + 1)\rangle .\ k\in j\})$$, $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j)$$
lemma (in ring0) Ring_ZF_2_L2:

assumes $$a\in R$$, $$b\in R$$, $$c\in R$$, $$d\in R$$

shows $$a - (b + 1 )\cdot c = (a - d - c) + (d - b\cdot c)$$, $$a + b + (c + d) = a + b + c + d$$, $$a + b + (c + d) = a + (b + c) + d$$
lemma (in ring3) sum_ring_distrib:

assumes $$n\in nat$$ and $$\forall k\in n.\ p(k) \in R$$, $$\forall k\in n.\ q(k) \in R$$

shows $$(\sum \{\langle k,p(k) + q(k)\rangle .\ k\in n\}) = (\sum \{\langle k,p(k)\rangle .\ k\in n\}) + (\sum \{\langle k,q(k)\rangle .\ k\in n\})$$
lemma (in ring3) bt_rec_identity:

assumes $$M \text{ is commutative on } R$$, $$j\in nat$$, $$k\in j$$, $$x\in R$$, $$y\in R$$

shows $$\text{BT}(j,k + 1,x,y)\cdot x + \text{BT}(j,k,x,y)\cdot y = \text{BT}(j + 1,k + 1,x,y)$$
lemma (in ring3) rng_seq_sum_pull_one_elem:

assumes $$j \in nat$$, $$\forall k\in j + 1.\ q(k) \in R$$

shows $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = q(0) + (\sum \{\langle k,q(k + 1)\rangle .\ k\in j\})$$, $$(\sum \{\langle k,q(k)\rangle .\ k\in j + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in j\}) + q(j)$$
lemma (in ring3) bt_at_zero2:

assumes $$n\in nat$$, $$x\in R$$

shows $$\text{BT}(n,0,x,y)\cdot x = \text{BT}(n + 1,0,x,y)$$
lemma (in ring3) bt_at_right1:

assumes $$n\in nat$$, $$y\in R$$

shows $$\text{BT}(n,n,x,y)\cdot y = \text{BT}(n + 1,n + 1,x,y)$$