let m, n be Nat; :: thesis: ( m > 1 & n > 1 & m,n are_relative_prime implies Euler (m * n) = (Euler m) * (Euler n) )
assume that
A1: m > 1 and
A2: n > 1 and
A3: m,n are_relative_prime ; :: thesis: Euler (m * n) = (Euler m) * (Euler n)
set X = { i where i is Element of NAT : ( m * n,i are_relative_prime & 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_relative_prime & y <= n & x <= m & i >= 0 ) } ;
A4: m * n <> 0 by A1, A2, XCMPLX_1:6;
A5: { 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 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { 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 ) } or z in (Seg (m * n)) \/ {0 } )
assume z in { 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 ) } ; :: thesis: z in (Seg (m * n)) \/ {0 }
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_relative_prime & 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_relative_prime and
y <= n and
x <= m and
i >= 0 by A7;

per cases ( i > 0 or i = 0 ) ;

suppose A9: i > 0 ; :: thesis: z in (Seg (m * n)) \/ {0 }

A10: ((m * y) + (n * x)) mod (m * n) <= m * n

proof

set i2 = m * n;
set i1 = (m * y) + (n * x);
A11: [\(((m * y) + (n * x)) / (m * n))/] + 1 >= ((m * y) + (n * x)) / (m * n) by INT_1:52;
((m * y) + (n * x)) mod (m * n) = ((m * y) + (n * x)) - ((((m * y) + (n * x)) div (m * n)) * (m * n)) by A4, INT_1:def 8
.= ((m * y) + (n * x)) - ([\(((m * y) + (n * x)) / (m * n))/] * (m * n)) by INT_1:def 7 ;
hence ((m * y) + (n * x)) mod (m * n) <= m * n by A1, A2, A11, Lm1, XCMPLX_1:6; :: thesis: verum

end;

i >= 1 by A9, NAT_1:14;
then z in Seg (m * n) by A6, A8, A10, FINSEQ_1:3;
hence z in (Seg (m * n)) \/ {0 } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A12: i = 0 ; :: thesis: z in (Seg (m * n)) \/ {0 }

0 in {0 } by TARSKI:def 1;
hence z in (Seg (m * n)) \/ {0 } by A6, A12, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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 ;
set A = { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } ;
A13: { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } c= Seg n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } or x in Seg n )
assume x in { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } ; :: thesis: x in Seg n
then ex i being Element of NAT st
( i = x & n,i are_relative_prime & i >= 1 & i <= n ) ;
hence x in Seg n by FINSEQ_1:3; :: thesis: verum

end;

A14: 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 )
A15: m gcd n = 1 by A3, INT_2:def 4;
then (m + n) gcd m = 1 by Th8;
then A16: m,m + n are_relative_prime by INT_2:def 4;
(m + n) gcd n = 1 by A15, Th8;
then n,m + n are_relative_prime by INT_2:def 4;
then m * n,m + n are_relative_prime by A1, A16, Th15;
then A17: (m * n) gcd (m + n) = 1 by INT_2:def 4;
assume A18: ( y = 1 & x = 1 ) ; :: thesis: ((m * y) + (n * x)) mod (m * n) in C
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, Th9;
then m * n,t are_relative_prime by A18, A19, INT_2:def 4;
hence ((m * y) + (n * x)) mod (m * n) in C by A1, A2, A18, A19; :: thesis: verum

end;

reconsider A = { i where i is Element of NAT : ( n,i are_relative_prime & i >= 1 & i <= n ) } as finite set by A13;
A20: for a being Nat st a = 1 holds
a in A

proof

let a be Nat; :: thesis: ( a = 1 implies a in A )
assume A21: a = 1 ; :: thesis: a in A
then n gcd a = 1 by NEWTON:64;
then n,a are_relative_prime by INT_2:def 4;
hence a in A by A2, A21; :: thesis: verum

end;

set B = { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } ;
A22: { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } c= Seg m

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } or x in Seg m )
assume x in { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } ; :: thesis: x in Seg m
then ex i being Element of NAT st
( i = x & m,i are_relative_prime & i >= 1 & i <= m ) ;
hence x in Seg m by FINSEQ_1:3; :: thesis: verum

