:: NEWTON semantic presentation

theorem Th1: :: NEWTON:1

canceled;

theorem Th2: :: NEWTON:2

canceled;

theorem Th3: :: NEWTON:3

for b₁, b₂ being FinSequence st len b₁ = len b₂ & ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th4: :: NEWTON:4

canceled;

theorem Th5: :: NEWTON:5

for b₁ being Nat st b₁ >= 1 holds
Seg b₁ = ({1} \/ { b₂ where B is Nat : ( 1 < b₂ & b₂ < b₁ ) } ) \/ {b₁}

proof end;

theorem Th6: :: NEWTON:6

for b₁ being real number
for b₂ being FinSequence of REAL holds len (b₁ * b₂) = len b₂

proof end;

theorem Th7: :: NEWTON:7

for b₁ being Nat
for b₂ being real number
for b₃ being FinSequence of REAL holds
( b₁ in dom b₃ iff b₁ in dom (b₂ * b₃) )

proof end;

definition

let c₁ be natural number ;
let c₂ be real number ;
redefine func |-> as c₁ |-> c₂ -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let c₁ be real number ;
let c₂ be natural number ;
func c₁ |^ c₂ -> set equals :: NEWTON:def 1
Product (a₂ |-> a₁);
coherence ;

end;

:: deftheorem Def1 defines |^ NEWTON:def 1 :

registration

let c₁ be real number ;
let c₂ be natural number ;
cluster a₁ |^ a₂ -> real ;
coherence ;

end;

definition

let c₁ be Real;
let c₂ be natural number ;
redefine func |^ as c₁ |^ c₂ -> Real;
coherence ;

end;

theorem Th8: :: NEWTON:8

canceled;

theorem Th9: :: NEWTON:9

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

theorem Th10: :: NEWTON:10

for b₁ being real number holds b₁ |^ 1 = b₁

proof end;

theorem Th11: :: NEWTON:11

for b₁ being natural number
for b₂ being real number holds b₂ |^ (b₁ + 1) = (b₂ |^ b₁) * b₂

proof end;

registration

let c₁, c₂ be natural number ;
cluster a₁ |^ a₂ -> natural real ;
coherence

proof end;

end;

theorem Th12: :: NEWTON:12

for b₁ being natural number
for b₂, b₃ being real number holds (b₂ * b₃) |^ b₁ = (b₂ |^ b₁) * (b₃ |^ b₁)

proof end;

theorem Th13: :: NEWTON:13

for b₁, b₂ being natural number
for b₃ being real number holds b₃ |^ (b₁ + b₂) = (b₃ |^ b₁) * (b₃ |^ b₂)

proof end;

theorem Th14: :: NEWTON:14

for b₁, b₂ being natural number
for b₃ being real number holds (b₃ |^ b₁) |^ b₂ = b₃ |^ (b₁ * b₂)

proof end;

theorem Th15: :: NEWTON:15

for b₁ being natural number holds 1 |^ b₁ = 1

proof end;

theorem Th16: :: NEWTON:16

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

proof end;

definition

let c₁ be natural number ;
redefine func idseq as idseq c₁ -> FinSequence of REAL ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def2 defines ! NEWTON:def 2 :

registration

let c₁ be natural number ;
cluster a₁ ! -> real ;
coherence ;

end;

definition

let c₁ be natural number ;
redefine func ! as c₁ ! -> Real;
coherence ;

end;

theorem Th17: :: 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 Th20: :: NEWTON:20

2 ! = 2

proof end;

theorem Th21: :: NEWTON:21

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

proof end;

theorem Th22: :: NEWTON:22

for b₁ being natural number holds b₁ ! is Nat

proof end;

theorem Th23: :: NEWTON:23

for b₁ being natural number holds b₁ ! > 0

proof end;

theorem Th24: :: NEWTON:24

canceled;

theorem Th25: :: NEWTON:25

for b₁, b₂ being natural number holds (b₁ ! ) * (b₂ ! ) <> 0

proof end;

definition

let c₁, c₂ be natural number ;
func c₂ choose c₁ -> set means :Def3: :: NEWTON:def 3
for b₁ being natural number st b₁ = a₂ - a₁ holds
a₃ = (a₂ ! ) / ((a₁ ! ) * (b₁ ! )) if a₂ >= a₁
otherwise a₃ = 0;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines choose NEWTON:def 3 :

registration

let c₁, c₂ be natural number ;
cluster a₂ choose a₁ -> real ;
coherence

proof end;

end;

definition

let c₁, c₂ be natural number ;
redefine func choose as c₂ choose c₁ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th26: :: NEWTON:26

canceled;

theorem Th27: :: NEWTON:27

0 choose 0 = 1

proof end;

theorem Th28: :: NEWTON:28

