:: Factorial and Newton coefficients
::  by Rafa{\l} Kwiatek
::
:: Received July 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XREAL_0, ORDINAL1, FINSEQ_1, RELAT_1, FUNCT_1,
      XXREAL_0, XBOOLE_0, SUBSET_1, ARYTM_3, TARSKI, FINSEQ_2, XCMPLX_0,
      RVSUM_1, CARD_3, REAL_1, CARD_1, ORDINAL4, REALSET1, ARYTM_1, PARTFUN1,
      INT_2, INT_1, FINSET_1, SQUARE_1, FUNCOP_1, NEWTON, VALUED_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
      XREAL_0, REAL_1, FUNCT_1, PARTFUN1, FUNCT_2,
      VALUED_0, FINSET_1, FINSEQ_1,
      FINSEQ_2, FUNCOP_1, INT_1, INT_2, NAT_1, NAT_D, RVSUM_1, SQUARE_1,
      XXREAL_0;
 constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2,
      FINSOP_1, SEQ_1, RVSUM_1, FUNCOP_1, RELSET_1, FINSEQOP;
 registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, RVSUM_1, VALUED_0,
      CARD_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, FINSEQ_1, SQUARE_1, FINSEQ_2, RVSUM_1;
 theorems TARSKI, NAT_1, RVSUM_1, FINSEQ_1, FINSEQ_2, FUNCT_1, INT_1, XREAL_0,
      XBOOLE_0, XCMPLX_1, INT_2, CARD_2, CARD_1, XBOOLE_1, XREAL_1, XCMPLX_0,
      XXREAL_0, FINSOP_1, ORDINAL1, NAT_D, PARTFUN1, VALUED_1,
      FUNCOP_1, ZFMISC_1;
 schemes NAT_1, FINSEQ_1, SUBSET_1, NAT_D;

begin

reserve i,j,k,n,m,l,s,t,r for Nat;
reserve a,b for real number;
reserve F,G,H for FinSequence of REAL;

theorem Th1:
  n>=1 implies Seg n = {1} \/ {k where k is Element of NAT: 1<k & k <n} \/ {n}
proof
  assume
A1: n>=1;
A2: {1} \/ {k where k is Element of NAT: 1<k & k<n} \/ {n} c= Seg n
  proof
    let d be set;
A3: {k where k is Element of NAT: 1<k & k<n} c= Seg n
    proof
      let d be set;
      assume d in {k where k is Element of NAT: 1<k & k<n};
      then ex k being Element of NAT st d = k & 1<k & k<n;
      hence thesis;
    end;
    1 in Seg n by A1; then
    {1} c= Seg n by ZFMISC_1:31; then
A4: {1} \/ {k where k is Element of NAT: 1<k & k<n} c= Seg n by A3,XBOOLE_1:8;
    n in Seg n by A1,FINSEQ_1:3; then
    {n} c= Seg n by ZFMISC_1:31; then
    {1} \/ {k where k is Element of NAT: 1<k & k<n} \/ {n} c= Seg n
      by A4,XBOOLE_1:8;
    hence thesis;
  end;
  Seg n c= {1} \/ {k where k is Element of NAT: 1<k & k<n} \/ {n}
  proof
    let d be set;
    assume
A5: d in Seg n;
    per cases by A1,XXREAL_0:1;
    suppose
A6:   n>1;
      reconsider l = d as Element of NAT by A5;
A7:   l <= n by A5,FINSEQ_1:1;
      1 <= l by A5,FINSEQ_1:1;
      then 1 = l or 1<l & l<n or l = n or 1 = n by A7,XXREAL_0:1;
      then
      d in {1} or d in {k where k is Element of NAT: 1<k & k<n} or d in {n
      } by A6,TARSKI:def 1;
      then
      d in {1} \/ {k where k is Element of NAT: 1<k & k<n} or d in {n} by
XBOOLE_0:def 3;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
      n = 1;
      hence thesis by A5,FINSEQ_1:2,XBOOLE_0:def 3;
    end;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th2:
  len (a*F) = len F
proof
  reconsider G = F as Element of (len F)-tuples_on REAL by FINSEQ_2:92;
  len (a*G) = len G by CARD_1:def 7;
  hence thesis;
end;

theorem
  dom G = dom (a*G) by VALUED_1:def 5;

:: x |^ n Function

registration
  let x be complex number, n be Nat;
  cluster n |-> x -> complex-yielding;
  coherence;
end;

definition
  let x be complex number, n be Nat;
  func x |^ n equals
  Product (n |-> x);
  coherence;
end;

registration
  let x be real number, n be Nat;
  cluster x |^ n -> real;
  coherence;
end;

definition
  let x be Real, n be Nat;
  redefine func x |^ n -> Real;
  coherence by XREAL_0:def 1;
end;

reserve z for complex number;

registration
  let z be complex number, n be Nat;
  cluster z|^n -> complex;
  coherence;
end;

theorem
  z|^0 = 1 by RVSUM_1:94;

theorem Th5:
  z|^1 = z
proof
  thus z|^1 = Product(<*z*>) by FINSEQ_2:59
    .= z by RVSUM_1:95;
end;

theorem Th6:
  z|^(s+1) = z|^s * z
proof
  thus z|^(s+1) = Product((s |-> z) ^ <*z*>) by FINSEQ_2:60
    .= z|^s*z by RVSUM_1:96;
end;

registration
  let x, n be Nat;
  cluster x|^n -> natural;
  coherence
  proof
    defpred P[Nat] means x|^$1 is natural;
A1: for a being Nat st P[a] holds P[a+1]
    proof
      let a be Nat;
      assume P[a];
      then reconsider b = x|^a as Nat;
      x|^(a+1) = b*x by Th6;
      hence thesis;
    end;
A2: P[0] by RVSUM_1:94;
    for a being Nat holds P[a] from NAT_1:sch 2(A2,A1);
    hence thesis;
  end;
end;

reserve x,y for complex number;

theorem
  (x*y) |^ s = x|^s * y|^s
proof
  reconsider x, y as Element of COMPLEX by XCMPLX_0:def 2;
  x|^s*y|^s = Product(s |-> (x*y)) by RVSUM_1:113;
  hence thesis;
end;

theorem Th8:
  x|^(s+t) = x|^s * x|^t
proof
  reconsider x as Element of COMPLEX by XCMPLX_0:def 2;
  x|^s*x|^t = Product((s+t) |-> x) by RVSUM_1:111;
  hence thesis;
end;

theorem
  (x|^s) |^ t = x|^(s*t)
proof
  reconsider x as Element of COMPLEX by XCMPLX_0:def 2;
  x|^(s*t) = Product(t |-> x|^s) by RVSUM_1:112;
  hence thesis;
end;

theorem Th10:
  1|^s = 1
proof
  defpred P[Nat] means 1|^$1 = 1;
A1: now
    let s;
    assume P[s];
    then 1|^(s+1) = 1 * 1 by Th6;
    hence P[s+1];
  end;
A2: P[0] by RVSUM_1:94;
  for s holds P[s] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

theorem Th11:
  s >= 1 implies 0|^s = 0
proof
  defpred P[Nat] means 0|^$1 = 0;
A1: now
    let n be Nat;
    assume n>=1 & P[n];
    0|^(n+1) = 0|^n * 0 by Th6
      .= 0;
    hence P[n+1];
  end;
A2: P[1] by Th5;
  for n be Nat st n >=1 holds P[n] from NAT_1:sch 8(A2,A1);
  hence thesis;
end;

:: n! Function

registration
  let n be Nat;
  cluster idseq n -> natural-valued;
  coherence;
end;

definition
  let n be Nat;
  func n! -> Element of REAL equals
  Product idseq n;
  coherence by XREAL_0:def 1;
end;

registration
  let n be Nat;
  cluster n! -> real;
  coherence;
end;

theorem Th12:
  0! = 1 by RVSUM_1:94;

theorem
  1! = 1 by FINSEQ_2:50,RVSUM_1:95;

theorem
  2! = 2
proof
  thus 2! = 1*2 by FINSEQ_2:52,RVSUM_1:99
  .= 2;
end;

theorem Th15:
  (s+1)! = (s!) * (s+1)
proof
  idseq (s+1) = idseq s ^ <* s+1 *> by FINSEQ_2:51;
  hence thesis by RVSUM_1:96;
end;

theorem Th16:
  s! is Element of NAT
proof
  defpred P[Nat] means $1! is Element of NAT;
A1: now
    let s;
    assume P[s];
    then reconsider k=s! as Element of NAT;
    (s+1)! = (s+1) * k by Th15;
    hence P[s+1];
  end;
A2: P[0] by RVSUM_1:94;
  for s holds P[s] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

registration
  let n;
  cluster n! -> natural;
  coherence by Th16;
end;

theorem Th17:
  s! > 0
proof
  defpred P[Nat] means $1!>0;
A1: now
    let s;
    assume P[s];
    then (s+1) * (s!)>(s+1) * 0;
    hence P[s+1] by Th15;
  end;
A2: P[0] by RVSUM_1:94;
  for s holds P[s] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

registration
  let n;
  cluster n! -> positive;
  coherence by Th17;
end;

theorem
  (s!) * (t!) <> 0;

:: n choose k Function

definition
  let k,n be Nat;
  func n choose k means
  :Def3:
  for l be Nat st l = n-k holds it = (n!)/((k!) * (l!)) if n >= k
  otherwise it = 0;
  consistency;
  existence
  proof
    thus n >= k implies ex r1 be set st for l being Nat st l = n-k holds r1 =
    (n!)/((k!) * (l!))
    proof
      assume n >= k;
      then reconsider m = n-k as Element of NAT by INT_1:5;
      take (n!)/((k!)*(m!));
      thus thesis;
    end;
    thus thesis;
  end;
  uniqueness
  proof
    let r1,r2 be set;
    thus n>=k & (for l being Nat st l = n-k holds r1 = (n!)/((k!) * (l!))) & (
    for l being Nat st l = n-k holds r2 = (n!)/((k!) * (l!))) implies r1 = r2
    proof
      assume n>=k;
      then reconsider m = n-k as Element of NAT by INT_1:5;
      assume that