end;

A23: m * n <> 1 by A1, NAT_1:15;
A24: 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

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in C or z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } )
assume z in C ; :: thesis: z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) }
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_relative_prime & 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_relative_prime 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: [\(((m * y) + (n * x)) / (m * n))/] + 1 >= ((m * y) + (n * x)) / (m * n) by INT_1:52;
((m * y) + (n * x)) mod (m * n) = ((m * y) + (n * x)) - ((((m * y) + (n * x)) div (m * n)) * (m * n)) by A4, INT_1:def 8
.= ((m * y) + (n * x)) - ([\(((m * y) + (n * x)) / (m * n))/] * (m * n)) by INT_1:def 7 ;
hence ((m * y) + (n * x)) mod (m * n) <= m * n by A1, A2, A30, Lm1, XCMPLX_1:6; :: thesis: verum

end;

per cases ( i > 0 or i = 0 ) ;

suppose i > 0 ; :: thesis: z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) }

then i >= 1 by NAT_1:14;
hence z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } by A25, A27, A28, A29; :: thesis: verum

end;

suppose i = 0 ; :: thesis: z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) }

then (m * n) gcd 0 = 1 by A28, INT_2:def 4;
hence z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } by A23, NEWTON:65; :: thesis: verum

end;

end;

end;

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
A31: i = z and
A32: m * n,i are_relative_prime and
i >= 1 and
A33: i <= m * n ;
i <> m * n

proof

assume i = m * n ; :: thesis: contradiction
then (m * n) gcd (m * n) = 1 by A32, INT_2:def 4;
then m * n = 1 by NAT_D:32;
hence contradiction by A1, NAT_1:15; :: thesis: verum

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, Th11;
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 8
.= ((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 8;
then (m * y0) + (n * x0) = ((m * y1) + (n * x1)) + ((m * n) * ((y0 div n) + (x0 div m))) by A37, A38;
then A39: (m * y0) + (n * x0) = ((m * y1) + (n * x1)) mod (m * n) by A36, Th13;
A40: [\(y0 / n)/] + 1 >= y0 / n by INT_1:52;
A41: [\(x0 / m)/] + 1 >= x0 / m by INT_1:52;
y1 = y0 - ((y0 div n) * n) by A2, A38, INT_1:def 8
.= y0 - ([\(y0 / n)/] * n) by INT_1:def 7 ;
then A42: y1 <= n by A2, A40, Lm1;
x1 = x0 - ((x0 div m) * m) by A1, A37, INT_1:def 8
.= x0 - ([\(x0 / m)/] * m) by INT_1:def 7 ;
then x1 <= m by A1, A41, Lm1;
hence z in C by A31, A32, A35, A42, A39; :: thesis: verum

end;

reconsider B = { i where i is Element of NAT : ( m,i are_relative_prime & i >= 1 & i <= m ) } as finite set by A22;
A43: for b being Nat st b = 1 holds
b in B

proof

let b be Nat; :: thesis: ( b = 1 implies b in B )
assume A44: b = 1 ; :: thesis: b in B
then m gcd b = 1 by NEWTON:64;
then m,b are_relative_prime by INT_2:def 4;
hence b in B by A1, A44; :: 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 A13, A22, A5, A20, A43, A14, XBOOLE_1:1;
deffunc H₁( Element of A, Element of B) -> Element of NAT = ((m * $1) + (n * $2)) mod (m * n);
A45: for y being Element of A
for x being Element of B holds H₁(y,x) in C

proof

set l = n * m;
let y be Element of A; :: thesis: for x being Element of B holds H₁(y,x) in C
let x be Element of B; :: thesis: H₁(y,x) in C
y in A ;
then consider i being Element of NAT such that
A46: i = y and
A47: n,i are_relative_prime 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_relative_prime and
j >= 1 and
A52: j <= m ;
i * m,n are_relative_prime by A1, A2, A3, A47, Th15;
then (i * m) gcd n = 1 by INT_2:def 4;
then ((m * i) + (n * j)) gcd n = 1 by Th9;
then A53: n,(m * i) + (n * j) are_relative_prime by INT_2:def 4;
j * n,m are_relative_prime by A1, A2, A3, A51, Th15;
then (j * n) gcd m = 1 by INT_2:def 4;
then ((m * i) + (n * j)) gcd m = 1 by Th9;
then A54: m,(m * i) + (n * j) are_relative_prime by INT_2:def 4;
i * m <> 0 * m by A1, A48, XCMPLX_1:5;
then n * m,(m * i) + (n * j) are_relative_prime by A1, A53, A54, Th15;
then A55: (n * m) gcd ((m * i) + (n * j)) = 1 by INT_2:def 4;
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 (n * m)) gcd (n * m) = 1 by A55, Th9;
then n * m,q are_relative_prime by A56, INT_2:def 4;
hence H₁(y,x) in C by A46, A49, A50, A52, A56; :: thesis: verum

end;

consider f being Function of [:A,B:],C such that
A57: for y being Element of A
for x being Element of B holds f . y,x = H₁(y,x) from FUNCT_7:sch 1(A45);
A58: 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= proj2 f
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in C or z in proj2 f )
assume z in C ; :: thesis: z in proj2 f
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_relative_prime & 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_relative_prime 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:79;
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 8;
then (m * y0) + (n * x0) = ((m * y) + (n * x)) + ((m * n) * ((y0 div n) + (x0 div m))) by A63, A64;
hence ((m * y) + (n * x)) mod (m * n) = ((m * y0) + (n * x0)) mod (m * n) by Th13; :: thesis: verum

