:: WSIERP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let f be FinSequence of REAL ;
let k be Nat;
:: original: .
redefine func f . k -> Real;
coherence
f . k is Real
proof end;
end;

theorem :: WSIERP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: WSIERP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds
( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )
proof end;

theorem Th3: :: WSIERP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number
for a being Nat holds
( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
proof end;

theorem :: WSIERP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: WSIERP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number
for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y
proof end;

theorem Th6: :: WSIERP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number holds
( x > max y,z iff ( x > y & x > z ) )
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;

theorem :: WSIERP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number st x <= 0 & y >= z holds
( y - x >= z & y >= z + x ) by XREAL_1:37, XREAL_1:54;

theorem :: WSIERP_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being real number st ( ( x <= 0 & y > z ) or ( x < 0 & y >= z ) ) holds
( y > z + x & y - x > z ) by XREAL_1:38, XREAL_1:39, XREAL_1:55, XREAL_1:56;

Lm4: for a, b being Nat holds
( a divides b iff a divides b )
proof end;

Lm5: for a being Nat holds abs a = a
by ABSVALUE:def 1;

registration
let k be Integer;
let a be Nat;
cluster k |^ a -> integer ;
coherence
k |^ a is integer
proof end;
end;

definition
let a, b be Nat;
:: original: |^
redefine func a |^ b -> Nat;
coherence
a |^ b is Nat
by NEWTON:99;
end;

Lm6: for a being Nat ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 )
proof end;

Lm7: for d, a, b being Nat st d > 0 & a |^ d = b |^ d holds
a = b
by Th5;

theorem Th9: :: WSIERP_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m, n being Integer st k divides m & k divides n holds
k divides m + n
proof end;

theorem Th10: :: WSIERP_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, m, n, m1, n1 being Integer st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
proof end;

Lm8: for a, b being Nat holds a gcd b = a hcf b
proof end;

Lm9: for a, b being Nat holds
( a,b are_relative_prime iff a,b are_relative_prime )
proof end;

theorem Th11: :: WSIERP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, k being Integer st m gcd n = 1 & k gcd n = 1 holds
(m * k) gcd n = 1
proof end;

theorem Th12: :: WSIERP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Nat st a hcf b = 1 & c hcf b = 1 holds
(a * c) hcf b = 1
proof end;

theorem Th13: :: WSIERP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Integer holds
( 0 gcd m = abs m & 1 gcd m = 1 )
proof end;

theorem Th14: :: WSIERP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer holds 1,k are_relative_prime
proof end;

theorem Th15: :: WSIERP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Nat
for k, l being Integer st k,l are_relative_prime holds
k |^ a,l are_relative_prime
proof end;

theorem Th16: :: WSIERP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Nat
for k, l being Integer st k,l are_relative_prime holds
k |^ a,l |^ b are_relative_prime
proof end;

theorem Th17: :: WSIERP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

Lm10: for a, b, d, c being Nat st a hcf b = 1 holds
( a hcf (b |^ d) = 1 & (a |^ c) hcf (b |^ d) = 1 )
proof end;

theorem :: WSIERP_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, k being Integer holds
( abs m divides k iff m divides k )
proof end;

theorem Th19: :: WSIERP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Nat st a divides b holds
a |^ c divides b |^ c
proof end;

theorem Th20: :: WSIERP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Nat st a divides 1 holds
a = 1
proof end;

theorem Th21: :: WSIERP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for d, a, b being Nat st d divides a & a hcf b = 1 holds
d hcf b = 1
proof end;

Lm11: for a, b being Nat st a <> 0 holds
( a divides b iff b / a is Nat )
proof end;

theorem :: WSIERP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, l being Integer st k <> 0 holds
( k divides l iff l / k is Integer )
proof end;

Lm12: for b, a being Nat
for k being Integer st b <> 0 & a * k = b holds
k is Nat
proof end;

Lm13: for a being Nat
for k being Integer st a <= k holds
k is Nat
by INT_1:16;

Lm14: for a, b, c being Nat st a + b <= c holds
( a <= c & b <= c )
proof end;

theorem :: WSIERP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Nat st a <= b - c holds
( a <= b & c <= b )
proof end;

Lm15: for k, m being Integer holds
( k < m iff k <= m - 1 )
proof end;

Lm16: for k, m being Integer holds
( k < m + 1 iff k <= m )
proof end;

Lm17: for x being real number
for f being Function holds
( ( x in dom f & f . x in rng f ) or f . x = {} )
proof end;

Lm18: for a being Nat
for X being set st 0 in X holds
for s being FinSequence of X holds s . a is Element of X
proof end;

registration
let f be FinSequence of INT ;
let a be set ;
cluster f . a -> integer ;
coherence
f . a is integer
proof end;
end;

definition
let fp be FinSequence of NAT ;
let a be Nat;
:: original: .
redefine func fp . a -> Nat;
coherence
fp . a is Nat
by Lm18;
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
proof end;
end;

definition
let D be non empty set ;
let D1 be non empty Subset of D;
:: original: <*>
redefine func <*> D1 -> empty FinSequence of D1;
coherence
<*> D1 is empty FinSequence of D1
;
end;