A1:   for l being Nat st l = n-k holds r1 = (n!)/((k!) * (l!)) and
A2:   for l being Nat st l = n-k holds r2 = (n!)/((k!) * (l!));
      r1 = (n!)/((k!) * (m!)) by A1;
      hence thesis by A2;
    end;
    thus thesis;
  end;
end;

registration
  let k,n be Nat;
  cluster n choose k -> real;
  coherence
  proof
    per cases;
    suppose
A1:   n >= k;
      then reconsider l = n-k as Element of NAT by INT_1:5;
      n choose k = (n!)/((k!) * (l!)) by A1,Def3;
      hence thesis;
    end;
    suppose n < k;
      hence thesis by Def3;
    end;
  end;
end;

definition
  let k,n be Nat;
  redefine func n choose k -> Real;
  coherence by XREAL_0:def 1;
end;

theorem Th19:
  s choose 0 = 1
proof
  reconsider m = s-0 as Element of NAT by ORDINAL1:def 12;
  m = s;
  then (s choose 0) = (s!)/(1 * (s!)) by Def3,Th12
    .= 1 by XCMPLX_1:60;
  hence thesis;
end;

theorem Th20:
  s >= t & r = s-t implies s choose t = s choose r
proof
  assume
A1: s>=t;
  t-s>=0-s by XREAL_1:9;
  then
A2: --s>=-(t-s) by XREAL_1:24;
  assume
A3: r = s-t;
  then t = s-r;
  then s choose r = (s!)/((r!) * (t!)) by A2,Def3;
  hence thesis by A1,A3,Def3;
end;

theorem Th21:
  s choose s = 1
proof
  reconsider m = s-s as Element of NAT by INT_1:5;
  m = 0;
  then s choose s = s choose 0 by Th20;
  hence thesis by Th19;
end;

theorem Th22:
  (t+1) choose (s+1) = (t choose (s+1)) + (t choose s)
proof
  per cases by XXREAL_0:1;
  suppose
A1: s<t;
    thus ((t+1) choose (s+1)) = (t choose (s+1)) + (t choose s)
    proof
      reconsider m1 = t-s as Element of NAT by A1,INT_1:5;
A2:   s+1<=t by A1,NAT_1:13;
      then reconsider m2 = t-(s+1) as Element of NAT by INT_1:5;
A3:   s+1<=t+1 by A1,XREAL_1:6;
      then reconsider m = (t+1)-(s+1) as Element of NAT by INT_1:5;
      (t choose (s+1)) = (t!)/(((s+1)!) * (m2!)) by A2,Def3;
      then
A4:   (t choose (s+1)) + (t choose s) = (t!)/(((s+1)!) * (m2!)) + (t!)/((s
      !) * (m1!)) by A1,Def3
        .= ((t!)*((s!)*(m1!))+(t!)*(((s+1)!)*(m2!)))/((((s+1)!)*(m2!))*((s!)
      *(m1!))) by XCMPLX_1:116
        .= (t!*((s!)*(m1!))+(t!)*(s!*(s+1)*(m2!)))/((((s+1)!)*(m2!))*((s!)*(
      m1!))) by Th15
        .= (s!*((t!)*((m1!)+(s+1)*(m2!))))/(s!*((m1!)*((s+1)!*(m2!))))
        .=(t!*(((m2+1)!)+(s+1)*(m2!)))/(m1!*((s+1)!*(m2!))) by XCMPLX_1:91
        .= (t!*((m2!)*(m2+1)+(m2!)*(s+1)))/(m1!*((s+1)!*(m2!))) by Th15
        .= (m2!*((t!)*((m2+1)+(s+1))))/(m2!*(((s+1)!)*(m1!)))
        .= ((t!)*(t-(s-(s+1))))/(((s+1)!)*(m1!)) by XCMPLX_1:91
        .= ((t+1)!)/(((s+1)!)*(m1!)) by Th15;
      m = m1;
      hence thesis by A4,A3,Def3;
    end;
  end;
  suppose
A5: s=t;
    then s<t+1 by NAT_1:13;
    then
A6: t choose (s+1)=0 by A5,Def3;
    (t+1) choose (s+1)=1 by A5,Th21;
    hence thesis by A5,A6,Th21;
  end;
  suppose
A7: s>t;
    then s+1 >t+1 by XREAL_1:8;
    then
A8: (t+1) choose (s+1)=0 by Def3;
A9: s+1>t+0 by A7,XREAL_1:8;
    t choose s =0 by A7,Def3;
    hence thesis by A9,A8,Def3;
  end;
end;

theorem Th23:
  s >= 1 implies s choose 1 = s
proof
  defpred P[Nat] means $1 choose 1 = $1;
A1: now
    let n be Nat;
    assume that
    n>=1 and
A2: P[n];
    (n+1) choose 1 = (n+1) choose (0+1) .= n + n choose 0 by A2,Th22
      .= n+1 by Th19;
    hence P[n+1];
  end;
A3: P[1] by Th21;
  for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(A3,A1);
  hence thesis;
end;

theorem
  s>=1 & t = s-1 implies s choose t = s
proof
  assume that
A1: s>=1 and
A2: t = s-1;
  s choose t = s choose 1 by A1,A2,Th20;
  hence thesis by A1,Th23;
end;

theorem Th25:
  s choose r is Element of NAT
proof
  defpred P[Nat] means for r holds ($1 choose r) is Element of NAT;
A1: for s st P[s] holds P[s+1]
  proof
    let s;
    assume
A2: P[s];
A3: for r st r <> 0 holds ((s+1) choose r) is Element of NAT
    proof
      let r;
      assume
A4:   r <> 0;
      ((s+1) choose r) is Element of NAT
      proof
        consider t being Nat such that
A5:     r = t+1 by A4,NAT_1:6;
        reconsider t as Element of NAT by ORDINAL1:def 12;
        reconsider m1 = (s choose t), m2 = (s choose (t+1)) as Element of NAT
        by A2;
        m1 + m2 =(s choose t) + (s choose (t+1));
        hence thesis by A5,Th22;
      end;
      hence thesis;
    end;
    let r;
    r = 0 or r<>0;
    hence thesis by A3,Th19;
  end;
A6: P[0]
  proof
    let r;
    r = 0 or r > 0;
    hence thesis by Def3,Th19;
  end;
  for s holds P[s] from NAT_1:sch 2(A6,A1);
  hence thesis;
end;

theorem
  for m,F st m <> 0 & len F = m & (for i,l st i in dom F & l = n+i-1
  holds F.i = l choose n) holds Sum F = (n+m) choose (n+1)
proof
  defpred P[Nat] means for F st $1 <> 0 & len F = $1 & (for i,l st i in dom F
  & l = n+i-1 holds F.i = l choose n) holds Sum F = (n+$1) choose (n+1);
A1: for m st P[m] holds P[m+1]
  proof
    let m;
    assume
A2: P[m];
    let F;
    assume that
    m+1 <> 0 and
A3: len F = m+1 and
A4: for i,l st i in dom F & l = n+i-1 holds F.i = l choose n;
    consider G be FinSequence of REAL,x being Real such that
A5: F = G^<*x*> by A3,FINSEQ_2:19;
A6: m+1 = len G +1 by A3,A5,FINSEQ_2:16;
    per cases;
    suppose
A7:   m = 0;
A8:   n = n+1-1;
A9:   dom F = Seg 1 by A3,A7,FINSEQ_1:def 3;
      then 1 in dom F;
      then F.1 = n choose n by A4,A8;
      hence Sum F = Sum<*n choose n*> by A9,FINSEQ_1:def 8
        .= n choose n by FINSOP_1:11
        .= 1 by Th21
        .= (n+(m+1)) choose (n+1) by A7,Th21;
    end;
    suppose
A10:  m <> 0;
A11:  n+m = n +(m+1)-1;
A12:  for i,l st i in dom G & l = n+i-1 holds G.i = l choose n
      proof
A13:    dom G c= dom F by A5,FINSEQ_1:26;
        let i,l;
        assume that
A14:    i in dom G and
A15:    l = n+i-1;
        G.i = F.i by A5,A14,FINSEQ_1:def 7;
        hence thesis by A4,A14,A15,A13;
      end;
      dom F = Seg (m+1) by A3,FINSEQ_1:def 3;
      then
A16:  (n+m) choose n = (G^<*x*>).(len G +1) by A4,A5,A6,A11,FINSEQ_1:4
        .= x by FINSEQ_1:42;
      thus Sum F = Sum G + x by A5,RVSUM_1:74
        .= (n+m) choose (n+1) + (n+m) choose n by A2,A6,A10,A12,A16
        .= (n+m+1) choose (n+1) by Th22
        .= (n+(m+1)) choose (n+1);
    end;
  end;
A17: P[0];
  thus for m holds P[m] from NAT_1:sch 2(A17,A1);
end;

registration
  let k,n be Nat;
  cluster n choose k -> natural;
  coherence by Th25;
end;

definition
  let k,n be Nat;
  redefine func n choose k -> Element of NAT;
  coherence by ORDINAL1:def 12;
end;

definition
  let a,b be real number;
  let n be Nat;
  func (a,b) In_Power n -> FinSequence of REAL means
  :Def4:
  len it = n+1 & for i,l,m being Nat st i in dom it & m = i - 1 & l = n-m holds
    it.i = (n choose m) * a|^l * b|^m;
  existence
  proof
    reconsider n as Element of NAT by ORDINAL1:def 12;
    defpred P[Nat,set] means for l,m be Nat st m = $1 - 1 & l = n-m holds $2 =
    (n choose m)* a|^l * b|^m;
A1: for k be Nat st k in Seg(n+1) ex x being set st P[k,x]
    proof
      let k be Nat;
      assume
A2:   k in Seg (n+1);
      then k >= 1 by FINSEQ_1:1;
      then reconsider m1 = k-1 as Element of NAT by INT_1:5;
      k <= n+1 by A2,FINSEQ_1:1;
      then k-1<=n+1-1 by XREAL_1:9;
      then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
      take (n choose m1)*a|^l1*b|^m1;
      thus thesis;
    end;
    consider p being FinSequence such that