end;

A67: y <= n by A2, A64, NEWTON:79;
reconsider x = x, y = y as Element of NAT by A63, A64, INT_1:16, NEWTON:78;
A68: x <> 0

proof

set j = x0 div m;
set jj = (y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)));
assume x = 0 ; :: thesis: contradiction
then x0 - ((x0 div m) * m) = 0 by A1, A63, INT_1:def 8;
then A69: ((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 A4, INT_1:def 8
.= m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)))) ;
then reconsider g = m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)))) as Element of NAT by A61;
A70: (m * n) gcd (m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))))) = 1 by A61, A62, A69, INT_2:def 4;
A71: ( g > 0 or g = 0 ) ;
not (y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))) < 0

proof

assume (y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))) < 0 ; :: thesis: contradiction
then m * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)))) < 0 * ((y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n)))) by A1, XREAL_1:71;
hence contradiction by A71; :: thesis: verum

end;

then reconsider jj = (y0 + (n * (x0 div m))) - (n * ((m * (y0 + (n * (x0 div m)))) div (m * n))) as Element of NAT by INT_1:16;
jj = 0

proof

assume not jj = 0 ; :: thesis: contradiction
m * (n gcd jj) = 1 by A1, A2, A70, Th16;
hence contradiction by A1, NAT_1:15; :: thesis: verum

end;

then (m * n) gcd 0 = 1 by A61, A62, A69, INT_2:def 4;
hence contradiction by A23, NEWTON:65; :: thesis: verum

end;

A72: y <> 0

proof

set j = y0 div n;
set jj = ((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)));
assume y = 0 ; :: thesis: contradiction
then y0 - ((y0 div n) * n) = 0 by A2, A64, INT_1:def 8;
then A73: ((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 A4, INT_1:def 8
.= n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)))) ;
then reconsider g = n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)))) as Element of NAT by A61;
A74: (m * n) gcd (n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))))) = 1 by A61, A62, A73, INT_2:def 4;
A75: ( g > 0 or g = 0 ) ;
not ((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))) < 0

proof

assume ((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))) < 0 ; :: thesis: contradiction
then n * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)))) < 0 * (((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n)))) by A2, XREAL_1:71;
hence contradiction by A75; :: thesis: verum

end;

then reconsider jj = ((m * (y0 div n)) + x0) - (m * ((n * ((m * (y0 div n)) + x0)) div (m * n))) as Element of NAT by INT_1:16;
jj = 0

proof

assume not jj = 0 ; :: thesis: contradiction
n * (m gcd jj) = 1 by A1, A2, A74, Th16;
hence contradiction by A2, NAT_1:15; :: thesis: verum

end;

