Theory Ring_Binomial_ZF

(* 
This file is a part of IsarMathLib - 
a library of formalized mathematics for Isabelle/Isar.
Copyright (C) 2023  Slawomir Kolodynski
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 
  additive operation. ›

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) = 𝟭"
  using add_monoid.nat_mult_zero mul_monoid.nat_mult_zero by simp_all

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"
  using assms add_monoid.nat_mult_type mul_monoid.nat_mult_type 
  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"
  using assms add_monoid.nat_mult_add_one mul_monoid.nat_mult_add_one 
  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)"
    using nat_mult_pow_add_one(1) mult_pow_type ring_oper_distr(2) Ring_ZF_1_L4(3)
      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"
  using assms add_monoid.nat_mult_add by simp

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" 
    using add_monoid.sum_in_mono by simp
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)"
  using assms add_monoid.seq_sum_pull_one_elem by simp_all

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}"
    using add_monoid.sum_empty Ring_ZF_1_L6(1) by simp_all
  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"
        using mem_add_one_subset by blast
      ultimately have     
        "(∑{⟨k,q(k)⟩. k∈j #+ 1}) =  (∑{⟨k,q(k)⟩. k∈j}) \<ra> q(j)"
        using add_monoid.seq_sum_pull_one_elem(2) by simp
      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" 
        using add_monoid.sum_in_mono by simp_all
      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"
        using add_monoid.seq_sum_pull_one_elem(2) by simp
      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}"
    using add_monoid.sum_empty Ring_ZF_1_L6(2) by simp_all
  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"
        using mem_add_one_subset by blast
      ultimately have     
        "(∑{⟨k,q(k)⟩. k∈j #+ 1}) =  (∑{⟨k,q(k)⟩. k∈j}) \<ra> q(j)"
        using add_monoid.seq_sum_pull_one_elem(2) by simp
      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" 
        using add_monoid.sum_in_mono by simp_all
       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)"
        using add_monoid.seq_sum_pull_one_elem(2) by simp
      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) = 𝟭"
  using binom_zero_zero mult_pow_zero(2) add_monoid.nat_mult_one 
        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
    mult_pow_type(2) add_monoid.nat_mult_one Ring_ZF_1_L3(5) 
    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)
    add_monoid.nat_mult_one Ring_ZF_1_L2(2) mult_pow_type(2) Ring_ZF_1_L3(6)
  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) 
      nat_mult_assoc1 Ring_ZF_1_L11(2) nat_mult_pow_add_one(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))"
      using nat_mult_assoc1 Ring_ZF_2_L4(2) nat_mult_pow_add_one(2)
      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}) = 𝟭"
      using bt_at_zero Ring_ZF_1_L2(2) add_monoid.seq_sum_singleton
      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"
          using Ring_ZF_1_L4(1) mult_pow_type nat_mult_pow_add_one(2) 
            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"
        using bt_type Ring_ZF_1_L4(3) add_monoid.sum_in_mono Ring_ZF_2_L2(3)
        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