:: Factorial and Newton coefficients
:: by Rafa{\l} Kwiatek
::
:: Received July 27, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


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 &amp; k < n )  }  ) \/ {n}
proofend;

theorem Th2: :: NEWTON:2
for a being real number
for F being FinSequence of REAL holds len (a * F) = len F
proofend;

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;

:: x |^ n Function
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
proofend;

theorem Th6: :: NEWTON:6
for s being Nat
for z being complex number holds z |^ (s + 1) = (z |^ s) * z
proofend;

registration
let x, n be Nat;
clusterx |^ n ->  natural ;
coherence
 x |^ n is natural
proofend;
end;

theorem :: NEWTON:7
for s being Nat
for x, y being complex number holds (x * y) |^ s = (x |^ s) * (y |^ s)
proofend;

theorem Th8: :: NEWTON:8
for s, t being Nat
for x being complex number holds x |^ (s + t) = (x |^ s) * (x |^ t)
proofend;

theorem :: NEWTON:9
for s, t being Nat
for x being complex number holds (x |^ s) |^ t = x |^ (s * t)
proofend;

theorem Th10: :: NEWTON:10
for s being Nat holds 1 |^ s = 1
proofend;

theorem Th11: :: NEWTON:11
for s being Nat st s >= 1 holds
0 |^ s = 0
proofend;

:: n! Function
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
proofend;

theorem Th15: :: NEWTON:15
for s being Nat holds (s + 1) ! = (s !) * (s + 1)
proofend;

theorem Th16: :: NEWTON:16
for s being Nat holds s ! is Element of NAT
proofend;

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
proofend;

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 ;

