:: by Rafa{\l} Kwiatek

::

:: Received July 27, 1990

:: Copyright (c) 1990-2017 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}

Seg n = ({1} \/ { k where k is Element of NAT : ( 1 < k & k < n ) } ) \/ {n}

proof end;

theorem :: NEWTON:3

:: x |^ n Function

definition
end;

:: deftheorem defines |^ NEWTON:def 1 :

for x being Complex

for n being natural Number holds x |^ n = Product (n |-> x);

for x being Complex

for n being natural Number holds x |^ n = Product (n |-> x);

registration
end;

registration
end;

:: n! Function

registration
end;

registration
end;

:: n choose k Function

definition

let k, n be natural Number ;

for b_{1} being number holds verum
;

existence

( ( n >= k implies ex b_{1} being number st

for l being Nat st l = n - k holds

b_{1} = (n !) / ((k !) * (l !)) ) & ( not n >= k implies ex b_{1} being number st b_{1} = 0 ) )

for b_{1}, b_{2} being number holds

( ( n >= k & ( for l being Nat st l = n - k holds

b_{1} = (n !) / ((k !) * (l !)) ) & ( for l being Nat st l = n - k holds

b_{2} = (n !) / ((k !) * (l !)) ) implies b_{1} = b_{2} ) & ( not n >= k & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

end;
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 l being Nat st l = n - k holds

it = (n !) / ((k !) * (l !)) if n >= k

otherwise it = 0 ;

for b

existence

( ( n >= k implies ex b

for l being Nat st l = n - k holds

b

proof end;

uniqueness for b

( ( n >= k & ( for l being Nat st l = n - k holds

b

b

proof end;

:: deftheorem Def3 defines choose NEWTON:def 3 :

for k, n being natural Number

for b_{3} being number holds

( ( n >= k implies ( b_{3} = n choose k iff for l being Nat st l = n - k holds

b_{3} = (n !) / ((k !) * (l !)) ) ) & ( not n >= k implies ( b_{3} = n choose k iff b_{3} = 0 ) ) );

for k, n being natural Number

for b

( ( n >= k implies ( b

b

registration
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)

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;

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;
:: original: choose

redefine func n choose k -> Element of NAT ;

coherence

n choose k is Element of NAT by ORDINAL1:def 12;

definition

let a, b be Real;

let n be natural Number ;

ex b_{1} being FinSequence of REAL st

( len b_{1} = n + 1 & ( for i, l, m being Nat st i in dom b_{1} & m = i - 1 & l = n - m holds

b_{1} . i = ((n choose m) * (a |^ l)) * (b |^ m) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = n + 1 & ( for i, l, m being Nat st i in dom b_{1} & m = i - 1 & l = n - m holds

b_{1} . i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b_{2} = n + 1 & ( for i, l, m being Nat st i in dom b_{2} & m = i - 1 & l = n - m holds

b_{2} . i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds

b_{1} = b_{2}

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

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines In_Power NEWTON:def 4 :

for a, b being Real

for n being natural Number

for b_{4} being FinSequence of REAL holds

( b_{4} = (a,b) In_Power n iff ( len b_{4} = n + 1 & ( for i, l, m being Nat st i in dom b_{4} & m = i - 1 & l = n - m holds

b_{4} . i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

for a, b being Real

for n being natural Number

for b

( b

b

definition

let n be natural Number ;

ex b_{1} being FinSequence of REAL st

( len b_{1} = n + 1 & ( for i, k being Nat st i in dom b_{1} & k = i - 1 holds

b_{1} . i = n choose k ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = n + 1 & ( for i, k being Nat st i in dom b_{1} & k = i - 1 holds

b_{1} . i = n choose k ) & len b_{2} = n + 1 & ( for i, k being Nat st i in dom b_{2} & k = i - 1 holds

b_{2} . i = n choose k ) holds

b_{1} = b_{2}

end;
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 ( len it = n + 1 & ( for i, k being Nat st i in dom it & k = i - 1 holds

it . i = n choose k ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines Newton_Coeff NEWTON:def 5 :

for n being natural Number

for b_{2} being FinSequence of REAL holds

( b_{2} = Newton_Coeff n iff ( len b_{2} = n + 1 & ( for i, k being Nat st i in dom b_{2} & k = i - 1 holds

b_{2} . i = n choose k ) ) );

for n being natural Number

for b

( b

b

:: from NAT_LAT

definition

let n be Nat;

:: original: !

redefine func n ! -> Element of NAT ;

coherence

n ! is Element of NAT by Th16;

end;
:: original: !

redefine func n ! -> Element of NAT ;

coherence

n ! is Element of NAT by Th16;

theorem :: NEWTON:42

:: The fundamental properties of lcm, hcf

theorem :: NEWTON:66

theorem :: NEWTON:67

:: from NAT_LAT

definition

ex b_{1} being Subset of NAT st

for n being Nat holds

( n in b_{1} iff n is prime )

for b_{1}, b_{2} being Subset of NAT st ( for n being Nat holds

( n in b_{1} iff n is prime ) ) & ( for n being Nat holds

( n in b_{2} iff n is prime ) ) holds

b_{1} = b_{2}
end;

func SetPrimes -> Subset of NAT means :Def6: :: NEWTON:def 6

for n being Nat holds

( n in it iff n is prime );

existence for n being Nat holds

( n in it iff n is prime );

ex b

for n being Nat holds

( n in b

proof end;

uniqueness for b

( n in b

( n in b

b

proof end;

:: deftheorem Def6 defines SetPrimes NEWTON:def 6 :

for b_{1} being Subset of NAT holds

( b_{1} = SetPrimes iff for n being Nat holds

( n in b_{1} iff n is prime ) );

for b

( b

( n in b

registration

ex b_{1} being Element of NAT st b_{1} is prime
by INT_2:28;

ex b_{1} being Nat st b_{1} is prime
by INT_2:28;

end;

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

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

existence ex b

definition

let p be natural Number ;

ex b_{1} being Subset of NAT st

for q being Nat holds

( q in b_{1} iff ( q < p & q is prime ) )

for b_{1}, b_{2} being Subset of NAT st ( for q being Nat holds

( q in b_{1} iff ( q < p & q is prime ) ) ) & ( for q being Nat holds

( q in b_{2} iff ( q < p & q is prime ) ) ) holds

b_{1} = b_{2}

end;
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 for q being Nat holds

( q in it iff ( q < p & q is prime ) );

ex b

for q being Nat holds

( q in b

proof end;

uniqueness for b

( q in b

( q in b

b

proof end;

:: deftheorem Def7 defines SetPrimenumber NEWTON:def 7 :

for p being natural Number

for b_{2} being Subset of NAT holds

( b_{2} = SetPrimenumber p iff for q being Nat holds

( q in b_{2} iff ( q < p & q is prime ) ) );

for p being natural Number

for b

( b

( q in b

Lm1: SetPrimenumber 2 = {}

proof end;

registration
end;

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;

ex b_{1} being prime Element of NAT st n = card (SetPrimenumber b_{1})

for b_{1}, b_{2} being prime Element of NAT st n = card (SetPrimenumber b_{1}) & n = card (SetPrimenumber b_{2}) holds

b_{1} = b_{2}

end;
func primenumber n -> prime Element of NAT means :Def8: :: NEWTON:def 8

n = card (SetPrimenumber it);

existence n = card (SetPrimenumber it);

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines primenumber NEWTON:def 8 :

for n being Nat

for b_{2} being prime Element of NAT holds

( b_{2} = primenumber n iff n = card (SetPrimenumber b_{2}) );

for n being Nat

for b

( b

theorem :: NEWTON:78

:: 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 )

for m, n being Nat holds

( not i divides m * n or i divides m or i divides n )

proof end;

:: from SCMFSA9A, 2005.11.16, A.T

:: missing, 2006.07.17, A.T.

:: 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;
:: original: |^

redefine func m |^ n -> Element of NAT ;

coherence

m |^ n is Element of NAT by ORDINAL1:def 12;

defpred S

i |^ $1 >= $1 + 1;

Lm3: S

by RVSUM_1:94;

Lm4: for n being Nat st S

S

proof end;

scheme :: NEWTON:sch 1

Euklides9{ F_{1}( Nat) -> Element of NAT , F_{2}( Nat) -> Element of NAT , F_{3}() -> Element of NAT , F_{4}() -> Element of NAT } :

provided

Euklides9{ F

provided

A1:
0 < F_{4}()
and

A2: F_{4}() < F_{3}()
and

A3: F_{1}(0) = F_{3}()
and

A4: F_{2}(0) = F_{4}()
and

A5: for k being Nat st F_{2}(k) > 0 holds

( F_{1}((k + 1)) = F_{2}(k) & F_{2}((k + 1)) = F_{1}(k) mod F_{2}(k) )

A2: F

A3: F

A4: F

A5: for k being Nat st F

( F

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 )

( n1 = n2 & m1 = m2 )

proof end;