:: WSIERP_1 semantic presentation

definition

let c₁ be FinSequence of REAL ;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> Real;
coherence

proof end;

end;

theorem Th1: :: WSIERP_1:1

canceled;

theorem Th2: :: WSIERP_1:2

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

proof end;

theorem Th3: :: WSIERP_1:3

for b₁ being real number
for b₂ being Nat holds
( (- b₁) |^ (2 * b₂) = b₁ |^ (2 * b₂) & (- b₁) |^ ((2 * b₂) + 1) = - (b₁ |^ ((2 * b₂) + 1)) )

proof end;

theorem Th4: :: WSIERP_1:4

canceled;

theorem Th5: :: WSIERP_1:5

for b₁, b₂ being real number
for b₃ being Nat st b₁ >= 0 & b₂ >= 0 & b₃ > 0 & b₁ |^ b₃ = b₂ |^ b₃ holds
b₁ = b₂

proof end;

theorem Th6: :: WSIERP_1:6

for b₁, b₂, b₃ being real number holds
( b₁ > max b₂,b₃ iff ( b₁ > b₂ & b₁ > b₃ ) )

proof end;

Lemma5: for b₁, b₂ being real number holds
( ( b₁ >= 0 implies b₁ + b₂ >= b₂ ) & ( b₁ + b₂ >= b₂ implies b₁ >= 0 ) & ( b₁ > 0 implies b₁ + b₂ > b₂ ) & ( b₁ + b₂ > b₂ implies b₁ > 0 ) & ( b₁ >= 0 implies b₂ >= b₂ - b₁ ) & ( b₂ >= b₂ - b₁ implies b₁ >= 0 ) & ( b₁ > 0 implies b₂ > b₂ - b₁ ) & ( b₂ > b₂ - b₁ implies b₁ > 0 ) )

proof end;

Lemma6: for b₁, b₂, b₃ being real number st b₁ >= 0 & b₂ >= b₃ holds
( b₁ + b₂ >= b₃ & b₂ >= b₃ - b₁ )

proof end;

Lemma7: for b₁, b₂, b₃ being real number st ( ( b₁ >= 0 & b₂ > b₃ ) or ( b₁ > 0 & b₂ >= b₃ ) ) holds
( b₁ + b₂ > b₃ & b₂ > b₃ - b₁ )

proof end;

theorem Th7: :: WSIERP_1:7

for b₁, b₂, b₃ being real number st b₁ <= 0 & b₂ >= b₃ holds
( b₂ - b₁ >= b₃ & b₂ >= b₃ + b₁ ) by XREAL_1:37, XREAL_1:54;

theorem Th8: :: WSIERP_1:8

for b₁, b₂, b₃ being real number st ( ( b₁ <= 0 & b₂ > b₃ ) or ( b₁ < 0 & b₂ >= b₃ ) ) holds
( b₂ > b₃ + b₁ & b₂ - b₁ > b₃ ) by XREAL_1:38, XREAL_1:39, XREAL_1:55, XREAL_1:56;

Lemma8: for b₁, b₂ being Nat holds
( b₁ divides b₂ iff b₁ divides b₂ )

proof end;

Lemma9: for b₁ being Nat holds abs b₁ = b₁
by ABSVALUE:def 1;

registration

let c₁ be Integer;
let c₂ be Nat;
cluster a₁ |^ a₂ -> integer ;
coherence

proof end;

end;

definition

let c₁, c₂ be Nat;
redefine func |^ as c₁ |^ c₂ -> Nat;
coherence by NEWTON:99;

end;

Lemma10: for b₁ being Nat ex b₂ being Nat st
( b₁ = 2 * b₂ or b₁ = (2 * b₂) + 1 )

proof end;

Lemma11: for b₁, b₂, b₃ being Nat st b₁ > 0 & b₂ |^ b₁ = b₃ |^ b₁ holds
b₂ = b₃
by Th5;

theorem Th9: :: WSIERP_1:9

for b₁, b₂, b₃ being Integer st b₁ divides b₂ & b₁ divides b₃ holds
b₁ divides b₂ + b₃

proof end;