:: n choose k Function
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 !)) ) &amp; ( not n >= k implies ex b1 being set st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( n >= k &amp; ( for l being Nat st l = n - k holds
b1 = (n !) / ((k !) * (l !)) ) &amp; ( for l being Nat st l = n - k holds
b2 = (n !) / ((k !) * (l !)) ) implies b1 = b2 ) &amp; ( not n >= k &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
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 !)) ) ) &amp; ( 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
proofend;
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
proofend;

theorem Th20: :: NEWTON:20
for s, t, r being Nat st s >= t &amp; r = s - t holds
s choose t = s choose r
proofend;

theorem Th21: :: NEWTON:21
for s being Nat holds s choose s = 1
proofend;

theorem Th22: :: NEWTON:22
for t, s being Nat holds (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)
proofend;

theorem Th23: :: NEWTON:23
for s being Nat st s >= 1 holds
s choose 1 = s
proofend;

theorem :: NEWTON:24
for s, t being Nat st s >= 1 &amp; t = s - 1 holds
s choose t = s
proofend;

theorem Th25: :: NEWTON:25
for s, r being Nat holds s choose r is Element of NAT
proofend;

theorem :: NEWTON:26
for n, m being Nat
for F being FinSequence of REAL st m <> 0 &amp; len F = m &amp; ( for i, l being Nat st i in dom F &amp; l = (n + i) - 1 holds
F . i = l choose n ) holds
Sum F = (n + m) choose (n + 1)
proofend;

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 &amp; ( for i, l, m being Nat st i in dom it &amp; m = i - 1 &amp; 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 &amp; ( for i, l, m being Nat st i in dom b1 &amp; m = i - 1 &amp; l = n - m holds
b1 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = n + 1 &amp; ( for i, l, m being Nat st i in dom b1 &amp; m = i - 1 &amp; l = n - m holds
b1 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) &amp; len b2 = n + 1 &amp; ( for i, l, m being Nat st i in dom b2 &amp; m = i - 1 &amp; l = n - m holds
b2 . i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
proofend;
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 &amp; ( for i, l, m being Nat st i in dom b4 &amp; m = i - 1 &amp; 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*>
proofend;

theorem Th28: :: NEWTON:28
for s being Nat
for a, b being real number holds ((a,b) In_Power s) . 1 = a |^ s
proofend;

theorem Th29: :: NEWTON:29
for s being Nat
for a, b being real number holds ((a,b) In_Power s) . (s + 1) = b |^ s
proofend;

theorem Th30: :: NEWTON:30
for s being Nat
for a, b being real number holds (a + b) |^ s = Sum ((a,b) In_Power s)
proofend;

definition
let n be Nat;
func Newton_Coeff n ->  FinSequence of REAL  means :Def5: :: NEWTON:def 5
( len it = n + 1 &amp; ( for i, k being Nat st i in dom it &amp; k = i - 1 holds
it . i = n choose k ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = n + 1 &amp; ( for i, k being Nat st i in dom b1 &amp; k = i - 1 holds
b1 . i = n choose k ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = n + 1 &amp; ( for i, k being Nat st i in dom b1 &amp; k = i - 1 holds
b1 . i = n choose k ) &amp; len b2 = n + 1 &amp; ( for i, k being Nat st i in dom b2 &amp; k = i - 1 holds
b2 . i = n choose k ) holds
b1 = b2
proofend;
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 &amp; ( for i, k being Nat st i in dom b2 &amp; 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
proofend;

theorem :: NEWTON:32
for s being Nat holds 2 |^ s = Sum (Newton_Coeff s)
proofend;

begin

:: from NAT_LAT
theorem Th33: :: NEWTON:33
for l, k being Nat st l >= 1 holds
k * l >= k
proofend;

theorem Th34: :: NEWTON:34
for l, n, k being Nat st l >= 1 &amp; n >= k * l holds
n >= k
proofend;

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 !
proofend;

theorem :: NEWTON:36
for n being Nat st n <> 0 holds
(n + 1) / n > 1
proofend;

theorem Th37: :: NEWTON:37
for k being Nat holds k / (k + 1) < 1
proofend;

theorem Th38: :: NEWTON:38
for l being Nat holds l ! >= l
proofend;

theorem Th39: :: NEWTON:39
for m, n being Nat st m <> 1 &amp; m divides n holds
not m divides n + 1
proofend;

theorem Th40: :: NEWTON:40
for j, k being Nat st j <> 0 holds
j divides (j + k) !
proofend;

theorem Th41: :: NEWTON:41
for j, l being Nat st j <= l &amp; j <> 0 holds
j divides l !
proofend;

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

:: The fundamental properties of lcm, hcf
theorem :: NEWTON:43
for m, n, k being Nat holds m lcm (n lcm k) = (m lcm n) lcm k
proofend;

theorem Th44: :: NEWTON:44
for m, n being Nat holds
( m divides n iff m lcm n = n )
proofend;

theorem :: NEWTON:45
for n, m, k being Nat holds
( ( n divides m &amp; k divides m ) iff n lcm k divides m )
proofend;

theorem :: NEWTON:46
for m being Nat holds m lcm 1 = m
proofend;

theorem Th47: :: NEWTON:47
for m, n being Nat holds m lcm n divides m * n
proofend;

theorem :: NEWTON:48
for m, n, k being Nat holds m gcd (n gcd k) = (m gcd n) gcd k
proofend;

theorem Th49: :: NEWTON:49
for n, m being Nat st n divides m holds
n gcd m = n
proofend;

theorem :: NEWTON:50
for m, n, k being Nat holds
( ( m divides n &amp; m divides k ) iff m divides n gcd k )
proofend;

theorem :: NEWTON:51
for m being Nat holds m gcd 1 = 1
proofend;

theorem :: NEWTON:52
for m being Nat holds m gcd 0 = m
proofend;

theorem Th53: :: NEWTON:53
for m, n being Nat holds (m gcd n) lcm n = n
proofend;

theorem Th54: :: NEWTON:54
for m, n being Nat holds m gcd (m lcm n) = m
proofend;

theorem :: NEWTON:55
for m, n being Nat holds m gcd (m lcm n) = (n gcd m) lcm m
proofend;

theorem :: NEWTON:56
for m, n, k being Nat st m divides n holds
m gcd k divides n gcd k
proofend;

theorem :: NEWTON:57
for m, n, k being Nat st m divides n holds
k gcd m divides k gcd n
proofend;

theorem Th58: :: NEWTON:58
for n, m being Nat st n > 0 holds
n gcd m > 0
proofend;

theorem :: NEWTON:59
for m, n being Nat st m > 0 &amp; n > 0 holds
m lcm n > 0
proofend;

theorem :: NEWTON:60
for n, m, k being Nat holds (n gcd m) lcm (n gcd k) divides n gcd (m lcm k)
proofend;

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
proofend;

theorem :: NEWTON:62
for n, m being Nat holds n gcd m divides n lcm m
proofend;

theorem :: NEWTON:63
for m, n being Nat st 0 < m holds
n mod m = n - (m * (n div m))
proofend;

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;

:: [WP: ] Bezout's_Theorem
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
proofend;

:: from NAT_LAT
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 )
proofend;
uniqueness
 for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff n is prime ) ) &amp; ( for n being Nat holds
( n in b2 iff n is prime ) ) holds
b1 = b2
proofend;
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 &amp; q is prime ) );
existence
 ex b1 being Subset of NAT st
for q being Nat holds
( q in b1 iff ( q < p &amp; q is prime ) )
proofend;
uniqueness
 for b1, b2 being Subset of NAT st ( for q being Nat holds
( q in b1 iff ( q < p &amp; q is prime ) ) ) &amp; ( for q being Nat holds
( q in b2 iff ( q < p &amp; q is prime ) ) ) holds
b1 = b2
proofend;
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 &amp; q is prime ) ) );

theorem Th68: :: NEWTON:68
for p being Nat holds SetPrimenumber p c= SetPrimes
proofend;

theorem :: NEWTON:69
for p, q being Nat st p <= q holds
SetPrimenumber p c= SetPrimenumber q
proofend;

theorem Th70: :: NEWTON:70
for p being Nat holds SetPrimenumber p c= Seg p
proofend;

theorem Th71: :: NEWTON:71
for p being Nat holds SetPrimenumber p is finite
proofend;

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 &amp; p > l )
proofend;