canceled;

theorem Th29: :: NEWTON:29

for b₁ being natural number holds b₁ choose 0 = 1

proof end;

theorem Th30: :: NEWTON:30

for b₁, b₂ being natural number st b₁ >= b₂ holds
for b₃ being natural number st b₃ = b₁ - b₂ holds
b₁ choose b₂ = b₁ choose b₃

proof end;

theorem Th31: :: NEWTON:31

for b₁ being natural number holds b₁ choose b₁ = 1

proof end;

theorem Th32: :: NEWTON:32

for b₁, b₂ being natural number holds (b₁ + 1) choose (b₂ + 1) = (b₁ choose (b₂ + 1)) + (b₁ choose b₂)

proof end;

theorem Th33: :: NEWTON:33

for b₁ being natural number st b₁ >= 1 holds
b₁ choose 1 = b₁

proof end;

theorem Th34: :: NEWTON:34

for b₁, b₂ being natural number st b₁ >= 1 & b₂ = b₁ - 1 holds
b₁ choose b₂ = b₁

proof end;

theorem Th35: :: NEWTON:35

for b₁, b₂ being natural number holds b₁ choose b₂ is Nat

proof end;

theorem Th36: :: NEWTON:36

for b₁, b₂ being Nat
for b₃ being FinSequence of REAL st b₂ <> 0 & len b₃ = b₂ & ( for b₄, b₅ being Nat st b₄ in dom b₃ & b₅ = (b₁ + b₄) - 1 holds
b₃ . b₄ = b₅ choose b₁ ) holds
Sum b₃ = (b₁ + b₂) choose (b₁ + 1)

proof end;

definition