A3: dom p = Seg(n+1) and
A4: for k be Nat st k in Seg(n+1) holds P[k,p.k] from FINSEQ_1:sch 1(A1);
    rng p c= REAL
    proof
      let x be set;
      assume x in rng p;
      then consider y be set such that
A5:   y in dom p and
A6:   x = p.y by FUNCT_1:def 3;
      reconsider y as Element of NAT by A5;
      y >= 1 by A3,A5,FINSEQ_1:1;
      then reconsider m1 = y-1 as Element of NAT by INT_1:5;
      y <= n+1 by A3,A5,FINSEQ_1:1;
      then y-1<=n+1-1 by XREAL_1:9;
      then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
      p.y = (n choose m1) *a|^l1*b|^m1 by A3,A4,A5;
      then reconsider x as Real by A6;
      x in REAL;
      hence thesis;
    end;
    then reconsider p as FinSequence of REAL by FINSEQ_1:def 4;
    take p;
    thus thesis by A3,A4,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let G,H;
    assume that
A7: len G = n+1 and
A8: for i,l,m be Nat st i in dom G & m = i - 1 & l = n-m holds G.i =
    (n choose m)* a|^l * b|^m;
    assume that
A9: len H = n+1 and
A10: for i,l,m be Nat st i in dom H & m = i - 1 & l = n-m holds H.i =
    (n choose m)* a|^l * b|^m;
    for i st i in dom G holds G.i = H.i
    proof
      let i;
      assume
A11:  i in dom G;
      then
A12:  i in Seg (n+1) by A7,FINSEQ_1:def 3;
      then i>=1 by FINSEQ_1:1;
      then reconsider m = i-1 as Element of NAT by INT_1:5;
      i<=n+1 by A12,FINSEQ_1:1;
      then i-1<=n+1-1 by XREAL_1:9;
      then reconsider l = n-m as Element of NAT by INT_1:5;
      i in dom H by A9,A12,FINSEQ_1:def 3;
      then H.i = (n choose m)* a|^l *b|^m by A10;
      hence thesis by A8,A11;
    end;
    hence thesis by A7,A9,FINSEQ_2:9;
  end;
end;

theorem Th27:
  (a,b) In_Power 0 = <*1*>
proof
  set F = (a,b) In_Power 0;
A1: len F = 0+1 by Def4
    .= 1;
  then
A2: dom F = {1} by FINSEQ_1:2,def 3;
  then 1 in dom F by TARSKI:def 1;
  then consider i be set such that
A3: i in dom F;
  reconsider i as Element of NAT by A3;
A4: i = 1 by A2,A3,TARSKI:def 1;
  then reconsider m1 = i-1 as Element of NAT by INT_1:5;
  reconsider l1 = 0-m1 as Element of NAT by A4;
  1 in dom (a,b) In_Power 0 by A2,TARSKI:def 1;
  then F.1 = (0 choose 0)*a|^l1*b|^m1 by A4,Def4
    .= 1*a|^0*b|^0 by A4,Th21
    .= 1 by RVSUM_1:94;
  hence thesis by A1,FINSEQ_1:40;
end;

theorem Th28:
  ((a,b) In_Power s).1 = a|^s
proof
  reconsider m1 = 1-1 as Element of NAT by INT_1:5;
  reconsider l1 = s-m1 as Nat;
  len ((a,b) In_Power s) = s+1 by Def4;
  then
A1: dom ((a,b) In_Power s) = Seg (s+1) by FINSEQ_1:def 3;
  s+1>=0+1 by XREAL_1:6;
  then 1 in dom ((a,b) In_Power s) by A1;
  then ((a,b) In_Power s).1 = (s choose 0)*a|^l1*b|^m1 by Def4
    .= 1*a|^l1*b|^m1 by Th19
    .= a|^s by RVSUM_1:94;
  hence thesis;
end;

theorem Th29:
  ((a,b) In_Power s).(s+1) = b|^s
proof
  reconsider m1 = s+1-1 as Element of NAT by INT_1:5,NAT_1:12;
  reconsider l1 = s-m1 as Element of NAT by INT_1:5;
  len ((a,b) In_Power s) = s+1 by Def4;
  then dom ((a,b) In_Power s) = Seg (s+1) by FINSEQ_1:def 3;
  then s+1 in dom ((a,b) In_Power s) by FINSEQ_1:4;
  then ((a,b) In_Power s).(s+1) = (s choose s)*a|^l1*b|^m1 by Def4
    .= 1*a|^l1*b|^m1 by Th21
    .= 1*b|^m1 by RVSUM_1:94
    .= b|^s;
  hence thesis;
end;

theorem Th30:
  (a+b) |^ s = Sum((a,b) In_Power s)
proof
  defpred P[Nat] means (a+b) |^ $1 = Sum((a,b) In_Power $1);
A1: for n st P[n] holds P[n+1]
  proof
    reconsider a, b as Real by XREAL_0:def 1;
    let n;
    reconsider G1 = ((a*((a,b) In_Power n))^<*0 qua Real*>) as FinSequence of
    REAL;
    set G2 = (<*0 qua Real*>^(b*((a,b) In_Power n)));
    assume P[n];
    then
A2: (a+b) |^ (n+1) = (a+b)*Sum((a,b) In_Power n) by Th6
      .= a*Sum((a,b) In_Power n) + b*Sum((a,b) In_Power n)
      .= Sum(a*((a,b) In_Power n)) + b*Sum((a,b) In_Power n) by RVSUM_1:87
      .= Sum(a*((a,b) In_Power n)) + Sum(b*((a,b) In_Power n)) by RVSUM_1:87;
    len G2 = len <*0*> + len (b*((a,b) In_Power n)) by FINSEQ_1:22
      .= 1+ len (b*((a,b) In_Power n)) by FINSEQ_1:40
      .= 1+ len ((a,b) In_Power n) by Th2
      .= n+1+1 by Def4;
    then reconsider F2 = G2 as Element of (n+1+1)-tuples_on REAL by FINSEQ_2:92
;
    len G1 = len (a*((a,b) In_Power n)) + len <*0*> by FINSEQ_1:22
      .= len (a*((a,b) In_Power n)) +1 by FINSEQ_1:40
      .= len ((a,b) In_Power n) +1 by Th2
      .= n+1+1 by Def4;
    then reconsider F1 = G1 as Element of (n+1+1)-tuples_on REAL by FINSEQ_2:92
;
A3: Sum F2 = 0+ Sum(b*((a,b) In_Power n)) by RVSUM_1:76
      .= Sum(b*((a,b) In_Power n));
    Sum F1 = Sum(a*((a,b) In_Power n)) +0 by RVSUM_1:74
      .= Sum(a*((a,b) In_Power n));
    then
A4: Sum(G1+G2) = Sum(a*((a,b) In_Power n))+ Sum (b*((a,b) In_Power n)) by A3,
RVSUM_1:89;
    set F = F1 + F2;
A5: len F2 = n+1+1 by CARD_1:def 7;
A6: len F = n+1+1 by CARD_1:def 7;
A7: len F1 = n+1+1 by CARD_1:def 7;
A8: for i st i in dom ((a,b) In_Power (n+1)) holds F.i = ((a,b) In_Power
    (n+1)).i
    proof
      let i;
      assume
A9:   i in dom ((a,b) In_Power (n+1));
      set r2 = F2/.i;
      set r1 = F1/.i;
      set r = ((a,b) In_Power n)/.i;
A10:  len ((a,b) In_Power (n+1)) = n+1+1 by Def4;
      then
A11:  i in Seg (n+1+1) by A9,FINSEQ_1:def 3;
      then
A12:  i in dom F1 by A7,FINSEQ_1:def 3;
A13:  i in dom F2 by A5,A11,FINSEQ_1:def 3;
A14:  i in {1} implies F.i = ((a,b) In_Power (n+1)).i
      proof
        n+1>=0+1 by XREAL_1:6;
        then 1 in Seg (n+1);
        then 1 in Seg len (((a,b) In_Power n)) by Def4;
        then
A15:    1 in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
        then
A16:    1 in dom (a*((a,b) In_Power n)) by VALUED_1:def 5;
        assume i in {1};
        then
A17:    i = 1 by TARSKI:def 1;
        then
A18:    r = ((a,b) In_Power n).1 by A15,PARTFUN1:def 6;
        r = ((a,b) In_Power n).i by A17,A15,PARTFUN1:def 6;
        then
A19:    r = a|^n by A17,Th28;
A20:    r1 = ((a*((a,b) In_Power n))^<*0*>).1 by A12,A17,PARTFUN1:def 6
          .= (a*((a,b) In_Power n)).1 by A16,FINSEQ_1:def 7
          .= a *a|^n by A18,A19,RVSUM_1:44
          .= a|^(n+1) by Th6;
A21:    r2 = F2.i by A13,PARTFUN1:def 6;
A22:    r1 = F1.i by A12,PARTFUN1:def 6;
        r2 = (<*0*>^(b*((a,b) In_Power n))).1 by A13,A17,PARTFUN1:def 6
          .= 0 by FINSEQ_1:41;
        then F.i = r1+0 by A22,A21,RVSUM_1:11
          .= ((a,b) In_Power (n+1)).i by A17,A20,Th28;
        hence thesis;
      end;
      i>=1 by A11,FINSEQ_1:1;
      then reconsider j = i-1 as Element of NAT by INT_1:5;
      set x = ((a,b) In_Power n)/.j;
A23:  i = j+1;
A24:  i in dom F by A6,A11,FINSEQ_1:def 3;
A25:  i in {k where k is Element of NAT: k>1 & k<n+1+1} implies F.i = ((a
      ,b) In_Power (n+1)).i
      proof
        assume i in {k where k is Element of NAT: 1<k & k<n+1+1};
        then
A26:    ex k being Element of NAT st k=i & 1<k & k<n+1+1;
        then reconsider m1 = i-1 as Element of NAT by INT_1:5;