then (m * n) gcd 0 = 1 by A61, A62, A73, INT_2:def 4;
hence contradiction by A23, NEWTON:65; :: thesis: verum

end;

A76: m,x0 are_relative_prime

proof

set p = m gcd x0;
m gcd x0 divides m by INT_2:31;
then consider i1 being Integer such that
A77: m = (m gcd x0) * i1 by INT_1:def 9;
m gcd x0 divides x0 by INT_2:31;
then consider i2 being Integer such that
A78: x0 = (m gcd x0) * i2 by INT_1:def 9;
set jj = i1 * n;
set k = ((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n);
set j = ((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n);
A79: m gcd x0 <> 0 by A1, A77;
A80: ((m * y0) + (n * x0)) mod (m * n) = ((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) - ((((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n)) * (((m gcd x0) * i1) * n)) by A4, A77, A78, INT_1:def 8;
A81: ((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) - ((((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n)) * (((m gcd x0) * i1) * n)) = (m gcd x0) * (((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n)) ;
not ((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n) < 0

proof

assume ((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n) < 0 ; :: thesis: contradiction
then (m gcd x0) * (((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n)) < 0 * (((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n)) by A79, XREAL_1:71;
hence contradiction by A4, A61, A77, A78, A81, INT_1:def 8; :: thesis: verum

end;

then reconsider p = m gcd x0, j = ((i1 * y0) + (n * i2)) - ((i1 * (((((m gcd x0) * i1) * y0) + (n * ((m gcd x0) * i2))) div (((m gcd x0) * i1) * n))) * n) as Element of NAT by INT_1:16;
not i1 * n < 0

proof

assume i1 * n < 0 ; :: thesis: contradiction
then p * (i1 * n) < 0 * (i1 * n) by A79, XREAL_1:71;
hence contradiction by A4, A77; :: thesis: verum

end;

then reconsider jj = i1 * n as Element of NAT by INT_1:16;
A82: m * n = p * (i1 * n) by A77;

now

per cases ( ( p <> 0 & jj <> 0 & j <> 0 ) or ( p <> 0 & jj <> 0 & j = 0 ) ) by A1, A2, A82, XCMPLX_1:6;

suppose A83: ( p <> 0 & jj <> 0 & j <> 0 ) ; :: thesis: p = 1

(p * jj) gcd (p * j) = 1 by A61, A62, A77, A80, INT_2:def 4;
then p * (jj gcd j) = 1 by A83, Th16;
hence p = 1 by NAT_1:15; :: thesis: verum

end;

suppose ( p <> 0 & jj <> 0 & j = 0 ) ; :: thesis: p = 1

then (p * jj) gcd 0 = 1 by A61, A62, A77, A80, A81, INT_2:def 4;
then p * jj = 1 by NEWTON:65;
hence p = 1 by NAT_1:15; :: thesis: verum

end;

end;

end;

hence m,x0 are_relative_prime by INT_2:def 4; :: thesis: verum

end;

n,y0 are_relative_prime

proof

set p = n gcd y0;
n gcd y0 divides n by INT_2:31;
then consider i1 being Integer such that
A84: n = (n gcd y0) * i1 by INT_1:def 9;
n gcd y0 divides y0 by INT_2:31;
then consider i2 being Integer such that
A85: y0 = (n gcd y0) * i2 by INT_1:def 9;
set jj = i1 * m;
set k = ((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1));
set j = ((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m);
A86: n gcd y0 <> 0 by A2, A84;
A87: ((m * y0) + (n * x0)) mod (m * n) = ((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) - ((((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1))) * (m * ((n gcd y0) * i1))) by A4, A84, A85, INT_1:def 8;
A88: ((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) - ((((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1))) * (m * ((n gcd y0) * i1))) = (n gcd y0) * (((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m)) ;
((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m) >= 0

proof

assume ((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m) < 0 ; :: thesis: contradiction
then (n gcd y0) * (((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m)) < 0 * (((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m)) by A86, XREAL_1:71;
hence contradiction by A4, A61, A84, A85, A88, INT_1:def 8; :: thesis: verum

end;

then reconsider p = n gcd y0, j = ((m * i2) + (i1 * x0)) - ((i1 * (((m * ((n gcd y0) * i2)) + (((n gcd y0) * i1) * x0)) div (m * ((n gcd y0) * i1)))) * m) as Element of NAT by INT_1:16;
not i1 * m < 0

proof

assume i1 * m < 0 ; :: thesis: contradiction
then p * (i1 * m) < 0 * (i1 * m) by A86, XREAL_1:71;
hence contradiction by A4, A84; :: thesis: verum

end;

then reconsider jj = i1 * m as Element of NAT by INT_1:16;
A89: m * n = p * (i1 * m) by A84;

now

per cases ( ( p <> 0 & jj <> 0 & j <> 0 ) or ( p <> 0 & jj <> 0 & j = 0 ) ) by A1, A2, A89, XCMPLX_1:6;

suppose A90: ( p <> 0 & jj <> 0 & j <> 0 ) ; :: thesis: p = 1

(p * jj) gcd (p * j) = 1 by A61, A62, A84, A87, INT_2:def 4;
then p * (jj gcd j) = 1 by A90, Th16;
hence p = 1 by NAT_1:15; :: thesis: verum

end;

suppose ( p <> 0 & jj <> 0 & j = 0 ) ; :: thesis: p = 1

then (p * jj) gcd 0 = 1 by A61, A62, A84, A87, A88, INT_2:def 4;
then p * jj = 1 by NEWTON:65;
hence p = 1 by NAT_1:15; :: thesis: verum

end;

end;

end;

hence n,y0 are_relative_prime by INT_2:def 4; :: thesis: verum

end;

then A91: y0 gcd n = 1 by INT_2:def 4;
x = x0 - ((x0 div m) * m) by A1, A63, INT_1:def 8;
then x0 gcd m = (x + ((x0 div m) * m)) gcd m ;
then x0 gcd m = x gcd m by A68, Th17;
then m gcd x = 1 by A76, INT_2:def 4;
then A92: m,x are_relative_prime by INT_2:def 4;
x >= 0 + 1 by A68, INT_1:20;
then A93: x in B by A65, A92;
y = y0 - ((y0 div n) * n) by A2, A64, INT_1:def 8;
then y0 gcd n = (y + ((y0 div n) * n)) gcd n ;
then y0 gcd n = y gcd n by A72, Th17;
then A94: n,y are_relative_prime by A91, INT_2:def 4;
y >= 0 + 1 by A72, INT_1:20;
then y in A by A67, A94;
then reconsider y = y as Element of A ;
reconsider x = 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:106;
hence z in rng f by A59, A96, A95, FUNCT_1:def 5; :: thesis: verum

end;

A97: m * n >= 1 by A1, A2, NAT_1:14, XCMPLX_1:6;
f is one-to-one

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
A98: dom f = [:A,B:] by FUNCT_2:def 1;
assume x in dom f ; :: thesis: ( not y in proj1 f or not f . x = f . y or x = y )
then consider xx1 being Element of A, xx2 being Element of B such that
A99: x = [xx1,xx2] by A98, DOMAIN_1:9;
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
A100: y = [yy1,yy2] by A98, DOMAIN_1:9;
xx1 in A ;
then consider x1 being Element of NAT such that
A101: xx1 = x1 and
n,x1 are_relative_prime 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_relative_prime and
A105: x2 >= 1 and
A106: x2 <= m ;
consider p being Integer such that
A107: p = m ;
assume A108: f . x = f . y ; :: thesis: x = y
yy2 in B ;
then consider y2 being Element of NAT such that
A109: yy2 = y2 and
m,y2 are_relative_prime 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_relative_prime 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 = y1, y2 = y2, x1 = x1, x2 = 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)) & ((((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));
(y1 * m) + (y2 * n) = (((x1 * m) + (x2 * n)) mod (m * n)) + ((((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) * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n))) by A97, A116, 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 A118: p divides n * (x2 - y2) by A107, INT_1:def 9;
consider p being Integer such that
A119: p = n ;
m * (x1 - y1) = n * ((m * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x2 - y2)) by A117;
then A120: p divides m * (x1 - y1) by A119, INT_1:def 9;
then A121: n divides x1 - y1 by A3, A119, INT_2:40;
A122: x1 - y1 = 0

proof

per cases ( 0 <= x1 - y1 or x1 - y1 <= 0 ) ;

suppose A123: 0 <= x1 - y1 ; :: thesis: x1 - y1 = 0

consider k being Integer such that
A124: k = x1 - y1 ;
reconsider k = k as Element of NAT by A123, A124, INT_1:16;
k = 0

proof

set b = n + (- 1);
- y1 <= - 1 by A113, XREAL_1:26;
then A125: x1 + (- y1) <= n + (- 1) by A103, XREAL_1:9;
then n + (- 1) is Element of NAT by A123, INT_1:16;
then A126: k < (n + (- 1)) + 1 by A124, A125, NAT_1:13;
assume k <> 0 ; :: thesis: contradiction
hence contradiction by A3, A119, A120, A124, A126, INT_2:40, NAT_D:7; :: thesis: verum

end;

hence x1 - y1 = 0 by A124; :: thesis: verum

end;

suppose A127: x1 - y1 <= 0 ; :: thesis: x1 - y1 = 0

consider k being Integer such that
A128: k = - (x1 - y1) ;
A129: - 0 <= k by A127, A128;
A130: n divides k by A121, A128, INT_2:14;
reconsider k = k as Element of NAT by A127, A128, INT_1:16;
k = 0

proof

set b = n + (- 1);
- x1 <= - 1 by A102, XREAL_1:26;
then A131: (- x1) + y1 <= n + (- 1) by A114, XREAL_1:9;
then n + (- 1) is Element of NAT by A128, A129, INT_1:16;
then A132: k < (n + (- 1)) + 1 by A128, A131, NAT_1:13;
assume k <> 0 ; :: thesis: contradiction
hence contradiction by A130, A132, NAT_D:7; :: thesis: verum

end;

hence x1 - y1 = 0 by A128; :: thesis: verum

end;

end;

end;

A133: m divides x2 - y2 by A3, A107, A118, INT_2:40;
x2 - y2 = 0

proof

per cases ( 0 <= x2 - y2 or x2 - y2 <= 0 ) ;

suppose A134: 0 <= x2 - y2 ; :: thesis: x2 - y2 = 0

consider k being Integer such that
A135: k = x2 - y2 ;
reconsider k = k as Element of NAT by A134, A135, INT_1:16;
k = 0

proof

set b = m + (- 1);
- y2 <= - 1 by A110, XREAL_1:26;
then A136: x2 + (- y2) <= m + (- 1) by A106, XREAL_1:9;
then m + (- 1) is Element of NAT by A134, INT_1:16;
then A137: k < (m + (- 1)) + 1 by A135, A136, NAT_1:13;
assume k <> 0 ; :: thesis: contradiction
hence contradiction by A3, A107, A118, A135, A137, INT_2:40, NAT_D:7; :: thesis: verum

end;

hence x2 - y2 = 0 by A135; :: thesis: verum

end;

suppose A138: x2 - y2 <= 0 ; :: thesis: x2 - y2 = 0

consider k being Integer such that
A139: k = - (x2 - y2) ;
A140: - 0 <= k by A138, A139;
A141: m divides k by A133, A139, INT_2:14;
reconsider k = k as Element of NAT by A138, A139, INT_1:16;
k = 0

proof

set b = m + (- 1);
- x2 <= - 1 by A105, XREAL_1:26;
then A142: (- x2) + y2 <= m + (- 1) by A111, XREAL_1:9;
then m + (- 1) is Element of NAT by A139, A140, INT_1:16;
then A143: k < (m + (- 1)) + 1 by A139, A142, NAT_1:13;
assume k <> 0 ; :: thesis: contradiction
hence contradiction by A141, A143, NAT_D:7; :: thesis: verum

end;

hence x2 - y2 = 0 by A139; :: thesis: verum

end;

end;

end;

hence x = y by A99, A101, A104, A100, A112, A109, A122; :: thesis: verum

end;

then card [:A,B:] = card C by A58, Th12;
hence Euler (m * n) = (Euler m) * (Euler n) by A24, CARD_2:65; :: thesis: verum