Theory Ring_Binomial_ZF

(*
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.
This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the
following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR AS IS'' AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

section ‹Binomial theorem›

theory Ring_Binomial_ZF imports Monoid_ZF_1 Ring_ZF

begin

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

subsection‹Sums of multiplicities of powers of ring elements and binomial theorem›

text‹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. ›

text‹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 +
fixes listsum ("∑ _" 70)
defines listsum_def [simp]: "∑s ≡ Fold(A,𝟬,s)"

fixes listprod ("∏ _" 70)
defines listprod_def [simp]: "∏s ≡ Fold(M,𝟭,s)"

fixes nat_mult (infix "\<nm>" 95)
defines nat_mult_def [simp]: "n\<nm>x ≡ ∑{⟨k,x⟩. k∈n}"

fixes pow
defines pow_def [simp]: "pow(n,x) ≡ ∏{⟨k,x⟩. k∈n}"

text‹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

sublocale ring3 < add_monoid: monoid1 R A ringa ringzero listsum nat_mult
using ringAssum
unfolding IsAring_def IsAgroup_def monoid1_def monoid0_def
by auto

text‹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 R M ringm ringone listprod pow
using ringAssum
unfolding IsAring_def IsAgroup_def monoid1_def monoid0_def
by auto

text‹$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\<nm>x = 𝟬" and "pow(0,x) = 𝟭"

text‹Natural multiple and power of a ring element is a ring element.›

lemma (in ring3) mult_pow_type: assumes "n∈nat" "x∈R"
shows "n\<nm>x ∈ R" and "pow(n,x) ∈ R"
by simp_all

text‹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.›

lemma (in ring3) nat_mult_pow_add_one: assumes  "n∈nat" "x∈R"
shows "(n #+ 1)\<nm>x = (n\<nm>x) \<ra> x" and "pow(n #+ 1,x) = pow(n,x)⋅x"
by simp_all

text‹Associativity for the multiplication by natural number and the ring multiplication:›

lemma (in ring3) nat_mult_assoc: assumes "n∈nat" "x∈R" "y∈R"
shows "n\<nm>x⋅y = n\<nm>(x⋅y)"
proof -
from assms(1,3) have "n∈nat" and "0\<nm>x⋅y = 0\<nm>(x⋅y)"
using mult_pow_zero(1) Ring_ZF_1_L6 by simp_all
moreover from assms(2,3) have "∀k∈nat.
k\<nm>x⋅y = k\<nm>(x⋅y) ⟶ (k #+ 1)\<nm>x⋅y = (k #+ 1)\<nm>(x⋅y)"
by simp
ultimately show ?thesis by (rule ind_on_nat1)
qed

text‹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∈nat" "m∈nat" "x∈R"
shows "(n #+ m)\<nm>x = n\<nm>x \<ra> m\<nm>x"

text‹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∈nat" "x∈R" "y∈R" "z∈R"
shows "n\<nm>x⋅y⋅z = n\<nm>(x⋅y⋅z)"
using assms Ring_ZF_1_L4(3) nat_mult_assoc by simp

text‹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∈nat" "x∈R" and "∀k∈n. q(k) ∈ R"
shows "∀k∈n. q(k)⋅x ∈ R" and "(∑{⟨k,q(k)⋅x⟩. k∈n}) ∈ R"
using assms Ring_ZF_1_L4(3) add_monoid.sum_in_mono by simp_all

text‹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∈nat" "∀k∈n. q(k) ∈ R" "∀k∈n. p(k) ∈ R"
shows "∀k∈n. q(k)\<ra>p(k) ∈ R" and "(∑{⟨k,q(k)\<ra>p(k)⟩. k∈n}) ∈ R"
using assms Ring_ZF_1_L4(1) add_monoid.sum_in_mono by simp_all

text‹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∈nat" "x∈R"  "y∈R" "∀k∈n. q(k) ∈ R" "∀k∈n. p(k) ∈ R"
shows "∀k∈n. q(k)⋅x\<ra>p(k)⋅y ∈ R" and
"(∑{⟨k,q(k)⋅x\<ra>p(k)⋅y⟩. k∈n}) ∈ R"
proof -
from assms have "∀k∈n. q(k)⋅x ∈ R" and "∀k∈n. p(k)⋅y ∈ R"
using mult_elem_ring_type(1) by simp_all
with assms(1) show "∀k∈n. q(k)⋅x\<ra>p(k)⋅y ∈ R"
using sum_expr_ring_type(1) by simp
with assms(1) show "(∑{⟨k,q(k)⋅x\<ra>p(k)⋅y⟩. k∈n}) ∈ R"
qed

text‹A ‹ring3› version of ‹seq_sum_pull_one_elem› from ‹Monoid_ZF_1›: ›

lemma (in ring3) rng_seq_sum_pull_one_elem:
assumes "j ∈ nat" "∀k∈j #+ 1. q(k) ∈ R"
shows
"(∑{⟨k,q(k)⟩. k∈j #+ 1}) = q(0)\<ra>(∑{⟨k,q(k #+ 1)⟩. k∈j})"
"(∑{⟨k,q(k)⟩. k∈j #+ 1}) = (∑{⟨k,q(k)⟩. k∈j})\<ra> q(j)"

text‹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∈R"  "n∈nat" "∀k∈n. q(k) ∈ R"
shows
"(∑{⟨k,q(k)⟩. k∈n})⋅x = ∑{⟨k,q(k)⋅x⟩. k∈n}"
"x⋅(∑{⟨k,q(k)⟩. k∈n}) = ∑{⟨k,x⋅q(k)⟩. k∈n}"
proof -
from assms(1,2) have "n∈nat" and
"(∑{⟨k,q(k)⟩. k∈0})⋅x = ∑{⟨k,q(k)⋅x⟩. k∈0}"
moreover have
"∀j∈n. (∑{⟨k,q(k)⟩. k∈j})⋅x = (∑{⟨k,q(k)⋅x⟩. k∈j})
⟶ (∑{⟨k,q(k)⟩. k∈j #+ 1})⋅x = ∑{⟨k,q(k)⋅x⟩. k∈j #+ 1}"
proof -
{ fix j assume "j∈n" and
I: "(∑{⟨k,q(k)⟩. k∈j})⋅x = (∑{⟨k,q(k)⋅x⟩. k∈j})"
from assms(2) ‹j∈n› have "j∈nat" using elem_nat_is_nat(2)
by simp
moreover from assms(2,3) ‹j∈n› have II: "∀k∈j #+ 1. q(k) ∈ R"
ultimately have
"(∑{⟨k,q(k)⟩. k∈j #+ 1}) =  (∑{⟨k,q(k)⟩. k∈j}) \<ra> q(j)"
hence
"(∑{⟨k,q(k)⟩. k∈j #+ 1})⋅x = ((∑{⟨k,q(k)⟩. k∈j}) \<ra> q(j))⋅x"
by simp
moreover from assms(1) ‹j∈nat› II have
"(∑{⟨k,q(k)⟩. k∈j}) ∈ R" "q(j) ∈ R" and "x∈R"
ultimately have
"(∑{⟨k,q(k)⟩. k∈j #+ 1})⋅x = (∑{⟨k,q(k)⟩. k∈j})⋅x \<ra> q(j)⋅x"
using ring_oper_distr(2) by simp
with I have
"(∑{⟨k,q(k)⟩. k∈j #+ 1})⋅x = (∑{⟨k,q(k)⋅x⟩. k∈j})  \<ra> q(j)⋅x"
by simp
moreover
from assms(1) II have "∀k∈j #+ 1. q(k)⋅x ∈ R"
using Ring_ZF_1_L4(3) by simp
with ‹j∈nat› have
"(∑{⟨k,q(k)⋅x⟩. k∈j #+ 1}) = (∑{⟨k,q(k)⋅x⟩. k∈j}) \<ra> q(j)⋅x"
ultimately have
"(∑{⟨k,q(k)⟩. k∈j #+ 1})⋅x = (∑{⟨k,q(k)⋅x⟩. k∈j #+ 1})"
by simp
} thus ?thesis by simp
qed
ultimately show "(∑{⟨k,q(k)⟩. k∈n})⋅x = ∑{⟨k,q(k)⋅x⟩. k∈n}"
by (rule fin_nat_ind1)
from assms(1,2) have "n∈nat" and
"x⋅(∑{⟨k,q(k)⟩. k∈0}) = ∑{⟨k,x⋅q(k)⟩. k∈0}"
moreover have
"∀j∈n. x⋅(∑{⟨k,q(k)⟩. k∈j}) = (∑{⟨k,x⋅q(k)⟩. k∈j})
⟶ x⋅(∑{⟨k,q(k)⟩. k∈j #+ 1}) = ∑{⟨k,x⋅q(k)⟩. k∈j #+ 1}"
proof -
{ fix j assume "j∈n" and
I: "x⋅(∑{⟨k,q(k)⟩. k∈j}) = (∑{⟨k,x⋅q(k)⟩. k∈j})"
from assms(2) ‹j∈n› have "j∈nat" using elem_nat_is_nat(2)
by simp
moreover from assms(2,3) ‹j∈n› have II: "∀k∈j #+ 1. q(k) ∈ R"
ultimately have
"(∑{⟨k,q(k)⟩. k∈j #+ 1}) =  (∑{⟨k,q(k)⟩. k∈j}) \<ra> q(j)"
hence
"x⋅(∑{⟨k,q(k)⟩. k∈j #+ 1}) = x⋅((∑{⟨k,q(k)⟩. k∈j}) \<ra> q(j))"
by simp
moreover from assms(1) ‹j∈nat› II have
"(∑{⟨k,q(k)⟩. k∈j}) ∈ R" "q(j) ∈ R" and "x∈R"
ultimately have
"x⋅(∑{⟨k,q(k)⟩. k∈j #+ 1}) = x⋅(∑{⟨k,q(k)⟩. k∈j}) \<ra> x⋅q(j)"
using ring_oper_distr(1) by simp
with I have
"x⋅(∑{⟨k,q(k)⟩. k∈j #+ 1}) =  (∑{⟨k,x⋅q(k)⟩. k∈j})  \<ra> x⋅q(j)"
by simp
moreover
from assms(1) II have "∀k∈j #+ 1. x⋅q(k) ∈ R"
using Ring_ZF_1_L4(3) by simp
with ‹j∈nat› have
"(∑{⟨k,x⋅q(k)⟩. k∈j #+ 1}) = (∑{⟨k,x⋅q(k)⟩. k∈j}) \<ra> x⋅q(j)"
ultimately have
"x⋅(∑{⟨k,q(k)⟩. k∈j #+ 1}) = (∑{⟨k,x⋅q(k)⟩. k∈j #+ 1})"
by simp
} thus ?thesis by simp
qed
ultimately show  "x⋅(∑{⟨k,q(k)⟩. k∈n}) = ∑{⟨k,x⋅q(k)⟩. k∈n}"
by (rule fin_nat_ind1)
qed

text‹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∈nat" and  "∀k∈n. p(k) ∈ R" "∀k∈n. q(k) ∈ R"
shows
"(∑{⟨k,p(k)\<ra>q(k)⟩. k∈n}) = (∑{⟨k,p(k)⟩. k∈n}) \<ra> (∑{⟨k,q(k)⟩. k∈n})"
using assms Ring_ZF_1_L1(3) add_monoid.sum_comm_distrib by simp

text‹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) BT where
"BT(n,k,x,y) ≡ Binom(n,k)\<nm>pow(n #- k,x)⋅pow(k,y)"

text‹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∈nat" "k∈nat" "x∈R" "y∈R"
shows "BT(n,k,x,y) ∈ R"
using assms mult_pow_type binom_in_nat Ring_ZF_1_L4(3)
unfolding BT_def by simp

text‹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 "BT(0,0,x,y) = 𝟭"
Ring_ZF_1_L2(2) Ring_ZF_1_L3(5)
unfolding BT_def by simp

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

lemma (in ring3) bt_at_zero1: assumes "n∈nat" "x∈R"
shows "BT(n,0,x,y) = pow(n,x)"
unfolding BT_def using assms mult_pow_zero(2) binom_left_boundary
by simp

text‹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∈nat" "x∈R"
shows "BT(n,0,x,y)⋅x = BT(n #+ 1,0,x,y)"
using assms bt_at_zero1 nat_mult_pow_add_one(2) by simp

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

lemma (in ring3) bt_at_right: assumes "n∈nat" "y∈R"
shows "BT(n,n,x,y) = pow(n,y)"
unfolding BT_def using assms binom_right_boundary mult_pow_zero(2)
by simp

text‹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∈nat" "y∈R"
shows "BT(n,n,x,y)⋅y = BT(n #+ 1,n #+ 1,x,y)"
using assms bt_at_right nat_mult_pow_add_one(2) by simp

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

lemma (in ring3) bt_rec_identity:
assumes "M {is commutative on} R" "j∈nat" "k∈j" "x∈R" "y∈R"
shows
"BT(j,k #+ 1,x,y)⋅x \<ra> BT(j,k,x,y)⋅y = BT(j #+ 1,k #+ 1,x,y)"
proof -
from assms(2,3,4) have "k∈nat" "Binom(j,k #+ 1) ∈ nat"
and "Binom(j,k) ∈ nat" "Binom(j #+ 1,k #+ 1) ∈ nat"
and I: "pow(j #- (k #+ 1),x) ∈ R" and II: "pow(j #- k,x) ∈ R"
using elem_nat_is_nat(2) binom_in_nat mult_pow_type(2)
by simp_all
with assms(5) have III: "pow(k #+ 1,y) ∈ R"
using mult_pow_type(2) by blast
let ?L = "BT(j,k #+ 1,x,y)⋅x \<ra> BT(j,k,x,y)⋅y"
let ?p = "pow(j #- k,x)⋅pow(k #+ 1,y)"
from assms(2,4) ‹k∈nat› II III have "?p ∈ R"
using mult_pow_type(2) Ring_ZF_1_L4(3) by simp
from assms(2,3,4,5) have "BT(j,k,x,y)⋅y = Binom(j,k)\<nm>?p"
using elem_nat_is_nat(2) binom_in_nat mult_pow_type(2)
unfolding BT_def by simp
moreover have "BT(j,k #+ 1,x,y)⋅x = Binom(j,k #+ 1)\<nm>?p"
proof -
from assms(1,4) ‹Binom(j,k #+ 1) ∈ nat› I III have
"Binom(j,k #+ 1)\<nm>pow(j #- (k #+ 1),x)⋅pow(k #+ 1,y)⋅x =
Binom(j,k #+ 1)\<nm>(pow(j #- (k #+ 1) #+ 1,x)⋅pow(k #+ 1,y))"
by simp
with assms(2,3) have
"Binom(j,k #+ 1)\<nm>pow(j #- (k #+ 1),x)⋅pow(k #+ 1,y)⋅x =
Binom(j,k #+ 1)\<nm>(pow(j #- (k #+ 1) #+ 1,x)⋅pow(k #+ 1,y))"
using nat_subtr_simpl0 by blast
moreover from assms(2,3) have
"pow(j #- (k #+ 1) #+ 1,x) = pow(j #- k,x)"
using nat_subtr_simpl0 by simp
ultimately show ?thesis unfolding BT_def by simp
qed
ultimately have "?L = Binom(j,k #+ 1)\<nm>?p \<ra> Binom(j,k)\<nm>?p"
by simp
with assms(2,3) ‹Binom(j,k #+ 1) ∈ nat› ‹Binom(j,k) ∈ nat› ‹?p ∈ R›
have "?L = Binom(j #+ 1,k #+ 1)\<nm>?p"
using nat_add_mult_distrib binom_prop2 succ_ineq1(3) by simp
with assms(2,3) ‹Binom(j #+ 1,k #+ 1) ∈ nat› II III
show ?thesis using nat_mult_assoc nat_subtr_simpl0
unfolding BT_def by simp
qed

text‹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 {is commutative on} R" "n∈nat" "x∈R" "y∈R"
shows
"pow(n,x\<ra>y) = ∑{⟨k,Binom(n,k)\<nm>pow(n #- k,x) ⋅ pow(k,y)⟩. k∈n #+ 1}"
proof -
from assms(2) have "n∈nat" by simp
moreover have "pow(0,x\<ra>y) = ∑{⟨k,BT(0,k,x,y)⟩. k∈0 #+ 1}"
proof -
from assms(3,4) have "(∑{⟨k,BT(0,k,x,y)⟩. k∈0 #+ 1}) = 𝟭"
by simp
then show ?thesis using mult_pow_zero(2) by simp
qed
moreover have "∀j∈nat.
pow(j,x\<ra>y) = (∑{⟨k,BT(j,k,x,y)⟩. k∈j #+ 1})  ⟶
pow(j #+ 1,x\<ra>y) = (∑{⟨k,BT(j #+ 1,k,x,y)⟩. k∈j #+ 1 #+ 1})"
proof -
{ fix j
let ?s⇩0 = "∑{⟨k,BT(j,k,x,y)⟩. k∈j #+ 1}"
let ?s⇩1 = "∑{⟨k,BT(j,k,x,y)⋅x⟩. k∈j #+ 1}"
let ?s⇩2 = "∑{⟨k,BT(j,k,x,y)⋅y⟩. k∈j #+ 1}"
let ?s⇩3 = "∑{⟨k,BT(j,k #+ 1,x,y)⋅x⟩. k∈j}"
let ?s⇩4 = "∑{⟨k,BT(j,k,x,y)⋅y⟩. k∈j}"
let ?s⇩5 = "∑{⟨k,BT(j,k #+ 1,x,y)⋅x \<ra> BT(j,k,x,y)⋅y⟩. k∈j}"
let ?s⇩6 = "∑{⟨k,BT(j #+ 1,k #+ 1,x,y)⟩. k∈j}"
let ?s⇩7 = "∑{⟨k,BT(j #+ 1,k,x,y)⟩. k∈j #+ 1}"
let ?s⇩8 = "∑{⟨k,BT(j #+ 1,k,x,y)⟩. k∈j #+ 1 #+ 1}"
assume "j∈nat" and "pow(j,x\<ra>y) = ?s⇩0"
then have "j #+ 1 ∈ nat" and "j #+ 1 #+ 1 ∈ nat" by simp_all
have
I:  "∀k∈j #+ 1. BT(j,k,x,y) ∈ R" and
II: "∀k∈j #+ 1. BT(j,k,x,y)⋅x ∈ R" and
III: "∀k∈j #+ 1. BT(j,k,x,y)⋅y ∈ R" and
IV:  "∀k∈j. BT(j,k #+ 1,x,y)⋅x ∈ R" and
V:   "∀k∈j. BT(j,k,x,y)⋅y ∈ R" and
VI:  "∀k∈j #+ 1. BT(j #+ 1,k,x,y) ∈ R" and
VII: "∀k∈j #+ 1 #+ 1. BT(j #+ 1,k,x,y) ∈ R"
proof -
from assms(3,4) ‹j∈nat› show "∀k∈j #+ 1. BT(j,k,x,y) ∈ R"
using elem_nat_is_nat(2) bt_type by blast
with assms(3,4) ‹j∈nat› show
"∀k∈j #+ 1. BT(j,k,x,y)⋅x ∈ R" and
"∀k∈j #+ 1. BT(j,k,x,y)⋅y ∈ R" and
"∀k∈j. BT(j,k,x,y)⋅y ∈ R"
using Ring_ZF_1_L4(3) by simp_all
from assms(3,4) ‹j∈nat› have "∀k∈j. BT(j,k #+ 1,x,y) ∈ R"
using elem_nat_is_nat(2) bt_type by simp
with ‹j∈nat› assms(3) show "∀k∈j. BT(j,k #+ 1,x,y)⋅x ∈ R"
using mult_elem_ring_type(1) by simp
from assms(3,4) ‹j #+ 1 ∈ nat› show
"∀k∈j #+ 1. BT(j #+ 1,k,x,y) ∈ R"
using elem_nat_is_nat(2) bt_type by blast
from assms(3,4) ‹j #+ 1 #+ 1 ∈ nat› show
"∀k∈j #+ 1 #+ 1. BT(j #+ 1,k,x,y) ∈ R"
using elem_nat_is_nat(2) bt_type by blast
qed
have "pow(j #+ 1,x\<ra>y) = ?s⇩0⋅x \<ra> ?s⇩0⋅y"
proof -
from assms(3,4) ‹j∈nat› have
"pow(j #+ 1,x\<ra>y) = pow(j,x\<ra>y)⋅x \<ra> pow(j,x\<ra>y)⋅y"
ring_oper_distr(1) by simp
with ‹pow(j,x\<ra>y) = ?s⇩0› show  ?thesis by simp
qed
also have "?s⇩0⋅x \<ra> ?s⇩0⋅y = ?s⇩1 \<ra> ?s⇩2"
proof -
from assms(3) ‹j #+ 1 ∈ nat› I have "?s⇩0⋅x = ?s⇩1"
by (rule fin_sum_distrib)
moreover from assms(4) ‹j #+ 1 ∈ nat› I
have "?s⇩0⋅y = ?s⇩2" by (rule fin_sum_distrib)
ultimately show ?thesis by simp
qed
also have "?s⇩1 \<ra> ?s⇩2 =
(BT(j,0,x,y)⋅x \<ra> ?s⇩3) \<ra> (?s⇩4 \<ra> BT(j,j,x,y)⋅y)"
proof -
from ‹j∈nat› II have "?s⇩1 = BT(j,0,x,y)⋅x \<ra> ?s⇩3"
using rng_seq_sum_pull_one_elem(1) by simp
moreover from ‹j∈nat› III have "?s⇩2 = ?s⇩4 \<ra> BT(j,j,x,y)⋅y"
using rng_seq_sum_pull_one_elem(2) by simp
ultimately show ?thesis by simp
qed
also from assms(3,4) IV V ‹j∈nat› have
"(BT(j,0,x,y)⋅x \<ra> ?s⇩3) \<ra> (?s⇩4 \<ra> BT(j,j,x,y)⋅y) =
BT(j,0,x,y)⋅x \<ra> (?s⇩3 \<ra> ?s⇩4) \<ra> BT(j,j,x,y)⋅y"
by simp
also have "BT(j,0,x,y)⋅x \<ra> (?s⇩3 \<ra> ?s⇩4) \<ra> BT(j,j,x,y)⋅y =
BT(j,0,x,y)⋅x \<ra> ?s⇩5 \<ra> BT(j,j,x,y)⋅y"
proof -
from ‹j∈nat› IV V have "?s⇩3 \<ra> ?s⇩4 = ?s⇩5"
using sum_ring_distrib by simp
thus ?thesis by simp
qed
also from assms(1,3,4) ‹j∈nat› have
"BT(j,0,x,y)⋅x \<ra> ?s⇩5 \<ra> BT(j,j,x,y)⋅y =
BT(j,0,x,y)⋅x \<ra> ?s⇩6 \<ra> BT(j,j,x,y)⋅y"
using bt_rec_identity by simp
also have "BT(j,0,x,y)⋅x \<ra> ?s⇩6 \<ra> BT(j,j,x,y)⋅y =
?s⇩7 \<ra> BT(j,j,x,y)⋅y"
proof -
from ‹j∈nat› VI have "?s⇩7 = BT(j #+ 1,0,x,y) \<ra> ?s⇩6"
by (rule rng_seq_sum_pull_one_elem)
with assms(3) ‹j∈nat› show ?thesis
using bt_at_zero2 by simp
qed
also have "?s⇩7 \<ra> BT(j,j,x,y)⋅y = ?s⇩8"
proof -
from ‹j #+ 1 ∈ nat› VII have
"?s⇩8 = ?s⇩7 \<ra> BT(j #+ 1,j #+ 1,x,y)"
by (rule rng_seq_sum_pull_one_elem)
with assms(4) ‹j∈nat› show ?thesis
using bt_at_right1 by simp
qed
finally have "pow(j #+ 1,x\<ra>y) =  ?s⇩8" by simp
} thus ?thesis by simp
qed
ultimately have "pow(n,x\<ra>y) = ∑{⟨k,BT(n,k,x,y)⟩. k∈n #+ 1}"
by (rule ind_on_nat1)
then show ?thesis unfolding BT_def by simp
qed

end