:: NEWTON semantic presentation

begin


theorem Th1: :: NEWTON:1
for n being Nat st n >= 1 holds
Seg n = ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n}
proof
let n be Nat; ::_thesis: ( n >= 1 implies Seg n = ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} )
assume A1: n >= 1 ; ::_thesis: Seg n = ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n}
A2: ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} c= Seg n
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} or d in Seg n )
A3:  {  k where k is Element of NAT : ( 1 < k & k < n )  }  c= Seg n
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  k where k is Element of NAT : ( 1 < k & k < n )  }  or d in Seg n )
assume  d in  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ; ::_thesis: d in Seg n
then  ex k being Element of NAT st
( d = k & 1 < k & k < n ) ;
hence  d in Seg n ; ::_thesis: verum
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  ( not d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} or d in Seg n ) ; ::_thesis: verum
end;
 Seg n c= ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n}
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in Seg n or d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} )
assume A5: d in Seg n ; ::_thesis: d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n}
percases ( n > 1 or n = 1 ) by A1, XXREAL_0:1;
supposeA6: n > 1 ; ::_thesis: d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n}
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  d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n}
hence  d in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} by A5, FINSEQ_1:2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  Seg n = ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < n )  }  ) \/ {n} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th2: :: NEWTON:2
for a being real number
for F being FinSequence of REAL holds len (a * F) = len F
proof
let a be real number ; ::_thesis: for F being FinSequence of REAL holds len (a * F) = len F
let F be FinSequence of REAL ; ::_thesis: len (a * F) = len F
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  len (a * F) = len F ; ::_thesis: verum
end;

theorem :: NEWTON:3
for a being real number
for G being FinSequence of REAL holds dom G = dom (a * G) by VALUED_1:def_5;

registration
let x be complex number ;
let n be Nat;
clustern |-> x ->  complex-yielding ;
coherence
 n |-> x is complex-valued ;
end;

definition
let x be complex number ;
let n be Nat;
funcx |^ n ->  set  equals :: NEWTON:def 1
 Product (n |-> x);
coherence
 Product (n |-> x) is set ;
end;

:: deftheorem  defines |^ NEWTON:def_1_:_
 for x being complex number
for n being Nat holds x |^ n = Product (n |-> x);

registration
let x be real number ;
let n be Nat;
clusterx |^ n ->  real ;
coherence
 x |^ n is real ;
end;

definition
let x be Real;
let n be Nat;
:: original: |^
redefine funcx |^ n ->  Real;
coherence
 x |^ n is Real by XREAL_0:def_1;
end;

registration
let z be complex number ;
let n be Nat;
clusterz |^ n ->  complex ;
coherence
 z |^ n is complex ;
end;

theorem :: NEWTON:4
for z being complex number holds z |^ 0 = 1 by RVSUM_1:94;

theorem Th5: :: NEWTON:5
for z being complex number holds z |^ 1 = z
proof
let z be complex number ; ::_thesis: z |^ 1 = z
thus z |^ 1 = Product <*z*> by FINSEQ_2:59
.= z by RVSUM_1:95 ; ::_thesis: verum
end;

theorem Th6: :: NEWTON:6
for s being Nat
for z being complex number holds z |^ (s + 1) = (z |^ s) * z
proof
let s be Nat; ::_thesis: for z being complex number holds z |^ (s + 1) = (z |^ s) * z
let z be complex number ; ::_thesis: z |^ (s + 1) = (z |^ s) * z
thus z |^ (s + 1) = Product ((s |-> z) ^ <*z*>) by FINSEQ_2:60
.= (z |^ s) * z by RVSUM_1:96 ; ::_thesis: verum
end;

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


theorem :: NEWTON:7
for s being Nat
for x, y being complex number holds (x * y) |^ s = (x |^ s) * (y |^ s)
proof
let s be Nat; ::_thesis: for x, y being complex number holds (x * y) |^ s = (x |^ s) * (y |^ s)
let x, y be complex number ; ::_thesis: (x * y) |^ s = (x |^ s) * (y |^ s)
reconsider x = x, y = y as Element of COMPLEX by XCMPLX_0:def_2;
 (x |^ s) * (y |^ s) = Product (s |-> (x * y)) by RVSUM_1:113;
hence  (x * y) |^ s = (x |^ s) * (y |^ s) ; ::_thesis: verum
end;

theorem Th8: :: NEWTON:8
for s, t being Nat
for x being complex number holds x |^ (s + t) = (x |^ s) * (x |^ t)
proof
let s, t be Nat; ::_thesis: for x being complex number holds x |^ (s + t) = (x |^ s) * (x |^ t)
let x be complex number ; ::_thesis: x |^ (s + t) = (x |^ s) * (x |^ t)
reconsider x = x as Element of COMPLEX by XCMPLX_0:def_2;
 (x |^ s) * (x |^ t) = Product ((s + t) |-> x) by RVSUM_1:111;
hence  x |^ (s + t) = (x |^ s) * (x |^ t) ; ::_thesis: verum
end;

theorem :: NEWTON:9
for s, t being Nat
for x being complex number holds (x |^ s) |^ t = x |^ (s * t)
proof
let s, t be Nat; ::_thesis: for x being complex number holds (x |^ s) |^ t = x |^ (s * t)
let x be complex number ; ::_thesis: (x |^ s) |^ t = x |^ (s * t)
reconsider x = x as Element of COMPLEX by XCMPLX_0:def_2;
 x |^ (s * t) = Product (t |-> (x |^ s)) by RVSUM_1:112;
hence  (x |^ s) |^ t = x |^ (s * t) ; ::_thesis: verum
end;

theorem Th10: :: NEWTON:10
for s being Nat holds 1 |^ s = 1
proof
let s be Nat; ::_thesis: 1 |^ s = 1
defpred S1[ Nat] means 1 |^ $1 = 1;
A1: now__::_thesis:_for_s_being_Nat_st_S1[s]_holds_
S1[s_+_1]
let s be Nat; ::_thesis: ( S1[s] implies S1[s + 1] )
assume  S1[s] ; ::_thesis: S1[s + 1]
then  1 |^ (s + 1) = 1 * 1 by Th6;
hence  S1[s + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] by RVSUM_1:94;
 for s being Nat holds S1[s] from NAT_1:sch_2(A2, A1);
hence  1 |^ s = 1 ; ::_thesis: verum
end;

theorem Th11: :: NEWTON:11
for s being Nat st s >= 1 holds
0 |^ s = 0
proof
let s be Nat; ::_thesis: ( s >= 1 implies 0 |^ s = 0 )
defpred S1[ Nat] means 0 |^ $1 = 0 ;
A1: now__::_thesis:_for_n_being_Nat_st_n_>=_1_&_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume  ( n >= 1 & S1[n] ) ; ::_thesis: S1[n + 1]
0 |^ (n + 1) = (0 |^ n) * 0 by Th6
.= 0 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
A2: S1[1] by Th5;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A2, A1);
hence  ( s >= 1 implies 0 |^ s = 0 ) ; ::_thesis: verum
end;

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

definition
let n be Nat;
funcn !  ->  Element of REAL  equals :: NEWTON:def 2
 Product (idseq n);
coherence
 Product (idseq n) is Element of REAL by XREAL_0:def_1;
end;

:: deftheorem  defines ! NEWTON:def_2_:_
 for n being Nat holds n ! = Product (idseq n);

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

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

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

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

theorem Th15: :: NEWTON:15
for s being Nat holds (s + 1) ! = (s !) * (s + 1)
proof
let s be Nat; ::_thesis: (s + 1) ! = (s !) * (s + 1)
 idseq (s + 1) = (idseq s) ^ <*(s + 1)*> by FINSEQ_2:51;
hence  (s + 1) ! = (s !) * (s + 1) by RVSUM_1:96; ::_thesis: verum
end;

theorem Th16: :: NEWTON:16
for s being Nat holds s ! is Element of NAT
proof
let s be Nat; ::_thesis: s ! is Element of NAT
defpred S1[ Nat] means $1 ! is Element of NAT ;
A1: now__::_thesis:_for_s_being_Nat_st_S1[s]_holds_
S1[s_+_1]
let s be Nat; ::_thesis: ( S1[s] implies S1[s + 1] )
assume  S1[s] ; ::_thesis: S1[s + 1]
then reconsider k = s ! as Element of NAT ;
 (s + 1) ! = (s + 1) * k by Th15;
hence  S1[s + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] by RVSUM_1:94;
 for s being Nat holds S1[s] from NAT_1:sch_2(A2, A1);
hence  s ! is Element of NAT ; ::_thesis: verum
end;

registration
let n be Nat;
clustern !  ->  natural ;
coherence
 n ! is natural by Th16;
end;

theorem Th17: :: NEWTON:17
for s being Nat holds s ! > 0
proof
let s be Nat; ::_thesis: s ! > 0
defpred S1[ Nat] means $1 ! > 0 ;
A1: now__::_thesis:_for_s_being_Nat_st_S1[s]_holds_
S1[s_+_1]
let s be Nat; ::_thesis: ( S1[s] implies S1[s + 1] )
assume  S1[s] ; ::_thesis: S1[s + 1]
then  (s + 1) * (s !) > (s + 1) * 0 ;
hence  S1[s + 1] by Th15; ::_thesis: verum
end;
A2: S1[ 0 ] by RVSUM_1:94;
 for s being Nat holds S1[s] from NAT_1:sch_2(A2, A1);
hence  s ! > 0 ; ::_thesis: verum
end;

registration
let n be Nat;
clustern !  ->  positive ;
coherence
 n ! is positive by Th17;
end;

theorem :: NEWTON:18
for s, t being Nat holds (s !) * (t !) <> 0 ;

definition
let k, n be Nat;
funcn choose k ->  set  means :Def3: :: NEWTON:def 3
 for l being Nat st l = n - k holds
it = (n !) / ((k !) * (l !)) if n >= k
otherwise it = 0 ;
consistency
 for b1 being set holds verum ;
existence
 ( ( n >= k implies ex b1 being set st
for l being Nat st l = n - k holds
b1 = (n !) / ((k !) * (l !)) ) & ( not n >= k implies ex b1 being set st b1 = 0 ) )
proof
thus  ( n >= k implies ex r1 being set st
for l being Nat st l = n - k holds
r1 = (n !) / ((k !) * (l !)) ) ::_thesis: ( not n >= k implies ex b1 being set st b1 = 0 )
proof
assume  n >= k ; ::_thesis: ex r1 being set st
for l being Nat st l = n - k holds
r1 = (n !) / ((k !) * (l !))
then reconsider m = n - k as Element of NAT by INT_1:5;
take  (n !) / ((k !) * (m !)) ; ::_thesis: for l being Nat st l = n - k holds
(n !) / ((k !) * (m !)) = (n !) / ((k !) * (l !))
thus  for l being Nat st l = n - k holds
(n !) / ((k !) * (m !)) = (n !) / ((k !) * (l !)) ; ::_thesis: verum
end;
thus  ( not n >= k implies ex b1 being set st b1 = 0 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set holds
( ( n >= k & ( for l being Nat st l = n - k holds
b1 = (n !) / ((k !) * (l !)) ) & ( for l being Nat st l = n - k holds
b2 = (n !) / ((k !) * (l !)) ) implies b1 = b2 ) & ( not n >= k & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let r1, r2 be set ; ::_thesis: ( ( 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 ) & ( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 ) )
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 ) ::_thesis: ( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 )
proof
assume  n >= k ; ::_thesis: ( ex l being Nat st
( l = n - k & not r1 = (n !) / ((k !) * (l !)) ) or ex l being Nat st
( l = n - k & not r2 = (n !) / ((k !) * (l !)) ) or r1 = r2 )
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 !)) ; ::_thesis: r1 = r2
 r1 = (n !) / ((k !) * (m !)) by A1;
