:: NEWTON semantic presentation

theorem :: NEWTON:1

canceled;

theorem :: NEWTON:2

canceled;

theorem Th3: :: NEWTON:3

for F, G being FinSequence st len F = len G & ( for i being Nat st i in dom F holds
F . i = G . i ) holds
F = G

proof end;

theorem :: NEWTON:4

canceled;

theorem Th5: :: NEWTON:5

for n being Nat st n >= 1 holds
Seg n = ({1} \/ { k where k is Nat : ( 1 < k & k < n ) } ) \/ {n}

proof end;

theorem Th6: :: NEWTON:6

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

proof end;

theorem Th7: :: NEWTON:7

for n being Nat
for a being real number
for G being FinSequence of REAL holds
( n in dom G iff n in dom (a * G) )

proof end;

definition

let i be natural number ;
let x be real number ;
:: original: |->
redefine func i |-> x -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let x be real number ;
let n be natural number ;
func x |^ n -> set equals :: NEWTON:def 1
Product (n |-> x);
coherence ;

end;

:: deftheorem defines |^ NEWTON:def 1 :

registration

let x be real number ;
let n be natural number ;
cluster x |^ n -> real ;
coherence ;

end;

definition

let x be Real;
let n be natural number ;
:: original: |^
redefine func x |^ n -> Real;
coherence ;

end;

theorem :: NEWTON:8

canceled;

theorem Th9: :: NEWTON:9

for x being real number holds x |^ 0 = 1 by FINSEQ_2:72, RVSUM_1:124;

theorem Th10: :: NEWTON:10

for x being real number holds x |^ 1 = x

proof end;

theorem Th11: :: NEWTON:11

for s being natural number
for x being real number holds x |^ (s + 1) = (x |^ s) * x

proof end;

registration

let x, n be natural number ;
cluster x |^ n -> natural real ;
coherence

proof end;

end;

theorem :: NEWTON:12

for s being natural number
for x, y being real number holds (x * y) |^ s = (x |^ s) * (y |^ s)

proof end;

theorem :: NEWTON:13

for s, t being natural number
for x being real number holds x |^ (s + t) = (x |^ s) * (x |^ t)

proof end;

theorem :: NEWTON:14

for s, t being natural number
for x being real number holds (x |^ s) |^ t = x |^ (s * t)

proof end;

theorem Th15: :: NEWTON:15

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

proof end;

theorem :: NEWTON:16

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

proof end;

definition

let n be natural number ;
:: original: idseq
redefine func idseq n -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let n be natural number ;
func n ! -> set equals :: NEWTON:def 2
Product (idseq n);
coherence ;

end;

:: deftheorem defines ! NEWTON:def 2 :

registration

let n be natural number ;
cluster n ! -> real ;
coherence ;

end;

definition

let n be natural number ;
:: original: !
redefine func n ! -> Real;
coherence ;

end;

theorem :: NEWTON:17

canceled;

theorem Th18: :: NEWTON:18

0 ! = 1 by FINSEQ_2:58, RVSUM_1:124;

theorem Th19: :: NEWTON:19

1 ! = 1 by FINSEQ_2:59, RVSUM_1:125;

theorem :: NEWTON:20

2 ! = 2

proof end;

theorem Th21: :: NEWTON:21

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

proof end;

theorem Th22: :: NEWTON:22

for s being natural number holds s ! is Nat

proof end;

theorem Th23: :: NEWTON:23

for s being natural number holds s ! > 0

proof end;

theorem :: NEWTON:24

canceled;

theorem Th25: :: NEWTON:25

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

proof end;

definition

let k, n be natural number ;
func n choose k -> set means :Def3: :: NEWTON:def 3
for l being natural number st l = n - k holds
it = (n ! ) / ((k ! ) * (l ! )) if n >= k
otherwise it = 0;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines choose NEWTON:def 3 :

registration

let k, n be natural number ;
cluster n choose k -> real ;
coherence

proof end;

