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

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

theorem Th2: :: NEWTON:2

for a being Real
for F being FinSequence of REAL holds len (a * F) = len F

proof end;

theorem :: NEWTON:3

for a being Real
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;
let n be natural Number ;

cluster n |-> x -> complex-valued ;

coherence
n |-> x is complex-valued ;

end;

definition

let x be Complex;
let n be natural Number ;

func x |^ n -> number equals :: NEWTON:def 1
Product (n |-> x);

coherence
Product (n |-> x) is number by TARSKI:1;

end;

:: deftheorem defines |^ NEWTON:def 1 :
for x being Complex
for n being natural Number holds x |^ n = Product (n |-> x);

registration

let x be Real;
let n be natural Number ;

cluster x |^ n -> real ;

coherence
x |^ n is real ;

end;

registration

let z be Complex;
let n be natural Number ;

cluster z |^ n -> complex ;

coherence
z |^ n is complex ;

end;

theorem :: NEWTON:4

for z being Complex holds z |^ 0 = 1 by RVSUM_1:94;

theorem Th5: :: NEWTON:5

for z being Complex holds z |^ 1 = z

proof end;

registration

let a be Complex;

reduce a |^ 1 to a;

reducibility
a |^ 1 = a by Th5;

end;

theorem Th6: :: NEWTON:6

for s being Nat
for z being Complex holds z |^ (s + 1) = (z |^ s) * z

proof end;

registration

let x, n be natural Number ;

cluster x |^ n -> natural ;

coherence
x |^ n is natural

proof end;

end;

theorem :: NEWTON:7

for x, y being Complex
for s being natural Number holds (x * y) |^ s = (x |^ s) * (y |^ s)

proof end;

theorem Th8: :: NEWTON:8

for x being Complex
for s, t being natural Number holds x |^ (s + t) = (x |^ s) * (x |^ t)

proof end;

theorem :: NEWTON:9

for x being Complex
for s, t being natural Number holds (x |^ s) |^ t = x |^ (s * t)

proof end;

theorem Th10: :: NEWTON:10

for s being natural Number holds 1 |^ s = 1

proof end;

registration

let n be Nat;

reduce 1 |^ n to 1;

reducibility
1 |^ n = 1 by Th10;

end;

theorem Th11: :: NEWTON:11

for s being natural Number st s >= 1 holds
0 |^ s = 0

proof end;

:: n! Function

registration

let n be natural Number ;

cluster idseq n -> natural-valued ;

coherence
idseq n is natural-valued

proof end;

end;

definition

let n be natural Number ;

func n ! -> number equals :: NEWTON:def 2
Product (idseq n);

coherence
Product (idseq n) is number by TARSKI:1;

end;

:: deftheorem defines ! NEWTON:def 2 :
for n being natural Number holds n ! = Product (idseq n);

registration

let n be natural Number ;

cluster n ! -> 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;

theorem :: NEWTON:14

2 ! = 2

proof end;

theorem Th15: :: NEWTON:15

for s being natural Number holds (s + 1) ! = (s !) * (s + 1)

proof end;

theorem Th16: :: NEWTON:16

for s being natural Number holds s ! is Element of NAT

proof end;

registration

let n be natural Number ;

cluster n ! -> natural ;

coherence
n ! is natural by Th16;

end;

theorem Th17: :: NEWTON:17

for s being natural Number holds s ! > 0

proof end;

registration

let n be natural Number ;

cluster n ! -> positive ;

coherence
n ! is positive by Th17;

end;

theorem :: NEWTON:18

for s, t being natural Number holds (s !) * (t !) <> 0 ;

:: n choose k Function

definition

let k, n be natural Number ;