theorem Th10: :: WSIERP_1:10

for b₁, b₂, b₃, b₄, b₅ being Integer st b₁ divides b₂ & b₁ divides b₃ holds
b₁ divides (b₂ * b₄) + (b₃ * b₅)

proof end;

Lemma14: for b₁, b₂ being Nat holds b₁ gcd b₂ = b₁ hcf b₂

proof end;

Lemma15: for b₁, b₂ being Nat holds
( b₁,b₂ are_relative_prime iff b₁,b₂ are_relative_prime )

proof end;

theorem Th11: :: WSIERP_1:11

for b₁, b₂, b₃ being Integer st b₁ gcd b₂ = 1 & b₃ gcd b₂ = 1 holds
(b₁ * b₃) gcd b₂ = 1

proof end;

theorem Th12: :: WSIERP_1:12

for b₁, b₂, b₃ being Nat st b₁ hcf b₂ = 1 & b₃ hcf b₂ = 1 holds
(b₁ * b₃) hcf b₂ = 1

proof end;

theorem Th13: :: WSIERP_1:13

for b₁ being Integer holds
( 0 gcd b₁ = abs b₁ & 1 gcd b₁ = 1 )

proof end;

theorem Th14: :: WSIERP_1:14

for b₁ being Integer holds 1,b₁ are_relative_prime

proof end;

theorem Th15: :: WSIERP_1:15

for b₁ being Nat
for b₂, b₃ being Integer st b₂,b₃ are_relative_prime holds
b₂ |^ b₁,b₃ are_relative_prime

proof end;

theorem Th16: :: WSIERP_1:16

for b₁, b₂ being Nat
for b₃, b₄ being Integer st b₃,b₄ are_relative_prime holds
b₃ |^ b₁,b₄ |^ b₂ are_relative_prime

proof end;

theorem Th17: :: WSIERP_1:17

for b₁, b₂ being Nat
for b₃, b₄ being Integer st b₃ gcd b₄ = 1 holds
( b₃ gcd (b₄ |^ b₁) = 1 & (b₃ |^ b₂) gcd (b₄ |^ b₁) = 1 )

proof end;

Lemma23: for b₁, b₂, b₃, b₄ being Nat st b₁ hcf b₂ = 1 holds
( b₁ hcf (b₂ |^ b₃) = 1 & (b₁ |^ b₄) hcf (b₂ |^ b₃) = 1 )

proof end;

theorem Th18: :: WSIERP_1:18

for b₁, b₂ being Integer holds
( abs b₁ divides b₂ iff b₁ divides b₂ )

proof end;

theorem Th19: :: WSIERP_1:19

for b₁, b₂, b₃ being Nat st b₁ divides b₂ holds
b₁ |^ b₃ divides b₂ |^ b₃

proof end;

theorem Th20: :: WSIERP_1:20

for b₁ being Nat st b₁ divides 1 holds
b₁ = 1

proof end;

theorem Th21: :: WSIERP_1:21

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

proof end;

Lemma27: for b₁, b₂ being Nat st b₁ <> 0 holds
( b₁ divides b₂ iff b₂ / b₁ is Nat )

proof end;

theorem Th22: :: WSIERP_1:22

for b₁, b₂ being Integer st b₁ <> 0 holds
( b₁ divides b₂ iff b₂ / b₁ is Integer )

proof end;

Lemma28: for b₁, b₂ being Nat
for b₃ being Integer st b₁ <> 0 & b₂ * b₃ = b₁ holds
b₃ is Nat

proof end;

Lemma29: for b₁ being Nat
for b₂ being Integer st b₁ <= b₂ holds
b₂ is Nat
by INT_1:16;

Lemma30: for b₁, b₂, b₃ being Nat st b₁ + b₂ <= b₃ holds
( b₁ <= b₃ & b₂ <= b₃ )

proof end;

theorem Th23: :: WSIERP_1:23

for b₁, b₂, b₃ being Nat st b₁ <= b₂ - b₃ holds
( b₁ <= b₂ & b₃ <= b₂ )

proof end;

Lemma31: for b₁, b₂ being Integer holds
( b₁ < b₂ iff b₁ <= b₂ - 1 )