hence  r1 = r2 by A2; ::_thesis: verum
end;
thus  ( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 ) ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines choose NEWTON:def_3_:_
 for k, n being Nat
for b3 being set holds
( ( n >= k implies ( b3 = n choose k iff for l being Nat st l = n - k holds
b3 = (n !) / ((k !) * (l !)) ) ) & ( not n >= k implies ( b3 = n choose k iff b3 = 0 ) ) );

registration
let k, n be Nat;
clustern choose k ->  real ;
coherence
 n choose k is real
proof
percases ( n >= k or n < k ) ;
supposeA1: n >= k ; ::_thesis: n choose k is real
then reconsider l = n - k as Element of NAT by INT_1:5;
 n choose k = (n !) / ((k !) * (l !)) by A1, Def3;
hence  n choose k is real ; ::_thesis: verum
end;
suppose n < k ; ::_thesis: n choose k is real
hence  n choose k is real by Def3; ::_thesis: verum
end;
end;
end;
end;

definition
let k, n be Nat;
:: original: choose
redefine funcn choose k ->  Real;
coherence
 n choose k is Real by XREAL_0:def_1;
end;

theorem Th19: :: NEWTON:19
for s being Nat holds s choose 0 = 1
proof
let s be Nat; ::_thesis: s choose 0 = 1
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  s choose 0 = 1 ; ::_thesis: verum
end;

theorem Th20: :: NEWTON:20
for s, t, r being Nat st s >= t & r = s - t holds
s choose t = s choose r
proof
let s, t, r be Nat; ::_thesis: ( s >= t & r = s - t implies s choose t = s choose r )
assume A1: s >= t ; ::_thesis: ( not r = s - t or s choose t = s choose r )
 t - s >= 0 - s by XREAL_1:9;
then A2: - (- s) >= - (t - s) by XREAL_1:24;
assume A3: r = s - t ; ::_thesis: s choose t = s choose r
then  t = s - r ;
then  s choose r = (s !) / ((r !) * (t !)) by A2, Def3;
hence  s choose t = s choose r by A1, A3, Def3; ::_thesis: verum
end;

theorem Th21: :: NEWTON:21
for s being Nat holds s choose s = 1
proof
let s be Nat; ::_thesis: s choose s = 1
reconsider m = s - s as Element of NAT by INT_1:5;
 m = 0 ;
then  s choose s = s choose 0 by Th20;
hence  s choose s = 1 by Th19; ::_thesis: verum
end;

theorem Th22: :: NEWTON:22
for t, s being Nat holds (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)
proof
let t, s be Nat; ::_thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)
percases ( s < t or s = t or s > t ) by XXREAL_0:1;
supposeA1: s < t ; ::_thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)
thus  (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) ::_thesis: verum
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  (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A4, A3, Def3; ::_thesis: verum
end;
end;
supposeA5: s = t ; ::_thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)
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  (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A5, A6, Th21; ::_thesis: verum
end;
supposeA7: s > t ; ::_thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)
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  (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A9, A8, Def3; ::_thesis: verum
end;
end;
end;

theorem Th23: :: NEWTON:23
for s being Nat st s >= 1 holds
s choose 1 = s
proof
let s be Nat; ::_thesis: ( s >= 1 implies s choose 1 = s )
defpred S1[ Nat] means $1 choose 1 = $1;
A1: now__::_thesis:_for_n_being_Nat_st_n_>=_1_&_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A2: S1[n] ; ::_thesis: S1[n + 1]
(n + 1) choose 1 = (n + 1) choose (0 + 1)
.= n + (n choose 0) by A2, Th22
.= n + 1 by Th19 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
A3: S1[1] by Th21;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A3, A1);
hence  ( s >= 1 implies s choose 1 = s ) ; ::_thesis: verum
end;

theorem :: NEWTON:24
for s, t being Nat st s >= 1 & t = s - 1 holds
s choose t = s
proof
let s, t be Nat; ::_thesis: ( s >= 1 & t = s - 1 implies s choose t = s )
assume that
A1: s >= 1 and
A2: t = s - 1 ; ::_thesis: s choose t = s
 s choose t = s choose 1 by A1, A2, Th20;
hence  s choose t = s by A1, Th23; ::_thesis: verum
end;

theorem Th25: :: NEWTON:25
for s, r being Nat holds s choose r is Element of NAT
proof
let s, r be Nat; ::_thesis: s choose r is Element of NAT
defpred S1[ Nat] means  for r being Nat holds $1 choose r is Element of NAT ;
A1: for s being Nat st S1[s] holds
S1[s + 1]
proof
let s be Nat; ::_thesis: ( S1[s] implies S1[s + 1] )
assume A2: S1[s] ; ::_thesis: S1[s + 1]
A3: for r being Nat st r <> 0 holds
(s + 1) choose r is Element of NAT
proof
let r be Nat; ::_thesis: ( r <> 0 implies (s + 1) choose r is Element of NAT )
assume A4: r <> 0 ; ::_thesis: (s + 1) choose r is Element of NAT
 (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 = 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  (s + 1) choose r is Element of NAT by A5, Th22; ::_thesis: verum
end;
hence  (s + 1) choose r is Element of NAT ; ::_thesis: verum
end;
let r be Nat; ::_thesis: (s + 1) choose r is Element of NAT
 ( r = 0 or r <> 0 ) ;
hence  (s + 1) choose r is Element of NAT by A3, Th19; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
let r be Nat; ::_thesis: 0 choose r is Element of NAT
 ( r = 0 or r > 0 ) ;
hence  0 choose r is Element of NAT by Def3, Th19; ::_thesis: verum
end;
 for s being Nat holds S1[s] from NAT_1:sch_2(A6, A1);
hence  s choose r is Element of NAT ; ::_thesis: verum
end;

theorem :: NEWTON:26
for n, m being Nat
for F being FinSequence of REAL st m <> 0 & len F = m & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) holds
Sum F = (n + m) choose (n + 1)
proof
let n be Nat; ::_thesis: for m being Nat
for F being FinSequence of REAL st m <> 0 & len F = m & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) holds
Sum F = (n + m) choose (n + 1)
defpred S1[ Nat] means  for F being FinSequence of REAL st $1 <> 0 & len F = $1 & ( for i, l being Nat 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 being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; ::_thesis: S1[m + 1]
let F be FinSequence of REAL ; ::_thesis: ( m + 1 <> 0 & len F = m + 1 & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) implies Sum F = (n + (m + 1)) choose (n + 1) )
assume that
 m + 1 <> 0 and
A3: len F = m + 1 and
A4: for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ; ::_thesis: Sum F = (n + (m + 1)) choose (n + 1)
consider G being 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;
percases ( m = 0 or m <> 0 ) ;
supposeA7: m = 0 ; ::_thesis: Sum F = (n + (m + 1)) choose (n + 1)
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 ;
::_thesis: verum
end;
supposeA10: m <> 0 ; ::_thesis: Sum F = (n + (m + 1)) choose (n + 1)
A11: n + m = (n + (m + 1)) - 1 ;
A12: for i, l being Nat 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 be Nat; ::_thesis: ( i in dom G & l = (n + i) - 1 implies G . i = l choose n )
assume that
A14: i in dom G and
A15: l = (n + i) - 1 ; ::_thesis: G . i = l choose n
 G . i = F . i by A5, A14, FINSEQ_1:def_7;
hence  G . i = l choose n by A4, A14, A15, A13; ::_thesis: verum
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) ; ::_thesis: verum
end;
end;
end;
A17: S1[ 0 ] ;
thus  for m being Nat holds S1[m] from NAT_1:sch_2(A17, A1); ::_thesis: verum
end;

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

definition
let k, n be Nat;
:: original: choose
redefine funcn choose k ->  Element of NAT ;
coherence
 n choose k is Element of NAT 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: :: NEWTON:def 4
( 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
 ex b1 being FinSequence of REAL st
( len b1 = n + 1 & ( for i, l, m being Nat st i in dom b1 & m = i - 1 & l = n - m holds
b1 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
defpred S1[ Nat, set ] means  for l, m being Nat st m = $1 - 1 & l = n - m holds
$2 = ((n choose m) * (a |^ l)) * (b |^ m);
A1: for k being Nat st k in Seg (n + 1) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (n + 1) implies ex x being set st S1[k,x] )
assume A2: k in Seg (n + 1) ; ::_thesis: ex x being set st S1[k,x]
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) ; ::_thesis: S1[k,((n choose m1) * (a |^ l1)) * (b |^ m1)]
thus  S1[k,((n choose m1) * (a |^ l1)) * (b |^ m1)] ; ::_thesis: verum
end;
consider p being FinSequence such that
A3: dom p = Seg (n + 1) and
A4: for k being Nat st k in Seg (n + 1) holds
S1[k,p . k] from FINSEQ_1:sch_1(A1);
 rng p c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in REAL )
