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

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

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

for G being FinSequence of REAL holds dom G = dom (a * G) by VALUED_1:def 5;

:: x |^ n Function

:: deftheorem defines |^ NEWTON:def 1 :

for x being complex number

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

for x being complex number

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

registration
end;

definition

let x be Real;

let n be Nat;

:: original: |^

redefine func x |^ n -> Real;

coherence

x |^ n is Real by XREAL_0:def 1;

end;
let n be Nat;

:: original: |^

redefine func x |^ n -> Real;

coherence

x |^ n is Real by XREAL_0:def 1;

registration
end;

registration
end;

:: n! Function

registration
end;

:: n choose k Function

definition

let k, n be Nat;

for b_{1} being set holds verum
;

existence

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

for l being Nat st l = n - k holds

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

for b_{1}, b_{2} being set 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 -> 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 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 Nat

for b_{3} being set 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 Nat

for b

( ( n >= k implies ( b

b

registration
end;

definition

let k, n be Nat;

:: original: choose

redefine func n choose k -> Real;

coherence

n choose k is Real by XREAL_0:def 1;

end;
:: original: choose

redefine func n choose k -> Real;

coherence

n choose k is Real by XREAL_0:def 1;

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;

registration
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 number ;

let n be Nat;

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 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 ( 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 number

for n being Nat

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 number

for n being Nat

for b

( b

b

definition

let n be Nat;

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 Nat

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 Nat

for b

( b

b

begin

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

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

ex i, i1 being Integer st (i * m) + (i1 * n) = m gcd n

proof end;

:: 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 prime V35() finite cardinal V61() V62() V63() V64() V65() V66() for Element of NAT ;

existence ex b

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

existence ex b

definition

let p be Nat;

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 Nat

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 Nat

for b

( b

( q in b

registration
end;

Lm2: SetPrimenumber 2 = {}

proof end;

registration
end;

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

Lm4: S

by RVSUM_1:94;

Lm5: 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 Element of 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 Element of NAT st F

( F

proof end;

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

n1 <= n2

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

( n1 = n2 & m1 = m2 )

proof end;