The Fundamental Properties of Natural Numbers

by
Grzegorz Bancerek

Copyright (c) 1989 Association of Mizar Users

MML identifier: NAT_1
[ MML identifier index ]

```environ

vocabulary ORDINAL2, ARYTM, ARYTM_1, ARYTM_3, ORDINAL1, NAT_1, XREAL_0;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1;
constructors REAL_1, XREAL_0, XCMPLX_0, XBOOLE_0;
clusters REAL_1, NUMBERS, ORDINAL2, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions REAL_1;
theorems AXIOMS, REAL_1, TARSKI, ORDINAL2, XCMPLX_0, XCMPLX_1;
schemes REAL_1;

begin

definition
mode Nat is Element of NAT;
end;

reserve x for Real,
k,l,m,n for Nat,
h,i,j for natural number,
X for Subset of REAL;

:: The results of axioms of natural numbers

canceled;

theorem                       :: axiom of induction
Th2: for X st 0 in X & for x st x in X holds x + 1 in X
for k holds k in X
proof let A be Subset of REAL such that
A1:  0 in A;
assume x in A implies x + 1 in A;
then for x being real number st x in A holds x + 1 in A;
then A2:  NAT c= A by A1,AXIOMS:29;
let k;
thus k in A by A2,TARSKI:def 3;
end;

:: The natural numbers are real numbers therefore some theorems of real
:: numbers are translated for natural numbers.

definition let n,k be Nat;
redefine func n + k -> Nat;
coherence
proof
defpred _P[Real] means ex k st \$1 = k & n + k is Nat;
consider X such that
A1:    x in X iff _P[x] from SepReal;
n + 0 = n;
then A2:    0 in X by A1;
now let x; assume
x in X;
then consider k such that
A3:      x = k & n + k is Nat by A1;
A4:      (n + k) + 1 = n + (k + 1) by XCMPLX_1:1;
k + 1 is Nat & (n + k) + 1 is Nat by A3,AXIOMS:28;
hence x + 1 in X by A1,A3,A4;
end;
then k in X by A2,Th2;
then ex m st k = m & n + m is Nat by A1;
hence thesis;
end;
end;

definition let n,k be natural number;
cluster n + k -> natural;
coherence
proof
reconsider n,k as Nat by ORDINAL2:def 21;
n+k is Nat;
hence thesis;
end;
end;

:: Now we can form and prove the scheme of induction.

scheme Ind { P[Nat] } :
for k being Nat holds P[k]
provided
A1:   P[0] and
A2:   for k being Nat st P[k] holds P[k + 1]
proof let k;
defpred _P[Real] means ex k st P[k] & k = \$1;
consider X such that
A3:   x in X iff _P[x] from SepReal;
A4:   0 in X by A1,A3;
for x st x in X holds x + 1 in X
proof let x; assume
x in X;
then consider k such that
A5:      P[k] & k = x by A3;
P[k + 1] by A2,A5;
hence thesis by A3,A5;
end;
then k in X by A4,Th2;
then ex n st P[n] & n = k by A3;
hence P[k];
end;

scheme Nat_Ind { P[natural number] } :
for k being natural number holds P[k]
provided
A1:   P[0] and
A2:   for k be natural number st P[k] holds P[k + 1]
proof
defpred _P[Nat] means P[\$1];
A3: _P[0] by A1;
A4:   for k st _P[k] holds _P[k + 1] by A2;
A5:   for k holds _P[k] from Ind(A3,A4);
let k be natural number;
k is Nat by ORDINAL2:def 21;
hence thesis by A5;
end;

:: Like addition, the result of multiplication of two natural numbers is
:: a natural number.

definition let n,k be Nat;
redefine func n * k -> Nat;
coherence
proof          defpred _P[Nat] means n*\$1 is Nat;
A1:    _P[0];
A2:    _P[m] implies _P[m+1]
proof
assume _P[m];
then reconsider k = n * m as Nat;
A3:       k + n is Nat;
n * (m + 1) = n * m + n * 1 by XCMPLX_1:8
.= n * m + n;
hence n * (m + 1) is Nat by A3;
end;
_P[m] from Ind(A1,A2);
hence thesis;
end;
end;

definition let n,k be natural number;
cluster n * k -> natural;
coherence
proof
reconsider n,k as Nat by ORDINAL2:def 21;
n*k is Nat;
hence thesis;
end;
end;

::::::::::::::::::::
:: Order relation ::
::::::::::::::::::::

:: Some theorems of not great relation "<=" in real numbers are translated
:: to natural number easy and it is necessary to have them here.

canceled 15;

theorem
Th18: 0 <= i
proof
defpred _P[Nat] means 0 <= \$1;
A1:  _P[0];
A2:  now let n; assume _P[n];
then 0 + 1 <= n + 1 by AXIOMS:24;
hence _P[n + 1] by AXIOMS:22;
end;
A3:for k holds _P[k] from Ind(A1,A2);
i is Nat by ORDINAL2:def 21;
hence thesis by A3;
end;

theorem
0 <> i implies 0 < i by Th18;

theorem
Th20: i <= j implies i * h <= j * h
proof assume
A1:  i <= j;
0 <= h by Th18;
hence thesis by A1,AXIOMS:25;
end;

theorem 0 <> i + 1
proof assume
A1:  0 = i + 1;
0 <= i by Th18;
then 0 + 1 <= 0 by A1,REAL_1:55;
end;

theorem
Th22: i = 0 or ex k st i = k + 1
proof
defpred _P[natural number] means \$1 = 0 or ex k st \$1 = k + 1;
A1:  _P[0];
A2:  _P[h] implies _P[h + 1];
for i holds _P[i] from Nat_Ind(A1,A2);
hence thesis;
end;

theorem
Th23: i + j = 0 implies i = 0 & j = 0
proof assume
A1:  i + j = 0;
0 <= i & 0 <= j by Th18;
then 0 + i <= j + i & 0 + j <= i + j & 0 + i = i & 0 + j = j by REAL_1:55;
hence thesis by A1,Th18;
end;

definition
cluster non zero (natural number);
existence
proof
take 1;
thus thesis;
end;
end;

definition let m be natural number, n be non zero (natural number);
cluster m + n -> non zero;
coherence by Th23;
cluster n + m -> non zero;
coherence by Th23;
end;

scheme Def_by_Ind { N()->Nat, F(Nat,Nat)->Nat, P[Nat,Nat] } :
(for k ex n st P[k,n] ) &
for k,n,m st P[k,n] & P[k,m] holds n = m
provided
A1:    for k,n holds P[k,n] iff
k = 0 & n = N() or ex m,l st k = m + 1 & P[m,l] & n = F(k,l)
proof
defpred _P[Nat] means ex n st P[\$1,n];
P[0,N()] by A1;
then A2:   _P[0];
A3:   _P[k] implies _P[k+1]
proof given n such that
A4:      P[k,n];
take F(k+1,n);
thus P[k+1,F(k+1,n)] by A1,A4;
end;
thus for k holds _P[k] from Ind(A2,A3);
defpred _P[Nat] means for n,m st P[\$1,n] & P[\$1,m] holds n = m;
A5:   _P[0]
proof let n,m such that
A6:     P[0,n] & P[0,m];
(not ex m,l st 0 = m + 1 & P[m,l] & n = F(0,l) ) &
not ex n,l st 0 = n + 1 & P[n,l] & m = F(0,l);
then n = N() & m = N() by A1,A6;
hence n = m;
end;
A7:   for k st _P[k] holds _P[k+1]
proof let k such that
A8:      for n,m st P[k,n] & P[k,m] holds n = m;
let n,m such that
A9:      P[k+1,n] & P[k+1,m];
consider l,u be Nat such that
A10:      k + 1 = l + 1 & P[l,u] & n = F(k + 1,u) by A1,A9;
consider v,w be Nat such that
A11:      k + 1 = v + 1 & P[v,w] & m = F(k + 1,w) by A1,A9;
l = k & v = k by A10,A11,XCMPLX_1:2;
hence n = m by A8,A10,A11;
end;
thus for k holds _P[k] from Ind(A5,A7);
end;

canceled 2;

theorem
Th26: for i,j st i <= j + 1 holds i <= j or i = j + 1
proof
defpred _P[natural number] means
for j holds \$1 <= j + 1 implies \$1 <= j or \$1 = j+1;
A1:  _P[0] by Th18;
A2:  for i st _P[i] holds _P[i+1]
proof let i such that
A3:     i <= j + 1 implies i <= j or i = j + 1;
let j such that
A4:     i + 1 <= j + 1;
A5:    1 + (-1) = 0;
A6:     i + 1 + (-1) = i + (1 + (-1)) by XCMPLX_1:1 .= i;
A7:     now assume
A8:       j = 0;
then A9:       i <= 0 by A4,A5,A6,AXIOMS:24;
0 <= i by Th18;
hence thesis by A8,A9,AXIOMS:21;
end;
now given k such that
A10:       j = k + 1;
j + 1 + (-1) = j + (1 + (-1)) by XCMPLX_1:1 .= j;
then i <= k + 1 by A4,A6,A10,AXIOMS:24;
then i <= k or i = k + 1 by A3;
hence thesis by A10,AXIOMS:24;
end;
hence thesis by A7,Th22;
end;
thus for i holds _P[i] from Nat_Ind(A1,A2);
end;

theorem
i <= j & j <= i + 1 implies i = j or j = i + 1
proof assume
A1:   i <= j & j <= i + 1;
then j <= i or j = i + 1 by Th26;
hence thesis by A1,AXIOMS:21;
end;

theorem
Th28: for i,j st i <= j ex k st j = i + k
proof let i;
defpred _P[natural number] means
i <= \$1 implies ex k st \$1 = i + k;
A1: _P[0]
proof assume
A2:   i <= 0;
take 0;
thus thesis by A2,Th18;
end;
A3:  for j st _P[j] holds _P[j+1]
proof let j such that
A4:   i <= j implies ex k st j = i + k;
assume
A5:     i <= j + 1;
A6:     now assume i <= j;
then consider k such that
A7:     j = i + k by A4;
i + k + 1 = i + (k + 1) by XCMPLX_1:1;
hence thesis by A7;
end;
now assume i = j + 1; then j + 1 = i + 0;
hence thesis;
end;
hence thesis by A5,A6,Th26;
end;
thus for j holds _P[j] from Nat_Ind(A1,A3);
end;

theorem
Th29: i <= i + j
proof
A1:  0 + i = i;
0 <= j by Th18;
hence thesis by A1,REAL_1:55;
end;

scheme Comp_Ind { P[Nat] } :
for k holds P[k]
provided
A1:   for k st for n st n < k holds P[n] holds P[k]
proof
defpred _P[Nat] means for n st n < \$1 holds P[n];
A2:   _P[0] by Th18;
A3:   _P[k] implies _P[k+1]
proof assume
A4:   for n st n < k holds P[n];
let n; assume
n < k + 1;
then n <= k by Th26;
then n < k or n = k & n <= k by REAL_1:def 5;
hence thesis by A1,A4;
end;
let k;
for k holds _P[k] from Ind(A2,A3);
then for n st n < k holds P[n];
hence P[k] by A1;
end;

:: Principle of minimum

scheme Min { P[Nat] } :
ex k st P[k] & for n st P[n] holds k <= n
provided
A1:  ex k st P[k]
proof assume A2: not thesis;
defpred _P[Nat] means not P[\$1];
A3:   for k st for n st n < k holds _P[n] holds _P[k]
proof let k;
A4:    not (ex n st P[n] & not k <= n) implies not P[k] by A2;
assume for n st n < k holds not P[n];
hence thesis by A4;
end;
for k holds _P[k] from Comp_Ind(A3);
end;

:: Principle of maximum

scheme Max { P[Nat],N()->Nat } :
ex k st P[k] & for n st P[n] holds n <= k
provided
A1:   for k st P[k] holds k <= N() and
A2:   ex k st P[k]
proof
defpred _P[Nat] means for n st P[n] holds n <= \$1;
A3:   ex k st _P[k] by A1;
consider k such that
A4:   _P[k] &
for m st _P[m] holds k <= m from Min(A3);
take k;
thus P[k]
proof assume
A5:      not P[k];
consider n such that
A6:      P[n] by A2;
n <= k & n <> k by A4,A5,A6;
then k <> 0 by Th18;
then consider m such that
A7:      k = m + 1 by Th22;
now let n; assume
P[n];
then n <= k & n <> k by A4,A5;
hence n <= m by A7,Th26;
end;
then A8:    k <= m by A4;
A9:    m + (- m) = 0 by XCMPLX_0:def 6;
(- m) + m + 1 = (- m) + (m + 1) & (- m) + m + 0 = (- m) + (m + 0)
by XCMPLX_1:1;
end;
thus thesis by A4;
end;

canceled 7;

theorem
Th37: i <= j implies i <= j + h
proof assume
A1:  i <= j;
0 <= h by Th18;
then i + 0 <= i + h & i + h <= j + h & i + 0 = i by A1,REAL_1:55;
hence i <= j + h by AXIOMS:22;
end;

theorem
Th38: i < j + 1 iff i <= j
proof
thus i < j + 1 implies i <= j by Th26;
assume
A1:  i <= j;
hence i <= j + 1 by Th37;
assume A2: i = j + 1;
A3:  j + (- j) = 0 by XCMPLX_0:def 6;
j + 1 + (- j) = 1 + (j + (- j)) by XCMPLX_1:1
.= 1 by A3;
end;

canceled;

theorem
Th40: i * j = 1 implies i = 1 & j = 1
proof assume
A1:  i * j = 1;
then i <> 0;
then consider m such that
A2:  i = m + 1 by Th22;
j <> 0 by A1;
then consider l such that
A3:  j = l + 1 by Th22;
(m + 1) * (l + 1) = m * (l + 1) + 1 * (l + 1) by XCMPLX_1:8
.= m * l + m * 1 + 1 * (l + 1) by XCMPLX_1:8
.= m * l + m + l + 1 by XCMPLX_1:1;
then m * l + m + l + 1 = 0 + 1 by A1,A2,A3;
then m * l + m + l = 0 by XCMPLX_1:2;
then m * l + m = 0 & l = 0 by Th23;
hence thesis by A2,A3;
end;

scheme Regr { P[Nat] } :
P[0]
provided
A1:  ex k st P[k] and
A2:  for k st k <> 0 & P[k] ex n st n < k & P[n]
proof
defpred _P[Nat] means P[\$1];
A3: ex k st _P[k] by A1;
consider k such that
A4:  _P[k] & for n st _P[n] holds k <= n from Min(A3);
now assume k <> 0;
then ex n st n < k & P[n] by A2,A4;
end;
hence P[0] by A4;
end;

:: Exact division and rest of division

reserve k1,t,t1 for Nat;

canceled;

theorem
Th42:  for m st 0 < m for n ex k,t st n = (m*k)+t & t < m
proof let m;
assume
A1:   0 < m;
defpred _P[Nat] means ex k,t st \$1 = (m*k)+t & t < m;
0 = m*0+0;
then A2:   _P[0] by A1;
A3:   for n st _P[n] holds _P[n+1]
proof let n;
given k1,t1 such that
A4:     n = (m*k1)+t1 & t1 < m;
A5:        t1+1 <= m by A4,Th38;
A6:     t1+1 < m implies ex k,t st n+1 = (m*k)+t & t < m
proof assume
A7:        t1+1 < m;
take k = k1 , t = t1+1;
thus n+1 = m*k+t by A4,XCMPLX_1:1;
thus t < m by A7;
end;
t1+1 = m implies ex k,t st n+1 = (m*k)+t & t < m
proof assume
A8:        t1+1 = m;
take k = k1+1 , t = 0;
thus n+1 = m*k1+m*1 by A4,A8,XCMPLX_1:1
.= m*k+t by XCMPLX_1:8;
thus t < m by A1;
end;
hence ex k,t st n+1 = (m*k)+t & t < m by A5,A6,REAL_1:def 5;
end;
thus for n holds _P[n] from Ind(A2,A3);
end;

theorem
Th43:for n,m,k,k1,t,t1 being natural number
st n = m*k+t & t < m & n = m*k1+t1 & t1 < m holds
k = k1 & t = t1
proof let n,m,k,k1,t,t1 be natural number;
assume
A1:   n = m*k+t & t < m & n = m*k1+t1 & t1 < m;
A2:   now assume k <= k1;
then consider u being Nat such that
A3:     k1 = k + u by Th28;
m * (k + u) + t1 = m * k + m * u + t1 by XCMPLX_1:8
.= m * k + (m * u + t1) by XCMPLX_1:1;
then A4:     m * u + t1 = t by A1,A3,XCMPLX_1:2;
now given w being Nat such that
A5:       u = w + 1;
m * 1 = m;
then m * u + t1 = m + m * w + t1 by A5,XCMPLX_1:8
.= m + (m * w + t1) by XCMPLX_1:1;
end;
then A6:     u = 0 by Th22;
hence k = k1 by A3;
thus t = t1 by A1,A3,A6,XCMPLX_1:2;
end;
now assume k1 <= k;
then consider u being Nat such that
A7:     k = k1 + u by Th28;
m * (k1 + u) + t = m * k1 + m * u + t by XCMPLX_1:8
.= m * k1 + (m * u + t) by XCMPLX_1:1;
then A8:     m * u + t = t1 by A1,A7,XCMPLX_1:2;
now given w being Nat such that
A9:       u = w + 1;
m * 1 = m;
then m * u + t = m + m * w + t by A9,XCMPLX_1:8
.= m + (m * w + t) by XCMPLX_1:1;
end;
then A10:     u = 0 by Th22;
hence k = k1 by A7;
thus t = t1 by A1,A7,A10,XCMPLX_1:2;
end;
hence thesis by A2;
end;

definition let k,l be natural number;
A1: k is Nat & l is Nat by ORDINAL2:def 21;
func k div l -> Nat means       :: the exact division
:Def1:  ( ex t st k = l * it + t & t < l ) or it = 0 & l = 0;
existence
proof
now assume
A2:      l <> 0;
0 <= l by Th18;
hence thesis by A1,A2,Th42;
end;
hence thesis;
end;
uniqueness
proof let t1,t2 be Nat such that
A3:   ( ex t st k = l * t1 + t & t < l ) or t1 = 0 & l = 0 and
A4:   ( ex t st k = l * t2 + t & t < l ) or t2 = 0 & l = 0;
now let t; assume
A5:     t < 0;
then ex m st 0 = t + m by Th28;
end;
hence thesis by A3,A4,Th43;
end;

func k mod l -> Nat means         :: the rest of division
:Def2: ( ex t st k = l * t + it & it < l ) or it = 0 & l = 0;
existence
proof
now assume
A6:      l <> 0;
0 <= l by Th18;
then ex n,t st k = l * n + t & t < l by A1,A6,Th42;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof let t1,t2 be Nat such that
A7:  ( ex t st k = l * t + t1 & t1 < l ) or t1 = 0 & l = 0 and
A8:  ( ex t st k = l * t + t2 & t2 < l ) or t2 = 0 & l = 0;
now let t; assume
A9:     t < 0;
then ex m st 0 = t + m by Th28;
end;
hence thesis by A7,A8,Th43;
end;
end;

canceled 2;

theorem
Th46: 0 < i implies j mod i < i
proof assume 0 < i;
then ex t st j = i * t + (j mod i) & j mod i < i by Def2;
hence j mod i < i;
end;

theorem
Th47: 0 < i implies j = i * (j div i) + (j mod i)
proof assume 0 < i;
then ex k st j = i * k + (j mod i) & j mod i < i by Def2;
hence j = i * (j div i) + (j mod i) by Def1;
end;

:: The divisibility relation

definition let k,l be natural number;
pred k divides l means
:Def3:  ex t st l = k * t;
reflexivity
proof let i;
i = i * 1;
hence thesis;
end;
end;

canceled;

theorem
Th49: j divides i iff i = j * (i div j)
proof
thus j divides i implies i = j * (i div j)
proof assume j divides i;
then consider k such that
A1:       i = j * k by Def3;
A2:       i = j * k + 0 by A1;
now assume
A3:        j <> 0;
A4: 0 <= j by Th18;
then A5:        i = j * (i div j) + (i mod j) by A3,Th47;
i mod j < j by A3,A4,Th46;
hence i = j * (i div j) by A2,A3,A4,A5,Th43;
end;
hence i = j * (i div j) by A1;
end;
assume i = j * (i div j);
hence j divides i by Def3;
end;

canceled;

theorem
i divides j & j divides h implies i divides h
proof assume i divides j & j divides h;
then j = i * (j div i) & h = j * (h div j) by Th49;
then h = i * ((j div i)*(h div j)) by XCMPLX_1:4;
hence i divides h by Def3;
end;

theorem
Th52: i divides j & j divides i implies i = j
proof
assume i divides j & j divides i;
then A1:   j = i * (j div i) & i = j * (i div j) by Th49;
then A2:     i * 1 = i * ((j div i) * (i div j)) by XCMPLX_1:4;
A3:   i = 0 implies i = j by A1;
(j div i) * (i div j) = 1 implies i = j
proof assume (j div i) * (i div j) = 1;
then j div i = 1 by Th40;
hence i = j by A1;
end;
hence i = j by A2,A3,XCMPLX_1:5;
end;

theorem
Th53: i divides 0 & 1 divides i
proof
0 = i * 0;
hence i divides 0 by Def3;
A1: i is Nat by ORDINAL2:def 21;
i = i * 1;
hence thesis by A1,Def3;
end;

theorem
Th54: 0 < j & i divides j implies i <= j
proof assume
A1:   0 < j & i divides j;
then A2:   j = i * (j div i) by Th49;
then j div i <> 0 by A1;
then consider m such that
A3:   j div i = m + 1 by Th22;
i * (m + 1) = (i * m) + i * 1 by XCMPLX_1:8 .= i + i * m;
hence i <= j by A2,A3,Th29;
end;

theorem
Th55: i divides j & i divides h implies i divides j+h
proof
assume i divides j & i divides h;
then j = i * (j div i) & h = i * (h div i) by Th49;
then j + h = i * ((j div i) + (h div i)) by XCMPLX_1:8;
hence i divides j + h by Def3;
end;

theorem
Th56: i divides j implies i divides j * h
proof assume
i divides j;
then consider l such that
A1:  j = i * l by Def3;
A2:  l*h is Nat by ORDINAL2:def 21;
i * l * h = i * (l * h) by XCMPLX_1:4;
hence thesis by A1,A2,Def3;
end;

theorem
Th57: i divides j & i divides j + h implies i divides h
proof assume
A1:  i divides j & i divides j + h;
then consider t such that
A2:  j + h = i * t by Def3;
consider u be Nat such that
A3:  j = i * u by A1,Def3;
now assume i <> 0;
then A4: i <> 0 & 0 <= i by Th18;
then A5:    h = i * (h div i) + (h mod i) by Th47;
A6:    j + (i * (h div i) + (h mod i)) = j + i * (h div i) + (h mod i)
by XCMPLX_1:1
.= i * (u + (h div i)) + (h mod i) by A3,XCMPLX_1:8;
A7:    h mod i < i by A4,Th46;
j + h = i * t + 0 by A2;
then h mod i = 0 by A4,A5,A6,A7,Th43;
hence thesis by A5,Th49;
end;
hence thesis by A2,Th23;
end;

theorem
Th58: i divides j & i divides h implies i divides j mod h
proof assume
A1:  i divides j & i divides h;
A2:  now assume h = 0; then j mod h = 0 by Def2;
hence thesis by Th53;
end;
now assume
A3:    h <> 0;
0 <= h by Th18;
then A4:    j = h * (j div h) + (j mod h) by A3,Th47;
i divides h * (j div h) by A1,Th56;
hence thesis by A1,A4,Th57;
end;
hence thesis by A2;
end;

:: The least common multiple and the greatest common divisor

definition let k,n be Nat;
func k lcm n -> Nat means
:Def4:  k divides it & n divides it & for m st k divides m & n divides
m holds it divides m;
existence
proof
A1:    now assume
A2:      k = 0 or n = 0;
take w = 0;
thus k divides w & n divides w by Th53;
let m; assume k divides m & n divides m;
hence w divides m by A2;
end;
now assume
A3:      k <> 0 & n <> 0;
A4:      k divides k * n & n divides k * n by Def3;
defpred _P[Nat] means k divides \$1 & n divides \$1 & k <= \$1;
0 <= n by Th18; then 0 + 1 <= n by A3,Th38;
then k * 1 <= k * n by Th20;
then A5:  ex m st _P[m] by A4;
consider l such that
A6:      _P[l] & for m st _P[m] holds l <= m
from Min(A5);
take l;
thus k divides l & n divides l by A6;
let m such that
A7:      k divides m & n divides m;
now A8: 0 <= k by Th18;
then A9:        m = l * (m div l) + (m mod l) by A3,A6,Th47;
l = k * (l div k) & l = n * (l div n) by A6,Th49;
then l * (m div l) = k * ((l div k) * (m div l)) &
l * (m div l) = n * ((l div n) * (m div l)) by XCMPLX_1:4;
then k divides l * (m div l) & n divides l * (m div l) by Def3;
then A10:        k divides m mod l & n divides m mod l by A7,A9,Th57;
now assume
A11:          m mod l <> 0;
0 <= m mod l by Th18;
then k <= m mod l by A10,A11,Th54;
then l <= m mod l by A6,A10;
end; hence l divides m by A9,Th49;
end;
hence l divides m;
end;
hence thesis by A1;
end;
uniqueness
proof let m1,m2 be Nat such that
A12:    k divides m1 & n divides m1 & for m st k divides m & n divides
m holds m1 divides m and
A13:    k divides m2 & n divides m2 & for m st k divides m & n divides
m holds m2 divides m;
m1 divides m2 & m2 divides m1 by A12,A13;
hence m1 = m2 by Th52;
end;
idempotence;
commutativity;
end;

definition let k,n be Nat;
func k hcf n -> Nat means
:Def5:  it divides k & it divides n & for m st m divides k & m divides
n holds m divides it;
existence
proof
defpred _P[Nat] means \$1 divides k & \$1 divides n;
1 divides k & 1 divides n by Th53;
then A1:    ex m st _P[m];
A2:    now assume
A3:     k = 0;
take m = n;
thus m divides k & m divides n by A3,Th53;
let l; assume l divides k & l divides n;
hence l divides m;
end;
now assume
A4:      k <> 0;
0 <= k by Th18;
then A5:      for m st _P[m] holds m <= k by A4,Th54;
consider m such that
A6:      _P[m] & for l st _P[l] holds l <= m from Max(A5,A1);
take m;
thus m divides k & m divides n by A6;
let l; assume l divides k & l divides n;
then A7:      l lcm m divides k & l lcm m divides n by A6,Def4;
then A8:      l lcm m <= m by A6;
m <= l lcm m
proof
A9:        m divides l lcm m by Def4;
A10:        now assume l lcm m = 0;
then k = 0 * (k div 0) by A7,Th49;
end;
0 <= l lcm m by Th18;
hence thesis by A9,A10,Th54;
end;
then l lcm m = m by A8,AXIOMS:21;
hence l divides m by Def4;
end;
hence thesis by A2;
end;
uniqueness
proof let m1,m2 be Nat such that
A11:    m1 divides k & m1 divides n & for m st m divides k & m divides
n holds m divides m1 and
A12:    m2 divides k & m2 divides n & for m st m divides k & m divides
n holds m divides m2;
m1 divides m2 & m2 divides m1 by A11,A12;
hence m1 = m2 by Th52;
end;
idempotence;
commutativity;
end;

scheme Euklides { Q(Nat)->Nat, a,b()->Nat } :
ex n st Q(n) = a() hcf b() & Q(n + 1) = 0
provided
A1:   0 < b() & b() < a() and
A2:   Q(0) = a() & Q(1) = b() and
A3:   for n holds Q(n + 2) = Q(n) mod Q(n + 1)
proof
defpred _P[Nat] means ex n st \$1 = Q(n);
A4:  ex k st _P[k] by A2;
A5:  for k st k <> 0 & _P[k] holds ex n st n < k & _P[n]
proof let k; assume
A6:    k <> 0 & ex n st k = Q(n);
then consider n such that
A7:    k = Q(n);
take Q(n + 1);
A8:    (n = 0 implies Q(n + 1) < k) & ex m st m = n+1 & Q(n + 1) = Q(m)
by A1,A2,A7;
now given m such that
A9:      n = m + 1;
A10: 0 <= Q(n) by Th18;
A11:         Q(m + 2) = Q(m) mod Q(m + 1) by A3;
m + 1 + 1 = m + (1 + 1) by XCMPLX_1:1;
hence Q(n + 1) < k by A6,A7,A9,A10,A11,Th46;
take m = n + 1;
thus Q(n + 1) =Q(m);
end;
hence thesis by A8,Th22;
end;
A12:  _P[0] from Regr(A4,A5);
defpred _Q[Nat] means 0 = Q(\$1);
A13: ex n st _Q[n] by A12;
consider k such that
A14:  _Q[k] & for n st _Q[n] holds k <= n from Min(A13);
consider n such that
A15:  k = n + 1 by A1,A2,A14,Th22;
take n;
defpred _PP[Nat] means Q(n) divides Q(\$1) & Q(n) divides Q(\$1 + 1);
_PP[n] by A14,A15,Th53;
then A16:  ex k st _PP[k];
A17:  for k st k <> 0 & _PP[k] ex m st m < k & _PP[m]
proof let l; assume
A18:    l <> 0 & Q(n) divides Q(l) & Q(n) divides Q(l + 1);
then consider m such that
A19:    l = m + 1 by Th22;
take m;
A20:    m <= m + 1 by Th29;
now assume m = m + 1; then m + 0 = m + 1;
end;
hence m < l by A19,A20,REAL_1:def 5;
A21:    now assume
A22:      Q(m + 1) = 0;
now assume
A23:        m + 1 <> k;
k <= m + 1 by A14,A22;
then k < m + 1 by A23,REAL_1:def 5;
then A24:        k <= m by Th38;
defpred _Q[Nat] means k <= \$1 implies Q(\$1) = 0;
A25: _Q[0]
proof assume A26: k <= 0; 0 <= k by Th18;
hence thesis by A14,A26,AXIOMS:21;
end;
A27:  for m st _Q[m] holds _Q[m+1]
proof let m such that
A28:           k <= m implies Q(m) = 0 and
A29:           k <= m + 1;
now assume k <> m + 1; then A30: k < m + 1 by A29,REAL_1:def 5;
then consider l such that
A31:             m = l + 1 by A1,A2,A28,Th22,Th38;
A32:                Q(l + 2) = Q(l) mod Q(l + 1) by A3;
l + 1 + 1 = l + (1 + 1) by XCMPLX_1:1;
hence Q(m + 1) = 0 by A28,A30,A31,A32,Def2,Th38;
end;
hence Q(m + 1) = 0 by A14;
end;
for m holds _Q[m] from Ind(A25,A27);
then Q(m) = 0 by A24;
hence Q(n) divides Q(m) by Th53;
end;
hence Q(n) divides Q(m) by A15,XCMPLX_1:2;
end;
now assume
A33:      Q(m + 1) <> 0;
A34: 0 <= Q(m + 1) by Th18;
Q(m + 2) = Q(m) mod Q(m + 1) by A3;
then A35:      Q(m) = Q(m + 1) * (Q(m) div Q(m + 1)) + Q(m + 2) by A33,A34,Th47
;
m + 1 + 1 = m + (1 + 1) by XCMPLX_1:1;
then Q(n) divides Q(m + 1) * (Q(m) div Q(m + 1)) & Q(n) divides
Q(m + 2)
by A18,A19,Th56;
hence Q(n) divides Q(m) by A35,Th55;
end;
hence Q(n) divides Q(m) by A21;
thus Q(n) divides Q(m + 1) by A18,A19;
end;
now
_PP[0] from Regr(A16,A17);
hence Q(n) divides a() & Q(n) divides b() by A2;
let m;
defpred _P1[Nat] means m divides Q(\$1) & m divides Q(\$1 + 1);
assume
m divides a() & m divides b();
then A36: _P1[0] by A2;
A37:    for k st _P1[k] holds _P1[k+1]
proof let k; assume
A38:       m divides Q(k) & m divides Q(k + 1);
hence m divides Q(k + 1);
A39:       Q(k + 2) = Q(k) mod Q(k + 1) by A3;
k + 1 + 1 = k + (1 + 1) by XCMPLX_1:1;
hence m divides Q(k + 1 + 1) by A38,A39,Th58;
end;
for k holds _P1[k] from Ind(A36,A37);
hence m divides Q(n);
end;
hence Q(n) = a() hcf b() by Def5;
thus Q(n + 1) = 0 by A14,A15;
end;

definition
cluster -> ordinal Nat;
coherence;
end;

definition
cluster non empty ordinal Subset of REAL;
existence proof take NAT; thus thesis; end;
end;
```