A27:    r1 = ((a*((a,b) In_Power n))^<*0*>).i by A12,PARTFUN1:def 6;
        1<=j by A23,A26,NAT_1:13;
        then reconsider m2 = j-1 as Element of NAT by INT_1:5;
A28:    j<=n+1 by A23,A26,XREAL_1:6;
        then j-1<=n+1-1 by XREAL_1:9;
        then reconsider l2 = n-m2 as Element of NAT by INT_1:5;
        1<=j by A23,A26,NAT_1:13;
        then j in Seg (n+1) by A28;
        then j in Seg len ((a,b) In_Power n) by Def4;
        then
A29:    j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
        then
A30:    x = ((a,b) In_Power n).j by PARTFUN1:def 6;
A31:    i<=n+1 by A26,NAT_1:13;
        then i in Seg (n+1) by A26;
        then i in Seg len ((a,b) In_Power n) by Def4;
        then
A32:    i in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
        then
A33:    r = ((a,b) In_Power n).i by PARTFUN1:def 6;
        i in dom (a*((a,b) In_Power n)) by A32,VALUED_1:def 5;
        then
A34:    r1 = (a*((a,b) In_Power n)).i by A27,FINSEQ_1:def 7
          .= a*r by A33,RVSUM_1:44;
        i-1<=n+1-1 by A31,XREAL_1:9;
        then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
A35:    l1+1 = n+1-(m2+1);
A36:    j in dom (b*((a,b) In_Power n)) by A29,VALUED_1:def 5;
A37:    r2 = (<*0*>^(b*((a,b) In_Power n))).i by A13,PARTFUN1:def 6;
        then r2 = (<*0*>^(b*((a,b) In_Power n))).(len <*0*> +j) by A23,
FINSEQ_1:40
          .= (b*((a,b) In_Power n)).j by A36,FINSEQ_1:def 7
          .= b*x by A30,RVSUM_1:44;
        then F.i = a*r + b*x by A24,A27,A37,A34,VALUED_1:def 1
          .= a*(a|^l1*(n choose m1)*b|^m1) + b*x by A32,A33,Def4
          .= a*a|^l1*((n choose m1)*b|^m1) + b*x
          .= a|^(l1+1)*((n choose m1)*b|^m1) + b*x by Th6
          .= a|^(l1+1)*((n choose m1)*b|^m1) + b*(b|^m2*((n choose m2)*a|^l2
        )) by A29,A30,Def4
          .= a|^(l1+1)*((n choose m1)*b|^m1) + b*b|^m2*((n choose m2)*a|^l2)
          .= a|^(l1+1)*((n choose (m2+1))*b|^(m2+1)) + b|^(m2+1)*((n choose
        m2)*a|^l2) by Th6
          .= ((n choose (m2+1)) + (n choose m2))*a|^(l1+1)*b|^(m2+1)
          .= ((n+1) choose (m2+1))*a|^(l1+1)*b|^(m2+1) by Th22
          .= ((a,b) In_Power (n+1)).i by A9,A35,Def4;
        hence thesis;
      end;
A38:  i in {n+1+1} implies F.i = ((a,b) In_Power (n+1)).i
      proof
        assume
A39:    i in {n+1+1};
        then
A40:    i = n+1+1 by TARSKI:def 1;
A41:    j = n+1+1-1 by A39,TARSKI:def 1
          .= n+1;
        n+1 in Seg (n+1) by FINSEQ_1:4;
        then j in Seg len (((a,b) In_Power n)) by A41,Def4;
        then
A42:    j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
        then
A43:    x = ((a,b) In_Power n).(n+1) by A41,PARTFUN1:def 6
          .= b|^n by Th29;
A44:    x = ((a,b) In_Power n).j by A42,PARTFUN1:def 6;
A45:    j in dom (b*((a,b) In_Power n)) by A42,VALUED_1:def 5;
A46:    r2 = (<*0*>^(b*((a,b) In_Power n))).(1+n+1) by A13,A40,PARTFUN1:def 6
          .= (<*0*>^(b*((a,b) In_Power n))).(len <*0*> +j) by A41,FINSEQ_1:39
          .= (b*((a,b) In_Power n)).j by A45,FINSEQ_1:def 7
          .= b*b|^n by A44,A43,RVSUM_1:44
          .= b|^(n+1) by Th6;
A47:    r2 = F2.i by A13,PARTFUN1:def 6;
        n+1 = len ((a,b) In_Power n) by Def4
          .= len (a*((a,b) In_Power n)) by Th2;
        then
A48:    r1 = ((a*((a,b) In_Power n))^<*0*>).(len (a*((a,b) In_Power n))+1
        ) by A12,A40,PARTFUN1:def 6
          .= 0 by FINSEQ_1:42;
        r1 = F1.i by A12,PARTFUN1:def 6;
        then F.i = 0+r2 by A48,A47,RVSUM_1:11
          .= ((a,b) In_Power (n+1)).i by A40,A46,Th29;
        hence thesis;
      end;
A49:  now
        assume
        i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} \/ { n+1+1};
        then i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} or i in
        {n+1+1} by XBOOLE_0:def 3;
        hence thesis by A14,A25,A38,XBOOLE_0:def 3;
      end;
      dom ((a,b) In_Power (n+1)) = Seg (n+1+1) by A10,FINSEQ_1:def 3;
      hence thesis by A9,A49,Th1,NAT_1:12;
    end;
    len ((a,b) In_Power (n+1)) = len F by A6,Def4;
    hence thesis by A2,A4,A8,FINSEQ_2:9;
  end;
  (a+b) |^ 0 = Sum<*1 qua Real*> by FINSOP_1:11,RVSUM_1:94
    .= Sum((a,b) In_Power 0) by Th27;
  then
A50: P[0];
  for n holds P[n] from NAT_1:sch 2(A50,A1);
  hence thesis;
end;

definition
  let n be Nat;
  func Newton_Coeff n -> FinSequence of REAL means
  :Def5:
  len it = n+1 & for i,k be Nat st i in dom it & k = i-1 holds
  it.i = n choose k;
  existence
  proof
    reconsider n as Element of NAT by ORDINAL1:def 12;
    defpred P[Nat,set] means for s st s = $1-1 holds $2 = n choose s;
A1: for l be Nat st l in Seg (n+1) ex x being set st P[l,x]
    proof
      let l be Nat;
      assume l in Seg (n+1);
      then l>=1 by FINSEQ_1:1;
      then reconsider k = l-1 as Element of NAT by INT_1:5;
      set x = n choose k;
      take x;
      thus thesis;
    end;
    consider F being FinSequence such that
A2: dom F = Seg (n+1) & for l be Nat st l in Seg (n+1) holds P[l,F.l]
    from FINSEQ_1:sch 1(A1);
    rng F c= REAL
    proof
      let x be set;
      assume x in rng F;
      then consider y be set such that
A3:   y in dom F and
A4:   x = F.y by FUNCT_1:def 3;
      reconsider y as Element of NAT by A3;
      y >= 1 by A2,A3,FINSEQ_1:1;
      then reconsider m1 = y-1 as Element of NAT by INT_1:5;
      F.y = n choose m1 by A2,A3;
      then reconsider x as Real by A4;
      x in REAL;
      hence thesis;
    end;
    then reconsider F as FinSequence of REAL by FINSEQ_1:def 4;
    take F;
    thus thesis by A2,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let G,H;
    assume that
A5: len G = n+1 and
A6: for i,m be Nat st i in dom G & m = i - 1 holds G.i = n choose m;
    assume that
A7: len H = n+1 and
A8: for i,m be Nat st i in dom H & m = i - 1 holds H.i = n choose m;
    for i st i in dom G holds G.i = H.i
    proof
      let i;
      assume
A9:   i in dom G;
      then
A10:  i in Seg (n+1) by A5,FINSEQ_1:def 3;
      then i>=1 by FINSEQ_1:1;
      then reconsider m = i-1 as Element of NAT by INT_1:5;
      i in dom H by A7,A10,FINSEQ_1:def 3;
      then H.i = n choose m by A8;
      hence thesis by A6,A9;
    end;
    hence thesis by A5,A7,FINSEQ_2:9;
  end;
end;

theorem Th31:
  Newton_Coeff s = (1,1) In_Power s
proof
A1: for i st i in dom (Newton_Coeff s) holds (Newton_Coeff s).i = ((1,1)
  In_Power s).i
  proof
    let i;
    assume
A2: i in dom (Newton_Coeff s);
A3: dom (Newton_Coeff s) = Seg len (Newton_Coeff s) by FINSEQ_1:def 3
      .= Seg (s+1) by Def5;
    then i>=1 by A2,FINSEQ_1:1;
    then reconsider m1 = i-1 as Element of NAT by INT_1:5;
    i<=(s+1) by A2,A3,FINSEQ_1:1;
    then s+1-1>=i-1 by XREAL_1:9;
    then reconsider l1 = s-m1 as Element of NAT by INT_1:5;
    dom (Newton_Coeff s) = Seg len ((1,1) In_Power s) by A3,Def4
      .= dom ((1,1) In_Power s) by FINSEQ_1:def 3;
    then ((1,1) In_Power s).i = (s choose m1)*1|^l1*1|^m1 by A2,Def4
      .= (s choose m1)*1*1|^m1 by Th10
      .= (s choose m1)*1 by Th10
      .= (Newton_Coeff s).i by A2,Def5;
    hence thesis;
  end;
  len (Newton_Coeff s) = s+1 by Def5
    .= len ((1,1) In_Power s) by Def4;
  hence thesis by A1,FINSEQ_2:9;
end;

theorem
  2|^s = Sum(Newton_Coeff s)
proof
  2|^s = (1+1) |^ s .= Sum((1,1) In_Power s) by Th30
    .= Sum(Newton_Coeff s) by Th31;
  hence thesis;
end;

begin :: Addenda
:: from NAT_LAT

theorem Th33:
  l >= 1 implies k*l >= k
proof
  assume
