begin
:: deftheorem Def1 defines div NAT_D:def 1 :
for
k,
l,
b3 being
Nat holds
(
b3 = k div l iff ( ex
t being
Nat st
(
k = (l * b3) + t &
t < l ) or (
b3 = 0 &
l = 0 ) ) );
:: deftheorem Def2 defines mod NAT_D:def 2 :
for
k,
l,
b3 being
Nat holds
(
b3 = k mod l iff ( ex
t being
Nat st
(
k = (l * t) + b3 &
b3 < l ) or (
b3 = 0 &
l = 0 ) ) );
theorem Th1:
for
i,
j being
Nat st
0 < i holds
j mod i < i
theorem
:: deftheorem Def3 defines divides NAT_D:def 3 :
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
:: deftheorem Def4 defines lcm NAT_D:def 4 :
:: deftheorem Def5 defines gcd NAT_D:def 5 :
scheme
Euklides{
F1(
Nat)
-> Nat,
F2()
-> Nat,
F3()
-> Nat } :
provided
A1:
(
0 < F3() &
F3()
< F2() )
and A2:
(
F1(
0 )
= F2() &
F1(1)
= F3() )
and A3:
for
n being
Element of
NAT holds
F1(
(n + 2))
= F1(
n)
mod F1(
(n + 1))
theorem
theorem
theorem
for
k being
Nat st
k > 1 holds
1
mod k = 1
theorem
theorem
theorem
theorem
theorem
begin
theorem
theorem Th21:
theorem Th22:
theorem
theorem Th24:
for
k,
n being
Nat st
k < n holds
k mod n = k
theorem
theorem
theorem Th27:
for
i,
j being
Nat st
i < j holds
i div j = 0
theorem Th28:
theorem
theorem
theorem
theorem
theorem
theorem Th34:
theorem Th35:
theorem Th36:
for
n,
i being
Nat st
n -' i = 0 holds
n <= i
theorem
theorem
for
i,
j,
k being
Nat st
i <= j holds
(j + k) -' i = (j -' i) + k
theorem Th39:
theorem
theorem
theorem Th42:
theorem Th43:
theorem
theorem Th45:
theorem Th46:
theorem
theorem
theorem
theorem Th50:
theorem
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem
theorem