### The Mizar article:

### The Fundamental Properties of Natural Numbers

**by****Grzegorz Bancerek**

- Received January 11, 1989
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; :: Addition and multiplication :: 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; hence contradiction; 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); hence contradiction by A1; 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; hence contradiction by A7,A8,A9,AXIOMS:24; 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; hence contradiction by A1,A2,A3,AXIOMS:24; 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; hence contradiction by 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; hence contradiction by A1,A4,Th29; 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; hence contradiction by A1,A8,Th29; 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; hence contradiction by A5,Th23; 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; hence contradiction by A9,Th23; 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; hence contradiction by A3,A6,A8,Th46; 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; hence contradiction by A4; 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; hence contradiction by XCMPLX_1:2; 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;

Back to top