let c₁, c₂ be real number ;
let c₃ be natural number ;
func c₁,c₂ In_Power c₃ -> FinSequence of REAL means :Def4: :: NEWTON:def 4
( len a₄ = a₃ + 1 & ( for b₁, b₂, b₃ being natural number st b₁ in dom a₄ & b₃ = b₁ - 1 & b₂ = a₃ - b₃ holds
a₄ . b₁ = ((a₃ choose b₃) * (a₁ |^ b₂)) * (a₂ |^ b₃) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines In_Power NEWTON:def 4 :

theorem Th37: :: NEWTON:37

canceled;

theorem Th38: :: NEWTON:38

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

proof end;

theorem Th39: :: NEWTON:39

for b₁ being natural number
for b₂, b₃ being real number holds (b₂,b₃ In_Power b₁) . 1 = b₂ |^ b₁

proof end;

theorem Th40: :: NEWTON:40

for b₁ being natural number
for b₂, b₃ being real number holds (b₂,b₃ In_Power b₁) . (b₁ + 1) = b₃ |^ b₁

proof end;

theorem Th41: :: NEWTON:41

for b₁, b₂ being real number
for b₃ being natural number holds (b₁ + b₂) |^ b₃ = Sum (b₁,b₂ In_Power b₃)

proof end;

definition

let c₁ be natural number ;
func Newton_Coeff c₁ -> FinSequence of REAL means :Def5: :: NEWTON:def 5
( len a₂ = a₁ + 1 & ( for b₁, b₂ being natural number st b₁ in dom a₂ & b₂ = b₁ - 1 holds
a₂ . b₁ = a₁ choose b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Newton_Coeff NEWTON:def 5 :

theorem Th42: :: NEWTON:42

canceled;

theorem Th43: :: NEWTON:43

for b₁ being natural number holds Newton_Coeff b₁ = 1,1 In_Power b₁

proof end;

theorem Th44: :: NEWTON:44

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

proof end;

theorem Th45: :: NEWTON:45

for b₁, b₂ being Nat st b₁ >= 1 holds
b₂ * b₁ >= b₂

proof end;

theorem Th46: :: NEWTON:46

for b₁, b₂, b₃ being Nat st b₁ >= 1 & b₂ >= b₃ * b₁ holds
b₂ >= b₃

proof end;

definition

let c₁ be Nat;
redefine func ! as c₁ ! -> Nat;
coherence by Th22;

end;

theorem Th47: :: NEWTON:47

for b₁ being Nat st b₁ <> 0 holds
b₁ divides b₁ !

proof end;

theorem Th48: :: NEWTON:48

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

proof end;

theorem Th49: :: NEWTON:49

for b₁ being Nat holds b₁ / (b₁ + 1) < 1

proof end;

theorem Th50: :: NEWTON:50

for b₁ being Nat holds b₁ ! >= b₁

proof end;

theorem Th51: :: NEWTON:51

for b₁, b₂ being Nat st b₁ <> 1 & b₁ divides b₂ holds
not b₁ divides b₂ + 1

proof end;

theorem Th52: :: NEWTON:52

for b₁, b₂ being Nat holds
( ( b₂ divides b₁ & b₂ divides b₁ + 1 ) iff b₂ = 1 ) by Th51, NAT_1:53;

theorem Th53: :: NEWTON:53

for b₁, b₂ being Nat st b₂ <> 0 holds
b₂ divides (b₂ + b₁) !

proof end;

theorem Th54: :: NEWTON:54

for b₁, b₂ being Nat st b₂ <= b₁ & b₂ <> 0 holds
b₂ divides b₁ !

proof end;

theorem Th55: :: NEWTON:55

for b₁, b₂ being Nat st b₂ <> 1 & b₂ <> 0 & b₂ divides (b₁ ! ) + 1 holds
b₂ > b₁

proof end;

theorem Th56: :: NEWTON:56

for b₁, b₂, b₃ being Nat holds b₁ lcm (b₂ lcm b₃) = (b₁ lcm b₂) lcm b₃

proof end;

theorem Th57: :: NEWTON:57

for b₁, b₂ being Nat holds
( b₁ divides b₂ iff b₁ lcm b₂ = b₂ )

proof end;

theorem Th58: :: NEWTON:58

for b₁, b₂, b₃ being Nat holds
( ( b₁ divides b₂ & b₃ divides b₂ ) iff b₁ lcm b₃ divides b₂ )

proof end;

theorem Th59: :: NEWTON:59

for b₁ being Nat holds b₁ lcm 1 = b₁

proof end;

theorem Th60: :: NEWTON:60

for b₁, b₂ being Nat holds b₁ lcm b₂ divides b₁ * b₂

proof end;

theorem Th61: :: NEWTON:61

for b₁, b₂, b₃ being Nat holds b₁ hcf (b₂ hcf b₃) = (b₁ hcf b₂) hcf b₃

proof end;

theorem Th62: :: NEWTON:62

for b₁, b₂ being Nat st b₁ divides b₂ holds
b₁ hcf b₂ = b₁

proof end;

theorem Th63: :: NEWTON:63

for b₁, b₂, b₃ being Nat holds
( ( b₁ divides b₂ & b₁ divides b₃ ) iff b₁ divides b₂ hcf b₃ )

proof end;

theorem Th64: :: NEWTON:64

for b₁ being Nat holds b₁ hcf 1 = 1

proof end;

theorem Th65: :: NEWTON:65

for b₁ being Nat holds b₁ hcf 0 = b₁

proof end;

theorem Th66: :: NEWTON:66

for b₁, b₂ being Nat holds (b₁ hcf b₂) lcm b₂ = b₂

proof end;

theorem Th67: :: NEWTON:67

for b₁, b₂ being Nat holds b₁ hcf (b₁ lcm b₂) = b₁

proof end;

theorem Th68: :: NEWTON:68

for b₁, b₂ being Nat holds b₁ hcf (b₁ lcm b₂) = (b₂ hcf b₁) lcm b₁

proof end;

theorem Th69: :: NEWTON:69

for b₁, b₂, b₃ being Nat st b₁ divides b₂ holds
b₁ hcf b₃ divides b₂ hcf b₃

proof end;

theorem Th70: :: NEWTON:70

for b₁, b₂, b₃ being Nat st b₁ divides b₂ holds
b₃ hcf b₁ divides b₃ hcf b₂

proof end;

theorem Th71: :: NEWTON:71

for b₁, b₂ being Nat st b₁ > 0 holds
b₁ hcf b₂ > 0

proof end;

theorem Th72: :: NEWTON:72

canceled;

theorem Th73: :: NEWTON:73

for b₁, b₂ being Nat st b₁ > 0 & b₂ > 0 holds
b₁ lcm b₂ > 0

proof end;

theorem Th74: :: NEWTON:74

for b₁, b₂, b₃ being Nat holds (b₁ hcf b₂) lcm (b₁ hcf b₃) divides b₁ hcf (b₂ lcm b₃)

proof end;

theorem Th75: :: NEWTON:75

for b₁, b₂, b₃ being Nat st b₁ divides b₂ holds
b₁ lcm (b₃ hcf b₂) divides (b₁ lcm b₃) hcf b₂

proof end;

theorem Th76: :: NEWTON:76

for b₁, b₂ being Nat holds b₁ hcf b₂ divides b₁ lcm b₂

proof end;

theorem Th77: :: NEWTON:77

for b₁, b₂ being Nat st 0 < b₂ holds
b₁ mod b₂ = b₁ - (b₂ * (b₁ div b₂))

proof end;

theorem Th78: :: NEWTON:78

for b₁, b₂ being Integer st b₁ >= 0 holds
b₂ mod b₁ >= 0

proof end;

theorem Th79: :: NEWTON:79

for b₁, b₂ being Integer st b₁ > 0 holds
b₂ mod b₁ < b₁

proof end;

theorem Th80: :: NEWTON:80

for b₁, b₂ being Integer st b₁ <> 0 holds
b₂ = ((b₂ div b₁) * b₁) + (b₂ mod b₁)

proof end;

theorem Th81: :: NEWTON:81

for b₁, b₂ being Nat st ( b₁ > 0 or b₂ > 0 ) holds
ex b₃, b₄ being Integer st (b₃ * b₁) + (b₄ * b₂) = b₁ hcf b₂

proof end;

definition

func SetPrimes -> Subset of NAT means :Def6: :: NEWTON:def 6
for b₁ being Nat holds
( b₁ in a₁ iff b₁ 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 c₁ be Nat;
func SetPrimenumber c₁ -> Subset of NAT means :Def7: :: NEWTON:def 7
for b₁ being Nat holds
( b₁ in a₂ iff ( b₁ < a₁ & b₁ is prime ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines SetPrimenumber NEWTON:def 7 :

theorem Th82: :: NEWTON:82

for b₁ being Nat holds SetPrimenumber b₁ c= SetPrimes

proof end;

theorem Th83: :: NEWTON:83

for b₁, b₂ being Nat st b₁ < b₂ holds
SetPrimenumber b₁ c= SetPrimenumber b₂

proof end;

theorem Th84: :: NEWTON:84

for b₁ being Nat holds SetPrimenumber b₁ c= Seg b₁

proof end;

theorem Th85: :: NEWTON:85

for b₁ being Nat holds SetPrimenumber b₁ is finite

proof end;

Lemma50: for b₁ being Nat holds
( b₁ = 0 or b₁ = 1 or 2 <= b₁ )

proof end;

theorem Th86: :: NEWTON:86

for b₁ being Nat ex b₂ being Prime st
( b₂ is prime & b₂ > b₁ )

proof end;

theorem Th87: :: NEWTON:87

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

theorem Th88: :: NEWTON:88

{ b₁ where B is Nat : ( b₁ < 2 & b₁ is prime ) } = {}

proof end;

theorem Th89: :: NEWTON:89

for b₁ being Prime holds { b₂ where B is Nat : ( b₂ < b₁ & b₂ is prime ) } c= NAT

proof end;

theorem Th90: :: NEWTON:90

for b₁ being Nat holds { b₂ where B is Nat : ( b₂ < b₁ & b₂ is prime ) } c= Seg b₁

proof end;

theorem Th91: :: NEWTON:91

for b₁ being Nat holds { b₂ where B is Nat : ( b₂ < b₁ & b₂ is prime ) } is finite

proof end;

theorem Th92: :: NEWTON:92

for b₁ being Nat holds not b₁ in { b₂ where B is Nat : ( b₂ < b₁ & b₂ is prime ) }

proof end;

theorem Th93: :: NEWTON:93

for b₁ being Nat holds { b₂ where B is Nat : ( b₂ < b₁ & b₂ is prime ) } \/ {b₁} is finite

proof end;

theorem Th94: :: NEWTON:94

for b₁, b₂ being Prime st b₁ < b₂ holds
{ b₃ where B is Nat : ( b₃ < b₁ & b₃ is prime ) } \/ {b₁} c= { b₃ where B is Nat : ( b₃ < b₂ & b₃ is prime ) }

proof end;

theorem Th95: :: NEWTON:95

for b₁, b₂ being Nat st b₂ > b₁ holds
not b₂ in { b₃ where B is Nat : ( b₃ < b₁ & b₃ is prime ) }

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines primenumber NEWTON:def 8 :

theorem Th96: :: NEWTON:96

for b₁ being Prime holds SetPrimenumber b₁ = { b₂ where B is Nat : ( b₂ < b₁ & b₂ is prime ) }

proof end;

theorem Th97: :: NEWTON:97

not SetPrimes is finite

proof end;

registration

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

end;

Lemma60: for b₁ being Nat st b₁ is prime holds
b₁ > 0
by INT_2:def 5;

theorem Th98: :: NEWTON:98

for b₁ being Nat st b₁ is prime holds
for b₂, b₃ being Nat holds
( not b₁ divides b₂ * b₃ or b₁ divides b₂ or b₁ divides b₃ )

proof end;

theorem Th99: :: NEWTON:99

for b₁, b₂ being Nat holds b₂ |^ b₁ is Nat

proof end;

theorem Th100: :: NEWTON:100

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

proof end;

theorem Th101: :: NEWTON:101

for b₁, b₂ being natural number holds
( b₁ div b₂ = b₁ div b₂ & b₁ mod b₂ = b₁ mod b₂ )

proof end;