end;

definition

let k, n be natural number ;
:: original: choose
redefine func n choose k -> Real;
coherence by XREAL_0:def 1;

end;

theorem :: NEWTON:26

canceled;

theorem Th27: :: NEWTON:27

0 choose 0 = 1

proof end;

theorem :: NEWTON:28

canceled;

theorem Th29: :: NEWTON:29

for s being natural number holds s choose 0 = 1

proof end;

theorem Th30: :: NEWTON:30

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

proof end;

theorem Th31: :: NEWTON:31

for s being natural number holds s choose s = 1

proof end;

theorem Th32: :: NEWTON:32

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

proof end;

theorem Th33: :: NEWTON:33

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

proof end;

theorem :: NEWTON:34

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

proof end;

theorem :: NEWTON:35

for s, r being natural number holds s choose r is Nat

proof end;

theorem :: NEWTON:36

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;

definition

let a, b be real number ;
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 natural number st i in dom it & m = i - 1 & l = n - m holds
it . i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines In_Power NEWTON:def 4 :

theorem :: NEWTON:37

canceled;

theorem Th38: :: NEWTON:38

for a, b being real number holds a,b In_Power 0 = <*1*>

proof end;

theorem Th39: :: NEWTON:39

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

proof end;

theorem Th40: :: NEWTON:40

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

proof end;

theorem Th41: :: NEWTON:41

for a, b being real number
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 natural number st i in dom it & k = i - 1 holds
it . i = n choose k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Newton_Coeff NEWTON:def 5 :

theorem :: NEWTON:42

canceled;

theorem Th43: :: NEWTON:43

for s being natural number holds Newton_Coeff s = 1,1 In_Power s

proof end;

theorem :: NEWTON:44

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

proof end;

theorem Th45: :: NEWTON:45

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

proof end;

theorem Th46: :: NEWTON:46

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

proof end;

definition

let n be Nat;
:: original: !
redefine func n ! -> Nat;
coherence by Th22;

end;

theorem Th47: :: NEWTON:47

for l being Nat st l <> 0 holds
l divides l !

proof end;

theorem :: NEWTON:48

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

proof end;

theorem Th49: :: NEWTON:49

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

proof end;

theorem Th50: :: NEWTON:50

for l being Nat holds l ! >= l

proof end;

theorem Th51: :: NEWTON:51

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

proof end;

theorem :: NEWTON:52

for l, j being Nat holds
( ( j divides l & j divides l + 1 ) iff j = 1 ) by Th51, NAT_1:53;

theorem Th53: :: NEWTON:53

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

proof end;

theorem Th54: :: NEWTON:54

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

proof end;

theorem Th55: :: NEWTON:55

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

proof end;

theorem :: NEWTON:56

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

proof end;

theorem Th57: :: NEWTON:57

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

proof end;

theorem :: NEWTON:58

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

proof end;

theorem :: NEWTON:59

for m being Nat holds m lcm 1 = m

proof end;

theorem Th60: :: NEWTON:60

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

proof end;

theorem :: NEWTON:61

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

proof end;

theorem Th62: :: NEWTON:62

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

proof end;

theorem :: NEWTON:63

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

proof end;

theorem :: NEWTON:64

for m being Nat holds m hcf 1 = 1

proof end;

theorem :: NEWTON:65

for m being Nat holds m hcf 0 = m

proof end;

theorem Th66: :: NEWTON:66

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

proof end;

theorem Th67: :: NEWTON:67

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

proof end;

theorem :: NEWTON:68

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

proof end;

theorem :: NEWTON:69

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

proof end;

theorem :: NEWTON:70

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

proof end;

theorem :: NEWTON:71

for n, m being Nat st n > 0 holds
n hcf m > 0

proof end;

theorem :: NEWTON:72

canceled;

theorem :: NEWTON:73

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

proof end;

theorem :: NEWTON:74

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

proof end;

theorem :: NEWTON:75

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

proof end;

