:: Divisibility of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 3, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, INT_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0,
SUBSET_1, ARYTM_1, INT_2, COMPLEX1, ZFMISC_1, XBOOLE_0, FINSET_1,
ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, FINSET_1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, NAT_1, INT_2;
constructors XXREAL_0, NAT_1, INT_2, REAL_1, FINSET_1, CARD_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, ORDINAL1, CARD_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, NAT_1, INT_1, INT_2, ABSVALUE,
XREAL_0, CARD_1, ZFMISC_1, COMPLEX1, XCMPLX_0, TARSKI;
schemes NAT_1;
begin
reserve a,b,p,k,l,m,n,s,h,i,j,t,i1,i2 for natural Number;
:: Exact division and rest of division
Lm1: now
let k,l;
reconsider k1=k,l1=l as Nat by TARSKI:1;
k1 div l1 in NAT by INT_1:3;
hence k div l is Nat;
end;
Lm2: now
let k,l;
k mod l in NAT by INT_1:3;
hence k mod l is Nat;
end;
definition
let k,l be natural Number;
redefine func k div l -> Nat means :: the exact division :: redefines div (INT_1, definition)
:Def1:
( ex t being Nat st k = l * it + t & t < l ) or it = 0 & l = 0;
compatibility
proof
let r be Nat;
per cases;
suppose l = 0;
hence thesis;
end;
suppose
A1: l > 0;
then
A2: k = l * (k div l) + (k mod l) by INT_1:59;
A3: k mod l is Nat by Lm2;
hence r = k div l implies
(ex t being Nat st k = l * r + t & t < l) or r = 0 & l = 0
by A1,A2,INT_1:58;
assume
A4: ( ex t being Nat st k = l * r + t & t < l ) or r = 0 & l = 0;
A5: k mod l < l by A1,INT_1:58;
k div l is Nat by Lm1;
hence thesis by A2,A4,A5,NAT_1:18;
end;
end;
coherence by Lm1;
end;
definition
let k,l be natural Number;
redefine func k mod l -> Nat means :: the rest of division :: redefines mod (INT_1, definition)
:Def2:
( ex t being Nat st k = l * t + it & it < l ) or it = 0 & l = 0;
compatibility
proof
let r be Nat;
per cases;
suppose l = 0;
hence thesis;
end;
suppose
A1: l > 0;
then
A2: k = l * (k div l) + (k mod l) by INT_1:59;
hence r = k mod l implies
( ex t being Nat st k = l * t + r & r < l ) or r = 0 & l = 0
by A1,INT_1:58;
assume
A3: ( ex t being Nat st k = l * t + r & r < l ) or r = 0 & l = 0;
A4: k mod l < l by A1,INT_1:58;
k mod l is Nat by Lm2;
thus thesis by A2,A3,A4,NAT_1:18;
end;
end;
coherence by Lm2;
end;
definition
let k,l be Nat;
redefine func k div l -> Element of NAT; :: redefines div (INT_1, definition)
coherence
proof
k div l is Nat;
thus thesis by ORDINAL1:def 12;
end;
redefine func k mod l -> Element of NAT; :: redefines mod (INT_1, definition)
coherence
proof
k mod l is Nat;
thus thesis by ORDINAL1:def 12;
end;
end;
theorem Th1:
0 < i implies j mod i < i by INT_1:58;
theorem
0 < i implies j = i * (j div i) + (j mod i) by INT_1:59;
:: The divisibility relation
definition
let k,l be natural Number;
redefine pred k divides l means :: redefines divides (INT_1, definition)
ex t being Nat st l = k * t;
compatibility
proof
hereby
assume
A1: k divides l;
thus ex t being Nat st l = k * t
proof
consider t being Integer such that
A2: l = k * t by A1,INT_1:def 3;
per cases;
suppose 0 < l;
then 0 <= t by A2;
then reconsider t as Element of NAT by INT_1:3;
take t;
thus l = k * t by A2;
end;
suppose
A3: l = 0;
take 0;
thus l = k*0 by A3;
end;
end;
end;
thus thesis by INT_1:def 3;
end;
reflexivity
proof
let i;
i = i * 1;
hence thesis;
end;
end;
theorem Th3:
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 being Nat such that
A1: i = j * k;
A2: i = j * k + 0 by A1;
now
assume
A3: j <> 0;
then
A4: i = j * (i div j) + (i mod j) by INT_1:59;
i mod j < j by A3,Th1;
hence thesis by A2,A4,NAT_1:18;
end;
hence thesis by A1;
end;
thus thesis;
end;
theorem
i divides j & j divides h implies i divides h by INT_2:9;
theorem Th5:
i divides j & j divides i implies i = j
proof
assume that
A1: i divides j and
A2: j divides i;
A3: j = i * (j div i) by A1,Th3;
i = j * (i div j) by A2,Th3;
then
A4: i*1 = i * (j div i) * (i div j) by A3
.= i * ((j div i) * (i div j));
A5: i = 0 implies i = j by A3;
(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 NAT_1:15;
hence thesis by A3;
end;
hence thesis by A4,A5,XCMPLX_1:5;
end;
theorem Th6:
i divides 0 & 1 divides i by INT_2:12;
theorem
0 < j & i divides j implies i <= j by INT_2:27;
theorem Th8:
i divides j & i divides h implies i divides j+h
proof
assume that
A1: i divides j and
A2: i divides h;
A3: j = i * (j div i) by A1,Th3;
h = i * (h div i) by A2,Th3;
then j + h = i * ((j div i) + (h div i)) by A3;
hence thesis;
end;
theorem Th9:
i divides j implies i divides j * h by INT_2:2;
theorem Th10:
i divides j & i divides j + h implies i divides h
proof
assume that
A1: i divides j and
A2: i divides j + h;
consider t being Nat such that
A3: j + h = i * t by A2;
consider u being Nat such that
A4: j = i * u by A1;
now
assume
A5: i <> 0;
then
A6: h = i * (h div i) + (h mod i) by INT_1:59;
A7: j + (i * (h div i) + (h mod i)) = i * (u + (h div i)) + (h mod i) by A4;
A8: h mod i < i by A5,Th1;
j + h = i * t + 0 by A3;
then h mod i = 0 by A6,A7,A8,NAT_1:18;
hence thesis by A6;
end;
hence thesis by A3;
end;
theorem Th11:
i divides j & i divides h implies i divides j mod h
proof
assume that
A1: i divides j and
A2: i divides h;
A3: now
assume h = 0;
then j mod h = 0;
hence thesis by Th6;
end;
now
assume h <> 0;
then
A4: j = h * (j div h) + (j mod h) by INT_1:59;
i divides h * (j div h) by A2,Th9;
hence thesis by A1,A4,Th10;
end;
hence thesis by A3;
end;
:: The least common multiple and the greatest common divisor
definition
let k,n be natural Number;
redefine func k lcm n means :: redefines lcm (INT_2, definition)
:Def4:
k divides it & n divides it &
for m being Nat st k divides m & n divides m holds it divides m;
compatibility
proof
let IT be Nat;
thus IT = k lcm n implies k divides IT & n divides IT &
for m being Nat st k divides m & n divides m holds IT divides m
by INT_2:def 1;
assume that
A1: k divides IT and
A2: n divides IT and
A3: for m being Nat st k divides m & n divides m holds IT divides m;
for m being Integer st k divides m & n divides m holds IT divides m
proof
let m be Integer;
m in INT by INT_1:def 2;
then consider i being Nat such that
A4: m = i or m = -i by INT_1:def 1;
assume that
A5: k divides m and
A6: n divides m;
A7: k divides i by A4,A5,INT_2:10;
n divides i by A4,A6,INT_2:10;
then IT divides i by A3,A7;
hence thesis by A4,INT_2:10;
end;
hence thesis by A1,A2,INT_2:def 1;
end;
end;
definition
let k,n be Nat;
redefine func k lcm n -> Element of NAT; :: redefines lcm (NAT_D, redefinition) → lcm (INT_2, definition)
coherence by ORDINAL1:def 12;
end;
definition
let k,n be natural Number;
redefine func k gcd n means :: redefines gcd (INT_2, definition)
:Def5:
it divides k & it divides n &
for m being Nat st m divides k & m divides n holds m divides it;
compatibility
proof
let IT be Nat;
thus IT = k gcd n implies IT divides k & IT divides n &
for m being Nat st m divides k & m divides n holds m divides IT
by INT_2:def 2;
assume that
A1: IT divides k and
A2: IT divides n and
A3: for m being Nat st m divides k & m divides n holds m divides IT;
for m being Integer st m divides k & m divides n holds m divides IT
proof
let m be Integer;
m in INT by INT_1:def 2;
then consider i being Nat such that
A4: m = i or m = -i by INT_1:def 1;
assume that
A5: m divides k and
A6: m divides n;
A7: i divides k by A4,A5,INT_2:10;
i divides n by A4,A6,INT_2:10;
then i divides IT by A3,A7;
hence thesis by A4,INT_2:10;
end;
hence thesis by A1,A2,INT_2:def 2;
end;
end;
definition
let k,n be Nat;
redefine func k gcd n -> Element of NAT; :: redefines gcd (NAT_D, redefinition) → gcd (INT_2, definition)
coherence by ORDINAL1:def 12;
end;
::$N Correctness of Euclid's Algorithm
::$N Greatest Common Divisor Algorithm
::$L https://en.wikipedia.org/wiki/Euclidean_algorithm Euclidean algorithm
scheme Euklides { Q(Nat)->Nat, a,b()->Nat } :
ex n being Nat st Q(n) = a() gcd b() & Q(n + 1) = 0
provided
A1: 0 < b() & b() < a() and
A2: Q(0) = a() & Q(1) = b() and
A3: for n being Nat holds Q(n + 2) = Q(n) mod Q(n + 1)
proof
defpred P[Nat] means ex n being Element of NAT st $1 = Q(n);
A4: ex k being Nat st P[k] by A2;
A5: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof
let k be Nat;
assume that
A6: k <> 0 and
A7: ex n being Element of NAT st k = Q(n);
consider n being Element of NAT such that
A8: k = Q(n) by A7;
reconsider Q = Q(n+1) as Element of NAT by ORDINAL1:def 12;
A9: n = 0 implies Q < k by A1,A2,A8;
now
given m being Nat such that
A10: n = m + 1;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
Q(m1 + 2) = Q(m1) mod Q(m1 + 1) by A3;
hence Q(n + 1) < k by A6,A8,A10,Th1;
take m = n + 1;
thus Q(n + 1) =Q(m);
end;
hence thesis by A9,NAT_1:6;
end;
A11: P[0] from NAT_1:sch 7(A4,A5);
defpred Q[Nat] means 0 = Q($1);
A12: ex n being Nat st Q[n] by A11;
consider k being Nat such that
A13: Q[k] & for n being Nat st Q[n] holds k <= n from NAT_1:sch 5(A12);
consider n be Nat such that
A14: k = n + 1 by A1,A2,A13,NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
defpred PP[Nat] means Q(n) divides Q($1) & Q(n) divides Q($1 + 1);
PP[n] by A13,A14,Th6;
then
A15: ex k being Nat st PP[k];
A16: for k being Nat st k <> 0 & PP[k] ex m being Nat st m < k & PP[m]
proof
let l be Nat;
assume that
A17: l <> 0 and
A18: Q(n) divides Q(l) and
A19: Q(n) divides Q(l + 1);
consider m be Nat such that
A20: l = m + 1 by A17,NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
take m;
A21: m <= m + 1 by NAT_1:11;
m <> m + 1;
hence m < l by A20,A21,XXREAL_0:1;
A22: now
assume
A23: Q(m + 1) = 0;
now
assume
A24: m + 1 <> k;
k <= m + 1 by A13,A23;
then k < m + 1 by A24,XXREAL_0:1;
then
A25: k <= m by NAT_1:13;
defpred Q[Nat] means k <= $1 implies Q($1) = 0;
A26: Q[0] by A13;
A27: for m being Nat st Q[m] holds Q[m+1]
proof
let m be Nat 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,XXREAL_0:1;
then consider l be Nat such that
A31: m = l + 1 by A1,A2,A28,NAT_1:6,13;
reconsider l as Element of NAT by ORDINAL1:def 12;
Q(l + 2) = Q(l) mod Q(l + 1) by A3;
hence thesis by A28,A30,A31,NAT_1:13;
end;
hence thesis by A13;
end;
for m being Nat holds Q[m] from NAT_1:sch 2(A26,A27);
then Q(m) = 0 by A25;
hence Q(n) divides Q(m) by Th6;
end;
hence Q(n) divides Q(m) by A14;
end;
now
assume
A32: Q(m + 1) <> 0;
Q(m + 2) = Q(m) mod Q(m + 1) by A3;
then
A33: Q(m) = Q(m + 1) * (Q(m) div Q(m + 1)) + Q(m + 2) by A32,INT_1:59;
Q(n) divides Q(m + 1) * (Q(m) div Q(m + 1)) by A18,A20,Th9;
hence Q(n) divides Q(m) by A19,A20,A33,Th8;
end;
hence Q(n) divides Q(m) by A22;
thus Q(n) divides Q(m + 1) by A18,A20;
end;
now
PP[0] from NAT_1:sch 7(A15,A16);
hence Q(n) divides a() & Q(n) divides b() by A2;
let m be Nat;
defpred P1[Nat] means m divides Q($1) & m divides Q($1 + 1);
assume that
A34: m divides a() and
A35: m divides b();
A36: P1[0] by A2,A34,A35;
A37: for k be Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume that
A38: m divides Q(k) and
A39: m divides Q(k + 1);
thus m divides Q(k + 1) by A39;
Q(k + 2) = Q(k) mod Q(k + 1) by A3;
hence m divides Q(k + 1 + 1) by A38,A39,Th11;
end;
for k be Nat holds P1[k] from NAT_1:sch 2(A36,A37);
hence m divides Q(n);
end;
hence Q(n) = a() gcd b() by Def5;
thus thesis by A13,A14;
end;
theorem
n mod 2 = 0 or n mod 2 = 1
proof
assume
A1: n mod 2 <> 0;
A2: 2 = 1 + 1;
n mod 2 < 2 by Th1;
then
A3: n mod 2 <= 1 by A2,NAT_1:13;
n mod 2 >= 1 by A1,NAT_1:14;
hence thesis by A3,XXREAL_0:1;
end;
theorem
(k * n) mod k = 0
proof
A0: k is Nat & n is Nat by TARSKI:1;
per cases;
suppose k = 0;
thus thesis;
end;
suppose
A1: k <> 0;
k * n = k * n + 0;
thus thesis;
end;
end;
theorem
k > 1 implies 1 mod k = 1
proof
assume
A1: k > 1;
1 = k * 0 + 1;
hence thesis by A1,Def2;
end;
theorem
k mod n = 0 & l = k - m * n implies l mod n = 0
proof
assume that
A1: k mod n = 0 and
A2: l = k - m * n;
per cases;
suppose n = 0;
hence thesis;
end;
suppose n <> 0;
then consider t being Nat such that
A3: k = n * t + 0 and
A4: 0 < n by A1,Def2;
A5: l = n * (t - m) + 0 by A2,A3;
now
assume t < m + 0;
then t - m < 0 by XREAL_1:19;
then l < n * 0 by A4,A5,XREAL_1:68;
hence contradiction;
end;
then t - m is Element of NAT by NAT_1:21;
thus thesis by A5;
end;
end;
theorem
n <> 0 & k mod n = 0 & l < n implies k + l mod n = l
proof
A0: k is Nat & n is Nat & l is Nat by TARSKI:1;
assume that
A1: n <> 0 and
A2: k mod n = 0 and
A3: l < n;
ex t being Nat st k = n * t + 0 & 0 < n by A1,A2,Def2;
hence thesis by A0,A3,Def2;
end;
theorem
k mod n = 0 implies k + l mod n = l mod n
proof
assume that
A1: k mod n = 0;
per cases;
suppose
A2: n = 0;
hence k + l mod n = 0
.= l mod n by A2;
end;
suppose
A3: n <> 0;
then consider m being Nat such that
A4: k = n * m + 0 and 0 < n by A1,Def2;
consider t being Nat such that
A5: l = n * t + (l mod n) and
A6: l mod n < n by A3,Def2;
k + l = n * (m + t) + (l mod n) by A4,A5;
hence thesis by A6,Def2;
end;
end;
theorem
k <> 0 implies (k * n) div k = n
proof
A0: k is Nat & n is Nat by TARSKI:1;
assume
A1: k <> 0;
k * n = k * n + 0;
hence thesis by A0,A1,Def1;
end;
theorem
k mod n = 0 implies (k + l) div n = (k div n) + (l div n)
proof
assume
A1: k mod n = 0;
per cases;
suppose
A2: n <> 0;
then
A3: k = n * (k div n) + 0 by A1,INT_1:59;
A4: ex t being Nat st l = n * t + (l mod n) & l mod n < n by A2,Def2;
l = n * (l div n) + (l mod n) by A2,INT_1:59;
then k + l = n * ((k div n) + (l div n)) + (l mod n) by A3;
hence thesis by A4,Def1;
end;
suppose n = 0;
hence thesis;
end;
end;
begin :: Addenda
::$CT
:: from GR_CY_1, 2005.11.16, A.T.
theorem Th21:
m mod n = (n*k + m) mod n
proof
per cases;
suppose
A1: n > 0;
m mod n = t implies (n*k + m) mod n = t
proof
assume m mod n = t;
then consider q being Nat such that
A2: m = n * q + t and
A3: t < n by A1,Def2;
A0: k is Nat & m is Nat & n is Nat & t is Nat by TARSKI:1;
ex p be Nat st n*k + m = n*p + t & t < n
proof
reconsider p = k+q as Element of NAT by ORDINAL1:def 12;
take p;
thus thesis by A2,A3;
end;
hence thesis by A0,Def2;
end;
hence thesis;
end;
suppose n = 0;
hence thesis;
end;
end;
theorem Th22:
(p+s) mod n = ((p mod n)+s) mod n
proof
per cases;
suppose n > 0;
then (p + s) mod n = (n*(p div n) + (p mod n) + s) mod n by INT_1:59
.=(n*(p div n) + ((p mod n) + s)) mod n
.=((p mod n) + s) mod n by Th21;
hence thesis;
end;
suppose
A1: n = 0;
hence (p+s) mod n = 0
.= ((p mod n)+s) mod n by A1;
end;
end;
theorem
(p+s) mod n = (p + ( s mod n)) mod n by Th22;
theorem Th24:
k < n implies k mod n = k
proof
k=n*0 + k;
hence thesis by Def2;
end;
theorem Th25:
n mod n = 0
proof
per cases;
suppose
A1: n>0;
n=n*1+0;
hence thesis;
end;
suppose n = 0;
hence thesis;
end;
end;
theorem Th26:
0 = 0 mod n
proof
n = 0 or n > 0;
hence thesis by Th24;
end;
:: from JORDAN4
theorem Th27:
i < j implies i div j = 0
proof
assume
A1: i<j;
per cases by Def1;
suppose ex j1 being Nat st i=j*(i div j)+j1 & j1<j;
then consider j1 being Nat such that
A2: i=j*(i div j)+j1 and j1<j;
assume i div j<>0;
then consider k be Nat such that
A3: i div j = k+1 by NAT_1:6;
i = j + (j*k+j1) by A2,A3;
hence contradiction by A1,NAT_1:11;
end;
suppose i div j=0 & j=0;
hence thesis;
end;
end;
:: Moved from SCMP_GCD by AK on 28.12.2006
theorem Th28:
m > 0 implies n gcd m = m gcd (n mod m)
proof
set r=n mod m, x=n gcd m, y=m gcd r;
assume m>0;
then consider t be Nat such that
A1: n = m * t + r and r < m by Def2;
reconsider t as Element of NAT by ORDINAL1:def 12;
A2: x divides n by Def5;
A3: x divides m by Def5;
then x divides r by A2,Th11;
then
A4: x divides y by A3,Def5;
A5: y divides m by Def5;
A6: y divides r by Def5;
y divides m*t by A5,Th9;
then y divides n by A1,A6,Th8;
then y divides x by A5,Def5;
hence thesis by A4,Th5;
end;
:: from AMI_3, 2007.06.14, A.T.
scheme INDI{ k,n() -> Element of NAT, P[set] }: P[n()]
provided
A1: P[0] and
A2: k() > 0 and
A3: for i,j being Nat st P[k()*i] & j <> 0 & j <= k() holds P[k()*i+j]
proof
defpred R[Nat] means P[k()*$1];
A4: R[0] by A1;
A5: now
let i be Nat;
assume
A6: R[i];
k()*(i+1) = k()*i + k();
hence R[i+1] by A2,A3,A6;
end;
A7: for i be Nat holds R[i] from NAT_1:sch 2(A4,A5);
per cases;
suppose n() mod k() = 0;
then n() = k() * (n() div k()) + 0 by A2,INT_1:59;
hence thesis by A7;
end;
suppose
A8: n() mod k() <> 0;
A9: n() = k() * (n() div k()) + (n() mod k()) by A2,INT_1:59;
n() mod k() <= k() by A2,Th1;
hence thesis by A3,A7,A8,A9;
end;
end;
:: moved from INT_2, 2007.11.7, A.T,
theorem
i*j = (i lcm j)*(i gcd j)
proof
A0: i is Nat & j is Nat by TARSKI:1;
A1: i<>0 & j<>0 implies i*j = (i lcm j)*(i gcd j)
proof
assume that
A2: i<>0 and
A3: j<>0;
A4: i divides i implies i divides i*j by A0;
j divides j implies j divides j*i by A0;
then (i lcm j) divides i*j by A4,Def4;
then consider c being Nat such that
A5: i*j = (i lcm j)*c;
A6: i divides (i lcm j) by Def4;
A7: j divides (i lcm j) by Def4;
consider d being Nat such that
A8: (i lcm j) = i*d by A6;
consider e being Nat such that
A9: (i lcm j) = j*e by A7;
i*j = i*(c*d) by A5,A8;
then
A10: j = c*d by A2,XCMPLX_1:5;
i*j = j*(c*e) by A5,A9;
then i = c*e by A3,XCMPLX_1:5;
then
A11: c divides i;
A12: c divides j by A10;
for f being Nat holds f divides i & f divides j implies f divides c
proof
let f be Nat;
assume that
A13: f divides i and
A14: f divides j;
consider g being Nat such that
A15: i = f*g by A13;
consider h being Nat such that
A16: j = f*h by A14;
A17: j*g = g*h*f by A16;
i*h = g*h*f by A15;
then
A18: i divides g*h*f;
j divides g*h*f by A17;
then (i lcm j) divides g*h*f by A18,Def4;
then consider z being Nat such that
A19: g*h*f = (i lcm j)*z;
A20: c*(i lcm j) = (g*(h*f))*f by A5,A15,A16
.= (i lcm j)*z*f by A19
.= (z*f)*(i lcm j);
(i lcm j) <> 0 by A2,A3,INT_2:4;
then c = f*z by A20,XCMPLX_1:5;
hence thesis;
end;
hence thesis by A5,A11,A12,Def5;
end;
i = 0 or j = 0 implies i*j = (i lcm j)*(i gcd j)
proof
assume
A21: i = 0 or j = 0;
then i*j = 0*(i gcd j) .= (i lcm j)*(i gcd j) by A21,INT_2:4;
hence thesis;
end;
hence thesis by A1;
end;
:: from from SCMP_GCD, 2007.07.26, A.T.
theorem
for i,j being Integer st i>=0 & j>0 holds i gcd j= j gcd (i mod j)
proof
let i,j be Integer;
assume that
A1: i>=0 and
A2: j>0;
A3: |.j.|> 0 by A2,ABSVALUE:def 1;
thus i gcd j = |.i.| gcd |.j.| by INT_2:34
.=|.j.| gcd (|.i.| mod |.j.|) by A3,Th28
.=|.j.| gcd |.|.i.| mod |.j.|.| by ABSVALUE:def 1
.=j gcd (|.i.| mod |.j.|) by INT_2:34
.=j gcd (i mod j) by A1,A2,INT_2:32;
end;
:: ???, 2007.07.26, A.T.
theorem
i lcm i = i
proof
A0: i is Nat by TARSKI:1;
for m being Nat st i divides m & i divides m holds i divides m;
hence thesis by A0,Def4;
end;
theorem
i gcd i = i
proof
A0: i is Nat by TARSKI:1;
for m being Nat st m divides i & m divides i holds m divides i;
hence thesis by A0,Def5;
end;
:: from SCMPDS_9. 2008.05.06, A.T.
theorem
i < j & i <> 0 implies i/j is not integer
proof
assume that
A1: i < j and
A2: i <> 0;
assume i/j is integer;
then reconsider r = i/j as Integer;
r = [\ r /]
.= i qua Integer div j by INT_1:def 9;
hence thesis by A1,A2,Th27,XCMPLX_1:50;
end;
:: from BINARITH, 2008.08.18, A.T.
registration
let i,j be Nat;
cluster i -' j -> natural;
coherence
proof
i -' j = i - j & 0 <= i -' j or i -' j = 0 by XREAL_0:def 2;
then i-'j in NAT by INT_1:3;
hence thesis;
end;
end;
definition
let i,j be Nat;
redefine func i -' j -> Element of NAT; :: redefines -' (XREAL_0, definition)
coherence by ORDINAL1:def 12;
end;
theorem Th34:
i + j -' j = i
proof
i + j - j >= 0;
hence thesis by XREAL_0:def 2;
end;
theorem Th35:
a -' b <= a
proof
a-b <= a-0 by XREAL_1:230;
hence thesis by XREAL_0:def 2;
end;
theorem Th36:
n-'i=0 implies n<=i
proof
assume
A1: n-'i=0;
assume i<n;
then i+1<=n by NAT_1:13;
then i+1-i<=n-i by XREAL_1:9;
hence contradiction by A1,XREAL_0:def 2;
end;
theorem
i<=j implies j+k-'i=j+k-i by NAT_1:12,XREAL_1:233;
theorem
i<=j implies j+k-'i=j-'i+k
proof
assume
A1: i<=j;
hence j+k-'i=j+k-i by NAT_1:12,XREAL_1:233
.=j-i+k
.=j-'i+k by A1,XREAL_1:233;
end;
theorem Th39:
i-'i1>=1 or i-i1>=1 implies i-'i1=i-i1
proof
assume
A1: i-'i1>=1 or i-i1>=1;
per cases by A1;
suppose i-'i1>=1;
hence thesis by XREAL_0:def 2;
end;
suppose i-i1>=1;
hence thesis by XREAL_0:def 2;
end;
end;
theorem
n-'0=n
proof
n-'0=n-0 by XREAL_0:def 2
.=n;
hence thesis;
end;
theorem
i1<=i2 implies n-'i2<=n-'i1
proof
assume
A1: i1<=i2;
per cases;
suppose
A2: i2<=n;
then
A3: n-'i1=n-i1 by A1,XREAL_1:233,XXREAL_0:2;
n-'i2=n-i2 by A2,XREAL_1:233;
hence thesis by A1,A3,XREAL_1:10;
end;
suppose i2>n;
then n-i2<0 by XREAL_1:49;
hence thesis by XREAL_0:def 2;
end;
end;
theorem Th42:
i1<=i2 implies i1-'n<=i2-'n
proof
assume
A1: i1<=i2;
per cases;
suppose i1-n>=0;
then
A2: i1-'n=i1-n by XREAL_0:def 2;
i1-n<=i2-n by A1,XREAL_1:9;
hence thesis by A2,XREAL_0:def 2;
end;
suppose i1-n<0;
hence thesis by XREAL_0:def 2;
end;
end;
theorem Th43:
i-'i1>=1 or i-i1>=1 implies i-'i1+i1=i
proof
assume i-'i1>=1 or i-i1>=1;
then i-'i1+i1=i-i1+i1 by Th39
.=i;
hence thesis;
end;
theorem
i1<=i2 implies i1-'1<=i2
proof
assume
A1: i1<=i2;
reconsider i1,i2 as Nat by TARSKI:1;
per cases;
suppose i1-1>=0;
then i1-'1=i1-1 by XREAL_0:def 2;
then i1-'1<=i1-1+1 by NAT_1:12;
hence thesis by A1,XXREAL_0:2;
end;
suppose i1-1<0;
hence thesis by XREAL_0:def 2;
end;
end;
theorem Th45:
i-'2=i-'1-'1
proof
per cases;
suppose
A1: i>=2;
then 1<=i by XXREAL_0:2;
then i-1>=0 by XREAL_1:48;
then
A2: i-'1=i-1 by XREAL_0:def 2;
i-1>=1+1-1 by A1,XREAL_1:9;
then i-1-1>=1-1 by XREAL_1:9;
then i-'1-'1 =i-2 by A2,XREAL_0:def 2;
hence thesis by XREAL_0:def 2;
end;
suppose
A3: i<2;
then i-2<2-2 by XREAL_1:9;
then
A4: i-'2=0 by XREAL_0:def 2;
A5: i+1-1<=1+1-1 by A3,NAT_1:13;
now per cases;
case 1<=i;
then i=1 by A5,XXREAL_0:1;
then i-'1-'1=0-'1 by XREAL_1:232;
hence thesis by A4,Th35;
end;
case i<1;
then i-1<1-1 by XREAL_1:9;
then i-'1-'1=0-'1 by XREAL_0:def 2;
hence thesis by A4,Th35;
end;
end;
hence thesis;
end;
end;
theorem Th46:
i1+1<=i2 implies i1-'1<i2 & i1-'2<i2 & i1<=i2
proof
assume
A1: i1+1<=i2;
then
A2: i1<i2 by NAT_1:13;
i1-'1<=i1 by Th35;
hence
A3: i1-'1<i2 by A2,XXREAL_0:2;
A4: i1-'1-'1=i1-'2 by Th45;
reconsider i1 as Nat by TARSKI:1;
i1-'1-'1<=i1-'1 by Th35;
hence thesis by A1,A3,A4,XXREAL_0:2,NAT_1:13;
end;
theorem
i1+2<=i2 or i1+1+1<=i2 implies i1+1<i2 & i1+1-'1<i2 & i1+1-'2<i2 & i1+1<=i2 &
i1-'1+1<i2 & i1-'1+1-'1<i2 & i1<i2 & i1-'1<i2 & i1-'2<i2 & i1<=i2
proof
assume i1+2<=i2 or i1+1+1<=i2;
then i1+1+1<=i2;
hence
A1: i1+1<i2 & i1+1-'1<i2 & i1+1-'2<i2 & i1+1<=i2 by Th46,NAT_1:13;
i1-'1<=i1 by Th35;
then i1-'1+1<=i1+1 by XREAL_1:6;
then
A2: i1-'1+1<i2 by A1,XXREAL_0:2;
reconsider i1 as Nat by TARSKI:1;
i1-'1+1-'1<=i1-'1+1 by Th35;
hence thesis by A1,Th46,A2,XXREAL_0:2,NAT_1:13;
end;
theorem
i1<=i2 or i1<=i2-'1 implies
i1<i2+1 & i1<=i2+1 & i1<i2+1+1 & i1<=i2+1+1 & i1<i2+2 & i1<=i2+2
proof
assume
A1: i1<=i2 or i1<=i2-'1;
A2: now
assume i1<=i2;
then
A3: i1<i2+1 by NAT_1:13;
i2+1+1=i2+(1+1);
hence thesis by A3,NAT_1:13;
end;
now
assume
A4: i1<=i2-'1;
i2-'1<=i2 by Th35;
hence thesis by A2,A4,XXREAL_0:2;
end;
hence thesis by A1,A2;
end;
theorem
i1<i2 or i1+1<=i2 implies i1<=i2-'1
proof
assume
A1: i1<i2 or i1+1<=i2;
per cases by A1;
suppose
A2: i1<i2;
then i1+1<=i2 by NAT_1:13;
then
A3: i1+1-1<=i2-1 by XREAL_1:9;
0+1<=i2 by A2,NAT_1:13;
hence thesis by A3,XREAL_1:233;
end;
suppose
A4: i1+1<=i2;
then
A5: i1+1-1<=i2-1 by XREAL_1:9;
0+1<=i2 by A4,NAT_1:13;
hence thesis by A5,XREAL_1:233;
end;
end;
theorem Th50:
i>=i1 implies i>=i1-'i2
proof
assume
A1: i>=i1;
i1>=i1-'i2 by Th35;
hence thesis by A1,XXREAL_0:2;
end;
theorem
1<=i & 1<=i1-'i implies i1-'i<i1
proof
assume that
A1: 1<=i and
A2: 1<=i1-'i;
i1-i=(i1-'i)+i-i by A2,Th43
.=i1-'i;
hence thesis by A1,XREAL_1:231;
end;
theorem Th52:
i-'k <= j implies i <= j + k
proof
assume
A1: i-'k <= j;
per cases;
suppose
A2: i >= k;
i-'k +k <= j + k by A1,XREAL_1:6;
hence thesis by A2,XREAL_1:235;
end;
suppose
A3: i <= k;
k <= j + k by NAT_1:11;
hence thesis by A3,XXREAL_0:2;
end;
end;
theorem
i <= j + k implies i-'k <= j
proof
assume i <= j + k;
then i -' k <= j + k -' k by Th42;
hence thesis by Th34;
end;
theorem
i <= j -' k & k <= j implies i + k <= j
proof
assume that
A1: i <= j -' k and
A2: j >= k;
i + k <= j -' k + k by A1,XREAL_1:6;
hence thesis by A2,XREAL_1:235;
end;
theorem
j + k <= i implies k <= i -' j
proof
assume
A1: j + k <= i;
per cases by A1,XXREAL_0:1;
suppose j + k = i;
hence thesis by Th34;
end;
suppose j + k < i;
hence thesis by Th52;
end;
end;
theorem
k <= i & i < j implies i -' k < j -' k
proof
assume that
A1: k <= i and
A2: i < j;
i -' k + k = i by A1,XREAL_1:235;
then i -' k + k < j -' k + k by A1,A2,XREAL_1:235,XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
theorem
i < j & k < j implies i -' k < j -' k
proof
assume that
A1: i < j and
A2: k < j;
per cases;
suppose k <= i;
then
A3: i -' k = i - k by XREAL_1:233;
j -' k = j - k by A2,XREAL_1:233;
hence thesis by A1,A3,XREAL_1:9;
end;
suppose k > i;
then i - k < 0 by XREAL_1:49;
then
A4: i -' k = 0 by XREAL_0:def 2;
j -' k <> 0 by A2,Th36;
hence thesis by A4;
end;
end;
:: form JCT_MISC, 2008.08.21, A.T.
theorem
i <= j implies j-'(j-'i) = i
proof
assume
A1: i <= j;
j-'(j-'i) + (j-'i) = j by Th50,XREAL_1:235
.= i + (j-'i) by A1,XREAL_1:235;
hence thesis;
end;
:: from LEXBFS, 2008.08.23, A.T.
theorem
n < k implies k -' (n+1) + 1 = k -' n
proof
assume
A1: n < k;
A2: k -' n = k - n by A1,XREAL_1:233;
n+1 <= k by A1,NAT_1:13;
then k -' (n+1) = k - (n+1) by XREAL_1:233;
hence thesis by A2;
end;
theorem
for A being finite set holds A is trivial iff card A < 2
proof
let A be finite set;
hereby
assume
A1: A is trivial;
per cases;
suppose
A is empty;
hence card A < 2;
end;
suppose
A is non empty;
then ex x being object st A = {x} by A1,ZFMISC_1:131;
then card A = 1 by CARD_1:30;
hence card A < 2;
end;
end;
assume
A2: card A < 2;
per cases by A2,NAT_1:23;
suppose card A = 0;
hence thesis;
end;
suppose card A = 1;
then A is 1-element by CARD_1:def 7;
hence thesis;
end;
end;
:: from INT_3, 2011.04.28, A.T.
theorem Th61:
for n,a,k being Integer holds
(n <> 0 implies (a + n * k) div n = (a div n) + k) &
(a + n * k) mod n = a mod n
proof
let n,a,k be Integer;
thus
A1: now
assume
A2: n <> 0;
thus (a + n * k) div n = [\ (a + n * k)/n /] by INT_1:def 9
.= [\ (a + n * k) * n" /] by XCMPLX_0:def 9
.= [\ a * n" + (n * n") * k /]
.= [\ a * n" + 1 * k /] by A2,XCMPLX_0:def 7
.= [\ a * n" /] + k by INT_1:28
.= [\ a/n /] + k by XCMPLX_0:def 9
.= (a div n) + k by INT_1:def 9;
end;
per cases;
suppose
A3: n <> 0;
hence (a + n * k) mod n = (a + n * k) - ((a div n) + k) * n by A1,
INT_1:def 10
.= a - (a div n) * n
.= a mod n by A3,INT_1:def 10;
end;
suppose
n = 0;
hence thesis;
end;
end;
theorem Th62:
for n being natural Number st n > 0
for a being Integer holds a mod n >= 0 & a mod n < n
proof
let n be natural Number;
assume
A1: n > 0;
let a be Integer;
now
a div n = [\ a/n /] by INT_1:def 9;
then a div n <= a/n by INT_1:def 6;
then (a div n) * n <= a/n * n by XREAL_1:64;
then (a div n) * n <= (a * n") * n by XCMPLX_0:def 9;
then (a div n) * n <= a * (n" * n);
then (a div n) * n <= a * 1 by A1,XCMPLX_0:def 7;
then (a div n) * n - (a div n) * n <= a - (a div n) * n by XREAL_1:9;
thus 0 <= a mod n;
assume a mod n >= n;
then a - (a div n) * n >= n by A1,INT_1:def 10;
then (a + -(a div n) * n) + (a div n) * n >= n + (a div n) * n by XREAL_1:6
;
then a - n >= (n + (a div n) * n) - n by XREAL_1:9;
then (a - n) * n" >= ((a div n) * n) * n" by XREAL_1:64;
then (a - n) * n" >= (a div n) * (n * n");
then a * n" - n * n" >= (a div n) * 1 by A1,XCMPLX_0:def 7;
then a * n" - 1 >= (a div n) by A1,XCMPLX_0:def 7;
then
A2: a/n - 1 >= (a div n) by XCMPLX_0:def 9;
a div n = [\ a/n /] by INT_1:def 9;
hence contradiction by A2,INT_1:def 6;
end;
hence thesis;
end;
theorem Th63:
for n,a being Integer holds (0 <= a & a < n implies a mod n = a)
& (0 > a & a >= -n implies a mod n = n + a)
proof
let n,a be Integer;
per cases;
suppose
n = 0;
hence thesis;
end;
suppose
A1: n <> 0;
hereby
assume that
A2: 0 <= a and
A3: a < n;
reconsider aa = a as Element of NAT by A2,INT_1:3;
reconsider nn = n as Element of NAT by A2,A3,INT_1:3;
consider t being Nat such that
A4: aa = nn * t + (aa mod nn) and
(aa mod nn) < nn by A1,Def2;
t = 0
proof
assume t <> 0;
then t >= 1 + 0 by INT_1:7;
then
A5: t * n >= 1 * n by A2,A3,XREAL_1:64;
nn * t + (aa mod nn) >= nn * t by NAT_1:11;
hence thesis by A3,A4,A5,XXREAL_0:2;
end;
hence a mod n = a by A4;
end;
assume that
A6: 0 > a and
A7: a >= -n;
A8: n >= 0 by A6,A7;
A9: a/n - 1 < -1
proof
assume a/n - 1 >= -1;
then (a/n - 1) + 1 >= -1 + 1 by XREAL_1:6;
then a * n" >= 0 by XCMPLX_0:def 9;
then (a * n") * n >= 0 * n by A8;
then a * (n" * n) >= 0;
then a * 1 >= 0 by A1,XCMPLX_0:def 7;
hence thesis by A6;
end;
a * n" >= (-n) * n" by A7,A8,XREAL_1:64;
then a /n >= -(n * n") by XCMPLX_0:def 9;
then -1 <= a/n by A1,XCMPLX_0:def 7;
then [\ a/n /] = -1 by A9,INT_1:def 6;
then
A10: a div n = -1 by INT_1:def 9;
a mod n = a - (a div n) * n by A1,INT_1:def 10;
hence thesis by A10;
end;
end;
theorem Th64:
for n,a,b being Integer holds
(n <> 0 & a mod n = b mod n implies a,b are_congruent_mod n) &
(a,b are_congruent_mod n implies a mod n = b mod n)
proof
let n,a,b be Integer;
hereby
assume
A1: n <> 0;
assume a mod n = b mod n;
then a - (a div n) * n = b mod n by A1,INT_1:def 10;
then a - (a div n) * n = b - (b div n) * n by A1,INT_1:def 10;
then a - b = (-(b div n) + (a div n)) * n;
then n divides (a-b) by INT_1:def 3;
hence a,b are_congruent_mod n by INT_2:15;
end;
assume a,b are_congruent_mod n;
then n divides (a-b) by INT_2:15;
then consider k being Integer such that
A2: n * k = a - b by INT_1:def 3;
a = n * k + b by A2;
hence thesis by Th61;
end;
theorem
for n being natural Number, a being Integer holds (a mod n) mod n = a mod n
proof
let n be natural Number;
let a be Integer;
per cases;
suppose
A1: n = 0;
hence (a mod n) mod n = 0
.= a mod n by A1;
end;
suppose
n <> 0;
then a mod n >= 0 & a mod n < n by Th62;
hence thesis by Th63;
end;
end;
theorem Th66:
for n,a,b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n
proof
let n,a,b be Integer;
per cases;
suppose
A1: n = 0;
hence (a + b) mod n = 0
.= ((a mod n) + (b mod n)) mod n by A1;
end;
suppose
n <> 0;
then
a mod n + (a div n) * n = (a - (a div n) * n) + (a div n) * n & b mod
n + (b div n) * n = (b - (b div n) * n) + (b div n) * n by INT_1:def 10;
then (a + b) - ((a mod n) + (b mod n)) = ((a div n) + (b div n)) * n;
then n divides (a + b) - ((a mod n) + (b mod n)) by INT_1:def 3;
then a+b,(a mod n)+(b mod n) are_congruent_mod n by INT_2:15;
hence thesis by Th64;
end;
end;
theorem Th67:
for n,a,b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n
proof
let n,a,b be Integer;
per cases;
suppose
A1: n = 0;
hence (a * b) mod n = 0
.= ((a mod n) * (b mod n)) mod n by A1;
end;
suppose
n <> 0;
then
a mod n + (a div n) * n = (a - (a div n) * n) + (a div n) * n & b mod
n + (b div n) * n = (b - (b div n) * n) + (b div n) * n by INT_1:def 10;
then (a * b) - ((a mod n) * (b mod n)) = (((a mod n) * (b div n)) + (((a
div n) * (b mod n)) + (((a div n) * n) * (b div n)))) * n;
then n divides ((a * b) - ((a mod n) * (b mod n))) by INT_1:def 3;
then (a*b),((a mod n)*(b mod n)) are_congruent_mod n by INT_2:15;
hence thesis by Th64;
end;
end;
::$N Bezout's identity
::$N Bezout's lemma
theorem
for a,b being Integer ex s,t being Integer st a gcd b = s * a + t * b
proof
let a,b be Integer;
A1: for a,b being Integer st a > 0 & b > 0 holds ex s,t being Integer st (a
gcd b) = (s * a + t * b)
proof
let a,b be Integer;
assume that
A2: a > 0 and
A3: b > 0;
reconsider a,b as Element of NAT by A2,A3,INT_1:3;
set M = {z where z is Element of NAT : ex s,t being Integer st z = s * a +
t * b};
defpred P[Nat] means ($1 in M & $1 <> 0);
a = 1 * a + 0 * b;
then
A4: a in M;
then
A5: ex k being Nat st P[k] by A2;
consider g being Nat such that
A6: P[g] & for n being Nat st P[n] holds g <= n from NAT_1:sch 5(A5);
set G = {zz where zz is Element of NAT : ex s being Element of NAT st zz =
s * g};
ex z being Element of NAT st z = g & ex s,t being Integer st z = s * a
+ t * b by A6;
then consider s,t being Integer such that
A7: g = s * a + t * b;
A8: for x being object holds x in M implies x in G
proof
let x be object;
assume x in M;
then consider x9 being Element of NAT such that
A9: x9 = x and
A10: ex u,v being Integer st x9 = u * a + v * b;
consider u,v being Integer such that
A11: x = u * a + v * b by A9,A10;
consider r being Nat such that
A12: x9 = g * (x9 div g) + r and
A13: r < g by A6,Def1;
A14: r in NAT by ORDINAL1:def 12;
r = x9 - g * (x9 div g) by A12
.= a * (u + -(s * (x9 div g))) + b * (v + -(t * (x9 div g)))
by A7,A9,A11;
then r in M by A14;
then r = 0 by A6,A13;
hence thesis by A9,A12;
end;
for x being object holds x in G implies x in M
proof
let x be object;
assume x in G;
then
A15: ex x9 being Element of NAT st x9 = x & ex u being Element of NAT st
x9 = u * g;
then consider u being Integer such that
A16: x = u * g;
x = (u * s) * a + (u * t) * b by A7,A16;
hence thesis by A15;
end;
then
A17: G = M by A8,TARSKI:2;
A18: |.b.| = b by ABSVALUE:def 1;
A19: |.a.| = a by ABSVALUE:def 1;
A20: for m being Nat st m divides |.a.| & m divides |.b.| holds m divides g
proof
ex g9 being Element of NAT st g9 = g & ex s,t being Integer st g9 =
s * a + t * b by A6;
then consider s,t being Integer such that
A21: g = s * a + t * b;
let m be Nat;
assume that
A22: m divides |.a.| and
A23: m divides |.b.|;
consider u being Nat such that
A24: a = m * u by A19,A22;
consider v being Nat such that
A25: b = m * v by A18,A23;
A26: g = m * (s * u + t * v) by A24,A25,A21;
then s * u + t * v >= 0 by A6;
then s * u + t * v is Element of NAT by INT_1:3;
hence thesis by A26;
end;
b = 0 * a + 1 * b;
then b in M;
then
ex b9 being Element of NAT st b9 = b & ex t being Element of NAT st b9
= t * g by A17;
then
A27: g divides |.b.| by A18;
ex a9 being Element of NAT st a9 = a & ex s being Element of NAT st a9
= s * g by A4,A17;
then g divides |.a.| by A19;
then g = |.a.| gcd |.b.| by A27,A20,Def5
.= a gcd b by INT_2:34;
hence thesis by A7;
end;
now
per cases;
case
A28: a = 0 or b = 0;
A29: for a,b being Integer holds a = 0 implies a gcd b = |.b.|
proof
let a,b be Integer;
assume a = 0;
then |.a.| = 0 by ABSVALUE:def 1;
then
A30: |.b.| divides |.a.| by Th6;
a gcd b = |.a.| gcd |.b.| & for m being Nat st m divides |.a.|
& m divides |.b.| holds m divides |.b.| by INT_2:34;
hence thesis by A30,Def5;
end;
now
per cases by A28;
case
a = 0;
then
A31: a gcd b = |.b.| by A29;
now
per cases;
case
b >= 0;
hence a gcd b = 0 * a + 1 * b by A31,ABSVALUE:def 1;
end;
case
b < 0;
hence a gcd b = -(b * 1) by A31,ABSVALUE:def 1
.= 0 * a + (-1) * b;
end;
end;
hence thesis;
end;
case
b = 0;
then
A32: a gcd b = |.a.| by A29;
now
per cases;
case
a >= 0;
hence a gcd b = 1 * a + 0 * b by A32,ABSVALUE:def 1;
end;
case
a < 0;
hence a gcd b = -(a * 1) by A32,ABSVALUE:def 1
.= 0 * b + (-1) * a;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A33: a <> 0 & b <> 0;
now
per cases;
case
a >= 0 & b >= 0;
hence thesis by A1,A33;
end;
case
A34: a < 0 & b >= 0;
then -a > 0 by XREAL_1:58;
then consider s,t being Integer such that
A35: -a gcd b = s * -a + t * b by A1,A33,A34;
A36: a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.-a.| gcd |.b.| by COMPLEX1:52
.= -a gcd b by INT_2:34;
s * -a + t * b = (-s) * a + t * b;
hence thesis by A35,A36;
end;
case
A37: a >= 0 & b < 0;
then -b > 0 by XREAL_1:58;
then consider s,t being Integer such that
A38: a gcd -b = s * a + t * -b by A1,A33,A37;
A39: a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.a.| gcd |.-b.| by COMPLEX1:52
.= a gcd -b by INT_2:34;
s * a + t * -b = s * a + (-t) * b;
hence thesis by A38,A39;
end;
case
a < 0 & b < 0;
then -a > 0 & -b > 0 by XREAL_1:58;
then consider s,t being Integer such that
A40: -a gcd -b = s * -a + t * -b by A1;
A41: a gcd b = |.a.| gcd |.b.| by INT_2:34
.= |.a.| gcd |.-b.| by COMPLEX1:52
.= |.-a.| gcd |.-b.| by COMPLEX1:52
.= -a gcd -b by INT_2:34;
s * -a + t * -b = (-s) * a + (-t) * b;
hence thesis by A40,A41;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
:: from RADIX_1, 2011.07.31, A.T.
theorem
n mod k = k - 1 implies (n+1) mod k = 0
proof
per cases;
suppose
k <> 0;
then k >= 1 by NAT_1:14;
then reconsider K = k - 1 as Element of NAT by INT_1:3,XREAL_1:48;
A1: K + 1 = k - 0;
assume n mod k = k-1;
then (n+1) mod k = k mod k by A1,Th22;
hence thesis by Th25;
end;
suppose
k=0;
hence thesis;
end;
end;
theorem
n mod k < k - 1 implies (n+1) mod k = (n mod k) + 1
proof
assume n mod k < k - 1;
then
A1: (n mod k) + 1 < k by XREAL_1:20;
(n+1) mod k = ((n mod k)+1) mod k by Th22;
hence thesis by A1,Th24;
end;
theorem
for i being Integer, n being Nat holds (i*n) mod n = 0
proof
let i be Integer, n be Nat;
(i*n) mod n = ((i mod n) * (n mod n)) mod n by Th67
.= ((i mod n) * 0) mod n by Th25
.= 0 mod n;
thus thesis;
end;
theorem :: NAT_D:43
m-n >= 0 implies m-'n+n = m
proof
assume m-n >= 0;
then m-'n = m-n by XREAL_0:def 2;
hence thesis;
end;
:: from NTALGO_1
theorem
for m,n be Integer holds (m mod n) mod n = m mod n
proof
let m,n be Integer;
m mod n = (m + 0) mod n .= ((m mod n) + (0 mod n)) mod n by Th66
.= ((m mod n) + 0) mod n by INT_1:73;
hence thesis;
end;