let m, n be Nat; :: thesis: ( m > 1 & n > 1 & m,n are_relative_prime implies Euler (m * n) = (Euler m) * (Euler n) )
assume A1:
( m > 1 & n > 1 & m,n are_relative_prime )
; :: thesis: Euler (m * n) = (Euler m) * (Euler n)
then A2:
m * n <> 1
by NAT_1:15;
A3:
m * n <> 0
by A1, XCMPLX_1:6;
A4:
m * n >= 1
by A1, NAT_1:14, XCMPLX_1:6;
set A = { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } ;
set B = { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } ;
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_relative_prime & y <= n & x <= m & i >= 0 ) } ;
set X = { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } ;
A5:
{ i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } c= Seg n
then reconsider A = { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } as finite set ;
A8:
{ i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } c= Seg m
then reconsider B = { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } as finite set ;
A11:
{ 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_relative_prime & y <= n & x <= m & i >= 0 ) } c= (Seg (m * n)) \/ {0 }
then reconsider 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_relative_prime & y <= n & x <= m & i >= 0 ) } as finite set ;
A18:
C = { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) }
proof
thus
C c= { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) }
:: according to XBOOLE_0:def 10 :: thesis: { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } c= C
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } or z in C )
assume
z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) }
;
:: thesis: z in C
then consider i being
Element of
NAT such that A25:
i = z
and A26:
m * n,
i are_relative_prime
and A27:
(
i >= 1 &
i <= m * n )
;
i <> m * n
then A28:
i < m * n
by A27, XXREAL_0:1;
consider y0,
x0 being
Integer such that A29:
(y0 * m) + (x0 * n) = i
by A1, Th11;
consider x1,
y1 being
Integer such that A30:
x1 = x0 mod m
and A31:
y1 = y0 mod n
;
A32:
x0 mod m = x0 - ((x0 div m) * m)
by A1, INT_1:def 8;
set j =
x0 div m;
A33:
x1 =
x0 - ((x0 div m) * m)
by A1, A30, INT_1:def 8
.=
x0 - ([\(x0 / m)/] * m)
by INT_1:def 7
;
[\(x0 / m)/] + 1
>= x0 / m
by INT_1:52;
then A34:
x1 <= m
by A1, A33, Lm1;
A35:
y0 mod n = y0 - ((y0 div n) * n)
by A1, INT_1:def 8;
set k =
y0 div n;
A36:
y1 =
y0 - ((y0 div n) * n)
by A1, A31, INT_1:def 8
.=
y0 - ([\(y0 / n)/] * n)
by INT_1:def 7
;
[\(y0 / n)/] + 1
>= y0 / n
by INT_1:52;
then A37:
y1 <= n
by A1, A36, Lm1;
A38:
(m * y0) + (n * x0) = ((m * y1) + (n * x1)) + ((m * n) * ((y0 div n) + (x0 div m)))
by A30, A31, A32, A35;
((m * y0) + (n * x0)) mod (m * n) =
((m * y0) + (n * x0)) - ((((m * y0) + (n * x0)) div (m * n)) * (m * n))
by A3, INT_1:def 8
.=
((m * y0) + (n * x0)) - (0 * (m * n))
by A28, A29, PRE_FF:4
.=
(m * y0) + (n * x0)
;
then
(m * y0) + (n * x0) = ((m * y1) + (n * x1)) mod (m * n)
by A38, Th13;
hence
z in C
by A25, A26, A29, A34, A37;
:: thesis: verum
end;
A39:
for a being Nat st a = 1 holds
a in A
A41:
for b being Nat st b = 1 holds
b in B
A43:
for y, x being Integer st y = 1 & x = 1 holds
((m * y) + (n * x)) mod (m * n) in C
proof
let y,
x be
Integer;
:: thesis: ( y = 1 & x = 1 implies ((m * y) + (n * x)) mod (m * n) in C )
assume A44:
(
y = 1 &
x = 1 )
;
:: thesis: ((m * y) + (n * x)) mod (m * n) in C
then reconsider y' =
y,
x' =
x as
Element of
NAT ;
((m * y') + (n * x')) mod (m * n) = ((m * y) + (n * x)) mod (m * n)
;
then consider t being
Element of
NAT such that A45:
t = ((m * y) + (n * x)) mod (m * n)
;
A46:
m gcd n = 1
by A1, INT_2:def 4;
then
(m + n) gcd n = 1
by Th8;
then A47:
n,
m + n are_relative_prime
by INT_2:def 4;
(m + n) gcd m = 1
by A46, Th8;
then A48:
m,
m + n are_relative_prime
by INT_2:def 4;
m * n,
m + n are_relative_prime
by A1, A47, A48, Th15;
then A49:
(m * n) gcd (m + n) = 1
by INT_2:def 4;
consider d being
Nat such that A50:
m + n = ((m * n) * d) + ((m + n) mod (m * n))
and
(m + n) mod (m * n) < m * n
by A3, NAT_D:def 2;
((m + n) mod (m * n)) gcd (m * n) = 1
by A49, A50, Th9;
then
m * n,
t are_relative_prime
by A44, A45, INT_2:def 4;
hence
((m * y) + (n * x)) mod (m * n) in C
by A1, A44, A45;
:: thesis: verum
end;
{0 } c= NAT
by ZFMISC_1:37;
then
(Seg (m * n)) \/ {0 } c= NAT
by XBOOLE_1:8;
then reconsider A = A, B = B, C = C as non empty finite Subset of NAT by A5, A8, A11, A39, A41, A43, XBOOLE_1:1;
deffunc H1( Element of A, Element of B) -> Element of NAT = ((m * $1) + (n * $2)) mod (m * n);
A51:
for y being Element of A
for x being Element of B holds H1(y,x) in C
proof
let y be
Element of
A;
:: thesis: for x being Element of B holds H1(y,x) in Clet x be
Element of
B;
:: thesis: H1(y,x) in C
y in A
;
then consider i being
Element of
NAT such that A52:
i = y
and A53:
n,
i are_relative_prime
and A54:
i >= 1
and A55:
i <= n
;
x in B
;
then consider j being
Element of
NAT such that A56:
j = x
and A57:
m,
j are_relative_prime
and A58:
j >= 1
and A59:
j <= m
;
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 A60:
q = ((m * ii) + (n * jj)) mod (m * n)
;
i * m,
n are_relative_prime
by A1, A53, A54, Th15;
then A61:
(i * m) gcd n = 1
by INT_2:def 4;
j * n,
m are_relative_prime
by A1, A57, A58, Th15;
then A62:
(j * n) gcd m = 1
by INT_2:def 4;
((m * i) + (n * j)) gcd n = 1
by A61, Th9;
then A63:
n,
(m * i) + (n * j) are_relative_prime
by INT_2:def 4;
((m * i) + (n * j)) gcd m = 1
by A62, Th9;
then A64:
m,
(m * i) + (n * j) are_relative_prime
by INT_2:def 4;
(
i * m <> 0 * m &
j * n <> 0 * n )
by A1, A54, A58, XCMPLX_1:5;
then
(m * i) + (n * j) <> 0
;
then
n * m,
(m * i) + (n * j) are_relative_prime
by A1, A63, A64, Th15;
then A65:
(n * m) gcd ((m * i) + (n * j)) = 1
by INT_2:def 4;
consider t being
Nat such that A66:
(m * i) + (n * j) = ((n * m) * t) + (((m * i) + (n * j)) mod (n * m))
and
((m * i) + (n * j)) mod (n * m) < n * m
by A3, NAT_D:def 2;
set l =
n * m;
(((m * i) + (n * j)) mod (n * m)) gcd (n * m) = 1
by A65, A66, Th9;
then
n * m,
q are_relative_prime
by A60, INT_2:def 4;
hence
H1(
y,
x)
in C
by A52, A55, A56, A59, A60;
:: thesis: verum
end;
consider f being Function of [:A,B:],C such that
A67:
for y being Element of A
for x being Element of B holds f . y,x = H1(y,x)
from FUNCT_7:sch 1(A51);
A68:
f is one-to-one
proof
let x,
y be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
A69:
dom f = [:A,B:]
by FUNCT_2:def 1;
assume
x in dom f
;
:: thesis: ( not y in dom f or not f . x = f . y or x = y )
then consider xx1 being
Element of
A,
xx2 being
Element of
B such that A70:
x = [xx1,xx2]
by A69, DOMAIN_1:9;
xx1 in A
;
then consider x1 being
Element of
NAT such that A71:
xx1 = x1
and
n,
x1 are_relative_prime
and A72:
x1 >= 1
and A73:
x1 <= n
;
xx2 in B
;
then consider x2 being
Element of
NAT such that A74:
xx2 = x2
and
m,
x2 are_relative_prime
and A75:
x2 >= 1
and A76:
x2 <= m
;
assume
y in dom f
;
:: thesis: ( not f . x = f . y or x = y )
then consider yy1 being
Element of
A,
yy2 being
Element of
B such that A77:
y = [yy1,yy2]
by A69, DOMAIN_1:9;
yy1 in A
;
then consider y1 being
Element of
NAT such that A78:
yy1 = y1
and
n,
y1 are_relative_prime
and A79:
y1 >= 1
and A80:
y1 <= n
;
yy2 in B
;
then consider y2 being
Element of
NAT such that A81:
yy2 = y2
and
m,
y2 are_relative_prime
and A82:
y2 >= 1
and A83:
y2 <= m
;
assume A84:
f . x = f . y
;
:: thesis: x = y
A85:
((x1 * m) + (x2 * n)) mod (m * n) =
f . xx1,
xx2
by A67, A71, A74
.=
f . yy1,
yy2
by A70, A77, A84
.=
((y1 * m) + (y2 * n)) mod (m * n)
by A67, A78, A81
;
reconsider y1 =
y1,
y2 =
y2,
x1 =
x1,
x2 =
x2 as
Element of
NAT ;
set k =
((x1 * m) + (x2 * n)) mod (m * n);
A86:
(y1 * m) + (y2 * n) = (((x1 * m) + (x2 * n)) mod (m * n)) + ((((y1 * m) + (y2 * n)) div (m * n)) * (m * n))
by A4, A85, NAT_D:2;
A87:
((x1 * m) + (x2 * n)) - ((y1 * m) + (y2 * n)) = (m * (x1 - y1)) + (n * (x2 - y2))
;
A88:
((((x1 * m) + (x2 * n)) mod (m * n)) + ((((x1 * m) + (x2 * n)) div (m * n)) * (m * n))) - ((((x1 * m) + (x2 * n)) mod (m * n)) + ((((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));
consider p being
Integer such that A89:
p = m
;
A90:
(m * (x1 - y1)) + (n * (x2 - y2)) = (m * n) * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))
by A4, A86, A87, A88, NAT_D:2;
then
n * (x2 - y2) = m * ((n * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x1 - y1))
;
then A91:
p divides n * (x2 - y2)
by A89, INT_1:def 9;
then A92:
m divides x2 - y2
by A1, A89, INT_2:40;
A93:
x2 - y2 = 0
proof
per cases
( 0 <= x2 - y2 or x2 - y2 <= 0 )
;
suppose A94:
0 <= x2 - y2
;
:: thesis: x2 - y2 = 0 consider k being
Integer such that A95:
k = x2 - y2
;
reconsider k =
k as
Element of
NAT by A94, A95, INT_1:16;
k = 0
proof
assume
k <> 0
;
:: thesis: contradiction
then A96:
0 < k
;
- y2 <= - 1
by A82, XREAL_1:26;
then A97:
x2 + (- y2) <= m + (- 1)
by A76, XREAL_1:9;
set b =
m + (- 1);
m + (- 1) is
Element of
NAT
by A94, A97, INT_1:16;
then
k < (m + (- 1)) + 1
by A95, A97, NAT_1:13;
hence
contradiction
by A1, A89, A91, A95, A96, INT_2:40, NAT_D:7;
:: thesis: verum
end; hence
x2 - y2 = 0
by A95;
:: thesis: verum end;
end;
consider p being
Integer such that A104:
p = n
;
m * (x1 - y1) = n * ((m * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x2 - y2))
by A90;
then A105:
p divides m * (x1 - y1)
by A104, INT_1:def 9;
then A106:
n divides x1 - y1
by A1, A104, INT_2:40;
x1 - y1 = 0
proof
per cases
( 0 <= x1 - y1 or x1 - y1 <= 0 )
;
suppose A107:
0 <= x1 - y1
;
:: thesis: x1 - y1 = 0 consider k being
Integer such that A108:
k = x1 - y1
;
reconsider k =
k as
Element of
NAT by A107, A108, INT_1:16;
k = 0
proof
assume
k <> 0
;
:: thesis: contradiction
then A109:
0 < k
;
- y1 <= - 1
by A79, XREAL_1:26;
then A110:
x1 + (- y1) <= n + (- 1)
by A73, XREAL_1:9;
set b =
n + (- 1);
n + (- 1) is
Element of
NAT
by A107, A110, INT_1:16;
then
k < (n + (- 1)) + 1
by A108, A110, NAT_1:13;
hence
contradiction
by A1, A104, A105, A108, A109, INT_2:40, NAT_D:7;
:: thesis: verum
end; hence
x1 - y1 = 0
by A108;
:: thesis: verum end;
end;
hence
x = y
by A70, A71, A74, A77, A78, A81, A93;
:: thesis: verum
end;
f is onto
proof
thus
rng f c= C
by RELAT_1:def 19;
:: according to FUNCT_2:def 3,
XBOOLE_0:def 10 :: thesis: C c= rng f
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in C or z in rng f )
assume
z in C
;
:: thesis: z in rng f
then consider i being
Element of
NAT such that A117:
i = z
and A118:
ex
x0,
y0 being
Integer st
(
i = ((m * y0) + (n * x0)) mod (m * n) &
m * n,
i are_relative_prime &
y0 <= n &
x0 <= m &
i >= 0 )
;
consider x0,
y0 being
Integer such that A119:
i = ((m * y0) + (n * x0)) mod (m * n)
and A120:
m * n,
i are_relative_prime
and
(
y0 <= n &
x0 <= m &
i >= 0 )
by A118;
consider x,
y being
Integer such that A121:
x = x0 mod m
and A122:
y = y0 mod n
;
A123:
(
x <= m &
y <= n )
by A1, A121, A122, NEWTON:79;
A126:
((m * y) + (n * x)) mod (m * n) = ((m * y0) + (n * x0)) mod (m * n)
A129:
m,
x0 are_relative_prime
A138:
n,
y0 are_relative_prime
reconsider x =
x,
y =
y as
Element of
NAT by A121, A122, INT_1:16, NEWTON:78;
A147:
x <> 0
proof
assume
x = 0
;
:: thesis: contradiction
then A148:
x0 - ((x0 div m) * m) = 0
by A1, A121, INT_1:def 8;
set j =
x0 div m;
A149:
((m * y0) + (n * x0)) mod (m * n) =
(m * (y0 + (n * (x0 div m)))) - (((m * (y0 + (n * (x0 div m)))) div (m * n)) * (m * n))
by A3, A148, INT_1:def 8
.=
m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))))
;
set jj =
(y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)));
reconsider g =
m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)))) as
Element of
NAT by A119, A149;
A150:
(
g > 0 or
g = 0 )
;
A151:
not
(y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))) < 0
A152:
(m * n) gcd (m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))))) = 1
by A119, A120, A149, INT_2:def 4;
reconsider jj =
(y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))) as
Element of
NAT by A151, INT_1:16;
jj = 0
then
(m * n) gcd 0 = 1
by A119, A120, A149, INT_2:def 4;
hence
contradiction
by A2, NEWTON:65;
:: thesis: verum
end;
then A153:
x >= 0 + 1
by INT_1:20;
A154:
y <> 0
proof
assume
y = 0
;
:: thesis: contradiction
then A155:
y0 - ((y0 div n) * n) = 0
by A1, A122, INT_1:def 8;
set j =
y0 div n;
A156:
((m * y0) + (n * x0)) mod (m * n) =
(n * ((m * (y0 div n)) + x0)) - (((n * ((m * (y0 div n)) + x0)) div (m * n)) * (m * n))
by A3, A155, INT_1:def 8
.=
n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))))
;
set jj =
((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)));
reconsider g =
n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)))) as
Element of
NAT by A119, A156;
A157:
(
g > 0 or
g = 0 )
;
A158:
not
((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))) < 0
A159:
(m * n) gcd (n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))))) = 1
by A119, A120, A156, INT_2:def 4;
reconsider jj =
((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))) as
Element of
NAT by A158, INT_1:16;
jj = 0
then
(m * n) gcd 0 = 1
by A119, A120, A156, INT_2:def 4;
hence
contradiction
by A2, NEWTON:65;
:: thesis: verum
end;
then A160:
y >= 0 + 1
by INT_1:20;
A161:
m,
x are_relative_prime
A162:
n,
y are_relative_prime
x in B
by A123, A153, A161;
then reconsider x =
x as
Element of
B ;
y in A
by A123, A160, A162;
then reconsider y =
y as
Element of
A ;
A164:
dom f = [:A,B:]
by FUNCT_2:def 1;
consider w being
set such that A165:
w = [y,x]
;
A166:
w in dom f
by A164, A165, ZFMISC_1:106;
i = f . y,
x
by A67, A119, A126;
hence
z in rng f
by A117, A165, A166, FUNCT_1:def 5;
:: thesis: verum
end;
then
card [:A,B:] = card C
by A68, Th12;
hence
Euler (m * n) = (Euler m) * (Euler n)
by A18, CARD_2:65; :: thesis: verum