proof end;

Lemma32: for b₁, b₂ being Integer holds
( b₁ < b₂ + 1 iff b₁ <= b₂ )

proof end;

Lemma33: for b₁ being real number
for b₂ being Function holds
( ( b₁ in dom b₂ & b₂ . b₁ in rng b₂ ) or b₂ . b₁ = {} )

proof end;

Lemma34: for b₁ being Nat
for b₂ being set st 0 in b₂ holds
for b₃ being FinSequence of b₂ holds b₃ . b₁ is Element of b₂

proof end;

registration

let c₁ be FinSequence of INT ;
let c₂ be set ;
cluster a₁ . a₂ -> integer ;
coherence

proof end;

end;

definition

let c₁ be FinSequence of NAT ;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> Nat;
coherence by Lemma34;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of c₁;
let c₃, c₄ be FinSequence of c₂;
redefine func ^ as c₃ ^ c₄ -> FinSequence of a₂;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of c₁;
redefine func <*> as <*> c₂ -> empty FinSequence of a₂;
coherence ;

end;

definition

redefine func INT as INT -> non empty Subset of REAL ;
coherence by NUMBERS:15;

end;

definition

let c₁ be FinSequence of INT ;
redefine func Sum as Sum c₁ -> Element of INT ;
coherence

proof end;

redefine func Product as Product c₁ -> Element of INT ;
coherence

proof end;

end;

definition

let c₁ be FinSequence of NAT ;
redefine func Sum as Sum c₁ -> Nat;
coherence

proof end;

redefine func Product as Product c₁ -> Nat;
coherence

proof end;

end;

Lemma35: for b₁ being Nat
for b₂ being FinSequence st b₁ in dom b₂ holds
ex b₃, b₄ being FinSequence st
( b₂ = (b₃ ^ <*(b₂ . b₁)*>) ^ b₄ & len b₃ = b₁ - 1 & len b₄ = (len b₂) - b₁ )

proof end;

definition

let c₁ be Nat;
let c₂ be FinSequence;
redefine func Del c₂,c₁ -> set means :Def1: :: WSIERP_1:def 1
a₃ = a₂ if not a₁ in dom a₂
otherwise ( (len a₃) + 1 = len a₂ & ( for b₁ being Nat holds
( ( b₁ < a₁ implies a₃ . b₁ = a₂ . b₁ ) & ( b₁ >= a₁ implies a₃ . b₁ = a₂ . (b₁ + 1) ) ) ) );
compatibility

proof end;

correctness ;

end;

:: deftheorem Def1 defines Del WSIERP_1:def 1 :

Lemma37: for b₁ being Nat
for b₂, b₃, b₄ being FinSequence
for b₅ being set st b₁ in dom b₂ & b₂ = (b₃ ^ <*b₅*>) ^ b₄ & len b₃ = b₁ - 1 holds
Del b₂,b₁ = b₃ ^ b₄

proof end;

Lemma38: for b₁ being Nat
for b₂ being FinSequence holds dom (Del b₂,b₁) c= dom b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be FinSequence of c₁;
redefine func Del as Del c₃,c₂ -> FinSequence of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of c₁;
let c₃ be Nat;
let c₄ be FinSequence of c₂;
redefine func Del as Del c₄,c₃ -> FinSequence of a₂;
coherence

proof end;

end;

Lemma39: for b₁ being Nat
for b₂, b₃ being FinSequence holds
( ( b₁ <= len b₂ implies Del (b₂ ^ b₃),b₁ = (Del b₂,b₁) ^ b₃ ) & ( b₁ >= 1 implies Del (b₂ ^ b₃),((len b₂) + b₁) = b₂ ^ (Del b₃,b₁) ) )

proof end;

Lemma40: for b₁ being FinSequence
for b₂ being set holds
( Del (<*b₂*> ^ b₁),1 = b₁ & Del (b₁ ^ <*b₂*>),((len b₁) + 1) = b₁ )

proof end;

theorem Th24: :: WSIERP_1:24

canceled;

theorem Th25: :: WSIERP_1:25

canceled;

