:: Euler's Function
:: by Yoshinori Fujisawa and Yasushi Fuwa
::
:: Received December 10, 1997
:: Copyright (c) 1997-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, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1,
RELAT_1, INT_2, SUBSET_1, FINSET_1, XBOOLE_0, TARSKI, COMPLEX1, FUNCT_1,
FUNCT_2, FINSEQ_1, NEWTON, ZFMISC_1, EULER_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, INT_1, NAT_1, NAT_D, INT_2, FINSEQ_1, FINSET_1, RELAT_1,
FUNCT_1, FUNCT_2, BINOP_1, XXREAL_0, NEWTON;
constructors BINOP_1, XXREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, WELLORD2,
RELSET_1, MEMBERED;
registrations ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
CARD_1, FINSEQ_1, NEWTON, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_1, FUNCT_2, XBOOLE_0;
equalities TARSKI, XBOOLE_0, BINOP_1, ORDINAL1;
expansions FUNCT_2, XBOOLE_0;
theorems TARSKI, INT_2, AXIOMS, FINSEQ_1, CARD_1, NAT_1, ABSVALUE, CARD_2,
ZFMISC_1, INT_1, FUNCT_1, FUNCT_2, PRE_FF, DOMAIN_1, XBOOLE_0, XBOOLE_1,
XCMPLX_1, NEWTON, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, RELAT_1;
schemes NAT_1, FUNCT_7;
begin :: Preliminary
reserve a,b,c,k,l,m,n for Nat,
i,j,x,y for Integer;
Lm1: k <> 0 & ([\ j/k /]) + 1 >= j/k implies k >= j - (([\ j/k /])*k)
proof
assume that
A1: k <> 0 and
A2: ([\ j/k /]) + 1 >= j/k;
([\ j/k /]) + 1 + -1 >= j/k + -1 by A2,XREAL_1:6;
then ([\ j/k /]) *k >= ((j/k)-1)*k by XREAL_1:64;
then -(((j/k) - 1)*k) >= -(([\ j/k /])*k) by XREAL_1:24;
then j + -(((j/k) - 1)*k) >= j + -(([\ j/k /])*k) by XREAL_1:6;
then j - ((j/k)*k - 1*k) >= j - (([\ j/k /])*k);
then j -(j - k) >= j - (([\ j/k /])*k) by A1,XCMPLX_1:87;
hence thesis;
end;
Lm2: not 1 is prime by INT_2:def 4;
theorem Th1:
n,n are_coprime iff n = 1
proof
n gcd n = n by NAT_D:32;
hence thesis by INT_2:def 3;
end;
theorem Th2:
for k,n be Nat holds k <> 0 & k < n & n is prime implies k,n are_coprime
proof
let k,n be Nat;
assume that
A1: k <> 0 & k < n and
A2: n is prime;
A3: (k gcd n) divides n by NAT_D:def 5;
per cases by A2,A3,INT_2:def 4;
suppose
k gcd n = 1;
hence thesis by INT_2:def 3;
end;
suppose
k gcd n = n;
then n divides k by NAT_D:def 5;
hence thesis by A1,NAT_D:7;
end;
end;
theorem Th3:
n is prime & k in {kk where kk is Element of NAT: n,kk
are_coprime & kk >= 1 & kk <= n}
iff n is prime & k in Segm n & not k in {0}
proof
set X = {kk where kk is Element of NAT : n,kk are_coprime & kk >= 1 &
kk <= n};
thus n is prime & k in X implies n is prime & k in Segm n & not k in {0}
proof
assume that
A1: n is prime and
A2: k in X;
A3: ex kk being Element of NAT st kk = k & n,kk are_coprime & kk >=
1 & kk <= n by A2;
then k <> n by A1,Lm2,Th1;
then k < n by A3,XXREAL_0:1;
hence thesis by A1,A3,NAT_1:44,TARSKI:def 1;
end;
assume that
A4: n is prime and
A5: k in Segm n and
A6: not k in {0};
A7: k <> 0 by A6,TARSKI:def 1;
then
A8: k >= 1 by NAT_1:14;
A9: k < n by A5,NAT_1:44;
then k in NAT & k,n are_coprime by A4,A7,Th2,ORDINAL1:def 12;
hence thesis by A4,A9,A8;
end;
theorem Th4:
for A being finite set, x being set st x in A holds card(A \ {x})
= card A - card{x} by CARD_2:44,ZFMISC_1:31; :: dlaczego nie card A - 1
:: !!! ???
theorem Th5:
a gcd b = 1 implies for c holds a*c gcd b*c = c
proof
assume
A1: a gcd b = 1;
let m;
reconsider a9 = a, b9 = b as Integer;
a9,b9 are_coprime by A1,INT_2:def 3;
hence a*m gcd b*m = |.|.m.|.| by INT_2:24
.= m by ABSVALUE:def 1;
end;
theorem Th6:
a <> 0 & c <> 0 & a*c gcd b*c = c implies a,b are_coprime
proof
assume that
A1: a <> 0 and
A2: c <> 0 and
A3: a*c gcd b*c = c;
a*c <> 0*c by A1,A2,XCMPLX_1:5;
then consider a1,b1 being Integer such that
A4: a*c = (a*c gcd b*c)*a1 and
A5: b*c = (a*c gcd b*c)*b1 & a1,b1 are_coprime by INT_2:23;
a = a1 by A2,A3,A4,XCMPLX_1:5;
hence thesis by A2,A3,A5,XCMPLX_1:5;
end;
theorem Th7:
a gcd b = 1 implies (a + b) gcd b = 1
proof
assume
A1: a gcd b = 1;
set n = (a + b) gcd b;
A2: n divides b by NAT_D:def 5;
n divides (a + b) by NAT_D:def 5;
then n divides a by A2,NAT_D:10;
then n divides a gcd b by A2,NEWTON:50;
then
A3: n <= 1 + 0 by A1,NAT_D:7;
per cases by A3,NAT_1:9;
suppose
n = 1;
hence thesis;
end;
suppose
n = 0;
then b = 0 by INT_2:5;
hence thesis by A1;
end;
end;
theorem Th8:
for a, b, c be Nat holds (a + b*c) gcd b = a gcd b
proof
let a, b, c be Nat;
defpred P[Nat] means (a + b*$1) gcd b = a gcd b;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let kk be Nat;
assume
A2: (a + b*kk) gcd b = a gcd b;
now
per cases;
suppose
b = 0;
hence (a + b*(kk + 1)) gcd b = a gcd b;
end;
suppose
A3: b > 0;
set T = a gcd b;
A4: a gcd b > 0 by A3,NEWTON:58;
A5: a gcd b divides (a + b*kk) by A2,NAT_D:def 5;
then
A6: (a + b*kk) = (a gcd b)*((a + b*kk) div (a gcd b)) by NAT_D:3;
now
per cases;
suppose
A7: a + b*kk = 0;
then a gcd b = 0 gcd b by NAT_1:7
.= b by NEWTON:52;
hence (a + b*(kk + 1)) gcd b = a gcd b by A7,NAT_D:32;
end;
suppose
A8: (a + b*kk) > 0;
set T2 = (b div (a gcd b));
set T1 = ((a + b*kk) div (a gcd b));
A9: ((a + b*kk) div (a gcd b)) <> 0 by A6,A8;
a gcd b divides b by NAT_D:def 5;
then
A10: b = (a gcd b)*(b div (a gcd b)) by NAT_D:3;
then T1*T gcd T2*T = T by A2,A5,NAT_D:3;
then T1,T2 are_coprime by A4,A9,Th6;
then T1 gcd T2 = 1 by INT_2:def 3;
then
A11: (T1 + T2) gcd T2 = 1 by Th7;
(a + b*(kk + 1)) gcd b = ((a + b*kk) + b) gcd b
.= (T*T1 + T*T2) gcd T*T2 by A5,A10,NAT_D:3
.= (T*(T1 + T2)) gcd T*T2
.= a gcd b by A11,Th5;
hence (a + b*(kk + 1)) gcd b = a gcd b;
end;
end;
hence (a + b*(kk + 1)) gcd b = a gcd b;
end;
end;
hence thesis;
end;
A12: P[0];
for c be Nat holds P[c] from NAT_1:sch 2(A12,A1);
hence thesis;
end;
theorem Th9:
m,n are_coprime implies ex k st (ex i0,j0 being Integer
st k = i0*m + j0*n & k > 0) & for l st (ex i,j being Integer st l = i*m + j*n &
l > 0) holds k <= l
proof
defpred P[Nat] means ex i0,j0 being Integer st $1 = i0*m + j0*n & $1>0;
assume
A1: m,n are_coprime;
m > 0 or n > 0
proof
assume ( not m > 0)& not n > 0;
then m = 0 & n = 0;
then m gcd n <> 1 by NAT_D:32;
hence contradiction by A1,INT_2:def 3;
end;
then 1*m + 1*n > 0;
then
A2: ex k be Nat st P[k];
consider k be Nat such that
A3: P[k] and
A4: for l be Nat st P[l] holds k<=l from NAT_1:sch 5(A2);
take k;
thus ex i0,j0 being Integer st k = i0*m + j0*n & k > 0 by A3;
let l;
thus thesis by A4;
end;
theorem Th10:
m,n are_coprime implies for k holds ex i,j st i*m + j*n = k
proof
reconsider a9=1, 09=0 as Integer;
assume
A1: m,n are_coprime;
then consider a such that
A2: ex i0,j0 being Integer st a = i0*m + j0*n & a>0 and
A3: for c st (ex i,j st c = i*m + j*n & c>0) holds a <= c by Th9;
let k;
consider i0,j0 being Integer such that
A4: a = i0*m + j0*n and
A5: a > 0 by A2;
A6: for c st (ex i,j st c = i*m + j*n & c > 0) holds c mod a = 0
proof
let b;
assume ex i,j st b = i*m + j*n & b > 0;
then consider i,j such that
A7: b=i*m + j*n and
b>0;
set t2 = j - ((b div a)*j0);
set t1 = i - ((b div a)*i0);
A8: b mod a + a*(b div a) - a*(b div a) = b - a*(b div a) by A5,NAT_D:2;
then reconsider c = t1*m + t2*n as Element of NAT by A4,A7;
assume
A9: b mod a <> 0;
c < a by A4,A5,A7,A8,NAT_D:1;
hence contradiction by A3,A4,A9,A7,A8;
end;
A10: a divides n
proof
per cases;
suppose
n = 0;
hence thesis by NAT_D:6;
end;
suppose
n > 0;
then 09*m + a9*n > 0;
then n mod a = 0 by A6;
then n = a*(n div a) + 0 by A2,NAT_D:2;
hence thesis by NAT_D:3;
end;
end;
a divides m
proof
per cases;
suppose
m = 0;
hence thesis by NAT_D:6;
end;
suppose
m > 0;
then a9*m + 09*n > 0;
then m mod a = 0 by A6;
then m = a*(m div a) + 0 by A2,NAT_D:2;
hence thesis by NAT_D:3;
end;
end;
then a divides (m gcd n) by A10,NAT_D:def 5;
then a divides 1 by A1,INT_2:def 3;
then ex b be Nat st 1 = a*b by NAT_D:def 3;
then i0*m + j0*n = 1 by A4,NAT_1:15;
then k = k*(i0*m + j0*n) .= (k*i0)*m + k*(j0*n);
then k = (k*i0)*m + (k*j0)*n;
hence thesis;
end;
theorem Th11: ::: KNASTER:13
for A be set, B being non empty set,
f being Function of A, B st f is bijective holds card A = card B
proof
let A be set, B be non empty set,
f be Function of A, B;
assume f is bijective; then
A1: f is one-to-one onto;
A2: A = dom f by FUNCT_2:def 1;
B c= rng f by A1;
then A3: card B c= card A by A2,CARD_1:12;
card A c= card B by A2,A1,CARD_1:10;
hence thesis by A3;
end;
::$CT
theorem Th13:
c divides a*b & a,c are_coprime implies c divides b
proof
assume that
A1: c divides a*b and
A2: a,c are_coprime;
A3: c divides c*b by NAT_D:9;
a gcd c = 1 by A2,INT_2:def 3;
then (a*b gcd c*b) = b by Th5;
hence thesis by A1,A3,NEWTON:50;
end;
theorem Th14:
a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime implies a*b,c are_coprime
proof
assume that
A1: a <> 0 and
A2: c <> 0 and
A3: a,c are_coprime and
A4: b,c are_coprime;
A5: (a gcd c) = 1 by A3,INT_2:def 3;
A6: (a*b gcd c) divides c by NAT_D:def 5;
((a*b gcd c) gcd a) divides (a*b gcd c) by NAT_D:def 5;
then ((a*b gcd c) gcd a) divides a & ((a*b gcd c) gcd a) divides c by A6,
NAT_D:4,def 5;
then ((a*b gcd c) gcd a) divides 1 by A5,NEWTON:50;
then
A7: ((a*b gcd c) gcd a) <= 0 + 1 by NAT_D:7;
((a*b gcd c) gcd a) <> 0 by A1,NEWTON:58;
then ((a*b gcd c) gcd a) = 1 by A7,NAT_1:9;
then (a*b gcd c) divides a*b & a,(a*b gcd c) are_coprime by
INT_2:def 3,NAT_D:def 5;
then
A8: (a*b gcd c) divides b by Th13;
(b gcd c) = 1 by A4,INT_2:def 3;
then (a*b gcd c) divides 1 by A6,A8,NEWTON:50;
then
A9: a*b gcd c <= 0 + 1 by NAT_D:7;
(a*b) gcd c > 0 by A2,NEWTON:58;
then a*b gcd c = 1 by A9,NAT_1:9;
hence thesis by INT_2:def 3;
end;
theorem Th15:
x <> 0 & i >= 0 implies i*x gcd i*y = i*(x gcd y)
proof
assume that
A1: x <> 0 and
A2: i >= 0;
consider a2,b2 being Integer such that
A3: x = (x gcd y)*a2 & y = (x gcd y)*b2 and
A4: a2,b2 are_coprime by A1,INT_2:23;
i*x = (i*(x gcd y))*a2 & i*y = (i*(x gcd y))*b2 by A3;
then
A5: i*x gcd i*y = |.i*(x gcd y).| by A4,INT_2:24
.= |.i.|*|.(x gcd y).| by COMPLEX1:65;
i = |.i.| by A2,ABSVALUE:def 1;
hence thesis by A5,ABSVALUE:def 1;
end;
theorem Th16:
for x st a <> 0 holds (a + x*b) gcd b = a gcd b
proof
let xx be Integer;
set i = a gcd b;
A1: b = |.b.| by ABSVALUE:def 1;
assume
A2: a <> 0;
A3: for m be Nat st m divides |.a + xx*b.| & m divides |.b.| holds m
divides i
proof
let mm be Nat;
assume that
A4: mm divides |.(a + xx*b).| and
A5: mm divides |.b.|;
consider n being Nat such that
A6: b = mm*n by A1,A5,NAT_D:def 3;
reconsider mm as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
(a + xx*b) >= 0;
then |.(a + xx*b).| = (a + xx*b) by ABSVALUE:def 1;
then consider t being Integer such that
A7: (a + xx*b) = mm*t by A4,INT_1:def 3;
A8: a = mm*t - mm*(xx*n) by A6,A7,XCMPLX_1:26
.= mm*(t - (xx*n));
then (t - (xx*n)) >= 0 by A2;
then reconsider tt = (t - (xx*n)) as Element of NAT by INT_1:3;
a = mm*tt by A8;
hence mm divides a by NAT_D:def 3;
end;
suppose
(a + xx*b) < 0;
then |.(a + xx*b).| = -(a + xx*b) by ABSVALUE:def 1;
then consider t being Integer such that
A9: -(a + xx*b) = mm*t by A4,INT_1:def 3;
A10: a = -mm*t - mm*(xx*n) by A6,A9,XCMPLX_1:26
.= mm*(-t - (xx*n));
then (-t - (xx*n)) >= 0 by A2;
then reconsider tt = (-t - (xx*n)) as Element of NAT by INT_1:3;
a = mm*tt by A10;
hence mm divides a by NAT_D:def 3;
end;
end;
hence thesis by A1,A5,NEWTON:50;
end;
i divides a by NAT_D:def 5;
then
A11: a = i*(a div i) by NAT_D:3;
A12: i divides b by NAT_D:def 5;
then
A13: b = i*(b div i) by NAT_D:3;
i divides |.a + xx*b.|
proof
per cases;
suppose
a + xx*b < 0;
then
A14: |.(a + xx*b).| = -(a + xx*b) by ABSVALUE:def 1;
-(a + xx*b) = i * (-((a div i) + (xx*(b div i)))) by A11,A13;
hence thesis by A14,INT_1:def 3;
end;
suppose
(a + xx*b) >= 0;
then
A15: |.(a + xx*b).| = a + xx*b by ABSVALUE:def 1;
a + xx*b = i*((a div i) + (xx*(b div i))) by A11,A13;
hence thesis by A15,INT_1:def 3;
end;
end;
then |.(a + xx*b).| gcd |.b.| = i by A1,A12,A3,NAT_D:def 5;
hence thesis by INT_2:34;
end;
begin :: Euler's function
definition
let n be Nat;
func Euler n -> Element of NAT equals
card {k where k is Element of NAT: n,k are_coprime & k >= 1 & k <= n};
coherence
proof
set X = {k where k is Element of NAT : n,k are_coprime & k >= 1 & k
<= n};
X c= Seg n
proof
let x be object;
assume x in X;
then
ex k be Element of NAT st k = x & n,k are_coprime & k >= 1 &
k <= n;
hence thesis by FINSEQ_1:1;
end;
then reconsider X as finite set;
card X is Element of NAT;
hence thesis;
end;
end;
set X = {k where k is Element of NAT : 1,k are_coprime & k >= 1 & k <=
1};
for x being object holds x in X iff x = 1
proof
let x be object;
thus x in X implies x = 1
proof
assume x in X;
then
ex k be Element of NAT st k = x & 1,k are_coprime & k >= 1 & k <= 1;
hence thesis by XXREAL_0:1;
end;
1 gcd 1 = 1 by NAT_D:32;
then 1,1 are_coprime by INT_2:def 3;
hence thesis;
end;
then
Lm3: card {1} = Euler 1 by TARSKI:def 1;
theorem Th17:
Euler 1 = 1 by Lm3,CARD_1:30;
set X = {k where k is Element of NAT : 2,k are_coprime & k >= 1 & k <=
2};
for x being object holds x in X iff x = 1
proof
let x be object;
thus x in X implies x = 1
proof
assume x in X;
then consider k be Element of NAT such that
A1: k = x & 2,k are_coprime and
A2: k >= 1 & k <= 2;
A3: 2 gcd 2 = 2 by NAT_D:32;
k = 0 or ... or k = 2 by A2;
hence thesis by A1,A2,A3,INT_2:def 3;
end;
2 gcd 1 = 1 by NEWTON:51;
then 2,1 are_coprime by INT_2:def 3;
hence thesis;
end;
then
Lm4: card {1} = Euler 2 by TARSKI:def 1;
theorem
Euler 2 = 1 by Lm4,CARD_1:30;
theorem Th19:
n > 1 implies Euler n <= n - 1
proof
set X={kk where kk is Element of NAT : n,kk are_coprime & kk >= 1 &
kk <= n};
X c= Seg n
proof
let x be object;
assume x in X;
then ex k be Element of NAT st k = x & n,k are_coprime & k >= 1 & k
<= n;
hence thesis by FINSEQ_1:1;
end;
then reconsider X as finite set;
assume
A1: n > 1;
then 0 in {l where l is Nat: l < n};
then 0 in n by AXIOMS:4;
then
A2: card(n \ {0}) = card n - card {0} by Th4;
A3: X c= n \ {0}
proof
let x be object;
assume x in X;
then consider k be Element of NAT such that
A4: k = x and
A5: n,k are_coprime and
A6: k >= 1 and
A7: k <= n;
not n,n are_coprime by A1,Th1;
then k < n by A5,A7,XXREAL_0:1;
then k in {l where l is Nat: l < n};
then
A8: k in n by AXIOMS:4;
not k in {0} by A6,TARSKI:def 1;
hence thesis by A4,A8,XBOOLE_0:def 5;
end;
card n = n & card {0} = 1 by CARD_1:30;
hence thesis by A3,A2,NAT_1:43;
end;
theorem
n is prime implies Euler n = n - 1
proof
set X={kk where kk is Element of NAT : n,kk are_coprime & kk >= 1 &
kk <= n};
X c= Seg n
proof
let x be object;
assume x in X;
then ex k be Element of NAT st k = x & n,k are_coprime & k >= 1 & k
<= n;
hence thesis by FINSEQ_1:1;
end;
then reconsider X as finite set;
assume
A1: n is prime;
n <> 0
proof
assume n = 0;
then n in SetPrimenumber 2 by A1,NEWTON:def 7;
hence contradiction;
end;
then 0 in {l where l is Nat: l < n};
then
A2: 0 in n by AXIOMS:4;
Segm n \ {0} c= X
proof
let x be object;
assume
A3: x in Segm n \ {0};
then
A4:x in Segm n by XBOOLE_0:def 5;
not x in {0} by A3,XBOOLE_0:def 5;
hence thesis by A1,Th3,A4;
end;
then
A5: card (n \ {0}) <= card X by NAT_1:43;
A6: Euler n <= n - 1 by A1,Th19,INT_2:def 4;
card n = n & card {0} = 1 by CARD_1:30;
then n - 1 <= Euler n by A5,A2,Th4;
hence thesis by A6,XXREAL_0:1;
end;
LM:
Euler 0 = 0
proof
set A = {k where k is Element of NAT: 0,k are_coprime & k >= 1 & k <= 0};
assume Euler 0 <> 0;
then card A <> 0;
then consider a being object such that
A1: a in A by XBOOLE_0:7,CARD_1:27;
ex k being Element of NAT st k = a & 0,k are_coprime & k >= 1 & k <= 0
by A1;
hence contradiction;
end;
theorem
m,n are_coprime implies Euler (m*n) = Euler m * Euler n
proof
assume
A3: m,n are_coprime;
per cases;
suppose m <= 1;
then m = 0 or m = 1 by NAT_1:25;
hence thesis by LM,Th17;
end;
suppose n <= 1;
then n = 0 or n = 1 by NAT_1:25;
hence thesis by LM,Th17;
end;
suppose that
A1: m > 1 and
A2: n > 1;
set X={i where i is Element of NAT: m*n,i are_coprime & i >= 1 & i <=
m*n};
set C={i where i is Element of NAT:ex x,y being Integer st i = (m*y + n*x)
mod m*n & m*n,i are_coprime & y <= n & x <= m & i >= 0};
A4: m*n <> 0 by A1,A2,XCMPLX_1:6;
A5: C c= Seg (m*n) \/ {0}
proof
let z be object;
assume z in C;
then consider i being Element of NAT such that
A6: i = z and
A7: ex x,y being Integer st i = (m*y + n*x) mod m*n & m*n,i
are_coprime & y <= n & x <= m & i >= 0;
consider x,y being Integer such that
A8: i = (m*y + n*x) mod m*n and
m*n,i are_coprime and
y <= n and
x <= m and
i >= 0 by A7;
per cases;
suppose
A9: i > 0;
A10: (m*y + n*x) mod m*n <= m*n
proof
set i2 = m*n;
set i1 = (m*y + n*x);
A11: ([\ i1/i2 /]) + 1 >= i1/i2 by INT_1:29;
(m*y + n*x) mod m*n = i1 - (i1 div i2)*i2 by A4,INT_1:def 10
.= i1 - ([\ i1/i2 /])*i2 by INT_1:def 9;
hence thesis by A1,A2,A11,Lm1,XCMPLX_1:6;
end;
i >= 1 by A9,NAT_1:14;
then z in Seg (m*n) by A6,A8,A10,FINSEQ_1:1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A12: i = 0;
0 in {0} by TARSKI:def 1;
hence thesis by A6,A12,XBOOLE_0:def 3;
end;
end;
then reconsider C as finite set;
set A={i where i is Element of NAT:n,i are_coprime & i >= 1 & i <= n};
A13: A c= Seg n
proof
let x be object;
assume x in A;
then
ex i being Element of NAT st i = x & n,i are_coprime & i >= 1 &
i <= n;
hence thesis by FINSEQ_1:1;
end;
A14: y = 1 & x = 1 implies (m*y + n*x) mod m*n in C
proof
A15: m gcd n = 1 by A3,INT_2:def 3;
then (m + n) gcd m = 1 by Th7;
then
A16: m,(m + n) are_coprime by INT_2:def 3;
(m + n) gcd n = 1 by A15,Th7;
then n,(m + n) are_coprime by INT_2:def 3;
then m*n,(m + n) are_coprime by A1,A16,Th14;
then
A17: m*n gcd (m + n) = 1 by INT_2:def 3;
assume
A18: y = 1 & x = 1;
then reconsider y9= y,x9= x as Element of NAT;
(m*y9 + n*x9) mod m*n = (m*y + n*x) mod m*n;
then consider t being Element of NAT such that
A19: t = (m*y + n*x) mod m*n;
ex d being Nat st (m + n) = (m*n)*d + ((m + n) mod m*n) & ((m + n) mod
m*n) < (m*n) by A4,NAT_D:def 2;
then (m + n) mod m*n gcd m*n = 1 by A17,Th8;
then m*n,t are_coprime by A18,A19,INT_2:def 3;
hence thesis by A1,A2,A18,A19;
end;
reconsider A as finite set by A13;
A20: a = 1 implies a in A
proof
assume
A21: a = 1;
then n gcd a = 1 by NEWTON:51;
then n,a are_coprime by INT_2:def 3;
hence thesis by A2,A21;
end;
set B={i where i is Element of NAT:m,i are_coprime & i >= 1 & i <= m};
A22: B c= Seg m
proof
let x be object;
assume x in B;
then
ex i being Element of NAT st i = x & m,i are_coprime & i >= 1 &
i <= m;
hence thesis by FINSEQ_1:1;
end;
A23: m*n <> 1 by A1,NAT_1:15;
A24: C = X
proof
thus C c= X
proof
let z be object;
assume z in C;
then consider i being Element of NAT such that
A25: i = z and
A26: ex x,y being Integer st i = (m*y + n*x) mod m*n & m*n,i
are_coprime & y <= n & x <= m & i >= 0;
consider x,y being Integer such that
A27: i = (m*y + n*x) mod m*n and
A28: m*n,i are_coprime and
y <= n and
x <= m and
i >= 0 by A26;
A29: (m*y + n*x) mod m*n <= m*n
proof
set i2 = m*n;
set i1 = (m*y + n*x);
A30: ([\ i1/i2 /]) + 1 >= i1/i2 by INT_1:29;
(m*y + n*x) mod m*n = i1 - (i1 div i2)*i2 by A4,INT_1:def 10
.= i1 - ([\ i1/i2 /])*i2 by INT_1:def 9;
hence thesis by A1,A2,A30,Lm1,XCMPLX_1:6;
end;
per cases;
suppose
i > 0;
then i >= 1 by NAT_1:14;
hence thesis by A25,A27,A28,A29;
end;
suppose
i = 0;
then m*n gcd 0 = 1 by A28,INT_2:def 3;
hence thesis by A23,NEWTON:52;
end;
end;
let z be object;
assume z in X;
then consider i being Element of NAT such that
A31: i=z and
A32: m*n,i are_coprime and
i >= 1 and
A33: i <= m*n;
i <> m*n
proof
assume i = m*n;
then (m*n) gcd (m*n) = 1 by A32,INT_2:def 3;
then m*n = 1 by NAT_D:32;
hence contradiction by A1,NAT_1:15;
end;
then
A34: i < m*n by A33,XXREAL_0:1;
consider y0,x0 being Integer such that
A35: y0*m + x0*n = i by A3,Th10;
A36: (m*y0 + n*x0) mod (m*n) = (m*y0 + n*x0) - ((m*y0 + n*x0) div (m*n))*(
m*n) by A4,INT_1:def 10
.= (m*y0 + n*x0) - 0*(m*n) by A34,A35,PRE_FF:4
.= m*y0 + n*x0;
set k = y0 div n;
set j = x0 div m;
consider x1,y1 being Integer such that
A37: x1 = x0 mod m and
A38: y1 = y0 mod n;
x0 mod m = x0 - (x0 div m)*m & y0 mod n = y0- (y0 div n)*n by A1,A2,
INT_1:def 10;
then m*y0 + n*x0 = m*y1 + n*x1 + (m*n)*(k+j) by A37,A38;
then
A39: m*y0 + n*x0 = (m*y1 + n*x1) mod (m*n) by A36,NAT_D:61;
A40: ([\ y0/n /]) + 1 >= y0/n by INT_1:29;
A41: ([\ x0/m /]) + 1 >= x0/m by INT_1:29;
y1 = y0 - (y0 div n)*n by A2,A38,INT_1:def 10
.= y0 - ([\ y0/n /])*n by INT_1:def 9;
then
A42: y1 <= n by A2,A40,Lm1;
x1 = x0 - (x0 div m)*m by A1,A37,INT_1:def 10
.= x0 - ([\ x0/m /])*m by INT_1:def 9;
then x1 <= m by A1,A41,Lm1;
hence thesis by A31,A32,A35,A42,A39;
end;
reconsider B as finite set by A22;
A43: b = 1 implies b in B
proof
assume
A44: b = 1;
then m gcd b = 1 by NEWTON:51;
then m,b are_coprime by INT_2:def 3;
hence thesis by A1,A44;
end;
{0} c= NAT by ZFMISC_1:31;
then Seg (m*n) \/ {0} c= NAT by XBOOLE_1:8;
then reconsider
A,B,C as non empty finite Subset of NAT by A13,A22,A5,A20,A43,A14,XBOOLE_1:1;
deffunc F(Element of A,Element of B) = (m*$1+n*$2) mod (m*n);
A45: for y being Element of A, x being Element of B holds F(y,x) in C
proof
set l = n*m;
let y be Element of A, x be Element of B;
y in A;
then consider i being Element of NAT such that
A46: i = y and
A47: n,i are_coprime and
A48: i >= 1 and
A49: i <= n;
x in B;
then consider j being Element of NAT such that
A50: j = x and
A51: m,j are_coprime and
j >= 1 and
A52: j <= m;
i*m,n are_coprime by A1,A2,A3,A47,Th14;
then i*m gcd n = 1 by INT_2:def 3;
then (m*i + n*j) gcd n = 1 by Th8;
then
A53: n,(m*i + n*j) are_coprime by INT_2:def 3;
j*n,m are_coprime by A1,A2,A3,A51,Th14;
then j*n gcd m = 1 by INT_2:def 3;
then (m*i + n*j) gcd m = 1 by Th8;
then
A54: m,(m*i + n*j) are_coprime by INT_2:def 3;
i*m <> 0*m by A1,A48,XCMPLX_1:5;
then n*m,(m*i + n*j) are_coprime by A1,A53,A54,Th14;
then
A55: n*m gcd (m*i + n*j) = 1 by INT_2:def 3;
reconsider ii = i,jj = j as Integer;
m*ii + n*jj mod m*n = m*i + n*j mod m*n;
then consider q being Element of NAT such that
A56: q = (m*ii + n*jj) mod m*n;
ex t being Nat st (m*i + n*j) = (n*m)*t + ((m*i + n*j) mod n*m) & ((m
*i + n*j) mod n*m) < (n*m) by A4,NAT_D:def 2;
then ((m*i + n*j) mod l) gcd l = 1 by A55,Th8;
then l,q are_coprime by A56,INT_2:def 3;
hence thesis by A46,A49,A50,A52,A56;
end;
consider f being Function of [:A,B:], C such that
A57: for y being Element of A, x being Element of B holds f.(y,x) = F(y
,x) from FUNCT_7:sch 1(A45);
A58: f is onto
proof
thus rng f c= C by RELAT_1:def 19;
let z be object;
assume z in C;
then consider i being Element of NAT such that
A59: i = z and
A60: ex x0,y0 being Integer st i = (m*y0 + n*x0) mod m*n & m*n,i
are_coprime & y0 <= n & x0 <= m & i >= 0;
consider x0,y0 being Integer such that
A61: i = (m*y0 + n*x0) mod m*n and
A62: m*n,i are_coprime and
y0 <= n and
x0 <= m and
i >= 0 by A60;
consider x,y being Integer such that
A63: x = x0 mod m and
A64: y = y0 mod n;
A65: x <= m by A1,A63,NEWTON:65;
A66: (m*y + n*x) mod (m*n) = (m*y0 + n*x0) mod (m*n)
proof
set k = y0 div n;
set j = x0 div m;
x0 mod m = x0 - (x0 div m)*m & y0 mod n = y0- (y0 div n)*n by A1,A2,
INT_1:def 10;
then m*y0 + n*x0 = m*y + n*x + (m*n)*(k+j) by A63,A64;
hence thesis by NAT_D:61;
end;
A67: y <= n by A2,A64,NEWTON:65;
reconsider x,y as Element of NAT by A63,A64,INT_1:3;
A68: x <> 0
proof
set j = x0 div m;
set jj = (y0 + (n*j)) - (n*((m*(y0 + (n*j))) div m*n));
assume x = 0;
then x0 - (x0 div m)*m = 0 by A1,A63,INT_1:def 10;
then
A69: (m*y0 + n*x0) mod m*n = m*(y0 + (n*j)) - ((m*(y0 + (n*j))) div m*n
)*(m*n) by A4,INT_1:def 10
.= m*((y0 + (n*j)) - (n*((m*(y0 + (n*j))) div m*n)));
then reconsider g = m*jj as Element of NAT by A61;
A70: m*n gcd m*jj = 1 by A61,A62,A69,INT_2:def 3;
A71: g > 0 or g = 0;
not jj < 0
proof
assume jj < 0;
then m*jj < 0*jj by A1,XREAL_1:69;
hence contradiction by A71;
end;
then reconsider jj as Element of NAT by INT_1:3;
m*(n gcd jj) = 1 by A2,A70,Th15;
then jj = 0 by A1,NAT_1:15;
then m*n gcd 0 = 1 by A61,A62,A69,INT_2:def 3;
hence contradiction by A23,NEWTON:52;
end;
A72: y <> 0
proof
set j = y0 div n;
set jj = ((m*j) + x0) - (m*((n*((m*j) + x0)) div m*n));
assume y = 0;
then y0 - (y0 div n)*n = 0 by A2,A64,INT_1:def 10;
then
A73: (m*y0 + n*x0) mod m*n = n*((m*j) + x0) - ((n*((m*j) + x0)) div m*n
)*(m*n) by A4,INT_1:def 10
.= n*(((m*j) + x0) - (m*((n*((m*j) + x0)) div m*n)));
then reconsider g = n*jj as Element of NAT by A61;
A74: m*n gcd n*jj = 1 by A61,A62,A73,INT_2:def 3;
A75: g > 0 or g = 0;
not jj < 0
proof
assume jj < 0;
then n*jj < 0*jj by A2,XREAL_1:69;
hence contradiction by A75;
end;
then reconsider jj as Element of NAT by INT_1:3;
n*(m gcd jj) = 1 by A1,A74,Th15;
then jj = 0 by A2,NAT_1:15;
then m*n gcd 0 = 1 by A61,A62,A73,INT_2:def 3;
hence contradiction by A23,NEWTON:52;
end;
A76: m,x0 are_coprime
proof
set p = m gcd x0;
p divides m by INT_2:21;
then consider i1 being Integer such that
A77: m = p*i1 by INT_1:def 3;
p divides x0 by INT_2:21;
then consider i2 being Integer such that
A78: x0 = p*i2 by INT_1:def 3;
set jj = i1*n;
set k = ((p*i1)*y0 + n*(p*i2))div((p*i1)*n);
set j = (i1*y0 + n*i2) - ((i1*k)*n);
A79: p <> 0 by A1,A77;
A80: (m*y0 + n*x0) mod m*n = ((p*i1)*y0 + n*(p*i2)) - (((p*i1)*y0 + n*(
p*i2)) div((p*i1)*n))*((p*i1)*n) by A4,A77,A78,INT_1:def 10;
A81: ((p*i1)*y0 + n*(p*i2)) - k*((p*i1)*n) = p*((i1*y0 + n*i2) - ((i1*k )*n));
not j < 0
proof
assume j < 0;
then p*j < 0*j by A79,XREAL_1:69;
hence contradiction by A4,A61,A77,A78,A81,INT_1:def 10;
end;
then reconsider p,j as Element of NAT by INT_1:3;
not jj < 0
proof
assume jj < 0;
then p*jj < 0*jj by A79,XREAL_1:69;
hence contradiction by A4,A77;
end;
then reconsider jj as Element of NAT by INT_1:3;
A82: m*n = p*(i1*n) by A77;
now
per cases by A1,A2,A82,XCMPLX_1:6;
suppose
A83: p <> 0 & jj <> 0 & j <> 0;
p*jj gcd p*j = 1 by A61,A62,A77,A80,INT_2:def 3;
then p*(jj gcd j) = 1 by A83,Th15;
hence p = 1 by NAT_1:15;
end;
suppose
p <> 0 & jj <> 0 & j = 0;
then p*jj gcd 0 = 1 by A61,A62,A77,A80,A81,INT_2:def 3;
then p*jj = 1 by NEWTON:52;
hence p = 1 by NAT_1:15;
end;
end;
hence thesis by INT_2:def 3;
end;
n,y0 are_coprime
proof
set p = n gcd y0;
p divides n by INT_2:21;
then consider i1 being Integer such that
A84: n = p*i1 by INT_1:def 3;
p divides y0 by INT_2:21;
then consider i2 being Integer such that
A85: y0 = p*i2 by INT_1:def 3;
set jj = i1*m;
set k = (m*(p*i2) + (p*i1)*x0) div (m*(p*i1));
set j = (m*i2 + i1*x0) - ((i1*k)*m);
A86: p <> 0 by A2,A84;
A87: (m*y0 + n*x0) mod m*n = (m*(p*i2) + (p*i1)*x0) - ((m*(p*i2) + (p*
i1)*x0) div (m*(p*i1)))*(m*(p*i1)) by A4,A84,A85,INT_1:def 10;
A88: (m*(p*i2) + (p*i1)*x0) - k*(m*(p*i1)) = p*((m*i2 + i1*x0) - ((i1*k )*m));
j >= 0
proof
assume j < 0;
then p*j < 0*j by A86,XREAL_1:69;
hence contradiction by A4,A61,A84,A85,A88,INT_1:def 10;
end;
then reconsider p,j as Element of NAT by INT_1:3;
not jj < 0
proof
assume jj < 0;
then p*jj < 0*jj by A86,XREAL_1:69;
hence contradiction by A4,A84;
end;
then reconsider jj as Element of NAT by INT_1:3;
A89: m*n = p*(i1*m) by A84;
now
per cases by A1,A2,A89,XCMPLX_1:6;
suppose
A90: p <> 0 & jj <> 0 & j <> 0;
p*jj gcd p*j = 1 by A61,A62,A84,A87,INT_2:def 3;
then p*(jj gcd j) = 1 by A90,Th15;
hence p = 1 by NAT_1:15;
end;
suppose
p <> 0 & jj <> 0 & j = 0;
then p*jj gcd 0 = 1 by A61,A62,A84,A87,A88,INT_2:def 3;
then p*jj = 1 by NEWTON:52;
hence p = 1 by NAT_1:15;
end;
end;
hence thesis by INT_2:def 3;
end;
then
A91: y0 gcd n = 1 by INT_2:def 3;
x = x0 - (x0 div m)*m by A1,A63,INT_1:def 10;
then x0 gcd m = x + (x0 div m)*m gcd m;
then x0 gcd m = x gcd m by A68,Th16;
then m gcd x = 1 by A76,INT_2:def 3;
then
A92: m,x are_coprime by INT_2:def 3;
x >= 0 + 1 by A68,INT_1:7;
then
A93: x in B by A65,A92;
y = y0 - (y0 div n)*n by A2,A64,INT_1:def 10;
then y0 gcd n = y + (y0 div n)*n gcd n;
then y0 gcd n = y gcd n by A72,Th16;
then
A94: n,y are_coprime by A91,INT_2:def 3;
y >= 0 + 1 by A72,INT_1:7;
then y in A by A67,A94;
then reconsider y as Element of A;
reconsider x as Element of B by A93;
A95: i = f.(y,x) by A57,A61,A66;
consider w being set such that
A96: w = [y,x];
dom f = [:A,B:] by FUNCT_2:def 1;
then w in dom f by A96,ZFMISC_1:87;
hence z in rng f by A59,A96,A95,FUNCT_1:def 3;
end;
A97: m*n >= 1 by A1,A2,NAT_1:14,XCMPLX_1:6;
f is one-to-one
proof
let x,y be object;
A98: dom f = [:A,B:] by FUNCT_2:def 1;
assume x in dom f;
then consider xx1 being Element of A, xx2 being Element of B such that
A99: x = [xx1,xx2] by A98,DOMAIN_1:1;
assume y in dom f;
then consider yy1 being Element of A, yy2 being Element of B such that
A100: y = [yy1,yy2] by A98,DOMAIN_1:1;
xx1 in A;
then consider x1 being Element of NAT such that
A101: xx1 = x1 and
n,x1 are_coprime and
A102: x1 >= 1 and
A103: x1 <= n;
xx2 in B;
then consider x2 being Element of NAT such that
A104: xx2 = x2 and
m,x2 are_coprime and
A105: x2 >= 1 and
A106: x2 <= m;
consider p being Integer such that
A107: p = m;
assume
A108: f.x = f.y;
yy2 in B;
then consider y2 being Element of NAT such that
A109: yy2 = y2 and
m,y2 are_coprime and
A110: y2 >= 1 and
A111: y2 <= m;
yy1 in A;
then consider y1 being Element of NAT such that
A112: yy1 = y1 and
n,y1 are_coprime and
A113: y1 >= 1 and
A114: y1 <= n;
A115: (x1*m+x2*n) mod (m*n) = f.(xx1,xx2) by A57,A101,A104
.= f.(yy1,yy2) by A99,A100,A108
.= (y1*m+y2*n) mod (m*n) by A57,A112,A109;
reconsider y1,y2,x1,x2 as Element of NAT;
set k = (x1*m+x2*n) mod (m*n);
A116: (x1*m + x2*n)-(y1*m + y2*n) = m*(x1 - y1) + n*(x2 - y2) & k + ((x1*m
+ x2*n) div (m*n))*(m*n) - (k + ((y1*m + y2*n) div (m*n))*(m*n)) = (m*n)*(((x1*
m + x2*n ) div (m*n)) - ((y1*m + y2*n) div (m*n)));
set w = (((x1*m + x2*n) div (m*n)) - ((y1*m + y2*n) div (m*n)));
y1*m + y2*n = k + ((y1*m + y2*n) div (m*n))*(m*n) by A97,A115,NAT_D:2;
then
A117: m*(x1 - y1) + n*(x2 - y2) = (m*n)*w by A97,A116,NAT_D:2;
then n*(x2 - y2) = m*((n*w) - (x1 - y1));
then
A118: p divides n*(x2 - y2) by A107,INT_1:def 3;
consider p being Integer such that
A119: p = n;
m*(x1 - y1) = n*((m*w) - (x2 - y2)) by A117;
then
A120: p divides m*(x1 - y1) by A119,INT_1:def 3;
then
A121: n divides (x1 - y1) by A3,A119,INT_2:25;
A122: x1 - y1 = 0
proof
per cases;
suppose
A123: 0<=(x1 - y1);
consider k being Integer such that
A124: k = x1 - y1;
reconsider k as Element of NAT by A123,A124,INT_1:3;
k = 0
proof
set b = n + -1;
-y1 <= -1 by A113,XREAL_1:24;
then
A125: x1 + -y1 <= n + -1 by A103,XREAL_1:7;
A126: k < b + 1 by A124,A125,NAT_1:13;
assume k <> 0;
hence contradiction by A3,A119,A120,A124,A126,INT_2:25,NAT_D:7;
end;
hence thesis by A124;
end;
suppose
A127: (x1 - y1)<=0;
consider k being Integer such that
A128: k = -(x1 - y1);
A129: n divides k by A121,A128,INT_2:10;
reconsider k as Element of NAT by A127,A128,INT_1:3;
k = 0
proof
set b = n + -1;
-x1 <= -1 by A102,XREAL_1:24;
then
A130: - x1 + y1 <= n + -1 by A114,XREAL_1:7;
A131: k < b + 1 by A128,A130,NAT_1:13;
assume k <> 0;
hence contradiction by A129,A131,NAT_D:7;
end;
hence thesis by A128;
end;
end;
A132: m divides (x2 - y2) by A3,A107,A118,INT_2:25;
x2 - y2 = 0
proof
per cases;
suppose
A133: 0<=(x2 - y2);
consider k being Integer such that
A134: k = x2 - y2;
reconsider k as Element of NAT by A133,A134,INT_1:3;
k = 0
proof
set b = m + -1;
-y2 <= -1 by A110,XREAL_1:24;
then
A135: x2 + -y2 <= m + -1 by A106,XREAL_1:7;
A136: k < b + 1 by A134,A135,NAT_1:13;
assume k <> 0;
hence contradiction by A3,A107,A118,A134,A136,INT_2:25,NAT_D:7;
end;
hence thesis by A134;
end;
suppose
A137: (x2 - y2)<=0;
consider k being Integer such that
A138: k = -(x2 - y2);
A139: m divides k by A132,A138,INT_2:10;
reconsider k as Element of NAT by A137,A138,INT_1:3;
k = 0
proof
set b = m + -1;
-x2 <= -1 by A105,XREAL_1:24;
then
A140: - x2 + y2 <= m + -1 by A111,XREAL_1:7;
A141: k < b + 1 by A138,A140,NAT_1:13;
assume k <> 0;
hence contradiction by A139,A141,NAT_D:7;
end;
hence thesis by A138;
end;
end;
hence thesis by A99,A101,A104,A100,A112,A109,A122;
end; then
f is bijective by A58;
then card[:A,B:] = card C by Th11;
hence thesis by A24,CARD_2:46;
end;
end;