A1: l>=1;
  for k holds k*l>=k
  proof
    defpred P[Nat] means $1*l>=$1;
A2: for k st P[k] holds P[k+1]
    proof
      let k;
A3:   (k + 1)*l = k * l + 1*l;
A4:   k+l>=k+1 by A1,XREAL_1:7;
      assume k*l>=k;
      then (k+1)*l>=k+l by A3,XREAL_1:7;
      hence (k+1)*l>=k+1 by A4,XXREAL_0:2;
    end;
A5: P[0];
    thus for k holds P[k] from NAT_1:sch 2(A5,A2);
  end;
  hence thesis;
end;

theorem Th34:
  l >= 1 & n >= k*l implies n >= k
proof
  assume that
A1: l>=1 and
A2: n>=k*l;
  k*l>=k by A1,Th33;
  hence thesis by A2,XXREAL_0:2;
end;

definition
  let n;
  redefine func n! -> Element of NAT;
  coherence by Th16;
end;

theorem Th35:
  l <> 0 implies l divides l!
proof
  assume l<>0;
  then consider n being Nat such that
A1: l = n+1 by NAT_1:6;
  reconsider n as Element of NAT by ORDINAL1:def 12;
  (n+1)! = (n+1) * (n!) by Th15;
  hence thesis by A1,NAT_D:def 3;
end;

theorem
  n <> 0 implies (n+1)/n > 1
proof
  assume
A1: n<>0;
  (n+1)/n=n/n+1/n by XCMPLX_1:62
    .=1+1/n by A1,XCMPLX_1:60;
  hence thesis by A1,XREAL_1:29;
end;

theorem Th37:
  k/(k+1) < 1
proof
  m < m+1 by XREAL_1:29;
  hence thesis by XREAL_1:189;
end;

theorem Th38:
  l! >= l
proof
  defpred P[Nat] means $1! >= $1;
A1: for l st P[l] holds P[l+1]
  proof
    let l;
    assume
A2: l!>=l;
A3: l!*(l+1)=(l+1)! by Th15;
    l=0 & (l+1)!>=(l+1) or l>=1 & (l+1)!>=(l+1)
    proof
      per cases by NAT_1:14;
      case
        l=0;
        hence thesis by FINSEQ_2:50,RVSUM_1:95;
      end;
      case
A4:     l>=1;
        (l+1)!>=(l+1)*l by A2,A3,XREAL_1:64;
        hence thesis by A4,Th34;
      end;
    end;
    hence thesis;
  end;
A5: P[0];
  for l being Nat holds P[l] from NAT_1:sch 2(A5,A1);
  hence thesis;
end;

theorem Th39:
  m<>1 & m divides n implies not m divides (n+1)
proof
  assume that
A1: m<>1 and
A2: m divides n and
A3: m divides (n+1);
  consider t being Nat such that
A4: n = m * t by A2,NAT_D:def 3;
  consider s being Nat such that
A5: n+1 = m * s by A3,NAT_D:def 3;
  t <= s
  proof
    (n+1)*t=m*s*t by A5
      .= n*s by A4;
    then
A6: t=n*s/(n+1) by XCMPLX_1:89
      .=s*(n/(n+1)) by XCMPLX_1:74;
    assume
A7: t > s;
    s>0 by A5;
    hence contradiction by A7,A6,Th37,XREAL_1:157;
  end;
  then reconsider r =s-t as Element of NAT by INT_1:5;
  1=m*s-m*t by A4,A5;
  then 1=m*r;
  hence contradiction by A1,NAT_1:15;
end;

theorem Th40:
  j<>0 implies j divides (j+k)!
proof
  defpred P[Nat] means for j st j<>0 holds j divides (j+$1)!;
A1: for k st P[k] holds P[k+1]
  proof
    let k;
    assume
A2: for j st j<>0 holds j divides (j+k)!;
    let j;
    assume j<>0;
    then j divides ((j+k)!)*((j+k)+1) by A2,NAT_D:9;
    hence thesis by Th15;
  end;
A3: P[0] by Th35;
  for k holds P[k] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

theorem Th41:
  j<=l & j<>0 implies j divides l!
proof
  assume that
A1: j<=l and
A2: j<>0;
  ex k being Nat st l=j+k by A1,NAT_1:10;
  hence thesis by A2,Th40;
end;

theorem
  j<>1 & j<>0 & j divides (l!+1) implies j>l by Th39,Th41;

:: The fundamental properties of lcm, hcf

theorem
  m lcm (n lcm k) = (m lcm n) lcm k
proof
  set M = n lcm k;
  set K = m lcm M;
  set N = m lcm n;
  set L = N lcm k;
A1: m divides K by NAT_D:def 4;
A2: M divides K by NAT_D:def 4;
  n divides M by NAT_D:def 4;
  then n divides K by A2,NAT_D:4;
  then
A3: N divides K by A1,NAT_D:def 4;
  k divides M by NAT_D:def 4;
  then k divides K by A2,NAT_D:4;
  then
A4: L divides K by A3,NAT_D:def 4;
A5: N divides L by NAT_D:def 4;
A6: k divides L by NAT_D:def 4;
  n divides N by NAT_D:def 4;
  then n divides L by A5,NAT_D:4;
  then
A7: M divides L by A6,NAT_D:def 4;
  m divides N by NAT_D:def 4;
  then m divides L by A5,NAT_D:4;
  then K divides L by A7,NAT_D:def 4;
  hence thesis by A4,NAT_D:5;
end;

theorem Th44:
  m divides n iff m lcm n = n
proof
  thus m divides n implies m lcm n = n
  proof
    set M = m lcm n;
    assume m divides n;
    then
A1: M divides n by NAT_D:def 4;
    n divides M by NAT_D:def 4;
    hence thesis by A1,NAT_D:5;
  end;
  thus thesis by NAT_D:def 4;
end;

theorem
  n divides m & k divides m iff n lcm k divides m
proof
  n lcm k divides m implies n divides m & k divides m
  proof
    set M = n lcm k;
A1: n divides M by NAT_D:def 4;
A2: k divides M by NAT_D:def 4;
    assume n lcm k divides m;
    hence thesis by A1,A2,NAT_D:4;
  end;
  hence thesis by NAT_D:def 4;
end;

theorem
  m lcm 1 = m
proof
  set M = m lcm 1;
  1 divides m by NAT_D:6;
  then
A1: M divides m by NAT_D:def 4;
  m divides M by NAT_D:def 4;
  hence thesis by A1,NAT_D:5;
end;

theorem Th47:
  m lcm n divides m*n
proof
  set s=m*n;
A1: n divides s by NAT_D:9;
  m divides s by NAT_D:9;
  hence thesis by A1,NAT_D:def 4;
end;

theorem
  m gcd (n gcd k) = (m gcd n) gcd k
proof
  set M = n gcd k;
  set K = m gcd M;
  set N = m gcd n;
  set L = N gcd k;
A1: K divides M by NAT_D:def 5;
A2: K divides m by NAT_D:def 5;
  M divides n by NAT_D:def 5;
  then K divides n by A1,NAT_D:4;
  then
A3: K divides N by A2,NAT_D:def 5;
A4: L divides N by NAT_D:def 5;
A5: L divides k by NAT_D:def 5;
  N divides n by NAT_D:def 5;
  then L divides n by A4,NAT_D:4;
  then
A6: L divides M by A5,NAT_D:def 5;
  N divides m by NAT_D:def 5;
  then L divides m by A4,NAT_D:4;
  then
A7: L divides K by A6,NAT_D:def 5;
  M divides k by NAT_D:def 5;
  then K divides k by A1,NAT_D:4;
  then K divides L by A3,NAT_D:def 5;
  hence thesis by A7,NAT_D:5;
end;

theorem Th49:
  n divides m implies n gcd m = n
proof
  set N = n gcd m;
  assume n divides m;
  then
A1: n divides N by NAT_D:def 5;
  N divides n by NAT_D:def 5;
  hence thesis by A1,NAT_D:5;
end;

theorem
  m divides n & m divides k iff m divides n gcd k
proof
  m divides n gcd k implies m divides n & m divides k
  proof
    set M = n gcd k;
A1: M divides n by NAT_D:def 5;
A2: M divides k by NAT_D:def 5;
    assume m divides n gcd k;
    hence thesis by A1,A2,NAT_D:4;
  end;
  hence thesis by NAT_D:def 5;
end;

theorem
  m gcd 1 = 1
proof
  set M = m gcd 1;
A1: 1 divides M by NAT_D:6;
  M divides 1 by NAT_D:def 5;
  hence thesis by A1,NAT_D:5;
end;

theorem
  m gcd 0 = m
proof
  set M = m gcd 0;
  m divides 0 by NAT_D:6;
  then
A1: m divides M by NAT_D:def 5;
  M divides m by NAT_D:def 5;
  hence thesis by A1,NAT_D:5;
end;

theorem Th53:
  (m gcd n) lcm n = n
proof
  set M = m gcd n;
  M divides n by NAT_D:def 5;
  hence thesis by Th44;
end;

theorem Th54:
  m gcd (m lcm n) = m
proof
  set M = m lcm n;
  m divides M by NAT_D:def 4;
  hence thesis by Th49;
end;

theorem
  m gcd (m lcm n) = (n gcd m) lcm m
proof
  m gcd (m lcm n) = m by Th54;
  hence thesis by Th53;
end;

theorem
  m divides n implies m gcd k divides n gcd k
proof
  set M = m gcd k;
A1: M divides k by NAT_D:def 5;
  assume
A2: m divides n;
  M divides m by NAT_D:def 5;
  then M divides n by A2,NAT_D:4;
  hence thesis by A1,NAT_D:def 5;
end;

theorem
  m divides n implies k gcd m divides k gcd n
proof
  set M = k gcd m;
A1: M divides k by NAT_D:def 5;
  assume
A2: m divides n;
  M divides m by NAT_D:def 5;
  then M divides n by A2,NAT_D:4;
  hence thesis by A1,NAT_D:def 5;
end;

theorem Th58:
  n > 0 implies n gcd m > 0
