begin
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 ) )
Lm2:
for x, y, z being real number st x >= 0 & y >= z holds
( x + y >= z & y >= z - x )
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 )
Lm4:
for a being Nat ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 )
Lm5:
for a, b being Nat st a <> 0 holds
( a divides b iff b / a is Element of NAT )
Lm6:
for b, a being Nat
for k being Integer st b <> 0 & a * k = b holds
k is Element of NAT
Lm7:
for a, b, c being Nat st a + b <= c holds
( a <= c & b <= c )
theorem
for
a,
b,
c being
Nat st
a <= b - c holds
(
a <= b &
c <= b )
Lm8:
for k, m being Integer holds
( k < m iff k <= m - 1 )
Lm9:
for k, m being Integer holds
( k < m + 1 iff k <= m )
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 )
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
Lm12:
for a being Nat
for fs being FinSequence holds dom (Del (fs,a)) c= dom fs
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)) ) )
Lm14:
for fs being FinSequence
for v being set holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
theorem
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*> )
Lm15:
for fs being FinSequence st 1 <= len fs holds
( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )
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
theorem
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 )
theorem
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 )
Lm17:
for k, m being Integer holds
( k divides m iff k divides abs m )
Lm18:
for m, n being Integer holds (m * n) mod n = 0
Lm19:
for k, n, m being Integer st k mod n = m mod n holds
(k - m) mod n = 0
Lm20:
for n, m being Integer st n <> 0 & m mod n = 0 holds
n divides m
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 ) ) )
begin