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 \( \prod s \equiv \text{Fold}(M,1 ,s) \)
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.
sublocale ring0 < add_monoid: monoid1
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. (For some reason the sublocale below is not seen by Isabelle when we try to use it).
sublocale ring3 < mul_monoid: monoid1
using ringAssum unfolding IsAring_def, IsAgroup_def, monoid1_def, monoid0_def
The assumptions of the monoid1 context hold in the ring0 context
lemma (in ring0) monoid0_valid_in_ring0:
shows \( monoid1(R,A) \) 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 monoid0_valid_in_ring0, nat_mult_zero, nat_mult_zeroNatural 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, monoid0_valid_in_ring0, nat_mult_type, nat_mult_typeThe 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.
lemma (in ring3) nat_mult_pow_add_one:
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, monoid0_valid_in_ring0, nat_mult_add_one, nat_mult_add_oneAssociativity 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
qed
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 )
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.
lemma (in ring3) nat_add_mult_distrib:
assumes \( n\in nat \), \( m\in nat \), \( x\in R \)
shows \( (n + m)\cdot x = n\cdot x + m\cdot x \) using assms, monoid0_valid_in_ring0, nat_mult_addAssociativity 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_assocWhen 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), monoid0_valid_in_ring0, sum_in_monoThe 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), monoid0_valid_in_ring0, sum_in_monoCombining 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 monoid0_valid_in_ring0, 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, monoid0_valid_in_ring0, seq_sum_pull_one_elemDistributive 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 monoid0_valid_in_ring0, 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
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 )
{
}
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 monoid0_valid_in_ring0, 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 monoid0_valid_in_ring0, 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 monoid0_valid_in_ring0, 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
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 monoid0_valid_in_ring0, sum_empty, Ring_ZF_1_L6(2)
moreover
qed
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
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 )
{
}
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 monoid0_valid_in_ring0, 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 monoid0_valid_in_ring0, 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 monoid0_valid_in_ring0, 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
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), monoid0_valid_in_ring0, sum_comm_distribTo 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_defThe 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), monoid0_valid_in_ring0, nat_mult_one, Ring_ZF_1_L2(2), Ring_ZF_1_L3(5) unfolding BT_defThe 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), monoid0_valid_in_ring0, 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), monoid0_valid_in_ring0, 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
qed
have \( \text{BT}(j,k + 1,x,y)\cdot x = {{j}\choose {k + 1}}\cdot p \)proof
ultimately have \( L = {{j}\choose {k + 1}}\cdot p + {{j}\choose {k}}\cdot p \)
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
qed
from assms(2,3) have \( x^{j - (k + 1) + 1} = x^{j - k} \) using nat_subtr_simpl0
ultimately show \( thesis \) unfolding BT_def
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
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
qed
have \( (x + y)^{0} = \sum \{\langle k, \text{BT}(0,k,x,y)\rangle .\ k\in 0 + 1\} \)proof
moreover 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), monoid0_valid_in_ring0, seq_sum_singleton
then show \( thesis \) using mult_pow_zero(2)
qed
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
ultimately have \( (x + y)^{n} = \sum \{\langle k, \text{BT}(n,k,x,y)\rangle .\ k\in n + 1\} \) by (rule ind_on_nat1 )
{
}
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
also from assms(3), \( j + 1 \in nat \), I have \( s_0\cdot x = s_1 \) by (rule fin_sum_distrib )
moreover
qed
from assms(4), \( j + 1 \in nat \), I have \( s_0\cdot y = s_2 \) by (rule fin_sum_distrib )
ultimately show \( thesis \)
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
also 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
qed
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 \)
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), monoid0_valid_in_ring0, 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
also from \( j\in nat \), IV, V have \( s_3 + s_4 = s_5 \) using sum_ring_distrib
thus \( thesis \)
qed
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
also 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
have \( s_7 + \text{BT}(j,j,x,y)\cdot y = s_8 \)proof
finally have \( (x + y)^{j + 1} = s_8 \)
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
thus \( thesis \)
qed
then show \( thesis \) unfolding BT_def
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 ring0) monoid0_valid_in_ring0: shows \( monoid1(R,A) \)
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 \) lemma (in monoid1) nat_mult_add_one:
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 \) lemma (in ring3) nat_mult_pow_add_one:
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) \) lemma (in monoid1) nat_mult_add:
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 \) lemma mem_add_one_subset:
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} \) lemma (in ring3) nat_mult_pow_add_one:
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 \) lemma (in ring3) nat_add_mult_distrib:
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) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8