proof
  assume that
A1: n>0 and
A2: n gcd m <= 0;
A3: (n gcd m) divides n by NAT_D:def 5;
  n gcd m = 0 or n gcd m < 0 by A2;
  then ex r being Nat st n = 0*r by A3,NAT_D:def 3;
  hence contradiction by A1;
end;

theorem
  m > 0 & n > 0 implies m lcm n > 0
proof
  assume that
A1: m>0 and
A2: n>0 and
A3: m lcm n <= 0;
A4: (m lcm n) divides m*n by Th47;
  m lcm n = 0 or m lcm n < 0 by A3;
  then ex r being Nat st m*n = 0*r by A4,NAT_D:def 3;
  hence contradiction by A1,A2;
end;

theorem
  (n gcd m) lcm (n gcd k) divides n gcd (m lcm k)
proof
  set M = m lcm k;
  set N = n gcd k;
  set P = n gcd m;
  set L = P lcm N;
A1: N divides k by NAT_D:def 5;
  k divides M by NAT_D:def 4;
  then
A2: N divides M by A1,NAT_D:4;
A3: P divides m by NAT_D:def 5;
  m divides M by NAT_D:def 4;
  then P divides M by A3,NAT_D:4;
  then
A4: L divides M by A2,NAT_D:def 4;
A5: P divides n by NAT_D:def 5;
  N divides n by NAT_D:def 5;
  then L divides n by A5,NAT_D:def 4;
  hence thesis by A4,NAT_D:def 5;
end;

theorem
  m divides l implies m lcm (n gcd l) divides (m lcm n) gcd l
proof
  set M = m lcm n;
  set K = M gcd l;
  set N = n gcd l;
A1: m divides M by NAT_D:def 4;
A2: N divides n by NAT_D:def 5;
A3: N divides l by NAT_D:def 5;
  n divides M by NAT_D:def 4;
  then N divides M by A2,NAT_D:4;
  then
A4: N divides K by A3,NAT_D:def 5;
  assume m divides l;
  then m divides K by A1,NAT_D:def 5;
  hence thesis by A4,NAT_D:def 4;
end;

theorem
  n gcd m divides n lcm m
proof
A1: n divides n lcm m by NAT_D:def 4;
  n gcd m divides n by NAT_D:def 5;
  hence thesis by A1,NAT_D:4;
end;

:: from GR_CY_2

reserve p,q for Nat;
reserve i0,i,i1,i2,i4 for Integer;

theorem
  0 < m implies n mod m = n - m * (n div m)
proof
  reconsider z1=m * (n div m),z2=(n mod m) as Integer;
  assume m > 0;
  then n - z1 = z1 + z2 -z1 by NAT_D:2;
  hence thesis;
end;

theorem
  i2 >= 0 implies i1 mod i2 >= 0 by INT_1:57;

theorem
  i2 > 0 implies i1 mod i2 < i2 by INT_1:58;

theorem
  i2 <> 0 implies i1 = (i1 div i2) * i2 + (i1 mod i2) by INT_1:59;

::$N Bezout's Theorem
theorem
  m>0 or n>0 implies ex i,i1 st i*m + i1*n = m gcd n
proof
  defpred P[Nat] means $1>0 & ex i,i1 st i*m+i1*n=$1;
  assume
A1: m>0 or n>0;
A2: ex p being Nat st P[p]
  proof
    per cases by A1;
    suppose
A3:   m>0;
      1*m + 0*n=m;
      hence thesis by A3;
    end;
    suppose
A4:   n>0;
      0*m + 1*n=n;
      hence thesis by A4;
    end;
  end;
  ex p be Nat st P[p] & for n be Nat st P[n] holds p <= n from NAT_1:sch 5
  (A2);
  then consider p being Nat such that
A5: p>0 and
A6: ex i,i0 st i*m+i0*n=p and
A7: for k be Nat st (k>0 & ex i1,i2 st i1*m+i2*n=k) holds p <= k;
  consider i,i0 such that
A8: i*m+i0*n=p by A6;
A9: for k st ex i1,i2 st i1*m+i2*n=k holds p divides k
  proof
    let k;
    given i1,i2 such that
A10: i1*m+i2*n=k;
    consider l,s being Nat such that
A11: k=p*l+s and
A12: s<p by A5,NAT_1:17;
    reconsider l,s as Element of NAT by ORDINAL1:def 12;
    s=0
    proof
      s = k - p*l by A11;
      then
A13:  s=(i1-i*l)*m+(i2-i0*l)*n by A8,A10;
      assume s<>0;
      hence contradiction by A7,A12,A13;
    end;
    hence thesis by A11,NAT_D:def 3;
  end;
A14: for s be Nat st s divides m & s divides n holds s divides p
  proof
    let s be Nat;
    assume that
A15: s divides m and
A16: s divides n;
    consider r being Nat such that
A17: n = s*r by A16,NAT_D:def 3;
    reconsider p9=p,s9=s as Integer;
    consider l being Nat such that
A18: m = s*l by A15,NAT_D:def 3;
    ex i4 st p9=s9*i4
    proof
      take i*l+i0*r;
      thus thesis by A8,A18,A17;
    end;
    hence thesis by INT_1:def 3;
  end;
  0*m + 1*n=n;
  then
A19: p divides n by A9;
  1*m + 0*n=m;
  then p divides m by A9;
  then p= m gcd n by A19,A14,NAT_D:def 5;
  hence thesis by A6;
end;

:: from NAT_LAT

definition
  func SetPrimes -> Subset of NAT means
  :Def6:
  for n being Nat holds n in it iff n is prime;
  existence
  proof
    defpred P[Nat] means $1 is prime;
    consider X being Subset of NAT such that
A1: for n being Element of NAT holds n in X iff P[n] from SUBSET_1:sch 3;
    take X;
    let n be Nat;
    thus n in X implies n is prime by A1;
    assume
A2: n is prime;
    n in NAT by ORDINAL1:def 12;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    let A, B be Subset of NAT such that
A3: for n being Nat holds n in A iff n is prime and
A4: for n being Nat holds n in B iff n is prime;
    thus A c= B
    proof
      let x be set;
      assume
A5:   x in A;
      then reconsider x as Element of NAT;
      x is prime by A3,A5;
      hence thesis by A4;
    end;
    let x be set;
    assume
A6: x in B;
    then reconsider x as Element of NAT;
    x is prime by A4,A6;
    hence thesis by A3;
  end;
end;

registration
  cluster prime for Element of NAT;
  existence by INT_2:28;
  cluster prime for Nat;
  existence by INT_2:28;
end;

definition
  mode Prime is prime Nat;
end;

reserve x for set;

definition
  let p be Nat;
  func SetPrimenumber p -> Subset of NAT means
  :Def7:
  for q being Nat holds q in it iff q < p & q is prime;
  existence
  proof
    defpred P[Nat] means $1 < p & $1 is prime;
    consider X being Subset of NAT such that
A1: for q being Element of NAT holds q in X iff P[q] from SUBSET_1:sch 3;
    take X;
    let q be Nat;
    thus q in X implies q < p & q is prime by A1;
    assume that
A2: q < p and
A3: q is prime;
    q in NAT by ORDINAL1:def 12;
    hence thesis by A1,A2,A3;
  end;
  uniqueness
  proof
    let A, B be Subset of NAT such that
A4: for q being Nat holds q in A iff q < p & q is prime and
A5: for q being Nat holds q in B iff q < p & q is prime;
    thus A c= B
    proof
      let x be set;
      assume
A6:   x in A;
      then reconsider x as Element of NAT;
A7:   x is prime by A4,A6;
      x < p by A4,A6;
      hence thesis by A5,A7;
    end;
    let x be set;
    assume
A8: x in B;
    then reconsider x as Element of NAT;
A9: x is prime by A5,A8;
    x < p by A5,A8;
    hence thesis by A4,A9;
  end;
end;

theorem Th68:
  SetPrimenumber p c= SetPrimes
proof
  let x;
  assume
A1: x in SetPrimenumber p;
  then reconsider x9 = x as Element of NAT;
  x9 is prime by A1,Def7;
  hence thesis by Def6;
end;

theorem
  p <= q implies SetPrimenumber p c= SetPrimenumber q
proof
  assume
A1: p <= q;
  let x;
  assume
A2: x in SetPrimenumber p;
  then reconsider x9 = x as Element of NAT;
  x9 < p by A2,Def7;
  then
A3: x9 < q by A1,XXREAL_0:2;
  x9 is prime by A2,Def7;
  hence thesis by A3,Def7;
end;

theorem Th70:
  SetPrimenumber p c= Seg p
proof
  let x be set;
  assume
A1: x in SetPrimenumber p;
  then reconsider q = x as Element of NAT;
  q is prime by A1,Def7;
  then
A2: 1 <= q by INT_2:def 4;
  q < p by A1,Def7;
  hence thesis by A2;
end;

theorem Th71:
  SetPrimenumber p is finite
proof
  SetPrimenumber p c= Seg p by Th70;
  hence thesis;
end;

registration
  let n be Nat;
  cluster SetPrimenumber n -> finite;
  coherence by Th71;
end;

reserve p for Prime;

theorem Th72:
  ex p st p is prime & p>l
proof
  reconsider two = 2 as Prime by INT_2:28;
  reconsider l as Element of NAT by ORDINAL1:def 12;
  l=0 & (ex p st p is prime & p>l) or l=1 & (ex p st p is prime & p>l) or
  2<=l & ex p st p is prime & p>l
  proof
    per cases by NAT_1:26;
    case
A1:   l=0;
      take two;
      thus thesis by A1;
    end;
    case
A2:   l=1;
      take two;
      thus thesis by A2;
    end;
    case
A3:   2<=l;
      l<=l! by Th38;
      then 2<=l! by A3,XXREAL_0:2;
      then (2+0) <= (l!+1) by XREAL_1:7;
      then consider j being Element of NAT such that
A4:   j is prime and
A5:   j divides (l!+1) by INT_2:31;
      reconsider j9=j as Prime by A4;
      take j9;