definition
:: original: INT
redefine func INT -> non empty Subset of REAL ;
coherence
INT is non empty Subset of REAL
by NUMBERS:15;
end;

definition
let fr be FinSequence of INT ;
:: original: Sum
redefine func Sum fr -> Element of INT ;
coherence
Sum fr is Element of INT
proof end;
:: original: Product
redefine func Product fr -> Element of INT ;
coherence
Product fr is Element of INT
proof end;
end;

definition
let fp be FinSequence of NAT ;
:: original: Sum
redefine func Sum fp -> Nat;
coherence
Sum fp is Nat
proof end;
:: original: Product
redefine func Product fp -> Nat;
coherence
Product fp is Nat
proof end;
end;

Lm19: 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;
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
for b1 being set holds
( ( not a in dom fs implies ( b1 = Del fs,a iff b1 = fs ) ) & ( a in dom fs implies ( b1 = Del fs,a iff ( (len b1) + 1 = len fs & ( for b being Nat holds
( ( b < a implies b1 . b = fs . b ) & ( b >= a implies b1 . b = fs . (b + 1) ) ) ) ) ) ) )
proof end;
correctness
consistency
for b1 being set holds verum
;
;
end;

:: deftheorem Def1 defines Del WSIERP_1:def 1 :
for a being Nat
for fs being FinSequence
for b3 being set holds
( ( not a in dom fs implies ( b3 = Del fs,a iff b3 = fs ) ) & ( a in dom fs implies ( b3 = Del fs,a iff ( (len b3) + 1 = len fs & ( for b being Nat holds
( ( b < a implies b3 . b = fs . b ) & ( b >= a implies b3 . b = fs . (b + 1) ) ) ) ) ) ) );

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

Lm21: 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
proof end;
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
proof end;
end;

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

Lm23: 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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WSIERP_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WSIERP_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*> )
proof end;

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

Lm25: 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:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Nat
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:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Nat
for fp being FinSequence of NAT st a in dom fp holds
(Product fp) / (fp . a) is Nat
proof end;

theorem Th29: :: WSIERP_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q being Rational holds numerator q, denominator q are_relative_prime
proof end;

theorem :: WSIERP_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Nat
for k being Integer
for q being Rational st q <> 0 & q = k / a & a <> 0 & k,a are_relative_prime holds
( k = numerator q & a = denominator q )
proof end;

theorem Th31: :: WSIERP_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Nat st ex q being Rational st a = q |^ b holds
ex k being Integer st a = k |^ b
proof end;

theorem Th32: :: WSIERP_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, d being Nat st ex q being Rational st a = q |^ d holds
ex b being Nat st a = b |^ d
proof end;

theorem :: WSIERP_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e, a, b being Nat st e > 0 & a |^ e divides b |^ e holds
a divides b
proof end;

theorem Th34: :: WSIERP_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Nat ex m, n being Integer st a hcf b = (a * m) + (b * n)
proof end;

theorem Th35: :: WSIERP_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Integer ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
proof end;

theorem Th36: :: WSIERP_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, k being Integer st m divides n * k & m gcd n = 1 holds
m divides k
proof end;

theorem Th37: :: WSIERP_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Nat st a hcf b = 1 & a divides b * c holds
a divides c
proof end;

theorem Th38: :: WSIERP_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Nat st a <> 0 & b <> 0 holds
ex c, d being Nat st a hcf b = (a * c) - (b * d)
proof end;

theorem :: WSIERP_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g, a, b being Nat st f > 0 & g > 0 & f hcf g = 1 & a |^ f = b |^ g holds
ex e being Nat st
( a = e |^ g & b = e |^ f )
proof end;

theorem Th40: :: WSIERP_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, k being Integer holds
( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )
proof end;

theorem :: WSIERP_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))) )
proof end;

theorem :: WSIERP_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Nat st a hcf b = 1 & a * b = c |^ d holds
ex e, f being Nat st
( a = e |^ d & b = f |^ d )
proof end;

theorem Th43: :: WSIERP_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fp being FinSequence of NAT
for d being Nat st ( for a being Nat st a in dom fp holds
(fp . a) hcf d = 1 ) holds
(Product fp) hcf d = 1
proof end;

theorem :: WSIERP_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) hcf (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;

Lm26: for a, b being Nat st a divides b & b < a holds
b = 0
proof end;

Lm27: for k, m being Integer holds
( k divides m iff k divides abs m )
proof end;

Lm28: for a being Nat
for m being Integer holds
( a divides m iff a divides abs m )
proof end;

Lm29: for m, n being Integer holds (m * n) mod n = 0
proof end;

Lm30: for k, n, m being Integer st k mod n = m mod n holds
(k - m) mod n = 0
proof end;

Lm31: for n, m being Integer st n <> 0 & m mod n = 0 holds
n divides m
proof end;

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

theorem :: WSIERP_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WSIERP_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: WSIERP_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Nat
for fs being FinSequence holds dom (Del fs,a) c= dom fs by Lm21;

theorem :: WSIERP_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fs being FinSequence
for v being set holds
( Del (<*v*> ^ fs),1 = fs & Del (fs ^ <*v*>),((len fs) + 1) = fs ) by Lm23;