:: by Andrzej Kondracki

::

:: Received December 30, 1997

:: Copyright (c) 1997-2012 Association of Mizar Users

begin

theorem Th2: :: WSIERP_1:2

for x being real number

for a being Nat holds

( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )

for a being Nat holds

( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )

proof end;

Lm1: for x, y being real number holds

( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )

proof end;

Lm2: for x, y, z being real number st x >= 0 & y >= z holds

( x + y >= z & y >= z - x )

proof end;

Lm3: for x, y, z being real number st ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) holds

( x + y > z & y > z - x )

proof end;

registration
end;

Lm4: for a being Nat ex b being Nat st

( a = 2 * b or a = (2 * b) + 1 )

proof end;

theorem :: WSIERP_1:7

theorem Th11: :: WSIERP_1:11

for a, b being Nat

for k, l being Integer st k,l are_relative_prime holds

k |^ a,l |^ b are_relative_prime

for k, l being Integer st k,l are_relative_prime holds

k |^ a,l |^ b are_relative_prime

proof end;

theorem Th12: :: WSIERP_1:12

for b, a being Nat

for k, l being Integer st k gcd l = 1 holds

( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )

for k, l being Integer st k gcd l = 1 holds

( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )

proof end;

theorem :: WSIERP_1:16

Lm5: for a, b being Nat st a <> 0 holds

( a divides b iff b / a is Element of NAT )

proof end;

Lm6: for b, a being Nat

for k being Integer st b <> 0 & a * k = b holds

k is Element of NAT

proof end;

Lm7: for a, b, c being Nat st a + b <= c holds

( a <= c & b <= c )

proof end;

Lm8: for k, m being Integer holds

( k < m iff k <= m - 1 )

proof end;

Lm9: for k, m being Integer holds

( k < m + 1 iff k <= m )

proof end;

definition

let D be non empty set ;

let D1 be non empty Subset of D;

let f1, f2 be FinSequence of D1;

:: original: ^

redefine func f1 ^ f2 -> FinSequence of D1;

coherence

f1 ^ f2 is FinSequence of D1

end;
let D1 be non empty Subset of D;

let f1, f2 be FinSequence of D1;

:: original: ^

redefine func f1 ^ f2 -> FinSequence of D1;

coherence

f1 ^ f2 is FinSequence of D1

proof end;

definition

let fp be FinSequence of NAT ;

:: original: Sum

redefine func Sum fp -> Element of NAT ;

coherence

Sum fp is Element of NAT

end;
:: original: Sum

redefine func Sum fp -> Element of NAT ;

coherence

Sum fp is Element of NAT

proof end;

definition

let fp be FinSequence of NAT ;

:: original: Product

redefine func Product fp -> Element of NAT ;

coherence

Product fp is Element of NAT

end;
:: original: Product

redefine func Product fp -> Element of NAT ;

coherence

Product fp is Element of NAT

proof end;

Lm10: for a being Nat

for fs being FinSequence st a in dom fs holds

ex fs1, fs2 being FinSequence st

( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )

proof end;

definition

let a be Nat;

let fs be FinSequence;

for b_{1} being set holds

( ( not a in dom fs implies ( b_{1} = Del (fs,a) iff b_{1} = fs ) ) & ( a in dom fs implies ( b_{1} = Del (fs,a) iff ( (len b_{1}) + 1 = len fs & ( for b being Nat holds

( ( b < a implies b_{1} . b = fs . b ) & ( b >= a implies b_{1} . b = fs . (b + 1) ) ) ) ) ) ) )

consistency

for b_{1} being set holds verum;

;

end;
let fs be FinSequence;

redefine func Del (fs,a) means :Def1: :: WSIERP_1:def 1

it = fs if not a in dom fs

otherwise ( (len it) + 1 = len fs & ( for b being Nat holds

( ( b < a implies it . b = fs . b ) & ( b >= a implies it . b = fs . (b + 1) ) ) ) );

compatibility it = fs if not a in dom fs

otherwise ( (len it) + 1 = len fs & ( for b being Nat holds

( ( b < a implies it . b = fs . b ) & ( b >= a implies it . b = fs . (b + 1) ) ) ) );

for b