A6:   j<>0 by A4,INT_2:def 4;
      j<>1 by A4,INT_2:def 4;
      hence thesis by A5,A6,Th39,Th41;
    end;
  end;
  hence thesis;
end;

Lm2:
  SetPrimenumber 2 = {}
proof
  assume SetPrimenumber 2<>{};
  then consider x being set such that
A1: x in SetPrimenumber 2 by XBOOLE_0:def 1;
  reconsider x as Nat by A1;
A2: x is prime by A1,Def7;
  x<2 by A1,Def7;
  then 0 is prime or 1 is prime by A2,NAT_1:26;
  hence contradiction by INT_2:def 4;
end;

registration
  cluster SetPrimes -> non empty;
  coherence by Def6,INT_2:28;
end;

registration
  cluster SetPrimenumber 2 -> empty;
  coherence by Lm2;
end;

theorem
  SetPrimenumber m c= Seg m
proof
  let x be set;
  assume
A1: x in SetPrimenumber m;
  then reconsider x as Element of NAT;
  x is prime by A1,Def7;
  then
A2: 1 <= x by INT_2:def 4;
  x < m by A1,Def7;
  hence thesis by A2;
end;

theorem
  k>=m implies not k in SetPrimenumber m by Def7;

theorem
  SetPrimenumber n \/ {n} is finite;

theorem Th76:
  for f being Prime, g being Nat st f < g holds SetPrimenumber f
  \/ {f} c= SetPrimenumber g
proof
  let f be Prime,g be Nat;
  assume
A1: f<g;
  let x be set;
  assume
A2: x in SetPrimenumber f\/{f};
  then reconsider x as Nat;
  per cases by A2,XBOOLE_0:def 3;
  suppose
A3: x in SetPrimenumber f;
    then x < f by Def7;
    then
A4: x < g by A1,XXREAL_0:2;
    x is prime by A3,Def7;
    hence thesis by A4,Def7;
  end;
  suppose
    x in {f};
    then x = f by TARSKI:def 1;
    hence thesis by A1,Def7;
  end;
end;

theorem
  k>=m implies not k in SetPrimenumber m by Def7;

Lm3: SetPrimenumber n = {k where k is Element of NAT:k<n & k is prime}
proof
  thus SetPrimenumber n c= {k where k is Element of NAT:k<n & k is prime}
  proof
    let x be set;
    assume
A1: x in SetPrimenumber n;
    then reconsider x as Element of NAT;
A2: x is prime by A1,Def7;
    x < n by A1,Def7;
    hence thesis by A2;
  end;
  let x be set;
  assume x in {k where k is Element of NAT:k<n & k is prime};
  then ex k be Element of NAT st x=k & k<n & k is prime;
  hence thesis by Def7;
end;

definition
  let n be Nat;
  func primenumber n -> prime Element of NAT means
  :Def8:
  n = card SetPrimenumber it;
  existence
  proof
    defpred P1[Nat] means ex m st $1=card SetPrimenumber m & m is Prime;
A1: for n st P1[n] holds P1[n+1]
    proof
      let n;
      given m such that
A2:   n=card SetPrimenumber m and
A3:   m is Prime;
      defpred P[Nat] means $1 is prime & $1>m;
A4:   not m in SetPrimenumber m by Def7;
A5:   ex k be Nat st P[k]
      proof
        ex p st p is prime & p>m by Th72;
        hence thesis;
      end;
      consider k be Nat such that
A6:   P[k] & for l be Nat st P[l] holds k <= l from NAT_1:sch 5(A5);
      take k;
A7:   SetPrimenumber k c= SetPrimenumber m\/{m}
      proof
        let s be set;
        assume
A8:     s in SetPrimenumber k;
        then reconsider s as Element of NAT;
A9:     s is prime by A8,Def7;
        s<k by A8,Def7;
        then
A10:    s<=m by A6,A9;
        per cases by A10,XXREAL_0:1;
        suppose
          s=m;
          then s in {m} by TARSKI:def 1;
          hence thesis by XBOOLE_0:def 3;
        end;
        suppose
A11:      s<m;
A12:      SetPrimenumber m c= SetPrimenumber m\/{m} by XBOOLE_1:7;
          s in SetPrimenumber m by A9,A11,Def7;
          hence thesis by A12;
        end;
      end;
      SetPrimenumber m\/{m} c= SetPrimenumber k by A3,A6,Th76;
      then SetPrimenumber k=SetPrimenumber m\/{m} by A7,XBOOLE_0:def 10;
      hence n + 1 = card SetPrimenumber k by A2,A4,CARD_2:41;
      thus thesis by A6;
    end;
    SetPrimenumber 2 = {k where k is Element of NAT:k<2 & k is prime} by Lm3;
    then
A13: P1[0] by CARD_1:27,INT_2:28;
    for n holds P1[n] from NAT_1:sch 2(A13,A1);
    then consider m such that
A14: n=card SetPrimenumber m and
A15: m is Prime;
    m in NAT by ORDINAL1:def 12;
    hence thesis by A14,A15;
  end;
  uniqueness
  proof
    let f,g be prime Element of NAT;
    assume that
A16: n = card SetPrimenumber f and
A17: n = card SetPrimenumber g;
    assume
A18: f<>g;
    f<g & n+1 <= n or g<f & n+1 <= n
    proof
      per cases by A18,XXREAL_0:1;
      case
A19:    f<g;
A20:    not f in SetPrimenumber f by Def7;
        card (SetPrimenumber f\/{f}) <= card SetPrimenumber g by A19,Th76,
NAT_1:43;
        hence thesis by A16,A17,A20,CARD_2:41;
      end;
      case
A21:    g<f;
A22:    not g in SetPrimenumber g by Def7;
        card (SetPrimenumber g\/{g}) <= card SetPrimenumber f by A21,Th76,
NAT_1:43;
        hence thesis by A16,A17,A22,CARD_2:41;
      end;
    end;
    hence contradiction by NAT_1:13;
  end;
end;

theorem
  SetPrimenumber n = {k where k is Element of NAT: k<n & k is prime} by Lm3;

::$N The Infinitude of Primes
theorem Th79:
  SetPrimes is infinite
proof
  assume
A1: SetPrimes is finite;
  then reconsider SP = SetPrimes as finite set;
  consider n be Nat such that
A2: SetPrimes,Seg n are_equipotent by A1,FINSEQ_1:56;
  card SetPrimes = card Seg n by A2,CARD_1:5;
  then card SetPrimes = card n by FINSEQ_1:55;
  then
A3: card SP = n by CARD_1:def 2;
  set p=primenumber (n+1);
  set SPp = SetPrimenumber p;
A4: n+1 = card SetPrimenumber p by Def8;
  card SPp <= card SP by Th68,NAT_1:43;
  hence contradiction by A3,A4,NAT_1:13;
end;

registration
  cluster SetPrimes -> non empty infinite;
  coherence by Th79;
end;

reserve i for Nat;

:: divisibility

theorem
  i is prime implies for m,n being Nat holds i divides m * n implies
  i divides m or i divides n
proof
  defpred P[Nat] means $1 is prime & ex m,n being Nat st $1 divides m * n &
  not $1 divides m & not $1 divides n;
  assume
A1: i is prime;
  given m,n being Nat such that
A2: i divides m * n and
A3: not( (i divides m or i divides n));
A4: ex i be Nat st P[i] by A1,A2,A3;
  consider p9 being Nat such that
A5: P[p9] and
A6: for p1 being Nat st P[p1] holds p9 <= p1 from NAT_1:sch 5(A4);
  defpred Q[Nat] means ex n being Nat st p9 divides $1 * n & not p9 divides $1
  & not p9 divides n;
A7: ex i be Nat st Q[i] by A5;
  consider m be Nat such that
A8: Q[m] and
A9: for m1 being Nat st Q[m1] holds m <= m1 from NAT_1:sch 5(A7);
A10: m > 0 by A8;
  consider n being Nat such that
A11: p9 divides m * n and
A12: not p9 divides m and
A13: not p9 divides n by A8;
A14: m < p9
  proof
    set m1 = m mod p9;
    assume
A15: m >= p9;
A16: p9 > 0 by A5,INT_2:def 4;
    then m = p9* (m div p9) + m1 by NAT_D:2;
    then
A17: m * n = p9 * (m div p9) * n + m1 * n;
    m1 < p9 by A16,NAT_D:1;
    then
A18: m1 < m by A15,XXREAL_0:2;
A19: p9 divides p9 * (m div p9) by NAT_D:def 3;
    p9 divides p9 * ((m div p9) * n) by NAT_D:def 3;
    then
A20: p9 divides m1 * n by A11,A17,NAT_D:10;
    m = p9* (m div p9) + m1 by A16,NAT_D:2;
    then not p9 divides m1 by A12,A19,NAT_D:8;
    hence contradiction by A9,A13,A18,A20;
  end;
A21: m < 2
  proof
    assume m >= 2;
    then consider p1 being Element of NAT such that
A22: p1 is prime and
A23: p1 divides m by INT_2:31;
A24: p1 > 1 by A22,INT_2:def 4;
A25: not p1 divides p9
    proof
      assume p1 divides p9;
      then p1 = 1 or p1 = p9 by A5,INT_2:def 4;
      hence contradiction by A8,A22,A23,INT_2:def 4;
    end;
    p1 <= m by A10,A23,NAT_D:7;
    then
A26: not p9 <= p1 by A14,XXREAL_0:2;
A27: p1 <> 0 by A22,INT_2:def 4;
    consider k being Nat such that
A28: m * n = p9 * k by A11,NAT_D:def 3;
    p1 divides p9 * k by A23,A28,NAT_D:9;
    then p1 divides k by A6,A22,A26,A25;
    then consider k1 being Nat such that
A29: k = p1 * k1 by NAT_D:def 3;
    consider m1 being Nat such that
A30: m = p1 * m1 by A23,NAT_D:def 3;
A31: m1 > 0 by A8,A30;
A32: m1 <> m
    proof
      assume m1 = m;
      then m = 1 * m1;
      hence contradiction by A24,A30,A31,XREAL_1:68;
    end;
    m1 divides m by A30,NAT_D:def 3;
    then m1 <= m by A10,NAT_D:7;
    then