theorem Th26: :: WSIERP_1:26

for b₁, b₂, b₃ being set holds
( Del <*b₁*>,1 = {} & Del <*b₁,b₂*>,1 = <*b₂*> & Del <*b₁,b₂*>,2 = <*b₁*> & Del <*b₁,b₂,b₃*>,1 = <*b₂,b₃*> & Del <*b₁,b₂,b₃*>,2 = <*b₁,b₃*> & Del <*b₁,b₂,b₃*>,3 = <*b₁,b₂*> )

proof end;

Lemma41: for b₁ being FinSequence st 1 <= len b₁ holds
( b₁ = <*(b₁ . 1)*> ^ (Del b₁,1) & b₁ = (Del b₁,(len b₁)) ^ <*(b₁ . (len b₁))*> )

proof end;

Lemma42: for b₁ being Nat
for b₂ being FinSequence of REAL st b₁ in dom b₂ holds
(Product (Del b₂,b₁)) * (b₂ . b₁) = Product b₂

proof end;

theorem Th27: :: WSIERP_1:27

for b₁ being Nat
for b₂ being FinSequence of REAL st b₁ in dom b₂ holds
(Sum (Del b₂,b₁)) + (b₂ . b₁) = Sum b₂

proof end;

theorem Th28: :: WSIERP_1:28

for b₁ being Nat
for b₂ being FinSequence of NAT st b₁ in dom b₂ holds
(Product b₂) / (b₂ . b₁) is Nat

proof end;

theorem Th29: :: WSIERP_1:29

for b₁ being Rational holds numerator b₁, denominator b₁ are_relative_prime

proof end;

theorem Th30: :: WSIERP_1:30

for b₁ being Nat
for b₂ being Integer
for b₃ being Rational st b₃ <> 0 & b₃ = b₂ / b₁ & b₁ <> 0 & b₂,b₁ are_relative_prime holds
( b₂ = numerator b₃ & b₁ = denominator b₃ )

proof end;

theorem Th31: :: WSIERP_1:31

for b₁, b₂ being Nat st ex b₃ being Rational st b₁ = b₃ |^ b₂ holds
ex b₃ being Integer st b₁ = b₃ |^ b₂

proof end;

theorem Th32: :: WSIERP_1:32

for b₁, b₂ being Nat st ex b₃ being Rational st b₁ = b₃ |^ b₂ holds
ex b₃ being Nat st b₁ = b₃ |^ b₂

proof end;

theorem Th33: :: WSIERP_1:33

for b₁, b₂, b₃ being Nat st b₁ > 0 & b₂ |^ b₁ divides b₃ |^ b₁ holds
b₂ divides b₃

proof end;

theorem Th34: :: WSIERP_1:34

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

proof end;

theorem Th35: :: WSIERP_1:35

for b₁, b₂ being Integer ex b₃, b₄ being Integer st b₁ gcd b₂ = (b₁ * b₃) + (b₂ * b₄)

proof end;

theorem Th36: :: WSIERP_1:36

for b₁, b₂, b₃ being Integer st b₁ divides b₂ * b₃ & b₁ gcd b₂ = 1 holds
b₁ divides b₃

proof end;

theorem Th37: :: WSIERP_1:37

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

proof end;

theorem Th38: :: WSIERP_1:38

for b₁, b₂ being Nat st b₁ <> 0 & b₂ <> 0 holds
ex b₃, b₄ being Nat st b₁ hcf b₂ = (b₁ * b₃) - (b₂ * b₄)

proof end;

theorem Th39: :: WSIERP_1:39

for b₁, b₂, b₃, b₄ being Nat st b₁ > 0 & b₂ > 0 & b₁ hcf b₂ = 1 & b₃ |^ b₁ = b₄ |^ b₂ holds
ex b₅ being Nat st
( b₃ = b₅ |^ b₂ & b₄ = b₅ |^ b₁ )

proof end;

theorem Th40: :: WSIERP_1:40

for b₁, b₂, b₃ being Integer holds
( ex b₄, b₅ being Integer st (b₁ * b₄) + (b₂ * b₅) = b₃ iff b₁ gcd b₂ divides b₃ )