( ( not a in dom fs implies ( b

( ( b < a implies b

proof end;

correctness consistency

for b

;

:: deftheorem Def1 defines Del WSIERP_1:def 1 :

for a being Nat

for fs being FinSequence

for b_{3} being set holds

( ( not a in dom fs implies ( b_{3} = Del (fs,a) iff b_{3} = fs ) ) & ( a in dom fs implies ( b_{3} = Del (fs,a) iff ( (len b_{3}) + 1 = len fs & ( for b being Nat holds

( ( b < a implies b_{3} . b = fs . b ) & ( b >= a implies b_{3} . b = fs . (b + 1) ) ) ) ) ) ) );

for a being Nat

for fs being FinSequence

for b

( ( not a in dom fs implies ( b

( ( b < a implies b

Lm11: for a being Nat

for fs, fs1, fs2 being FinSequence

for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds

Del (fs,a) = fs1 ^ fs2

proof end;

Lm12: for a being Nat

for fs being FinSequence holds dom (Del (fs,a)) c= dom fs

proof end;

definition

let D be non empty set ;

let a be Nat;

let fs be FinSequence of D;

:: original: Del

redefine func Del (fs,a) -> FinSequence of D;

coherence

Del (fs,a) is FinSequence of D

end;
let a be Nat;

let fs be FinSequence of D;

:: original: Del

redefine func Del (fs,a) -> FinSequence of D;

coherence

Del (fs,a) is FinSequence of D

proof end;

definition

let D be non empty set ;

let D1 be non empty Subset of D;

let a be Nat;

let fs be FinSequence of D1;

:: original: Del

redefine func Del (fs,a) -> FinSequence of D1;

coherence

Del (fs,a) is FinSequence of D1

end;
let D1 be non empty Subset of D;

let a be Nat;

let fs be FinSequence of D1;

:: original: Del

redefine func Del (fs,a) -> FinSequence of D1;

coherence

Del (fs,a) is FinSequence of D1

proof end;

Lm13: for a being Nat

for fs1, fs2 being FinSequence holds

( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )

proof end;

Lm14: for fs being FinSequence

for v being set holds

( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )

proof end;

theorem :: WSIERP_1:19

for v1, v2, v3 being set holds

( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )

( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )

proof end;

Lm15: for fs being FinSequence st 1 <= len fs holds

( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )

proof end;

Lm16: for a being Nat

for ft being FinSequence of REAL st a in dom ft holds

(Product (Del (ft,a))) * (ft . a) = Product ft

proof end;

theorem :: WSIERP_1:20

for a being Nat

for ft being FinSequence of REAL st a in dom ft holds

(Sum (Del (ft,a))) + (ft . a) = Sum ft

for ft being FinSequence of REAL st a in dom ft holds

(Sum (Del (ft,a))) + (ft . a) = Sum ft

proof end;

theorem :: WSIERP_1:21

for a being Nat

for fp being FinSequence of NAT st a in dom fp holds

(Product fp) / (fp . a) is Element of NAT

for fp being FinSequence of NAT st a in dom fp holds

(Product fp) / (fp . a) is Element of NAT

proof end;

:: BEGINING

theorem :: WSIERP_1:23

for a being Nat

for k being Integer

for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds

( k = numerator q & a = denominator q )

for k being Integer

for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds

( k = numerator q & a = denominator q )

proof end;

theorem :: WSIERP_1:30

theorem :: WSIERP_1:32

for f, g, a, b being Nat st f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g holds

ex e being Nat st

( a = e |^ g & b = e |^ f )

ex e being Nat st

( a = e |^ g & b = e |^ f )

proof end;

theorem Th33: :: WSIERP_1:33

for m, n, k being Integer holds

( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )

( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )

proof end;

theorem :: WSIERP_1:34

for m, n, m1, n1, k being Integer st m <> 0 & n <> 0 & (m * m1) + (n * n1) = k holds

for x, y being Integer st (m * x) + (n * y) = k holds

ex t being Integer st

( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )

for x, y being Integer st (m * x) + (n * y) = k holds

ex t being Integer st

( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )

proof end;

theorem :: WSIERP_1:35

for a, b, c, d being Nat st a gcd b = 1 & a * b = c |^ d holds

ex e, f being Nat st

( a = e |^ d & b = f |^ d )

ex e, f being Nat st

( a = e |^ d & b = f |^ d )

proof end;

theorem Th36: :: WSIERP_1:36

for fp being FinSequence of NAT

for d being Nat st ( for a being Nat st a in dom fp holds

(fp . a) gcd d = 1 ) holds

(Product fp) gcd d = 1

for d being Nat st ( for a being Nat st a in dom fp holds

(fp . a) gcd d = 1 ) holds

(Product fp) gcd d = 1

proof end;

theorem :: WSIERP_1:37

for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds

(fp . b) gcd (fp . c) = 1 ) holds

for fr being FinSequence of INT st len fr = len fp holds

ex fr1 being FinSequence of INT st

( len fr1 = len fp & ( for b being Nat st b in dom fp holds

((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) )

(fp . b) gcd (fp . c) = 1 ) holds

for fr being FinSequence of INT st len fr = len fp holds

ex fr1 being FinSequence of INT st

( len fr1 = len fp & ( for b being Nat st b in dom fp holds

((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) )

proof end;

Lm17: for k, m being Integer holds

( k divides m iff k divides abs m )

proof end;

Lm18: for m, n being Integer holds (m * n) mod n = 0

proof end;

Lm19: for k, n, m being Integer st k mod n = m mod n holds

(k - m) mod n = 0

proof end;

Lm20: for n, m being Integer st n <> 0 & m mod n = 0 holds

n divides m

proof end;

Lm21: for x being Integer holds

( ( 1 < x implies ( 1 < sqrt x & sqrt x < x ) ) & ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) )

proof end;

:: Thue Theorem

theorem :: WSIERP_1:38

for a being Nat

for k being Integer st a <> 0 & a gcd k = 1 holds

ex b, e being Nat st

( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )

for k being Integer st a <> 0 & a gcd k = 1 holds

ex b, e being Nat st

( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )

proof end;

theorem :: WSIERP_1:39

theorem :: WSIERP_1:40

begin