A33: m1 < m by A32,XXREAL_0:1;
    (p9 * k1) * p1 = p1 *(m1 * n) by A28,A29,A30;
    then m1 * n = p9 * k1 by A27,XCMPLX_1:5;
    then
A34: p9 divides m1 * n by NAT_D:def 3;
    not p9 divides m1 by A12,A30,NAT_D:9;
    hence contradiction by A9,A13,A33,A34;
  end;
  m >= 2
  proof
A35: m >= 0 + 1 by A10,NAT_1:13;
    assume
A36: m < 2;
    then m <= 1 + 1;
    then m = 1 by A36,A35,NAT_1:9;
    hence contradiction by A11,A13;
  end;
  hence thesis by A21;
end;

theorem
  for x being complex number holds x |^ 2 = x * x & x^2 = x |^ 2
proof
  let x be complex number;
  thus x * x = (x |^ 1) * x by Th5
    .= x |^ (1+1) by Th6
    .= x |^ 2;
  hence thesis;
end;

:: from SCMFSA9A, 2005.11.16, A.T

theorem
  m qua Integer div n = m div n & m qua Integer mod n = m mod n;

:: from HEINE, 2006.01.07, A.T

reserve x for real number;

theorem
  x > 0 implies x|^k > 0
proof
  defpred P[Nat] means for x st x > 0 holds x|^$1 > 0;
A1: for k holds P[k] implies P[k+1]
  proof
    let k such that
A2: for x st x > 0 holds x|^k > 0;
    let x;
A3: x|^(k+1) = x * x|^k by Th6;
    assume
A4: x > 0;
    then x|^k > 0 by A2;
    hence thesis by A4,A3;
  end;
A5: P[0] by RVSUM_1:94;
  for k holds P[k] from NAT_1:sch 2(A5,A1);
  hence thesis;
end;

:: missing, 2006.07.17, A.T.

theorem
  n > 0 implies 0 |^ n = 0
proof
  assume n>0;
  then n>=1+0 by NAT_1:13;
  hence thesis by Th11;
end;

:: from CARD_4 and WSIERP_1, 2007.02.07, AK

definition
  let m,n be Element of NAT;
  redefine func m|^n -> Element of NAT;
  coherence by ORDINAL1:def 12;
end;

:: from HEINE, 2007.07.27, A.T.

defpred P[Nat] means 2|^$1 >= $1 + 1;

Lm4: P[0] by RVSUM_1:94;

Lm5: for n st P[n] holds P[n+1]
proof
  let n;
  assume 2|^n >= n+1;
  then 2|^n - n >= 1 by XREAL_1:19;
  then
A1: 2*(2|^n - n) >= 2*1 by XREAL_1:64;
  2|^(n+1) - (n + 1 + 1) = 2*2|^n - (2*n - n + 2) by Th6
    .= 2*(2|^n - n) + (n - 2);
  then 2|^(n+1) - (n + 1 + 1) >= 2 + (n - 2) by A1,XREAL_1:6;
  then 2|^(n+1) >= 0 + (n + 1 + 1) by XREAL_1:19;
  hence 2|^(n+1) >= n + 1 + 1;
end;

theorem Th85:
  2|^n >= n + 1
proof
  for n holds P[n] from NAT_1:sch 2(Lm4,Lm5);
  hence thesis;
end;

theorem
  2|^n > n
proof
  2|^n >= n + 1 by Th85;
  hence thesis by NAT_1:13;
end;

:: from AMI_4, 2008.02.14, A.T.

reserve k for Element of NAT;

scheme
  Euklides9 { F(Nat) -> Element of NAT, G(Nat) -> Element of NAT,
    a() -> Element of NAT, b() -> Element of NAT } :
    ex k st F(k) = a() gcd b() & G(k) = 0
provided
A1: 0 < b() and
A2: b() < a() and
A3: F(0) = a() and
A4: G(0) = b() and
A5: for k st G(k) > 0 holds F(k+1) = G(k) & G(k+1) = F(k) mod G(k)
proof
  deffunc F(Nat,set) = IFEQ($2,0,0,G($1));
  consider q being Function of NAT,NAT such that
A6: q.0 = a() and
A7: for i being Nat holds q.(i+1) = F(i,q.i) from NAT_1:sch 12;
  deffunc Q(Element of NAT) = q.$1;
  q.(0+1) = IFEQ(q.0,0,0,G(0)) by A7
    .= G(0) by A2,A6,FUNCOP_1:def 8;
  then
A8: Q(0) = a() & Q(1 qua Element of NAT) = b() by A4,A6;
A9: for k st q.k qua Element of NAT > 0 holds q.k = F(k)
  proof
    let k such that
A10: q.k qua Element of NAT > 0;
    now
      per cases;
      case
        k = 0;
        hence thesis by A3,A6;
      end;
      case
        k <> 0;
        then consider i being Nat such that
A11:    k = i+1 by NAT_1:6;
        reconsider i as Element of NAT by ORDINAL1:def 12;
A12:    now
          assume
A13:      q.i qua Element of NAT = 0;
          q.k = IFEQ(q.i,0,0,G(i)) by A7,A11
            .= 0 by A13,FUNCOP_1:def 8;
          hence contradiction by A10;
        end;
        q.k = IFEQ(q.i,0,0,G(i)) by A7,A11
          .= G(i) by A12,FUNCOP_1:def 8;
        hence thesis by A5,A10,A11;
      end;
    end;
    hence thesis;
  end;
A14: for k holds Q(k+2) = Q(k) mod Q(k+1)
  proof
    let k;
    now
      per cases;
      case
A15:    q.(k+1) <> 0;
A16:    now
A17:      q.k = 0 or q.k <> 0;
          assume
A18:      G(k) = 0;
          q.(k+1) = IFEQ(q.k,0,0,G(k)) by A7
            .= 0 by A18,A17,FUNCOP_1:def 8;
          hence contradiction by A15;
        end;
A19:    q.(k+(1+1)) = q.((k+1)+1) .= IFEQ(q.(k+1),0,0,G(k+1)) by A7
          .= G(k+1) by A15,FUNCOP_1:def 8
          .= F(k) mod G(k) by A5,A16;
A20:    now
          assume
A21:      q.k = 0;
          q.(k+1) = IFEQ(q.k,0,0,G(k)) by A7
            .= 0 by A21,FUNCOP_1:def 8;
          hence contradiction by A15;
        end;
        q.(k+1) = IFEQ(q.k,0,0,G(k)) by A7
          .= G(k) by A20,FUNCOP_1:def 8;
        hence thesis by A9,A19,A20;
      end;
      case
A22:    q.(k+1) = 0;
        thus q.(k+2) = q.((k+1)+1) .= IFEQ(q.(k+1),0,0,G(k+1)) by A7
          .= 0 by A22,FUNCOP_1:def 8
          .= q.(k) mod q.(k+1) by A22,NAT_D:def 2;
      end;
    end;
    hence thesis;
  end;
A23: 0 < b() & b() < a() by A1,A2;
  consider k such that
A24: Q(k) = a() gcd b() & Q(k + 1) = 0 from NAT_D:sch 1(A23,A8,A14);
  take k;
  thus F(k) = a() gcd b() by A1,A9,A24,Th58;
  a() gcd b() > 0 by A1,Th58;
  hence G(k) = IFEQ(q.k,0,0,G(k)) by A24,FUNCOP_1:def 8
    .= 0 by A7,A24;
end;

:: from CARD_4, 2008.05.11, A.T.

reserve k,n,n1,n2,m1,m2 for Nat;

theorem Th87:
  r <> 0 or n = 0 iff r|^n <> 0
proof
  defpred P[Nat] means r <> 0 or $1 = 0 iff r|^$1 <> 0;
A1: P[k] implies P[k+1]
  proof
    assume
A2: P[k];
    r|^(k+1) = r|^k*r by Th6;
    hence thesis by A2;
  end;
A3: P[0] by RVSUM_1:94;
  P[k] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

Lm6: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 <= n2
proof
  assume
A1: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
  assume
A2: n1 > n2;
  then consider n being Nat such that
A3: n1 = n2+n by NAT_1:10;
  n <> 0 by A2,A3;
  then consider k being Nat such that
A4: n = k+1 by NAT_1:6;
A5: 2|^n2 <> 0 by Th87;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  2|^n1 = (2|^n2)*(2|^(k+1)) by A3,A4,Th8;
  then (2|^n1)*(2*m1+1) = 2|^n2*(2|^(k+1)*(2*m1+1));
  then 2|^(k+1)*(2*m1+1) = 2*m2+1 by A1,A5,XCMPLX_1:5;
  then 2*m2+1 = 2|^k*(2|^1)*(2*m1+1) by Th8
    .= 2*(2|^k)*(2*m1+1) by Th5
    .= 2*((2|^k)*(2*m1+1));
  then
A6: 2 divides 2*m2+1 by NAT_D:def 3;
  2 divides 2*m2 by NAT_D:def 3;
  hence contradiction by A6,NAT_D:7,10;
end;

theorem
  (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1) implies n1 = n2 & m1 = m2
proof
A1: 2|^n1 <> 0 by Th87;
  assume
A2: (2|^n1)*(2*m1+1) = (2|^n2)*(2*m2+1);
  then
A3: n2 <= n1 by Lm6;
  n1 <= n2 by A2,Lm6;
  hence n1 = n2 by A3,XXREAL_0:1;
  then 2*m1+1 = 2*m2+1 by A2,A1,XCMPLX_1:5;
  hence thesis;
end;

theorem
  k <= n implies m |^ k divides m |^ n
proof
  assume k <= n;
  then consider t being Nat such that
A1: n = k + t by NAT_1:10;
  reconsider t as Element of NAT by ORDINAL1:def 12;
  m |^ n = (m |^ k)*(m |^ t) by A1,Th8;
  hence thesis by NAT_D:def 3;
end;