func n choose k -> number 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 b₁ being number holds verum ;
existence
( ( n >= k implies ex b₁ being number st
for l being Nat st l = n - k holds
b₁ = (n !) / ((k !) * (l !)) ) & ( not n >= k implies ex b₁ being number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being number holds
( ( n >= k & ( for l being Nat st l = n - k holds
b₁ = (n !) / ((k !) * (l !)) ) & ( for l being Nat st l = n - k holds
b₂ = (n !) / ((k !) * (l !)) ) implies b₁ = b₂ ) & ( not n >= k & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

end;

:: deftheorem Def3 defines choose NEWTON:def 3 :
for k, n being natural Number
for b₃ being number holds
( ( n >= k implies ( b₃ = n choose k iff for l being Nat st l = n - k holds
b₃ = (n !) / ((k !) * (l !)) ) ) & ( not n >= k implies ( b₃ = n choose k iff b₃ = 0 ) ) );

registration

let k, n be natural Number ;

cluster n choose k -> real ;

coherence
n choose k is real

proof end;

end;

theorem Th19: :: NEWTON:19

for s being natural Number holds s choose 0 = 1

proof end;

theorem Th20: :: NEWTON:20

for r, s, t being natural Number st s >= t & r = s - t holds
s choose t = s choose r

proof end;

theorem Th21: :: NEWTON:21

for s being natural Number holds s choose s = 1

proof end;

theorem Th22: :: NEWTON:22

for s, t being natural Number holds (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)

proof end;

theorem Th23: :: NEWTON:23

for s being natural Number st s >= 1 holds
s choose 1 = s

proof end;

theorem :: NEWTON:24

for s, t being natural Number st s >= 1 & t = s - 1 holds
s choose t = s

proof end;

theorem Th25: :: NEWTON:25

for r, s being natural Number holds s choose r is Element of NAT

proof 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 end;

registration

let k, n be natural Number ;

cluster n choose k -> natural ;

coherence
n choose k is natural by Th25;

end;

definition

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

end;

definition

let a, b be Real;
let n be natural Number ;

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

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = n + 1 & ( for i, l, m being Nat st i in dom b₁ & m = i - 1 & l = n - m holds
b₁ . i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b₂ = n + 1 & ( for i, l, m being Nat st i in dom b₂ & m = i - 1 & l = n - m holds
b₂ . i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines In_Power NEWTON:def 4 :
for a, b being Real
for n being natural Number
for b₄ being FinSequence of REAL holds
( b₄ = (a,b) In_Power n iff ( len b₄ = n + 1 & ( for i, l, m being Nat st i in dom b₄ & m = i - 1 & l = n - m holds
b₄ . i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

theorem Th27: :: NEWTON:27

for a, b being Real holds (a,b) In_Power 0 = <*1*>

proof end;

theorem Th28: :: NEWTON:28

for a, b being Real
for s being natural Number holds ((a,b) In_Power s) . 1 = a |^ s

proof end;

theorem Th29: :: NEWTON:29

for a, b being Real
for s being natural Number holds ((a,b) In_Power s) . (s + 1) = b |^ s

proof end;

theorem Th30: :: NEWTON:30

for a, b being Real
for s being natural Number holds (a + b) |^ s = Sum ((a,b) In_Power s)

proof end;

definition

let n be natural Number ;

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 b₁ being FinSequence of REAL st
( len b₁ = n + 1 & ( for i, k being Nat st i in dom b₁ & k = i - 1 holds
b₁ . i = n choose k ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = n + 1 & ( for i, k being Nat st i in dom b₁ & k = i - 1 holds
b₁ . i = n choose k ) & len b₂ = n + 1 & ( for i, k being Nat st i in dom b₂ & k = i - 1 holds
b₂ . i = n choose k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Newton_Coeff NEWTON:def 5 :
for n being natural Number
for b₂ being FinSequence of REAL holds
( b₂ = Newton_Coeff n iff ( len b₂ = n + 1 & ( for i, k being Nat st i in dom b₂ & k = i - 1 holds
b₂ . i = n choose k ) ) );

theorem Th31: :: NEWTON:31

for s being natural Number holds Newton_Coeff s = (1,1) In_Power s

proof end;

theorem :: NEWTON:32

for s being natural Number holds 2 |^ s = Sum (Newton_Coeff s)

proof end;

:: from NAT_LAT

theorem Th33: :: NEWTON:33

for k, l being Nat st l >= 1 holds
k * l >= k

proof end;

theorem Th34: :: NEWTON:34

for k, n, l being Nat st l >= 1 & n >= k * l holds
n >= k

proof end;

definition

let n be Nat;
:: original: !
redefine func n ! -> 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 end;

theorem :: NEWTON:36

for n being Nat st n <> 0 holds
(n + 1) / n > 1

proof end;

theorem Th37: :: NEWTON:37

for k being Nat holds k / (k + 1) < 1

proof end;

theorem Th38: :: NEWTON:38

for l being Nat holds l ! >= l

proof end;

theorem Th39: :: NEWTON:39

for n, m being Nat st m <> 1 & m divides n holds
not m divides n + 1

proof end;

theorem Th40: :: NEWTON:40

for j, k being Nat st j <> 0 holds
j divides (j + k) !

proof end;

theorem Th41: :: NEWTON:41

for j, l being Nat st j <= l & j <> 0 holds
j divides l !

proof end;

theorem :: NEWTON:42

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

:: The fundamental properties of lcm, hcf

theorem :: NEWTON:43

for k, n, m being Nat holds m lcm (n lcm k) = (m lcm n) lcm k

proof end;

theorem Th44: :: NEWTON:44

for n, m being Nat holds
( m divides n iff m lcm n = n )

proof end;

theorem :: NEWTON:45

for k, n, m being Nat holds
( ( n divides m & k divides m ) iff n lcm k divides m )

proof end;

theorem :: NEWTON:46

for m being Nat holds m lcm 1 = m

proof end;

theorem Th47: :: NEWTON:47

for n, m being Nat holds m lcm n divides m * n

proof end;

theorem :: NEWTON:48

for k, n, m being Nat holds m gcd (n gcd k) = (m gcd n) gcd k

proof end;

theorem Th49: :: NEWTON:49

for n, m being Nat st n divides m holds
n gcd m = n

proof end;

theorem :: NEWTON:50

for k, n, m being Nat holds
( ( m divides n & m divides k ) iff m divides n gcd k )

proof end;

theorem :: NEWTON:51

for m being Nat holds m gcd 1 = 1

proof end;

theorem :: NEWTON:52

for m being Nat holds m gcd 0 = m

proof end;

theorem Th53: :: NEWTON:53

for n, m being Nat holds (m gcd n) lcm n = n

proof end;

theorem Th54: :: NEWTON:54

for n, m being Nat holds m gcd (m lcm n) = m

proof end;

theorem :: NEWTON:55

for n, m being Nat holds m gcd (m lcm n) = (n gcd m) lcm m

proof end;

theorem :: NEWTON:56

for k, n, m being Nat st m divides n holds
m gcd k divides n gcd k

proof end;

theorem :: NEWTON:57

for k, n, m being Nat st m divides n holds
k gcd m divides k gcd n

proof end;

theorem Th58: :: NEWTON:58

for m, n being Integer st n > 0 holds
n gcd m > 0

proof end;

theorem :: NEWTON:59

for n, m being Nat st m > 0 & n > 0 holds
m lcm n > 0

proof end;

theorem :: NEWTON:60

for k, n, m being Nat holds (n gcd m) lcm (n gcd k) divides n gcd (m lcm k)

proof end;

theorem :: NEWTON:61

for n, m, l being Nat st m divides l holds
m lcm (n gcd l) divides (m lcm n) gcd l

proof end;

theorem :: NEWTON:62

for n, m being Nat holds n gcd m divides n lcm m

proof end;

theorem :: NEWTON:63

for n, m being Nat st 0 < m holds
n mod m = n - (m * (n div m))

proof end;

theorem :: NEWTON:64

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

theorem :: NEWTON:65

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

theorem :: NEWTON:66

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

:: Bezout's identity

theorem :: NEWTON:67

for n, m being Nat ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n by NAT_D:68;

:: 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 b₁ being Subset of NAT st
for n being Nat holds
( n in b₁ iff n is prime )

proof end;

uniqueness
for b₁, b₂ being Subset of NAT st ( for n being Nat holds
( n in b₁ iff n is prime ) ) & ( for n being Nat holds
( n in b₂ iff n is prime ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines SetPrimes NEWTON:def 6 :
for b₁ being Subset of NAT holds
( b₁ = SetPrimes iff for n being Nat holds
( n in b₁ iff n is prime ) );

registration

cluster epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer dim-like prime finite cardinal V57() for Element of NAT ;

existence
ex b₁ being Element of NAT st b₁ is prime by INT_2:28;

cluster epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer dim-like prime finite cardinal for set ;

existence
ex b₁ being Nat st b₁ is prime by INT_2:28;

end;

definition

mode Prime is prime Nat;

end;

definition

let p be natural Number ;

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 b₁ being Subset of NAT st
for q being Nat holds
( q in b₁ iff ( q < p & q is prime ) )

proof end;

uniqueness
for b₁, b₂ being Subset of NAT st ( for q being Nat holds
( q in b₁ iff ( q < p & q is prime ) ) ) & ( for q being Nat holds
( q in b₂ iff ( q < p & q is prime ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines SetPrimenumber NEWTON:def 7 :
for p being natural Number
for b₂ being Subset of NAT holds
( b₂ = SetPrimenumber p iff for q being Nat holds
( q in b₂ iff ( q < p & q is prime ) ) );

theorem Th68: :: NEWTON:68

for p being natural Number holds SetPrimenumber p c= SetPrimes

proof end;

theorem :: NEWTON:69

for p, q being natural Number st p <= q holds
SetPrimenumber p c= SetPrimenumber q

proof end;

theorem Th70: :: NEWTON:70

for p being natural Number holds SetPrimenumber p c= Seg p

proof end;

theorem Th71: :: NEWTON:71

for p being natural Number holds SetPrimenumber p is finite

proof end;

registration

let n be natural Number ;

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 > l

proof end;

Lm1: SetPrimenumber 2 = {}

proof 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 Lm1;

end;

theorem :: NEWTON:73

for m being Nat holds SetPrimenumber m c= Seg m

proof 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 end;

theorem :: NEWTON:77

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

Lm2: for n being Nat holds SetPrimenumber n = { k where k is Element of NAT : ( k < n & k is prime ) }

proof end;

definition

let n be Nat;

func primenumber n -> prime Element of NAT means :Def8: :: NEWTON:def 8
n = card (SetPrimenumber it);

existence
ex b₁ being prime Element of NAT st n = card (SetPrimenumber b₁)

proof end;

uniqueness
for b₁, b₂ being prime Element of NAT st n = card (SetPrimenumber b₁) & n = card (SetPrimenumber b₂) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines primenumber NEWTON:def 8 :
for n being Nat
for b₂ being prime Element of NAT holds
( b₂ = primenumber n iff n = card (SetPrimenumber b₂) );

theorem :: NEWTON:78

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

:: The Infinitude of Primes

theorem Th79: :: NEWTON:79

SetPrimes is infinite

proof end;

registration

cluster SetPrimes -> non empty infinite ;

coherence
( not SetPrimes is empty & 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 )

proof end;

theorem :: NEWTON:81

for x being Complex holds
( x |^ 2 = x * x & x ^2 = x |^ 2 )

proof end;

:: from SCMFSA9A, 2005.11.16, A.T

theorem :: NEWTON:82

for n, m 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 st x > 0 holds
x |^ k > 0

proof end;

:: missing, 2006.07.17, A.T.

theorem :: NEWTON:84

for n being Nat st n > 0 holds
0 |^ n = 0

proof end;

:: from CARD_4 and WSIERP_1, 2007.02.07, AK

definition

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

end;

defpred S₁[ Nat] means for i being Nat st 2 <= i holds
i |^ $1 >= $1 + 1;

Lm3: S₁[ 0 ]
by RVSUM_1:94;

Lm4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof end;

theorem Th85: :: NEWTON:85

for n, i being Nat st 2 <= i holds
i |^ n >= n + 1

proof end;

theorem :: NEWTON:86

for n, i being Nat st 2 <= i holds
i |^ n > n

proof end;

scheme :: NEWTON:sch 1
Euklides9{ F₁( Nat) -> Element of NAT , F₂( Nat) -> Element of NAT , F₃() -> Element of NAT , F₄() -> Element of NAT } :

ex k being Nat st
( F₁(k) = F₃() gcd F₄() & F₂(k) = 0 )

provided

A1: 0 < F₄() and
A2: F₄() < F₃() and
A3: F₁(0) = F₃() and
A4: F₂(0) = F₄() and
A5: for k being Nat st F₂(k) > 0 holds
( F₁((k + 1)) = F₂(k) & F₂((k + 1)) = F₁(k) mod F₂(k) )

proof end;

theorem Th87: :: NEWTON:87

for r being natural Number
for n being Nat holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )

proof end;

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

proof end;

theorem :: NEWTON:88

for n1, n2, m1, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 & m1 = m2 )

proof end;

theorem :: NEWTON:89

for m, k, n being Nat st k <= n holds
m |^ k divides m |^ n

proof end;