proof end;

theorem Th41: :: WSIERP_1:41

for b₁, b₂, b₃, b₄, b₅ being Integer st b₁ <> 0 & b₂ <> 0 & (b₁ * b₃) + (b₂ * b₄) = b₅ holds
for b₆, b₇ being Integer st (b₁ * b₆) + (b₂ * b₇) = b₅ holds
ex b₈ being Integer st
( b₆ = b₃ + (b₈ * (b₂ / (b₁ gcd b₂))) & b₇ = b₄ - (b₈ * (b₁ / (b₁ gcd b₂))) )

proof end;

theorem Th42: :: WSIERP_1:42

for b₁, b₂, b₃, b₄ being Nat st b₁ hcf b₂ = 1 & b₁ * b₂ = b₃ |^ b₄ holds
ex b₅, b₆ being Nat st
( b₁ = b₅ |^ b₄ & b₂ = b₆ |^ b₄ )

proof end;

theorem Th43: :: WSIERP_1:43

for b₁ being FinSequence of NAT
for b₂ being Nat st ( for b₃ being Nat st b₃ in dom b₁ holds
(b₁ . b₃) hcf b₂ = 1 ) holds
(Product b₁) hcf b₂ = 1

proof end;

theorem Th44: :: WSIERP_1:44

for b₁ being FinSequence of NAT st len b₁ >= 2 & ( for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & b₂ <> b₃ holds
(b₁ . b₂) hcf (b₁ . b₃) = 1 ) holds
for b₂ being FinSequence of INT st len b₂ = len b₁ holds
ex b₃ being FinSequence of INT st
( len b₃ = len b₁ & ( for b₄ being Nat st b₄ in dom b₁ holds
((b₁ . b₄) * (b₃ . b₄)) + (b₂ . b₄) = ((b₁ . 1) * (b₃ . 1)) + (b₂ . 1) ) )

proof end;

Lemma53: for b₁, b₂ being Nat st b₁ divides b₂ & b₂ < b₁ holds
b₂ = 0

proof end;

Lemma54: for b₁, b₂ being Integer holds
( b₁ divides b₂ iff b₁ divides abs b₂ )

proof end;

Lemma55: for b₁ being Nat
for b₂ being Integer holds
( b₁ divides b₂ iff b₁ divides abs b₂ )

proof end;

Lemma56: for b₁, b₂ being Integer holds (b₁ * b₂) mod b₂ = 0

proof end;

Lemma57: for b₁, b₂, b₃ being Integer st b₁ mod b₂ = b₃ mod b₂ holds
(b₁ - b₃) mod b₂ = 0

proof end;

Lemma58: for b₁, b₂ being Integer st b₁ <> 0 & b₂ mod b₁ = 0 holds
b₁ divides b₂

proof end;

Lemma59: for b₁ being Integer holds
( ( 1 < b₁ implies ( 1 < sqrt b₁ & sqrt b₁ < b₁ ) ) & ( 0 < b₁ & b₁ < 1 implies ( 0 < sqrt b₁ & sqrt b₁ < 1 & b₁ < sqrt b₁ ) ) )

proof end;

theorem Th45: :: WSIERP_1:45

canceled;

theorem Th46: :: WSIERP_1:46

for b₁ being Nat
for b₂ being Integer st b₁ <> 0 & b₁ gcd b₂ = 1 holds
ex b₃, b₄ being Nat st
( 0 <> b₃ & 0 <> b₄ & b₃ <= sqrt b₁ & b₄ <= sqrt b₁ & ( b₁ divides (b₂ * b₃) + b₄ or b₁ divides (b₂ * b₃) - b₄ ) )

proof end;

theorem Th47: :: WSIERP_1:47

for b₁ being Nat
for b₂ being FinSequence holds dom (Del b₂,b₁) c= dom b₂ by Lemma38;

theorem Th48: :: WSIERP_1:48

for b₁ being FinSequence
for b₂ being set holds
( Del (<*b₂*> ^ b₁),1 = b₁ & Del (b₁ ^ <*b₂*>),((len b₁) + 1) = b₁ ) by Lemma40;