Lm2:  SetPrimenumber 2 = {}
proofend;

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
proofend;

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
proofend;

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 &amp; k is prime )  }
proofend;

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)
proofend;
uniqueness
 for b1, b2 being prime Element of NAT st n = card (SetPrimenumber b1) &amp; n = card (SetPrimenumber b2) holds
b1 = b2
proofend;
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 &amp; k is prime )  }  by Lm3;

:: [WP: ] The_Infinitude_of_Primes
theorem Th79: :: NEWTON:79
SetPrimes is infinite
proofend;

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

:: divisibility
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 )
proofend;

theorem :: NEWTON:81
for x being complex number holds
( x |^ 2 = x * x &amp; x ^2 = x |^ 2 )
proofend;

:: from SCMFSA9A, 2005.11.16, A.T
theorem :: NEWTON:82
for m, n being Nat holds
( m div n = m div n &amp; 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
proofend;

:: missing, 2006.07.17, A.T.
theorem :: NEWTON:84
for n being Nat st n > 0 holds
0 |^ n = 0
proofend;

:: from CARD_4 and WSIERP_1, 2007.02.07, AK
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]
proofend;

theorem Th85: :: NEWTON:85
for n being Nat holds 2 |^ n >= n + 1
proofend;

theorem :: NEWTON:86
for n being Nat holds 2 |^ n > n
proofend;

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() &amp; 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) &amp; F2((k + 1)) = F1(k) mod F2(k) )
proofend;

theorem Th87: :: NEWTON:87
for r, n being Nat holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
proofend;

Lm6:  for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2
proofend;

theorem :: NEWTON:88
for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 &amp; m1 = m2 )
proofend;

theorem :: NEWTON:89
for m, k, n being Nat st k <= n holds
m |^ k divides m |^ n
proofend;