theorem :: NEWTON:76

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

proof end;

theorem :: NEWTON:77

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

proof end;

theorem Th78: :: NEWTON:78

for i2, i1 being Integer st i2 >= 0 holds
i1 mod i2 >= 0

proof end;

theorem Th79: :: NEWTON:79

for i2, i1 being Integer st i2 > 0 holds
i1 mod i2 < i2

proof end;

theorem Th80: :: NEWTON:80

for i2, i1 being Integer st i2 <> 0 holds
i1 = ((i1 div i2) * i2) + (i1 mod i2)

proof end;

theorem :: NEWTON:81

for m, n being Nat st ( m > 0 or n > 0 ) holds
ex i, i1 being Integer st (i * m) + (i1 * n) = m hcf n

proof 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines SetPrimes NEWTON:def 6 :

registration

cluster prime Element of NAT ;
existence by INT_2:44;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines SetPrimenumber NEWTON:def 7 :

theorem Th82: :: NEWTON:82

for p being Nat holds SetPrimenumber p c= SetPrimes

proof end;

theorem :: NEWTON:83

for p, q being Nat st p < q holds
SetPrimenumber p c= SetPrimenumber q

proof end;

theorem Th84: :: NEWTON:84

for p being Nat holds SetPrimenumber p c= Seg p

proof end;

theorem :: NEWTON:85

for p being Nat holds SetPrimenumber p is finite

proof end;

Lm1: for k being Nat holds
( k = 0 or k = 1 or 2 <= k )

proof end;

theorem Th86: :: NEWTON:86

for l being Nat ex p being Prime st
( p is prime & p > l )

proof end;

theorem :: NEWTON:87

SetPrimes <> {} by Def6, INT_2:44;

theorem Th88: :: NEWTON:88

{ k where k is Nat : ( k < 2 & k is prime ) } = {}

proof end;

theorem :: NEWTON:89

for p being Prime holds { k where k is Nat : ( k < p & k is prime ) } c= NAT

proof end;

theorem Th90: :: NEWTON:90

for m being Nat holds { k where k is Nat : ( k < m & k is prime ) } c= Seg m

proof end;

theorem Th91: :: NEWTON:91

for m being Nat holds { k where k is Nat : ( k < m & k is prime ) } is finite

proof end;

theorem Th92: :: NEWTON:92

for f being Nat holds not f in { k where k is Nat : ( k < f & k is prime ) }

proof end;

theorem :: NEWTON:93

for f being Nat holds { k where k is Nat : ( k < f & k is prime ) } \/ {f} is finite

proof end;

theorem Th94: :: NEWTON:94

for f, g being Prime st f < g holds
{ k1 where k1 is Nat : ( k1 < f & k1 is prime ) } \/ {f} c= { k2 where k2 is Nat : ( k2 < g & k2 is prime ) }

proof end;

theorem :: NEWTON:95

for m, k being Nat st k > m holds
not k in { k1 where k1 is Nat : ( k1 < m & k1 is prime ) }

proof end;

definition

let n be Nat;
func primenumber n -> Prime means :Def8: :: NEWTON:def 8
ex B being finite set st
( B = { k where k is Nat : ( k < it & k is prime ) } & n = card B );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines primenumber NEWTON:def 8 :

theorem Th96: :: NEWTON:96

for p being Prime holds SetPrimenumber p = { k where k is Nat : ( k < p & k is prime ) }

proof end;

theorem Th97: :: NEWTON:97

not SetPrimes is finite

proof end;

registration

cluster SetPrimes -> non empty infinite ;
coherence by Th97;

end;

Lm2: for n being Nat st n is prime holds
n > 0
by INT_2:def 5;

theorem :: NEWTON:98

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

for n, m being Nat holds m |^ n is Nat

proof end;

theorem :: NEWTON:100

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

proof end;

theorem :: NEWTON:101

for m, n being natural number holds
( m div n = m div n & m mod n = m mod n )

proof end;