assume  x in rng p ; ::_thesis: x in REAL
then consider y being set  such that
A5: y in dom p and
A6: x = p . y by FUNCT_1:def_3;
reconsider y = 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 = x as Real by A6;
 x in REAL ;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider p = p as FinSequence of REAL by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = n + 1 & ( for i, l, m being Nat st i in dom p & m = i - 1 & l = n - m holds
p . i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
thus  ( len p = n + 1 & ( for i, l, m being Nat st i in dom p & m = i - 1 & l = n - m holds
p . i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) by A3, A4, FINSEQ_1:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = n + 1 & ( for i, l, m being Nat st i in dom b1 & m = i - 1 & l = n - m holds
b1 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b2 = n + 1 & ( for i, l, m being Nat st i in dom b2 & m = i - 1 & l = n - m holds
b2 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
proof
let G, H be FinSequence of REAL ; ::_thesis: ( len G = n + 1 & ( for i, l, m being Nat st i in dom G & m = i - 1 & l = n - m holds
G . i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len H = n + 1 & ( for i, l, m being Nat st i in dom H & m = i - 1 & l = n - m holds
H . i = ((n choose m) * (a |^ l)) * (b |^ m) ) implies G = H )
assume that
A7: len G = n + 1 and
A8: for i, l, m being Nat st i in dom G & m = i - 1 & l = n - m holds
G . i = ((n choose m) * (a |^ l)) * (b |^ m) ; ::_thesis: ( not len H = n + 1 or ex i, l, m being Nat st
( i in dom H & m = i - 1 & l = n - m & not H . i = ((n choose m) * (a |^ l)) * (b |^ m) ) or G = H )
assume that
A9: len H = n + 1 and
A10: for i, l, m being Nat st i in dom H & m = i - 1 & l = n - m holds
H . i = ((n choose m) * (a |^ l)) * (b |^ m) ; ::_thesis: G = H
 for i being Nat st i in dom G holds
G . i = H . i
proof
let i be Nat; ::_thesis: ( i in dom G implies G . i = H . i )
assume A11: i in dom G ; ::_thesis: G . i = H . i
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  G . i = H . i by A8, A11; ::_thesis: verum
end;
hence  G = H by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines In_Power NEWTON:def_4_:_
 for a, b being real number
for n being Nat
for b4 being FinSequence of REAL holds
( b4 = (a,b) In_Power n iff ( len b4 = n + 1 & ( for i, l, m being Nat st i in dom b4 & m = i - 1 & l = n - m holds
b4 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

theorem Th27: :: NEWTON:27
for a, b being real number holds (a,b) In_Power 0 = <*1*>
proof
let a, b be real number ; ::_thesis: (a,b) In_Power 0 = <*1*>
set F = (a,b) In_Power 0;
A1: len ((a,b) In_Power 0) = 0 + 1 by Def4
.= 1 ;
then A2: dom ((a,b) In_Power 0) = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then  1 in dom ((a,b) In_Power 0) by TARSKI:def_1;
then consider i being set  such that
A3: i in dom ((a,b) In_Power 0) ;
reconsider i = 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 ((a,b) In_Power 0) . 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  (a,b) In_Power 0 = <*1*> by A1, FINSEQ_1:40; ::_thesis: verum
end;

theorem Th28: :: NEWTON:28
for s being Nat
for a, b being real number holds ((a,b) In_Power s) . 1 = a |^ s
proof
let s be Nat; ::_thesis: for a, b being real number holds ((a,b) In_Power s) . 1 = a |^ s
let a, b be real number ; ::_thesis: ((a,b) In_Power s) . 1 = a |^ s
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  ((a,b) In_Power s) . 1 = a |^ s ; ::_thesis: verum
end;

theorem Th29: :: NEWTON:29
for s being Nat
for a, b being real number holds ((a,b) In_Power s) . (s + 1) = b |^ s
proof
let s be Nat; ::_thesis: for a, b being real number holds ((a,b) In_Power s) . (s + 1) = b |^ s
let a, b be real number ; ::_thesis: ((a,b) In_Power s) . (s + 1) = b |^ s
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  ((a,b) In_Power s) . (s + 1) = b |^ s ; ::_thesis: verum
end;

theorem Th30: :: NEWTON:30
for s being Nat
for a, b being real number holds (a + b) |^ s = Sum ((a,b) In_Power s)
proof
let s be Nat; ::_thesis: for a, b being real number holds (a + b) |^ s = Sum ((a,b) In_Power s)
let a, b be real number ; ::_thesis: (a + b) |^ s = Sum ((a,b) In_Power s)
defpred S1[ Nat] means (a + b) |^ $1 = Sum ((a,b) In_Power $1);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
reconsider a = a, b = b as Real by XREAL_0:def_1;
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider G1 = (a * ((a,b) In_Power n)) ^ <*0*> as FinSequence of REAL ;
set G2 = <*0*> ^ (b * ((a,b) In_Power n));
assume  S1[n] ; ::_thesis: S1[n + 1]
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 (<*0*> ^ (b * ((a,b) In_Power n))) = (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 = <*0*> ^ (b * ((a,b) In_Power n)) 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 + (<*0*> ^ (b * ((a,b) In_Power n)))) = (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 (F1 + F2) = (n + 1) + 1 by CARD_1:def_7;
A7: len F1 = (n + 1) + 1 by CARD_1:def_7;
A8: for i being Nat st i in dom ((a,b) In_Power (n + 1)) holds
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
proof
let i be Nat; ::_thesis: ( i in dom ((a,b) In_Power (n + 1)) implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
assume A9: i in dom ((a,b) In_Power (n + 1)) ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
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 (F1 + F2) . 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} ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then A17: i = 1 by TARSKI:def_1;
then A18: ((a,b) In_Power n) /. i = ((a,b) In_Power n) . 1 by A15, PARTFUN1:def_6;
 ((a,b) In_Power n) /. i = ((a,b) In_Power n) . i by A17, A15, PARTFUN1:def_6;
then A19: ((a,b) In_Power n) /. i = a |^ n by A17, Th28;
A20: F1 /. i = ((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: F2 /. i = F2 . i by A13, PARTFUN1:def_6;
A22: F1 /. i = F1 . i by A12, PARTFUN1:def_6;
F2 /. i = (<*0*> ^ (b * ((a,b) In_Power n))) . 1 by A13, A17, PARTFUN1:def_6
.= 0 by FINSEQ_1:41 ;
then (F1 + F2) . i = (F1 /. i) + 0 by A22, A21, RVSUM_1:11
.= ((a,b) In_Power (n + 1)) . i by A17, A20, Th28 ;
hence  (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i ; ::_thesis: verum
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 (F1 + F2) by A6, A11, FINSEQ_1:def_3;
A25: ( i in  {  k where k is Element of NAT : ( k > 1 & k < (n + 1) + 1 )  }  implies (F1 + F2) . 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 )  }  ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
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: F1 /. i = ((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: ((a,b) In_Power n) /. j = ((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: ((a,b) In_Power n) /. i = ((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: F1 /. i = (a * ((a,b) In_Power n)) . i by A27, FINSEQ_1:def_7
.= a * (((a,b) In_Power n) /. i) 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: F2 /. i = (<*0*> ^ (b * ((a,b) In_Power n))) . i by A13, PARTFUN1:def_6;
then F2 /. i = (<*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 * (((a,b) In_Power n) /. j) by A30, RVSUM_1:44 ;
then (F1 + F2) . i = (a * (((a,b) In_Power n) /. i)) + (b * (((a,b) In_Power n) /. j)) by A24, A27, A37, A34, VALUED_1:def_1
.= (a * (((a |^ l1) * (n choose m1)) * (b |^ m1))) + (b * (((a,b) In_Power n) /. j)) by A32, A33, Def4
.= ((a * (a |^ l1)) * ((n choose m1) * (b |^ m1))) + (b * (((a,b) In_Power n) /. j))
.= ((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (b * (((a,b) In_Power n) /. j)) 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  (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i ; ::_thesis: verum
end;
A38: ( i in {((n + 1) + 1)} implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
proof
assume A39: i in {((n + 1) + 1)} ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
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: ((a,b) In_Power n) /. j = ((a,b) In_Power n) . (n + 1) by A41, PARTFUN1:def_6
.= b |^ n by Th29 ;
A44: ((a,b) In_Power n) /. j = ((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: F2 /. i = (<*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: F2 /. i = 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: F1 /. i = ((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 ;
 F1 /. i = F1 . i by A12, PARTFUN1:def_6;
then (F1 + F2) . i = 0 + (F2 /. i) by A48, A47, RVSUM_1:11
.= ((a,b) In_Power (n + 1)) . i by A40, A46, Th29 ;
hence  (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i ; ::_thesis: verum
end;
A49: now__::_thesis:_(_i_in_({1}_\/__{__k_where_k_is_Element_of_NAT_:_(_1_<_k_&_k_<_(n_+_1)_+_1_)__}__)_\/_{((n_+_1)_+_1)}_implies_(F1_+_F2)_._i_=_((a,b)_In_Power_(n_+_1))_._i_)
assume  i in ({1} \/  {  k where k is Element of NAT : ( 1 < k & k < (n + 1) + 1 )  }  ) \/ {((n + 1) + 1)} ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
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  (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i by A14, A25, A38, XBOOLE_0:def_3; ::_thesis: verum
end;
 dom ((a,b) In_Power (n + 1)) = Seg ((n + 1) + 1) by A10, FINSEQ_1:def_3;
hence  (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i by A9, A49, Th1, NAT_1:12; ::_thesis: verum
end;
 len ((a,b) In_Power (n + 1)) = len (F1 + F2) by A6, Def4;
hence  S1[n + 1] by A2, A4, A8, FINSEQ_2:9; ::_thesis: verum
end;
(a + b) |^ 0 = Sum <*1*> by FINSOP_1:11, RVSUM_1:94
.= Sum ((a,b) In_Power 0) by Th27 ;
then A50: S1[ 0 ] ;
 for n being Nat holds S1[n] from NAT_1:sch_2(A50, A1);
hence  (a + b) |^ s = Sum ((a,b) In_Power s) ; ::_thesis: verum
end;

definition
let n be Nat;
func Newton_Coeff n ->  FinSequence of REAL  means :Def5: :: NEWTON:def 5
( len it = n + 1 & ( for i, k being Nat st i in dom it & k = i - 1 holds
it . i = n choose k ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = n + 1 & ( for i, k being Nat st i in dom b1 & k = i - 1 holds
b1 . i = n choose k ) )
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
defpred S1[ Nat, set ] means  for s being Nat st s = $1 - 1 holds
$2 = n choose s;
A1: for l being Nat st l in Seg (n + 1) holds
ex x being set st S1[l,x]
proof
let l be Nat; ::_thesis: ( l in Seg (n + 1) implies ex x being set st S1[l,x] )
assume  l in Seg (n + 1) ; ::_thesis: ex x being set st S1[l,x]
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  n choose k ; ::_thesis: S1[l,n choose k]
thus  S1[l,n choose k] ; ::_thesis: verum
end;
consider F being FinSequence such that
A2: ( dom F = Seg (n + 1) & ( for l being Nat st l in Seg (n + 1) holds
S1[l,F . l] ) ) from FINSEQ_1:sch_1(A1);
 rng F c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in REAL )
assume  x in rng F ; ::_thesis: x in REAL
then consider y being set  such that
A3: y in dom F and
A4: x = F . y by FUNCT_1:def_3;
reconsider y = 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 = x as Real by A4;
 x in REAL ;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider F = F as FinSequence of REAL by FINSEQ_1:def_4;
take  F ; ::_thesis: ( len F = n + 1 & ( for i, k being Nat st i in dom F & k = i - 1 holds
F . i = n choose k ) )
thus  ( len F = n + 1 & ( for i, k being Nat st i in dom F & k = i - 1 holds
F . i = n choose k ) ) by A2, FINSEQ_1:def_3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = n + 1 & ( for i, k being Nat st i in dom b1 & k = i - 1 holds
b1 . i = n choose k ) & len b2 = n + 1 & ( for i, k being Nat st i in dom b2 & k = i - 1 holds
b2 . i = n choose k ) holds
b1 = b2
proof
let G, H be FinSequence of REAL ; ::_thesis: ( len G = n + 1 & ( for i, k being Nat st i in dom G & k = i - 1 holds
G . i = n choose k ) & len H = n + 1 & ( for i, k being Nat st i in dom H & k = i - 1 holds
H . i = n choose k ) implies G = H )
assume that
A5: len G = n + 1 and
A6: for i, m being Nat st i in dom G & m = i - 1 holds
G . i = n choose m ; ::_thesis: ( not len H = n + 1 or ex i, k being Nat st
( i in dom H & k = i - 1 & not H . i = n choose k ) or G = H )
assume that
A7: len H = n + 1 and
A8: for i, m being Nat st i in dom H & m = i - 1 holds
H . i = n choose m ; ::_thesis: G = H
 for i being Nat st i in dom G holds
G . i = H . i
proof
let i be Nat; ::_thesis: ( i in dom G implies G . i = H . i )
assume A9: i in dom G ; ::_thesis: G . i = H . i
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  G . i = H . i by A6, A9; ::_thesis: verum
end;
hence  G = H by A5, A7, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Newton_Coeff NEWTON:def_5_:_
 for n being Nat
for b2 being FinSequence of REAL holds
( b2 = Newton_Coeff n iff ( len b2 = n + 1 & ( for i, k being Nat st i in dom b2 & k = i - 1 holds
b2 . i = n choose k ) ) );

theorem Th31: :: NEWTON:31
for s being Nat holds Newton_Coeff s = (1,1) In_Power s
proof
let s be Nat; ::_thesis: Newton_Coeff s = (1,1) In_Power s
A1: for i being Nat st i in dom (Newton_Coeff s) holds
(Newton_Coeff s) . i = ((1,1) In_Power s) . i
proof
let i be Nat; ::_thesis: ( i in dom (Newton_Coeff s) implies (Newton_Coeff s) . i = ((1,1) In_Power s) . i )
assume A2: i in dom (Newton_Coeff s) ; ::_thesis: (Newton_Coeff s) . i = ((1,1) In_Power s) . i
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  (Newton_Coeff s) . i = ((1,1) In_Power s) . i ; ::_thesis: verum
end;
len (Newton_Coeff s) = s + 1 by Def5
.= len ((1,1) In_Power s) by Def4 ;
hence  Newton_Coeff s = (1,1) In_Power s by A1, FINSEQ_2:9; ::_thesis: verum
end;

theorem :: NEWTON:32
for s being Nat holds 2 |^ s = Sum (Newton_Coeff s)
proof
let s be Nat; ::_thesis: 2 |^ s = Sum (Newton_Coeff s)
2 |^ s = (1 + 1) |^ s
.= Sum ((1,1) In_Power s) by Th30
.= Sum (Newton_Coeff s) by Th31 ;
hence  2 |^ s = Sum (Newton_Coeff s) ; ::_thesis: verum
end;

begin

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

theorem Th34: :: NEWTON:34
for l, n, k being Nat st l >= 1 & n >= k * l holds
n >= k
proof
let l, n, k be Nat; ::_thesis: ( l >= 1 & n >= k * l implies n >= k )
assume that
A1: l >= 1 and
A2: n >= k * l ; ::_thesis: n >= k
 k * l >= k by A1, Th33;
hence  n >= k by A2, XXREAL_0:2; ::_thesis: verum
end;

definition
let n be Nat;
:: original: !
redefine funcn !  ->  Element of NAT ;
coherence
 n ! is Element of NAT by Th16;
end;

theorem Th35: :: NEWTON:35
for l being Nat st l <> 0 holds
l divides l !
proof
let l be Nat; ::_thesis: ( l <> 0 implies l divides l ! )
assume  l <> 0 ; ::_thesis: l divides l !
then consider n being Nat such that
A1: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 (n + 1) ! = (n + 1) * (n !) by Th15;
hence  l divides l ! by A1, NAT_D:def_3; ::_thesis: verum
end;

theorem :: NEWTON:36
for n being Nat st n <> 0 holds
(n + 1) / n > 1
proof
let n be Nat; ::_thesis: ( n <> 0 implies (n + 1) / n > 1 )
assume A1: n <> 0 ; ::_thesis: (n + 1) / n > 1
(n + 1) / n = (n / n) + (1 / n) by XCMPLX_1:62
.= 1 + (1 / n) by A1, XCMPLX_1:60 ;
hence  (n + 1) / n > 1 by A1, XREAL_1:29; ::_thesis: verum
end;

theorem Th37: :: NEWTON:37
for k being Nat holds k / (k + 1) < 1
proof
let k be Nat; ::_thesis: k / (k + 1) < 1
 for m being Nat holds m < m + 1 by XREAL_1:29;
hence  k / (k + 1) < 1 by XREAL_1:189; ::_thesis: verum
end;

theorem Th38: :: NEWTON:38
for l being Nat holds l ! >= l
proof
let l be Nat; ::_thesis: l ! >= l
defpred S1[ Nat] means $1 ! >= $1;
A1: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be Nat; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A2: l ! >= l ; ::_thesis: S1[l + 1]
A3: (l !) * (l + 1) = (l + 1) ! by Th15;
 ( ( l = 0 & (l + 1) ! >= l + 1 ) or ( l >= 1 & (l + 1) ! >= l + 1 ) )
proof
percases ( l = 0 or l >= 1 ) by NAT_1:14;
case l = 0 ; ::_thesis: (l + 1) ! >= l + 1
hence  (l + 1) ! >= l + 1 by FINSEQ_2:50, RVSUM_1:95; ::_thesis: verum
end;
caseA4: l >= 1 ; ::_thesis: (l + 1) ! >= l + 1
 (l + 1) ! >= (l + 1) * l by A2, A3, XREAL_1:64;
hence  (l + 1) ! >= l + 1 by A4, Th34; ::_thesis: verum
end;
end;
end;
hence  S1[l + 1] ; ::_thesis: verum
end;
A5: S1[ 0 ] ;
 for l being Nat holds S1[l] from NAT_1:sch_2(A5, A1);
hence  l ! >= l ; ::_thesis: verum
end;

theorem Th39: :: NEWTON:39
for m, n being Nat st m <> 1 & m divides n holds
not m divides n + 1
proof
let m, n be Nat; ::_thesis: ( m <> 1 & m divides n implies not m divides n + 1 )
assume that
A1: m <> 1 and
A2: m divides n and
A3: m divides n + 1 ; ::_thesis: contradiction
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 ; ::_thesis: contradiction
 s > 0 by A5;
hence  contradiction by A7, A6, Th37, XREAL_1:157; ::_thesis: verum
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; ::_thesis: verum
end;

theorem Th40: :: NEWTON:40
for j, k being Nat st j <> 0 holds
j divides (j + k) !
proof
let j, k be Nat; ::_thesis: ( j <> 0 implies j divides (j + k) ! )
defpred S1[ Nat] means  for j being Nat st j <> 0 holds
j divides (j + $1) ! ;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for j being Nat st j <> 0 holds
j divides (j + k) ! ; ::_thesis: S1[k + 1]
let j be Nat; ::_thesis: ( j <> 0 implies j divides (j + (k + 1)) ! )
assume  j <> 0 ; ::_thesis: j divides (j + (k + 1)) !
then  j divides ((j + k) !) * ((j + k) + 1) by A2, NAT_D:9;
hence  j divides (j + (k + 1)) ! by Th15; ::_thesis: verum
end;
A3: S1[ 0 ] by Th35;
 for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence  ( j <> 0 implies j divides (j + k) ! ) ; ::_thesis: verum
end;

theorem Th41: :: NEWTON:41
for j, l being Nat st j <= l & j <> 0 holds
j divides l !
proof
let j, l be Nat; ::_thesis: ( j <= l & j <> 0 implies j divides l ! )
assume that
A1: j <= l and
A2: j <> 0 ; ::_thesis: j divides l !
 ex k being Nat st l = j + k by A1, NAT_1:10;
hence  j divides l ! by A2, Th40; ::_thesis: verum
end;

theorem :: NEWTON:42
for j, l being Nat st j <> 1 & j <> 0 & j divides (l !) + 1 holds
j > l by Th39, Th41;

theorem :: NEWTON:43
for m, n, k being Nat holds m lcm (n lcm k) = (m lcm n) lcm k
proof
let m, n, k be Nat; ::_thesis: m lcm (n lcm k) = (m lcm n) lcm k
set M = n lcm k;
set K = m lcm (n lcm k);
set N = m lcm n;
set L = (m lcm n) lcm k;
A1: m divides m lcm (n lcm k) by NAT_D:def_4;
A2: n lcm k divides m lcm (n lcm k) by NAT_D:def_4;
 n divides n lcm k by NAT_D:def_4;
then  n divides m lcm (n lcm k) by A2, NAT_D:4;
then A3: m lcm n divides m lcm (n lcm k) by A1, NAT_D:def_4;
 k divides n lcm k by NAT_D:def_4;
then  k divides m lcm (n lcm k) by A2, NAT_D:4;
then A4: (m lcm n) lcm k divides m lcm (n lcm k) by A3, NAT_D:def_4;
A5: m lcm n divides (m lcm n) lcm k by NAT_D:def_4;
A6: k divides (m lcm n) lcm k by NAT_D:def_4;
 n divides m lcm n by NAT_D:def_4;
then  n divides (m lcm n) lcm k by A5, NAT_D:4;
then A7: n lcm k divides (m lcm n) lcm k by A6, NAT_D:def_4;
 m divides m lcm n by NAT_D:def_4;
then  m divides (m lcm n) lcm k by A5, NAT_D:4;
then  m lcm (n lcm k) divides (m lcm n) lcm k by A7, NAT_D:def_4;
hence  m lcm (n lcm k) = (m lcm n) lcm k by A4, NAT_D:5; ::_thesis: verum
end;

theorem Th44: :: NEWTON:44
for m, n being Nat holds
( m divides n iff m lcm n = n )
proof
let m, n be Nat; ::_thesis: ( m divides n iff m lcm n = n )
thus  ( m divides n implies m lcm n = n ) ::_thesis: ( m lcm n = n implies m divides n )
proof
set M = m lcm n;
assume  m divides n ; ::_thesis: m lcm n = n
then A1: m lcm n divides n by NAT_D:def_4;
 n divides m lcm n by NAT_D:def_4;
hence  m lcm n = n by A1, NAT_D:5; ::_thesis: verum
end;
thus  ( m lcm n = n implies m divides n ) by NAT_D:def_4; ::_thesis: verum
end;

theorem :: NEWTON:45
for n, m, k being Nat holds
( ( n divides m & k divides m ) iff n lcm k divides m )
proof
let n, m, k be Nat; ::_thesis: ( ( n divides m & k divides m ) iff n lcm k divides m )
 ( n lcm k divides m implies ( n divides m & k divides m ) )
proof
set M = n lcm k;
A1: n divides n lcm k by NAT_D:def_4;
A2: k divides n lcm k by NAT_D:def_4;
assume  n lcm k divides m ; ::_thesis: ( n divides m & k divides m )
hence  ( n divides m & k divides m ) by A1, A2, NAT_D:4; ::_thesis: verum
end;
hence  ( ( n divides m & k divides m ) iff n lcm k divides m ) by NAT_D:def_4; ::_thesis: verum
end;

theorem :: NEWTON:46
for m being Nat holds m lcm 1 = m
proof
let m be Nat; ::_thesis: m lcm 1 = m
set M = m lcm 1;
 1 divides m by NAT_D:6;
then A1: m lcm 1 divides m by NAT_D:def_4;
 m divides m lcm 1 by NAT_D:def_4;
hence  m lcm 1 = m by A1, NAT_D:5; ::_thesis: verum
end;

theorem Th47: :: NEWTON:47
for m, n being Nat holds m lcm n divides m * n
proof
let m, n be Nat; ::_thesis: m lcm n divides m * n
set s = m * n;
A1: n divides m * n by NAT_D:9;
 m divides m * n by NAT_D:9;
hence  m lcm n divides m * n by A1, NAT_D:def_4; ::_thesis: verum
end;

theorem :: NEWTON:48
for m, n, k being Nat holds m gcd (n gcd k) = (m gcd n) gcd k
proof
let m, n, k be Nat; ::_thesis: m gcd (n gcd k) = (m gcd n) gcd k
set M = n gcd k;
set K = m gcd (n gcd k);
set N = m gcd n;
set L = (m gcd n) gcd k;
A1: m gcd (n gcd k) divides n gcd k by NAT_D:def_5;
A2: m gcd (n gcd k) divides m by NAT_D:def_5;
 n gcd k divides n by NAT_D:def_5;
then  m gcd (n gcd k) divides n by A1, NAT_D:4;
then A3: m gcd (n gcd k) divides m gcd n by A2, NAT_D:def_5;
A4: (m gcd n) gcd k divides m gcd n by NAT_D:def_5;
A5: (m gcd n) gcd k divides k by NAT_D:def_5;
 m gcd n divides n by NAT_D:def_5;
then  (m gcd n) gcd k divides n by A4, NAT_D:4;
then A6: (m gcd n) gcd k divides n gcd k by A5, NAT_D:def_5;
 m gcd n divides m by NAT_D:def_5;
then  (m gcd n) gcd k divides m by A4, NAT_D:4;
then A7: (m gcd n) gcd k divides m gcd (n gcd k) by A6, NAT_D:def_5;
 n gcd k divides k by NAT_D:def_5;
then  m gcd (n gcd k) divides k by A1, NAT_D:4;
then  m gcd (n gcd k) divides (m gcd n) gcd k by A3, NAT_D:def_5;
hence  m gcd (n gcd k) = (m gcd n) gcd k by A7, NAT_D:5; ::_thesis: verum
end;

theorem Th49: :: NEWTON:49
for n, m being Nat st n divides m holds
n gcd m = n
proof
let n, m be Nat; ::_thesis: ( n divides m implies n gcd m = n )
set N = n gcd m;
assume  n divides m ; ::_thesis: n gcd m = n
then A1: n divides n gcd m by NAT_D:def_5;
 n gcd m divides n by NAT_D:def_5;
hence  n gcd m = n by A1, NAT_D:5; ::_thesis: verum
end;

theorem :: NEWTON:50
for m, n, k being Nat holds
( ( m divides n & m divides k ) iff m divides n gcd k )
proof
let m, n, k be Nat; ::_thesis: ( ( m divides n & m divides k ) iff m divides n gcd k )
 ( m divides n gcd k implies ( m divides n & m divides k ) )
proof
set M = n gcd k;
A1: n gcd k divides n by NAT_D:def_5;
A2: n gcd k divides k by NAT_D:def_5;
assume  m divides n gcd k ; ::_thesis: ( m divides n & m divides k )
hence  ( m divides n & m divides k ) by A1, A2, NAT_D:4; ::_thesis: verum
end;
hence  ( ( m divides n & m divides k ) iff m divides n gcd k ) by NAT_D:def_5; ::_thesis: verum
end;

theorem :: NEWTON:51
for m being Nat holds m gcd 1 = 1
proof
let m be Nat; ::_thesis: m gcd 1 = 1
set M = m gcd 1;
A1: 1 divides m gcd 1 by NAT_D:6;
 m gcd 1 divides 1 by NAT_D:def_5;
hence  m gcd 1 = 1 by A1, NAT_D:5; ::_thesis: verum
end;

theorem :: NEWTON:52
for m being Nat holds m gcd 0 = m
proof
let m be Nat; ::_thesis: m gcd 0 = m
set M = m gcd 0;
 m divides 0 by NAT_D:6;
then A1: m divides m gcd 0 by NAT_D:def_5;
 m gcd 0 divides m by NAT_D:def_5;
hence  m gcd 0 = m by A1, NAT_D:5; ::_thesis: verum
end;

theorem Th53: :: NEWTON:53
for m, n being Nat holds (m gcd n) lcm n = n
proof
let m, n be Nat; ::_thesis: (m gcd n) lcm n = n
set M = m gcd n;
 m gcd n divides n by NAT_D:def_5;
hence  (m gcd n) lcm n = n by Th44; ::_thesis: verum
end;

theorem Th54: :: NEWTON:54
for m, n being Nat holds m gcd (m lcm n) = m
proof
let m, n be Nat; ::_thesis: m gcd (m lcm n) = m
set M = m lcm n;
 m divides m lcm n by NAT_D:def_4;
hence  m gcd (m lcm n) = m by Th49; ::_thesis: verum
end;

theorem :: NEWTON:55
for m, n being Nat holds m gcd (m lcm n) = (n gcd m) lcm m
proof
let m, n be Nat; ::_thesis: m gcd (m lcm n) = (n gcd m) lcm m
 m gcd (m lcm n) = m by Th54;
hence  m gcd (m lcm n) = (n gcd m) lcm m by Th53; ::_thesis: verum
end;

theorem :: NEWTON:56
for m, n, k being Nat st m divides n holds
m gcd k divides n gcd k
proof
let m, n, k be Nat; ::_thesis: ( m divides n implies m gcd k divides n gcd k )
set M = m gcd k;
A1: m gcd k divides k by NAT_D:def_5;
assume A2: m divides n ; ::_thesis: m gcd k divides n gcd k
 m gcd k divides m by NAT_D:def_5;
then  m gcd k divides n by A2, NAT_D:4;
hence  m gcd k divides n gcd k by A1, NAT_D:def_5; ::_thesis: verum
end;

theorem :: NEWTON:57
for m, n, k being Nat st m divides n holds
k gcd m divides k gcd n
proof
let m, n, k be Nat; ::_thesis: ( m divides n implies k gcd m divides k gcd n )
set M = k gcd m;
A1: k gcd m divides k by NAT_D:def_5;
assume A2: m divides n ; ::_thesis: k gcd m divides k gcd n
 k gcd m divides m by NAT_D:def_5;
then  k gcd m divides n by A2, NAT_D:4;
hence  k gcd m divides k gcd n by A1, NAT_D:def_5; ::_thesis: verum
end;

theorem Th58: :: NEWTON:58
for n, m being Nat st n > 0 holds
n gcd m > 0
proof
let n, m be Nat; ::_thesis: ( n > 0 implies n gcd m > 0 )
assume that
A1: n > 0 and
A2: n gcd m <= 0 ; ::_thesis: contradiction
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; ::_thesis: verum
end;

theorem :: NEWTON:59
for m, n being Nat st m > 0 & n > 0 holds
m lcm n > 0
proof
let m, n be Nat; ::_thesis: ( m > 0 & n > 0 implies m lcm n > 0 )
assume that
A1: m > 0 and
A2: n > 0 and
A3: m lcm n <= 0 ; ::_thesis: contradiction
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; ::_thesis: verum
end;

theorem :: NEWTON:60
for n, m, k being Nat holds (n gcd m) lcm (n gcd k) divides n gcd (m lcm k)
proof
let n, m, k be Nat; ::_thesis: (n gcd m) lcm (n gcd k) divides n gcd (m lcm k)
set M = m lcm k;
set N = n gcd k;
set P = n gcd m;
set L = (n gcd m) lcm (n gcd k);
A1: n gcd k divides k by NAT_D:def_5;
 k divides m lcm k by NAT_D:def_4;
then A2: n gcd k divides m lcm k by A1, NAT_D:4;
A3: n gcd m divides m by NAT_D:def_5;
 m divides m lcm k by NAT_D:def_4;
then  n gcd m divides m lcm k by A3, NAT_D:4;
then A4: (n gcd m) lcm (n gcd k) divides m lcm k by A2, NAT_D:def_4;
A5: n gcd m divides n by NAT_D:def_5;
 n gcd k divides n by NAT_D:def_5;
then  (n gcd m) lcm (n gcd k) divides n by A5, NAT_D:def_4;
hence  (n gcd m) lcm (n gcd k) divides n gcd (m lcm k) by A4, NAT_D:def_5; ::_thesis: verum
end;

theorem :: NEWTON:61
for m, l, n being Nat st m divides l holds
m lcm (n gcd l) divides (m lcm n) gcd l
proof
let m, l, n be Nat; ::_thesis: ( m divides l implies m lcm (n gcd l) divides (m lcm n) gcd l )
set M = m lcm n;
set K = (m lcm n) gcd l;
set N = n gcd l;
A1: m divides m lcm n by NAT_D:def_4;
A2: n gcd l divides n by NAT_D:def_5;
A3: n gcd l divides l by NAT_D:def_5;
 n divides m lcm n by NAT_D:def_4;
then  n gcd l divides m lcm n by A2, NAT_D:4;
then A4: n gcd l divides (m lcm n) gcd l by A3, NAT_D:def_5;
assume  m divides l ; ::_thesis: m lcm (n gcd l) divides (m lcm n) gcd l
then  m divides (m lcm n) gcd l by A1, NAT_D:def_5;
hence  m lcm (n gcd l) divides (m lcm n) gcd l by A4, NAT_D:def_4; ::_thesis: verum
end;

theorem :: NEWTON:62
for n, m being Nat holds n gcd m divides n lcm m
proof
let n, m be Nat; ::_thesis: n gcd m divides n lcm m
A1: n divides n lcm m by NAT_D:def_4;
 n gcd m divides n by NAT_D:def_5;
hence  n gcd m divides n lcm m by A1, NAT_D:4; ::_thesis: verum
end;


theorem :: NEWTON:63
for m, n being Nat st 0 < m holds
n mod m = n - (m * (n div m))
proof
let m, n be Nat; ::_thesis: ( 0 < m implies n mod m = n - (m * (n div m)) )
reconsider z1 = m * (n div m), z2 = n mod m as Integer ;
assume  m > 0 ; ::_thesis: n mod m = n - (m * (n div m))
then  n - z1 = (z1 + z2) - z1 by NAT_D:2;
hence  n mod m = n - (m * (n div m)) ; ::_thesis: verum
end;

theorem :: NEWTON:64
for i2, i1 being Integer st i2 >= 0 holds
i1 mod i2 >= 0 by INT_1:57;

theorem :: NEWTON:65
for i2, i1 being Integer st i2 > 0 holds
i1 mod i2 < i2 by INT_1:58;

theorem :: NEWTON:66
for i2, i1 being Integer st i2 <> 0 holds
i1 = ((i1 div i2) * i2) + (i1 mod i2) by INT_1:59;

theorem :: NEWTON:67
for m, n being Nat st ( m > 0 or n > 0 ) holds
ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n
proof
let m, n be Nat; ::_thesis: ( ( m > 0 or n > 0 ) implies ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n )
defpred S1[ Nat] means ( $1 > 0 & ex i, i1 being Integer st (i * m) + (i1 * n) = $1 );
assume A1: ( m > 0 or n > 0 ) ; ::_thesis: ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n
A2: ex p being Nat st S1[p]
proof
percases ( m > 0 or n > 0 ) by A1;
supposeA3: m > 0 ; ::_thesis: ex p being Nat st S1[p]
 (1 * m) + (0 * n) = m ;
hence  ex p being Nat st S1[p] by A3; ::_thesis: verum
end;
supposeA4: n > 0 ; ::_thesis: ex p being Nat st S1[p]
 (0 * m) + (1 * n) = n ;
hence  ex p being Nat st S1[p] by A4; ::_thesis: verum
end;
end;
end;
 ex p being Nat st
( S1[p] & ( for n being Nat st S1[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 being Integer st (i * m) + (i0 * n) = p and
A7: for k being Nat st k > 0 & ex i1, i2 being Integer st (i1 * m) + (i2 * n) = k holds
p <= k ;
consider i, i0 being Integer such that
A8: (i * m) + (i0 * n) = p by A6;
A9: for k being Nat st ex i1, i2 being Integer st (i1 * m) + (i2 * n) = k holds
p divides k
proof
let k be Nat; ::_thesis: ( ex i1, i2 being Integer st (i1 * m) + (i2 * n) = k implies p divides k )
given i1, i2 being Integer such that A10: (i1 * m) + (i2 * n) = k ; ::_thesis: p divides k
consider l, s being Nat such that
A11: k = (p * l) + s and
A12: s < p by A5, NAT_1:17;
reconsider l = l, s = 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 ; ::_thesis: contradiction
hence  contradiction by A7, A12, A13; ::_thesis: verum
end;
hence  p divides k by A11, NAT_D:def_3; ::_thesis: verum
end;
A14: for s being Nat st s divides m & s divides n holds
s divides p
proof
let s be Nat; ::_thesis: ( s divides m & s divides n implies s divides p )
assume that
A15: s divides m and
A16: s divides n ; ::_thesis: s divides p
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 being Integer st p9 = s9 * i4
proof
take  (i * l) + (i0 * r) ; ::_thesis: p9 = s9 * ((i * l) + (i0 * r))
thus  p9 = s9 * ((i * l) + (i0 * r)) by A8, A18, A17; ::_thesis: verum
end;
hence  s divides p by INT_1:def_3; ::_thesis: verum
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  ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n by A6; ::_thesis: verum
end;

definition
func SetPrimes  ->  Subset of NAT means :Def6: :: NEWTON:def 6
 for n being Nat holds
( n in it iff n is prime );
existence
 ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff n is prime )
proof
defpred S1[ 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 S1[n] ) from SUBSET_1:sch_3();
take  X ; ::_thesis: for n being Nat holds
( n in X iff n is prime )
let n be Nat; ::_thesis: ( n in X iff n is prime )
thus  ( n in X implies n is prime ) by A1; ::_thesis: ( n is prime implies n in X )
assume A2: n is prime ; ::_thesis: n in X
 n in NAT by ORDINAL1:def_12;
hence  n in X by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff n is prime ) ) & ( for n being Nat holds
( n in b2 iff n is prime ) ) holds
b1 = b2
proof
let A, B be Subset of NAT; ::_thesis: ( ( for n being Nat holds
( n in A iff n is prime ) ) & ( for n being Nat holds
( n in B iff n is prime ) ) implies A = B )
assume 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 ) ; ::_thesis: A = B
thus  A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A5: x in A ; ::_thesis: x in B
then reconsider x = x as Element of NAT ;
 x is prime by A3, A5;
hence  x in B by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume A6: x in B ; ::_thesis: x in A
then reconsider x = x as Element of NAT ;
 x is prime by A4, A6;
hence  x in A by A3; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines SetPrimes NEWTON:def_6_:_
 for b1 being Subset of NAT holds
( b1 = SetPrimes iff for n being Nat holds
( n in b1 iff n is prime ) );

registration
cluster epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer prime V35() finite cardinal V61() V62() V63() V64() V65() V66() for Element of NAT ;
existence
 ex b1 being Element of NAT st b1 is prime by INT_2:28;
cluster epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer prime finite cardinal for set ;
existence
 ex b1 being Nat st b1 is prime by INT_2:28;
end;

definition
mode Prime is prime Nat;
end;

definition
let p be Nat;
func SetPrimenumber p ->  Subset of NAT means :Def7: :: NEWTON:def 7
 for q being Nat holds
( q in it iff ( q < p & q is prime ) );
existence
 ex b1 being Subset of NAT st
for q being Nat holds
( q in b1 iff ( q < p & q is prime ) )
proof
defpred S1[ 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 S1[q] ) from SUBSET_1:sch_3();
take  X ; ::_thesis: for q being Nat holds
( q in X iff ( q < p & q is prime ) )
let q be Nat; ::_thesis: ( q in X iff ( q < p & q is prime ) )
thus  ( q in X implies ( q < p & q is prime ) ) by A1; ::_thesis: ( q < p & q is prime implies q in X )
assume that
A2: q < p and
A3: q is prime ; ::_thesis: q in X
 q in NAT by ORDINAL1:def_12;
hence  q in X by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of NAT st ( for q being Nat holds
( q in b1 iff ( q < p & q is prime ) ) ) & ( for q being Nat holds
( q in b2 iff ( q < p & q is prime ) ) ) holds
b1 = b2
proof
let A, B be Subset of NAT; ::_thesis: ( ( for q being Nat holds
( q in A iff ( q < p & q is prime ) ) ) & ( for q being Nat holds
( q in B iff ( q < p & q is prime ) ) ) implies A = B )
assume 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 ) ) ; ::_thesis: A = B
thus  A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A6: x in A ; ::_thesis: x in B
then reconsider x = x as Element of NAT ;
A7: x is prime by A4, A6;
 x < p by A4, A6;
hence  x in B by A5, A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume A8: x in B ; ::_thesis: x in A
then reconsider x = x as Element of NAT ;
A9: x is prime by A5, A8;
 x < p by A5, A8;
hence  x in A by A4, A9; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines SetPrimenumber NEWTON:def_7_:_
 for p being Nat
for b2 being Subset of NAT holds
( b2 = SetPrimenumber p iff for q being Nat holds
( q in b2 iff ( q < p & q is prime ) ) );

theorem Th68: :: NEWTON:68
for p being Nat holds SetPrimenumber p c= SetPrimes
proof
let p be Nat; ::_thesis: SetPrimenumber p c= SetPrimes
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetPrimenumber p or x in SetPrimes )
assume A1: x in SetPrimenumber p ; ::_thesis: x in SetPrimes
then reconsider x9 = x as Element of NAT ;
 x9 is prime by A1, Def7;
hence  x in SetPrimes by Def6; ::_thesis: verum
end;

theorem :: NEWTON:69
for p, q being Nat st p <= q holds
SetPrimenumber p c= SetPrimenumber q
proof
let p, q be Nat; ::_thesis: ( p <= q implies SetPrimenumber p c= SetPrimenumber q )
assume A1: p <= q ; ::_thesis: SetPrimenumber p c= SetPrimenumber q
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetPrimenumber p or x in SetPrimenumber q )
assume A2: x in SetPrimenumber p ; ::_thesis: x in SetPrimenumber q
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  x in SetPrimenumber q by A3, Def7; ::_thesis: verum
end;

theorem Th70: :: NEWTON:70
for p being Nat holds SetPrimenumber p c= Seg p
proof
let p be Nat; ::_thesis: SetPrimenumber p c= Seg p
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetPrimenumber p or x in Seg p )
assume A1: x in SetPrimenumber p ; ::_thesis: x in Seg 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  x in Seg p by A2; ::_thesis: verum
end;

theorem Th71: :: NEWTON:71
for p being Nat holds SetPrimenumber p is finite
proof
let p be Nat; ::_thesis: SetPrimenumber p is finite
 SetPrimenumber p c= Seg p by Th70;
hence  SetPrimenumber p is finite ; ::_thesis: verum
end;

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

theorem Th72: :: NEWTON:72
for l being Nat ex p being Prime st
( p is prime & p > l )
proof
let l be Nat; ::_thesis: ex p being Prime st
( p is prime & p > l )
reconsider two = 2 as Prime by INT_2:28;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
 ( ( l = 0 & ex p being Prime st
( p is prime & p > l ) ) or ( l = 1 & ex p being Prime st
( p is prime & p > l ) ) or ( 2 <= l & ex p being Prime st
( p is prime & p > l ) ) )
proof
percases ( l = 0 or l = 1 or 2 <= l ) by NAT_1:26;
caseA1: l = 0 ; ::_thesis: ex p being Prime st
( p is prime & p > l )
take  two ; ::_thesis: ( two is prime & two > l )
thus  ( two is prime & two > l ) by A1; ::_thesis: verum
end;
caseA2: l = 1 ; ::_thesis: ex p being Prime st
( p is prime & p > l )
take  two ; ::_thesis: ( two is prime & two > l )
thus  ( two is prime & two > l ) by A2; ::_thesis: verum
end;
caseA3: 2 <= l ; ::_thesis: ex p being Prime st
( p is prime & p > 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 ; ::_thesis: ( j9 is prime & j9 > l )
A6: j <> 0 by A4, INT_2:def_4;
 j <> 1 by A4, INT_2:def_4;
hence  ( j9 is prime & j9 > l ) by A5, A6, Th39, Th41; ::_thesis: verum
end;
end;
end;
hence  ex p being Prime st
( p is prime & p > l ) ; ::_thesis: verum
end;

Lm2:  SetPrimenumber 2 = {}
proof
assume  SetPrimenumber 2 <> {} ; ::_thesis: contradiction
then consider x being set  such that
A1: x in SetPrimenumber 2 by XBOOLE_0:def_1;
reconsider x = 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; ::_thesis: verum
end;

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

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

theorem :: NEWTON:73
for m being Nat holds SetPrimenumber m c= Seg m
proof
let m be Nat; ::_thesis: SetPrimenumber m c= Seg m
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetPrimenumber m or x in Seg m )
assume A1: x in SetPrimenumber m ; ::_thesis: x in Seg m
then reconsider x = 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  x in Seg m by A2; ::_thesis: verum
end;

theorem :: NEWTON:74
for k, m being Nat st k >= m holds
not k in SetPrimenumber m by Def7;

theorem :: NEWTON:75
for n being Nat holds (SetPrimenumber n) \/ {n} is finite ;

theorem Th76: :: NEWTON:76
for f being Prime
for g being Nat st f < g holds
(SetPrimenumber f) \/ {f} c= SetPrimenumber g
proof
let f be Prime; ::_thesis: for g being Nat st f < g holds
(SetPrimenumber f) \/ {f} c= SetPrimenumber g
let g be Nat; ::_thesis: ( f < g implies (SetPrimenumber f) \/ {f} c= SetPrimenumber g )
assume A1: f < g ; ::_thesis: (SetPrimenumber f) \/ {f} c= SetPrimenumber g
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SetPrimenumber f) \/ {f} or x in SetPrimenumber g )
assume A2: x in (SetPrimenumber f) \/ {f} ; ::_thesis: x in SetPrimenumber g
then reconsider x = x as Nat ;
percases ( x in SetPrimenumber f or x in {f} ) by A2, XBOOLE_0:def_3;
supposeA3: x in SetPrimenumber f ; ::_thesis: x in SetPrimenumber g
then  x < f by Def7;
then A4: x < g by A1, XXREAL_0:2;
 x is prime by A3, Def7;
hence  x in SetPrimenumber g by A4, Def7; ::_thesis: verum
end;
suppose x in {f} ; ::_thesis: x in SetPrimenumber g
then  x = f by TARSKI:def_1;
hence  x in SetPrimenumber g by A1, Def7; ::_thesis: verum
end;
end;
end;

theorem :: NEWTON:77
for k, m being Nat st k >= m holds
not k in SetPrimenumber m by Def7;

Lm3:  for n being Nat holds SetPrimenumber n =  {  k where k is Element of NAT : ( k < n & k is prime )  }
proof
let n be Nat; ::_thesis: SetPrimenumber n =  {  k where k is Element of NAT : ( k < n & k is prime )  }
thus  SetPrimenumber n c=  {  k where k is Element of NAT : ( k < n & k is prime )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  k where k is Element of NAT : ( k < n & k is prime )  }  c= SetPrimenumber n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetPrimenumber n or x in  {  k where k is Element of NAT : ( k < n & k is prime )  }  )
assume A1: x in SetPrimenumber n ; ::_thesis: x in  {  k where k is Element of NAT : ( k < n & k is prime )  }
then reconsider x = x as Element of NAT ;
A2: x is prime by A1, Def7;
 x < n by A1, Def7;
hence  x in  {  k where k is Element of NAT : ( k < n & k is prime )  }  by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  k where k is Element of NAT : ( k < n & k is prime )  }  or x in SetPrimenumber n )
assume  x in  {  k where k is Element of NAT : ( k < n & k is prime )  }  ; ::_thesis: x in SetPrimenumber n
then  ex k being Element of NAT st
( x = k & k < n & k is prime ) ;
hence  x in SetPrimenumber n by Def7; ::_thesis: verum
end;

definition
let n be Nat;
func primenumber n ->  prime Element of NAT  means :Def8: :: NEWTON:def 8
n = card (SetPrimenumber it);
existence
 ex b1 being prime Element of NAT st n = card (SetPrimenumber b1)
proof
defpred S1[ Nat] means  ex m being Nat st
( $1 = card (SetPrimenumber m) & m is Prime );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
given m being Nat such that A2: n = card (SetPrimenumber m) and
A3: m is Prime ; ::_thesis: S1[n + 1]
defpred S2[ Nat] means ( $1 is prime & $1 > m );
A4: not m in SetPrimenumber m by Def7;
A5: ex k being Nat st S2[k]
proof
 ex p being Prime st
( p is prime & p > m ) by Th72;
hence  ex k being Nat st S2[k] ; ::_thesis: verum
end;
consider k being Nat such that
A6: ( S2[k] & ( for l being Nat st S2[l] holds
k <= l ) ) from NAT_1:sch_5(A5);
take  k ; ::_thesis: ( n + 1 = card (SetPrimenumber k) & k is Prime )
A7: SetPrimenumber k c= (SetPrimenumber m) \/ {m}
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in SetPrimenumber k or s in (SetPrimenumber m) \/ {m} )
assume A8: s in SetPrimenumber k ; ::_thesis: s in (SetPrimenumber m) \/ {m}
then reconsider s = s as Element of NAT ;
A9: s is prime by A8, Def7;
 s < k by A8, Def7;
then A10: s <= m by A6, A9;
percases ( s = m or s < m ) by A10, XXREAL_0:1;
suppose s = m ; ::_thesis: s in (SetPrimenumber m) \/ {m}
then  s in {m} by TARSKI:def_1;
hence  s in (SetPrimenumber m) \/ {m} by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA11: s < m ; ::_thesis: s in (SetPrimenumber m) \/ {m}
A12: SetPrimenumber m c= (SetPrimenumber m) \/ {m} by XBOOLE_1:7;
 s in SetPrimenumber m by A9, A11, Def7;
hence  s in (SetPrimenumber m) \/ {m} by A12; ::_thesis: verum
end;
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; ::_thesis: k is Prime
thus  k is Prime by A6; ::_thesis: verum
end;
 SetPrimenumber 2 =  {  k where k is Element of NAT : ( k < 2 & k is prime )  }  by Lm3;
then A13: S1[ 0 ] by CARD_1:27, INT_2:28;
 for n being Nat holds S1[n] from NAT_1:sch_2(A13, A1);
then consider m being Nat such that
A14: n = card (SetPrimenumber m) and
A15: m is Prime ;
 m in NAT by ORDINAL1:def_12;
hence  ex b1 being prime Element of NAT st n = card (SetPrimenumber b1) by A14, A15; ::_thesis: verum
end;
uniqueness
 for b1, b2 being prime Element of NAT st n = card (SetPrimenumber b1) & n = card (SetPrimenumber b2) holds
b1 = b2
proof
let f, g be prime Element of NAT ; ::_thesis: ( n = card (SetPrimenumber f) & n = card (SetPrimenumber g) implies f = g )
assume that
A16: n = card (SetPrimenumber f) and
A17: n = card (SetPrimenumber g) ; ::_thesis: f = g
assume A18: f <> g ; ::_thesis: contradiction
 ( ( f < g & n + 1 <= n ) or ( g < f & n + 1 <= n ) )
proof
percases ( f < g or g < f ) by A18, XXREAL_0:1;
caseA19: f < g ; ::_thesis: n + 1 <= n
A20: not f in SetPrimenumber f by Def7;
 card ((SetPrimenumber f) \/ {f}) <= card (SetPrimenumber g) by A19, Th76, NAT_1:43;
hence  n + 1 <= n by A16, A17, A20, CARD_2:41; ::_thesis: verum
end;
caseA21: g < f ; ::_thesis: n + 1 <= n
A22: not g in SetPrimenumber g by Def7;
 card ((SetPrimenumber g) \/ {g}) <= card (SetPrimenumber f) by A21, Th76, NAT_1:43;
hence  n + 1 <= n by A16, A17, A22, CARD_2:41; ::_thesis: verum
end;
end;
end;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines primenumber NEWTON:def_8_:_
 for n being Nat
for b2 being prime Element of NAT holds
( b2 = primenumber n iff n = card (SetPrimenumber b2) );

theorem :: NEWTON:78
for n being Nat holds SetPrimenumber n =  {  k where k is Element of NAT : ( k < n & k is prime )  }  by Lm3;

theorem Th79: :: NEWTON:79
SetPrimes is infinite
proof
assume A1: SetPrimes is finite ; ::_thesis: contradiction
then reconsider SP = SetPrimes as finite set ;
consider n being 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 (primenumber (n + 1));
A4: n + 1 = card (SetPrimenumber (primenumber (n + 1))) by Def8;
 card (SetPrimenumber (primenumber (n + 1))) <= card SP by Th68, NAT_1:43;
hence  contradiction by A3, A4, NAT_1:13; ::_thesis: verum
end;

registration
cluster SetPrimes  ->  non empty infinite ;
coherence
 ( not SetPrimes is empty & not SetPrimes is finite ) by Th79;
end;

theorem :: NEWTON:80
for i being Nat st i is prime holds
for m, n being Nat holds
( not i divides m * n or i divides m or i divides n )
proof
let i be Nat; ::_thesis: ( i is prime implies for m, n being Nat holds
( not i divides m * n or i divides m or i divides n ) )
defpred S1[ 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 ; ::_thesis: for m, n being Nat holds
( not i divides m * n or i divides m or i divides n )
given m, n being Nat such that A2: i divides m * n and
A3: ( not i divides m & not i divides n ) ; ::_thesis: contradiction
A4: ex i being Nat st S1[i] by A1, A2, A3;
consider p9 being Nat such that
A5: S1[p9] and
A6: for p1 being Nat st S1[p1] holds
p9 <= p1 from NAT_1:sch_5(A4);
defpred S2[ Nat] means  ex n being Nat st
( p9 divides $1 * n & not p9 divides $1 & not p9 divides n );
A7: ex i being Nat st S2[i] by A5;
consider m being Nat such that
A8: S2[m] and
A9: for m1 being Nat st S2[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 ; ::_thesis: contradiction
A16: p9 > 0 by A5, INT_2:def_4;
then  m = (p9 * (m div p9)) + (m mod p9) by NAT_D:2;
then A17: m * n = ((p9 * (m div p9)) * n) + ((m mod p9) * n) ;
 m mod p9 < p9 by A16, NAT_D:1;
then A18: m mod p9 < 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 (m mod p9) * n by A11, A17, NAT_D:10;
 m = (p9 * (m div p9)) + (m mod p9) by A16, NAT_D:2;
then  not p9 divides m mod p9 by A12, A19, NAT_D:8;
hence  contradiction by A9, A13, A18, A20; ::_thesis: verum
end;
A21: m < 2
proof
assume  m >= 2 ; ::_thesis: contradiction
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 ; ::_thesis: contradiction
then  ( p1 = 1 or p1 = p9 ) by A5, INT_2:def_4;
hence  contradiction by A8, A22, A23, INT_2:def_4; ::_thesis: verum
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 ; ::_thesis: contradiction
then  m = 1 * m1 ;
hence  contradiction by A24, A30, A31, XREAL_1:68; ::_thesis: verum
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; ::_thesis: verum
end;
 m >= 2
proof
A35: m >= 0 + 1 by A10, NAT_1:13;
assume A36: m < 2 ; ::_thesis: contradiction
then  m <= 1 + 1 ;
then  m = 1 by A36, A35, NAT_1:9;
hence  contradiction by A11, A13; ::_thesis: verum
end;
hence  contradiction by A21; ::_thesis: verum
end;

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

theorem :: NEWTON:82
for m, n being Nat holds
( m div n = m div n & m mod n = m mod n ) ;

theorem :: NEWTON:83
for k being Nat
for x being real number st x > 0 holds
x |^ k > 0
proof
let k be Nat; ::_thesis: for x being real number st x > 0 holds
x |^ k > 0
let x be real number ; ::_thesis: ( x > 0 implies x |^ k > 0 )
defpred S1[ Nat] means  for x being real number st x > 0 holds
x |^ $1 > 0 ;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for x being real number st x > 0 holds
x |^ k > 0 ; ::_thesis: S1[k + 1]
let x be real number ; ::_thesis: ( x > 0 implies x |^ (k + 1) > 0 )
A3: x |^ (k + 1) = x * (x |^ k) by Th6;
assume A4: x > 0 ; ::_thesis: x |^ (k + 1) > 0
then  x |^ k > 0 by A2;
hence  x |^ (k + 1) > 0 by A4, A3; ::_thesis: verum
end;
A5: S1[ 0 ] by RVSUM_1:94;
 for k being Nat holds S1[k] from NAT_1:sch_2(A5, A1);
hence  ( x > 0 implies x |^ k > 0 ) ; ::_thesis: verum
end;

theorem :: NEWTON:84
for n being Nat st n > 0 holds
0 |^ n = 0
proof
let n be Nat; ::_thesis: ( n > 0 implies 0 |^ n = 0 )
assume  n > 0 ; ::_thesis: 0 |^ n = 0
then  n >= 1 + 0 by NAT_1:13;
hence  0 |^ n = 0 by Th11; ::_thesis: verum
end;

definition
let m, n be Element of NAT ;
:: original: |^
redefine funcm |^ n ->  Element of NAT ;
coherence
 m |^ n is Element of NAT by ORDINAL1:def_12;
end;

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

Lm4:  S1[ 0 ]
by RVSUM_1:94;

Lm5:  for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  2 |^ n >= n + 1 ; ::_thesis: S1[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 ; ::_thesis: verum
end;

theorem Th85: :: NEWTON:85
for n being Nat holds 2 |^ n >= n + 1
proof
let n be Nat; ::_thesis: 2 |^ n >= n + 1
 for n being Nat holds S1[n] from NAT_1:sch_2(Lm4, Lm5);
hence  2 |^ n >= n + 1 ; ::_thesis: verum
end;

theorem :: NEWTON:86
for n being Nat holds 2 |^ n > n
proof
let n be Nat; ::_thesis: 2 |^ n > n
 2 |^ n >= n + 1 by Th85;
hence  2 |^ n > n by NAT_1:13; ::_thesis: verum
end;

scheme :: NEWTON:sch 1
Euklides9{ F1( Nat) ->  Element of NAT , F2( Nat) ->  Element of NAT , F3() ->  Element of NAT , F4() ->  Element of NAT } :
 ex k being Element of NAT st
( F1(k) = F3() gcd F4() & F2(k) = 0 )
provided
A1: 0 < F4() and
A2: F4() < F3() and
A3: F1(0) = F3() and
A4: F2(0) = F4() and
A5: for k being Element of NAT st F2(k) > 0 holds
( F1((k + 1)) = F2(k) & F2((k + 1)) = F1(k) mod F2(k) )
proof
deffunc H1( Nat, set ) ->  Element of NAT = IFEQ ($2,0,0,F2($1));
consider q being Function of NAT,NAT such that
A6: q . 0 = F3() and
A7: for i being Nat holds q . (i + 1) = H1(i,q . i) from NAT_1:sch_12();
deffunc H2( Element of NAT ) ->  Element of NAT = q . $1;
q . (0 + 1) = IFEQ ((q . 0),0,0,F2(0)) by A7
.= F2(0) by A2, A6, FUNCOP_1:def_8 ;
then A8: ( H2( 0 ) = F3() & H2(1) = F4() ) by A4, A6;
A9: for k being Element of NAT st q . k > 0 holds
q . k = F1(k)
proof
let k be Element of NAT ; ::_thesis: ( q . k > 0 implies q . k = F1(k) )
assume A10: q . k > 0 ; ::_thesis: q . k = F1(k)
now__::_thesis:_(_(_k_=_0_&_q_._k_=_F1(k)_)_or_(_k_<>_0_&_q_._k_=_F1(k)_)_)
percases ( k = 0 or k <> 0 ) ;
case k = 0 ; ::_thesis: q . k = F1(k)
hence  q . k = F1(k) by A3, A6; ::_thesis: verum
end;
case k <> 0 ; ::_thesis: q . k = F1(k)
then consider i being Nat such that
A11: k = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A12: now__::_thesis:_not_q_._i_=_0
assume A13: q . i = 0 ; ::_thesis: contradiction
q . k = IFEQ ((q . i),0,0,F2(i)) by A7, A11
.= 0 by A13, FUNCOP_1:def_8 ;
hence  contradiction by A10; ::_thesis: verum
end;
q . k = IFEQ ((q . i),0,0,F2(i)) by A7, A11
.= F2(i) by A12, FUNCOP_1:def_8 ;
hence  q . k = F1(k) by A5, A10, A11; ::_thesis: verum
end;
end;
end;
hence  q . k = F1(k) ; ::_thesis: verum
end;
A14: for k being Element of NAT holds H2(k + 2) = H2(k) mod H2(k + 1)
proof
let k be Element of NAT ; ::_thesis: H2(k + 2) = H2(k) mod H2(k + 1)
now__::_thesis:_(_(_q_._(k_+_1)_<>_0_&_H2(k_+_2)_=_H2(k)_mod_H2(k_+_1)_)_or_(_q_._(k_+_1)_=_0_&_q_._(k_+_2)_=_(q_._k)_mod_(q_._(k_+_1))_)_)
percases ( q . (k + 1) <> 0 or q . (k + 1) = 0 ) ;
caseA15: q . (k + 1) <> 0 ; ::_thesis: H2(k + 2) = H2(k) mod H2(k + 1)
A16: now__::_thesis:_not_F2(k)_=_0
A17: ( q . k = 0 or q . k <> 0 ) ;
assume A18: F2(k) = 0 ; ::_thesis: contradiction
q . (k + 1) = IFEQ ((q . k),0,0,F2(k)) by A7
.= 0 by A18, A17, FUNCOP_1:def_8 ;
hence  contradiction by A15; ::_thesis: verum
end;
A19: q . (k + (1 + 1)) = q . ((k + 1) + 1)
.= IFEQ ((q . (k + 1)),0,0,F2((k + 1))) by A7
.= F2((k + 1)) by A15, FUNCOP_1:def_8
.= F1(k) mod F2(k) by A5, A16 ;
A20: now__::_thesis:_not_q_._k_=_0
assume A21: q . k = 0 ; ::_thesis: contradiction
q . (k + 1) = IFEQ ((q . k),0,0,F2(k)) by A7
.= 0 by A21, FUNCOP_1:def_8 ;
hence  contradiction by A15; ::_thesis: verum
end;
q . (k + 1) = IFEQ ((q . k),0,0,F2(k)) by A7
.= F2(k) by A20, FUNCOP_1:def_8 ;
hence  H2(k + 2) = H2(k) mod H2(k + 1) by A9, A19, A20; ::_thesis: verum
end;
caseA22: q . (k + 1) = 0 ; ::_thesis: q . (k + 2) = (q . k) mod (q . (k + 1))
thus q . (k + 2) = q . ((k + 1) + 1)
.= IFEQ ((q . (k + 1)),0,0,F2((k + 1))) by A7
.= 0 by A22, FUNCOP_1:def_8
.= (q . k) mod (q . (k + 1)) by A22, NAT_D:def_2 ; ::_thesis: verum
end;
end;
end;
hence  H2(k + 2) = H2(k) mod H2(k + 1) ; ::_thesis: verum
end;
A23: ( 0 < F4() & F4() < F3() ) by A1, A2;
consider k being Element of NAT  such that
A24: ( H2(k) = F3() gcd F4() & H2(k + 1) = 0 ) from NAT_D:sch_1(A23, A8, A14);
take  k ; ::_thesis: ( F1(k) = F3() gcd F4() & F2(k) = 0 )
thus  F1(k) = F3() gcd F4() by A1, A9, A24, Th58; ::_thesis: F2(k) = 0
 F3() gcd F4() > 0 by A1, Th58;
hence F2(k) = IFEQ ((q . k),0,0,F2(k)) by A24, FUNCOP_1:def_8
.= 0 by A7, A24 ;
::_thesis: verum
end;


theorem Th87: :: NEWTON:87
for r, n being Nat holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
proof
let r, n be Nat; ::_thesis: ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
defpred S2[ Nat] means ( ( r <> 0 or $1 = 0 ) iff r |^ $1 <> 0 );
A1: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A2: S2[k] ; ::_thesis: S2[k + 1]
 r |^ (k + 1) = (r |^ k) * r by Th6;
hence  S2[k + 1] by A2; ::_thesis: verum
end;
A3: S2[ 0 ] by RVSUM_1:94;
 for k being Nat holds S2[k] from NAT_1:sch_2(A3, A1);
hence  ( ( r <> 0 or n = 0 ) iff r |^ n <> 0 ) ; ::_thesis: verum
end;

Lm6:  for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2
proof
let n1, m1, n2, m2 be Nat; ::_thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies n1 <= n2 )
assume A1: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; ::_thesis: n1 <= n2
assume A2: n1 > n2 ; ::_thesis: contradiction
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 = 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, NAT_D:10; ::_thesis: verum
end;

theorem :: NEWTON:88
for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 & m1 = m2 )
proof
let n1, m1, n2, m2 be Nat; ::_thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies ( n1 = n2 & m1 = m2 ) )
A1: 2 |^ n1 <> 0 by Th87;
assume A2: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; ::_thesis: ( n1 = n2 & m1 = m2 )
then A3: n2 <= n1 by Lm6;
 n1 <= n2 by A2, Lm6;
hence  n1 = n2 by A3, XXREAL_0:1; ::_thesis: m1 = m2
then  (2 * m1) + 1 = (2 * m2) + 1 by A2, A1, XCMPLX_1:5;
hence  m1 = m2 ; ::_thesis: verum
end;

theorem :: NEWTON:89
for m, k, n being Nat st k <= n holds
m |^ k divides m |^ n
proof
let m, k, n be Nat; ::_thesis: ( k <= n implies m |^ k divides m |^ n )
assume  k <= n ; ::_thesis: m |^ k divides m |^ n
then consider t being Nat such that
A1: n = k + t by NAT_1:10;
reconsider t = t as Element of NAT by ORDINAL1:def_12;
 m |^ n = (m |^ k) * (m |^ t) by A1, Th8;
hence  m |^ k divides m |^ n by NAT_D:def_3; ::_thesis: verum
end;