:: EULER_1 semantic presentation
begin
Lm1: for k being Nat
for j being Integer st k <> 0 & [\(j / k)/] + 1 >= j / k holds
k >= j - ([\(j / k)/] * k)
proof
let k be Nat; ::_thesis: for j being Integer st k <> 0 & [\(j / k)/] + 1 >= j / k holds
k >= j - ([\(j / k)/] * k)
let j be Integer; ::_thesis: ( k <> 0 & [\(j / k)/] + 1 >= j / k implies k >= j - ([\(j / k)/] * k) )
assume that
A1: k <> 0 and
A2: [\(j / k)/] + 1 >= j / k ; ::_thesis: k >= j - ([\(j / k)/] * 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 k >= j - ([\(j / k)/] * k) ; ::_thesis: verum
end;
Lm2: not 1 is prime
by INT_2:def_4;
theorem Th1: :: EULER_1:1
for n being Nat holds
( n,n are_relative_prime iff n = 1 )
proof
let n be Nat; ::_thesis: ( n,n are_relative_prime iff n = 1 )
n gcd n = n by NAT_D:32;
hence ( n,n are_relative_prime iff n = 1 ) by INT_2:def_3; ::_thesis: verum
end;
theorem Th2: :: EULER_1:2
for k, n being Nat st k <> 0 & k < n & n is prime holds
k,n are_relative_prime
proof
let k, n be Nat; ::_thesis: ( k <> 0 & k < n & n is prime implies k,n are_relative_prime )
assume that
A1: ( k <> 0 & k < n ) and
A2: n is prime ; ::_thesis: k,n are_relative_prime
A3: k gcd n divides n by NAT_D:def_5;
percases ( k gcd n = 1 or k gcd n = n ) by A2, A3, INT_2:def_4;
suppose k gcd n = 1 ; ::_thesis: k,n are_relative_prime
hence k,n are_relative_prime by INT_2:def_3; ::_thesis: verum
end;
suppose k gcd n = n ; ::_thesis: k,n are_relative_prime
then n divides k by NAT_D:def_5;
hence k,n are_relative_prime by A1, NAT_D:7; ::_thesis: verum
end;
end;
end;
theorem Th3: :: EULER_1:3
for n, k being Nat holds
( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } iff ( n is prime & k in n & not k in {0} ) )
proof
let n, k be Nat; ::_thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } iff ( n is prime & k in n & not k in {0} ) )
set X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ;
thus ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } implies ( n is prime & k in n & not k in {0} ) ) ::_thesis: ( n is prime & k in n & not k in {0} implies ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ) )
proof
assume that
A1: n is prime and
A2: k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ; ::_thesis: ( n is prime & k in n & not k in {0} )
A3: ex kk being Element of NAT st
( kk = k & n,kk are_relative_prime & kk >= 1 & kk <= n ) by A2;
then k <> n by A1, Lm2, Th1;
then k < n by A3, XXREAL_0:1;
hence ( n is prime & k in n & not k in {0} ) by A1, A3, NAT_1:44, TARSKI:def_1; ::_thesis: verum
end;
assume that
A4: n is prime and
A5: k in n and
A6: not k in {0} ; ::_thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } )
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_relative_prime ) by A4, A7, Th2, ORDINAL1:def_12;
hence ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ) by A4, A9, A8; ::_thesis: verum
end;
theorem Th4: :: EULER_1:4
for A being finite set
for x being set st x in A holds
card (A \ {x}) = (card A) - (card {x})
proof
let A be finite set ; ::_thesis: for x being set st x in A holds
card (A \ {x}) = (card A) - (card {x})
let x be set ; ::_thesis: ( x in A implies card (A \ {x}) = (card A) - (card {x}) )
assume x in A ; ::_thesis: card (A \ {x}) = (card A) - (card {x})
then {x} c= A by ZFMISC_1:31;
hence card (A \ {x}) = (card A) - (card {x}) by CARD_2:44; ::_thesis: verum
end;
theorem Th5: :: EULER_1:5
for a, b being Nat st a gcd b = 1 holds
for c being Nat holds (a * c) gcd (b * c) = c
proof
let a, b be Nat; ::_thesis: ( a gcd b = 1 implies for c being Nat holds (a * c) gcd (b * c) = c )
assume A1: a gcd b = 1 ; ::_thesis: for c being Nat holds (a * c) gcd (b * c) = c
let m be Nat; ::_thesis: (a * m) gcd (b * m) = m
reconsider a9 = a, b9 = b as Integer ;
a9,b9 are_relative_prime by A1, INT_2:def_3;
hence (a * m) gcd (b * m) = abs (abs m) by INT_2:24
.= m by ABSVALUE:def_1 ;
::_thesis: verum
end;
theorem Th6: :: EULER_1:6
for a, c, b being Nat st a <> 0 & c <> 0 & (a * c) gcd (b * c) = c holds
a,b are_relative_prime
proof
let a, c, b be Nat; ::_thesis: ( a <> 0 & c <> 0 & (a * c) gcd (b * c) = c implies a,b are_relative_prime )
assume that
A1: a <> 0 and
A2: c <> 0 and
A3: (a * c) gcd (b * c) = c ; ::_thesis: a,b are_relative_prime
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_relative_prime ) by INT_2:23;
a = a1 by A2, A3, A4, XCMPLX_1:5;
hence a,b are_relative_prime by A2, A3, A5, XCMPLX_1:5; ::_thesis: verum
end;
theorem Th7: :: EULER_1:7
for a, b being Nat st a gcd b = 1 holds
(a + b) gcd b = 1
proof
let a, b be Nat; ::_thesis: ( a gcd b = 1 implies (a + b) gcd b = 1 )
assume A1: a gcd b = 1 ; ::_thesis: (a + b) gcd b = 1
set n = (a + b) gcd b;
A2: (a + b) gcd b divides b by NAT_D:def_5;
(a + b) gcd b divides a + b by NAT_D:def_5;
then (a + b) gcd b divides a by A2, NAT_D:10;
then (a + b) gcd b divides a gcd b by A2, NEWTON:50;
then A3: (a + b) gcd b <= 1 + 0 by A1, NAT_D:7;
percases ( (a + b) gcd b = 1 or (a + b) gcd b = 0 ) by A3, NAT_1:9;
suppose (a + b) gcd b = 1 ; ::_thesis: (a + b) gcd b = 1
hence (a + b) gcd b = 1 ; ::_thesis: verum
end;
suppose (a + b) gcd b = 0 ; ::_thesis: (a + b) gcd b = 1
then b = 0 by INT_2:5;
hence (a + b) gcd b = 1 by A1; ::_thesis: verum
end;
end;
end;
theorem Th8: :: EULER_1:8
for a, b, c being Nat holds (a + (b * c)) gcd b = a gcd b
proof
let a, b, c be Nat; ::_thesis: (a + (b * c)) gcd b = a gcd b
defpred S1[ Nat] means (a + (b * $1)) gcd b = a gcd b;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let kk be Nat; ::_thesis: ( S1[kk] implies S1[kk + 1] )
assume A2: (a + (b * kk)) gcd b = a gcd b ; ::_thesis: S1[kk + 1]
now__::_thesis:_(a_+_(b_*_(kk_+_1)))_gcd_b_=_a_gcd_b
percases ( b = 0 or b > 0 ) ;
suppose b = 0 ; ::_thesis: (a + (b * (kk + 1))) gcd b = a gcd b
hence (a + (b * (kk + 1))) gcd b = a gcd b ; ::_thesis: verum
end;
supposeA3: b > 0 ; ::_thesis: (a + (b * (kk + 1))) gcd b = a gcd b
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__::_thesis:_(a_+_(b_*_(kk_+_1)))_gcd_b_=_a_gcd_b
percases ( a + (b * kk) = 0 or a + (b * kk) > 0 ) ;
supposeA7: a + (b * kk) = 0 ; ::_thesis: (a + (b * (kk + 1))) gcd b = a gcd b
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; ::_thesis: verum
end;
supposeA8: a + (b * kk) > 0 ; ::_thesis: (a + (b * (kk + 1))) gcd b = a gcd b
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 (((a + (b * kk)) div (a gcd b)) * (a gcd b)) gcd ((b div (a gcd b)) * (a gcd b)) = a gcd b by A2, A5, NAT_D:3;
then (a + (b * kk)) div (a gcd b),b div (a gcd b) are_relative_prime by A4, A9, Th6;
then ((a + (b * kk)) div (a gcd b)) gcd (b div (a gcd b)) = 1 by INT_2:def_3;
then A11: (((a + (b * kk)) div (a gcd b)) + (b div (a gcd b))) gcd (b div (a gcd b)) = 1 by Th7;
(a + (b * (kk + 1))) gcd b = ((a + (b * kk)) + b) gcd b
.= (((a gcd b) * ((a + (b * kk)) div (a gcd b))) + ((a gcd b) * (b div (a gcd b)))) gcd ((a gcd b) * (b div (a gcd b))) by A5, A10, NAT_D:3
.= ((a gcd b) * (((a + (b * kk)) div (a gcd b)) + (b div (a gcd b)))) gcd ((a gcd b) * (b div (a gcd b)))
.= a gcd b by A11, Th5 ;
hence (a + (b * (kk + 1))) gcd b = a gcd b ; ::_thesis: verum
end;
end;
end;
hence (a + (b * (kk + 1))) gcd b = a gcd b ; ::_thesis: verum
end;
end;
end;
hence S1[kk + 1] ; ::_thesis: verum
end;
A12: S1[ 0 ] ;
for c being Nat holds S1[c] from NAT_1:sch_2(A12, A1);
hence (a + (b * c)) gcd b = a gcd b ; ::_thesis: verum
end;
theorem Th9: :: EULER_1:9
for m, n being Nat st m,n are_relative_prime holds
ex k being Nat st
( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) )
proof
let m, n be Nat; ::_thesis: ( m,n are_relative_prime implies ex k being Nat st
( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) ) )
defpred S1[ Nat] means ex i0, j0 being Integer st
( $1 = (i0 * m) + (j0 * n) & $1 > 0 );
assume A1: m,n are_relative_prime ; ::_thesis: ex k being Nat st
( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) )
( m > 0 or n > 0 )
proof
assume ( not m > 0 & not n > 0 ) ; ::_thesis: contradiction
then ( m = 0 & n = 0 ) ;
then m gcd n <> 1 by NAT_D:32;
hence contradiction by A1, INT_2:def_3; ::_thesis: verum
end;
then (1 * m) + (1 * n) > 0 ;
then A2: ex k being Nat st S1[k] ;
consider k being Nat such that
A3: S1[k] and
A4: for l being Nat st S1[l] holds
k <= l from NAT_1:sch_5(A2);
take k ; ::_thesis: ( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) )
thus ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) by A3; ::_thesis: for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l
let l be Nat; ::_thesis: ( ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) implies k <= l )
thus ( ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) implies k <= l ) by A4; ::_thesis: verum
end;
theorem Th10: :: EULER_1:10
for m, n being Nat st m,n are_relative_prime holds
for k being Nat ex i, j being Integer st (i * m) + (j * n) = k
proof
let m, n be Nat; ::_thesis: ( m,n are_relative_prime implies for k being Nat ex i, j being Integer st (i * m) + (j * n) = k )
reconsider a9 = 1, 09 = 0 as Integer ;
assume A1: m,n are_relative_prime ; ::_thesis: for k being Nat ex i, j being Integer st (i * m) + (j * n) = k
then consider a being Nat such that
A2: ex i0, j0 being Integer st
( a = (i0 * m) + (j0 * n) & a > 0 ) and
A3: for c being Nat st ex i, j being Integer st
( c = (i * m) + (j * n) & c > 0 ) holds
a <= c by Th9;
let k be Nat; ::_thesis: ex i, j being Integer st (i * m) + (j * n) = k
consider i0, j0 being Integer such that
A4: a = (i0 * m) + (j0 * n) and
A5: a > 0 by A2;
A6: for c being Nat st ex i, j being Integer st
( c = (i * m) + (j * n) & c > 0 ) holds
c mod a = 0
proof
let b be Nat; ::_thesis: ( ex i, j being Integer st
( b = (i * m) + (j * n) & b > 0 ) implies b mod a = 0 )
assume ex i, j being Integer st
( b = (i * m) + (j * n) & b > 0 ) ; ::_thesis: b mod a = 0
then consider i, j being Integer 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 = ((i - ((b div a) * i0)) * m) + ((j - ((b div a) * j0)) * n) as Element of NAT by A4, A7;
assume A9: b mod a <> 0 ; ::_thesis: contradiction
c < a by A4, A5, A7, A8, NAT_D:1;
hence contradiction by A3, A4, A9, A7, A8; ::_thesis: verum
end;
A10: a divides n
proof
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: a divides n
hence a divides n by NAT_D:6; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: a divides n
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 a divides n by NAT_D:3; ::_thesis: verum
end;
end;
end;
a divides m
proof
percases ( m = 0 or m > 0 ) ;
suppose m = 0 ; ::_thesis: a divides m
hence a divides m by NAT_D:6; ::_thesis: verum
end;
suppose m > 0 ; ::_thesis: a divides m
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 a divides m by NAT_D:3; ::_thesis: verum
end;
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 being 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 ex i, j being Integer st (i * m) + (j * n) = k ; ::_thesis: verum
end;
theorem Th11: :: EULER_1:11
for A being set
for B being non empty set
for f being Function of A,B st f is bijective holds
card A = card B
proof
let A be set ; ::_thesis: for B being non empty set
for f being Function of A,B st f is bijective holds
card A = card B
let B be non empty set ; ::_thesis: for f being Function of A,B st f is bijective holds
card A = card B
let f be Function of A,B; ::_thesis: ( f is bijective implies card A = card B )
assume f is bijective ; ::_thesis: card A = card B
then A1: ( f is one-to-one & f is onto ) by FUNCT_2:def_4;
A2: A = dom f by FUNCT_2:def_1;
B c= rng f by A1, FUNCT_2:def_3;
then A3: card B c= card A by A2, CARD_1:12;
rng f c= B by RELAT_1:def_19;
then card A c= card B by A2, A1, CARD_1:10;
hence card A = card B by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th12: :: EULER_1:12
for i, k, n being Integer holds (i + (k * n)) mod n = i mod n
proof
let i, k, n be Integer; ::_thesis: (i + (k * n)) mod n = i mod n
percases ( n <> 0 or n = 0 ) ;
supposeA1: n <> 0 ; ::_thesis: (i + (k * n)) mod n = i mod n
then (i + (k * n)) mod n = (i + (k * n)) - (((i + (k * n)) div n) * n) by INT_1:def_10
.= (i + (k * n)) - ([\((i + (k * n)) / n)/] * n) by INT_1:def_9
.= (i + (k * n)) - ([\((i / n) + ((k * n) / n))/] * n) by XCMPLX_1:62
.= (i + (k * n)) - ([\((i / n) + (k / (n / n)))/] * n) by XCMPLX_1:77
.= (i + (k * n)) - ([\((i / n) + (k / 1))/] * n) by A1, XCMPLX_1:60
.= (i + (k * n)) - (([\(i / n)/] + k) * n) by INT_1:28
.= i - ([\(i / n)/] * n)
.= i - ((i div n) * n) by INT_1:def_9
.= i mod n by A1, INT_1:def_10 ;
hence (i + (k * n)) mod n = i mod n ; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (i + (k * n)) mod n = i mod n
hence (i + (k * n)) mod n = i mod n ; ::_thesis: verum
end;
end;
end;
theorem Th13: :: EULER_1:13
for c, a, b being Nat st c divides a * b & a,c are_relative_prime holds
c divides b
proof
let c, a, b be Nat; ::_thesis: ( c divides a * b & a,c are_relative_prime implies c divides b )
assume that
A1: c divides a * b and
A2: a,c are_relative_prime ; ::_thesis: c divides b
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 c divides b by A1, A3, NEWTON:50; ::_thesis: verum
end;
theorem Th14: :: EULER_1:14
for a, c, b being Nat st a <> 0 & c <> 0 & a,c are_relative_prime & b,c are_relative_prime holds
a * b,c are_relative_prime
proof
let a, c, b be Nat; ::_thesis: ( a <> 0 & c <> 0 & a,c are_relative_prime & b,c are_relative_prime implies a * b,c are_relative_prime )
assume that
A1: a <> 0 and
A2: c <> 0 and
A3: a,c are_relative_prime and
A4: b,c are_relative_prime ; ::_thesis: a * b,c are_relative_prime
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, NAT_D: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_relative_prime ) 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 a * b,c are_relative_prime by INT_2:def_3; ::_thesis: verum
end;
theorem Th15: :: EULER_1:15
for x, i, y being Integer st x <> 0 & i > 0 holds
(i * x) gcd (i * y) = i * (x gcd y)
proof
let x, i, y be Integer; ::_thesis: ( x <> 0 & i > 0 implies (i * x) gcd (i * y) = i * (x gcd y) )
assume that
A1: x <> 0 and
A2: i > 0 ; ::_thesis: (i * x) gcd (i * y) = i * (x gcd y)
consider a2, b2 being Integer such that
A3: ( x = (x gcd y) * a2 & y = (x gcd y) * b2 ) and
A4: a2,b2 are_relative_prime 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) = abs (i * (x gcd y)) by A4, INT_2:24
.= (abs i) * (abs (x gcd y)) by COMPLEX1:65 ;
i = abs i by A2, ABSVALUE:def_1;
hence (i * x) gcd (i * y) = i * (x gcd y) by A5, ABSVALUE:def_1; ::_thesis: verum
end;
theorem Th16: :: EULER_1:16
for a, b being Nat
for x being Integer st a <> 0 holds
(a + (x * b)) gcd b = a gcd b
proof
let a, b be Nat; ::_thesis: for x being Integer st a <> 0 holds
(a + (x * b)) gcd b = a gcd b
let xx be Integer; ::_thesis: ( a <> 0 implies (a + (xx * b)) gcd b = a gcd b )
set i = a gcd b;
A1: b = abs b by ABSVALUE:def_1;
assume A2: a <> 0 ; ::_thesis: (a + (xx * b)) gcd b = a gcd b
A3: for m being Nat st m divides abs (a + (xx * b)) & m divides abs b holds
m divides a gcd b
proof
let mm be Nat; ::_thesis: ( mm divides abs (a + (xx * b)) & mm divides abs b implies mm divides a gcd b )
assume that
A4: mm divides abs (a + (xx * b)) and
A5: mm divides abs b ; ::_thesis: mm divides a gcd b
consider n being Nat such that
A6: b = mm * n by A1, A5, NAT_D:def_3;
reconsider mm = mm as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_mm_divides_a
percases ( a + (xx * b) >= 0 or a + (xx * b) < 0 ) ;
suppose a + (xx * b) >= 0 ; ::_thesis: mm divides a
then abs (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; ::_thesis: verum
end;
suppose a + (xx * b) < 0 ; ::_thesis: mm divides a
then abs (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; ::_thesis: verum
end;
end;
end;
hence mm divides a gcd b by A1, A5, NEWTON:50; ::_thesis: verum
end;
a gcd b divides a by NAT_D:def_5;
then A11: a = (a gcd b) * (a div (a gcd b)) by NAT_D:3;
A12: a gcd b divides b by NAT_D:def_5;
then A13: b = (a gcd b) * (b div (a gcd b)) by NAT_D:3;
a gcd b divides abs (a + (xx * b))
proof
percases ( a + (xx * b) < 0 or a + (xx * b) >= 0 ) ;
suppose a + (xx * b) < 0 ; ::_thesis: a gcd b divides abs (a + (xx * b))
then A14: abs (a + (xx * b)) = - (a + (xx * b)) by ABSVALUE:def_1;
- (a + (xx * b)) = (a gcd b) * (- ((a div (a gcd b)) + (xx * (b div (a gcd b))))) by A11, A13;
hence a gcd b divides abs (a + (xx * b)) by A14, INT_1:def_3; ::_thesis: verum
end;
suppose a + (xx * b) >= 0 ; ::_thesis: a gcd b divides abs (a + (xx * b))
then A15: abs (a + (xx * b)) = a + (xx * b) by ABSVALUE:def_1;
a + (xx * b) = (a gcd b) * ((a div (a gcd b)) + (xx * (b div (a gcd b)))) by A11, A13;
hence a gcd b divides abs (a + (xx * b)) by A15, INT_1:def_3; ::_thesis: verum
end;
end;
end;
then (abs (a + (xx * b))) gcd (abs b) = a gcd b by A1, A12, A3, NAT_D:def_5;
hence (a + (xx * b)) gcd b = a gcd b by INT_2:34; ::_thesis: verum
end;
begin
definition
let n be Nat;
func Euler n -> Element of NAT equals :: EULER_1:def 1
card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;
coherence
card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } is Element of NAT
proof
set X = { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;
{ k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } c= Seg n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } or x in Seg n )
assume x in { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ; ::_thesis: x in Seg n
then ex k being Element of NAT st
( k = x & n,k are_relative_prime & k >= 1 & k <= n ) ;
hence x in Seg n by FINSEQ_1:1; ::_thesis: verum
end;
then reconsider X = { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } as finite set ;
card X is Element of NAT ;
hence card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } is Element of NAT ; ::_thesis: verum
end;
end;
:: deftheorem defines Euler EULER_1:def_1_:_
for n being Nat holds Euler n = card { k where k is Element of NAT : ( n,k are_relative_prime & k >= 1 & k <= n ) } ;
set X = { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } ;
for x being set holds
( x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } iff x = 1 )
proof
let x be set ; ::_thesis: ( x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } iff x = 1 )
thus ( x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } implies x = 1 ) ::_thesis: ( x = 1 implies x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } )
proof
assume x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } ; ::_thesis: x = 1
then ex k being Element of NAT st
( k = x & 1,k are_relative_prime & k >= 1 & k <= 1 ) ;
hence x = 1 by XXREAL_0:1; ::_thesis: verum
end;
1 gcd 1 = 1 by NAT_D:32;
then 1,1 are_relative_prime by INT_2:def_3;
hence ( x = 1 implies x in { k where k is Element of NAT : ( 1,k are_relative_prime & k >= 1 & k <= 1 ) } ) ; ::_thesis: verum
end;
then Lm3: card {1} = Euler 1
by TARSKI:def_1;
theorem :: EULER_1:17
Euler 1 = 1 by Lm3, CARD_1:30;
set X = { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } ;
for x being set holds
( x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } iff x = 1 )
proof
let x be set ; ::_thesis: ( x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } iff x = 1 )
thus ( x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } implies x = 1 ) ::_thesis: ( x = 1 implies x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } )
proof
assume x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } ; ::_thesis: x = 1
then consider k being Element of NAT such that
A1: ( k = x & 2,k are_relative_prime ) and
A2: ( k >= 1 & k <= 2 ) ;
A3: 2 gcd 2 = 2 by NAT_D:32;
( k = 1 or k = 2 ) by A2, NAT_1:26;
hence x = 1 by A1, A3, INT_2:def_3; ::_thesis: verum
end;
2 gcd 1 = 1 by NEWTON:51;
then 2,1 are_relative_prime by INT_2:def_3;
hence ( x = 1 implies x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } ) ; ::_thesis: verum
end;
then Lm4: card {1} = Euler 2
by TARSKI:def_1;
theorem :: EULER_1:18
Euler 2 = 1 by Lm4, CARD_1:30;
theorem Th19: :: EULER_1:19
for n being Nat st n > 1 holds
Euler n <= n - 1
proof
let n be Nat; ::_thesis: ( n > 1 implies Euler n <= n - 1 )
set X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ;
{ kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } c= Seg n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } or x in Seg n )
assume x in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ; ::_thesis: x in Seg n
then ex k being Element of NAT st
( k = x & n,k are_relative_prime & k >= 1 & k <= n ) ;
hence x in Seg n by FINSEQ_1:1; ::_thesis: verum
end;
then reconsider X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } as finite set ;
assume A1: n > 1 ; ::_thesis: Euler n <= n - 1
then 0 in { l where l is Element of 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in n \ {0} )
assume x in X ; ::_thesis: x in n \ {0}
then consider k being Element of NAT such that
A4: k = x and
A5: n,k are_relative_prime and
A6: k >= 1 and
A7: k <= n ;
not n,n are_relative_prime by A1, Th1;
then k < n by A5, A7, XXREAL_0:1;
then k in { l where l is Element of NAT : l < n } ;
then A8: k in n by AXIOMS:4;
not k in {0} by A6, TARSKI:def_1;
hence x in n \ {0} by A4, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
( card n = n & card {0} = 1 ) by CARD_1:30, CARD_1:def_2;
hence Euler n <= n - 1 by A3, A2, NAT_1:43; ::_thesis: verum
end;
theorem :: EULER_1:20
for n being Nat st n is prime holds
Euler n = n - 1
proof
let n be Nat; ::_thesis: ( n is prime implies Euler n = n - 1 )
set X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ;
{ kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } c= Seg n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } or x in Seg n )
assume x in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ; ::_thesis: x in Seg n
then ex k being Element of NAT st
( k = x & n,k are_relative_prime & k >= 1 & k <= n ) ;
hence x in Seg n by FINSEQ_1:1; ::_thesis: verum
end;
then reconsider X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } as finite set ;
assume A1: n is prime ; ::_thesis: Euler n = n - 1
n <> 0
proof
assume n = 0 ; ::_thesis: contradiction
then n in SetPrimenumber 2 by A1, NEWTON:def_7;
hence contradiction ; ::_thesis: verum
end;
then 0 in { l where l is Element of NAT : l < n } ;
then A2: 0 in n by AXIOMS:4;
n \ {0} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n \ {0} or x in X )
assume A3: x in n \ {0} ; ::_thesis: x in X
then x in n ;
then x in { k where k is Element of NAT : k < n } by AXIOMS:4;
then A4: ex k being Element of NAT st
( k = x & k < n ) ;
not x in {0} by A3, XBOOLE_0:def_5;
hence x in X by A1, A3, A4, Th3; ::_thesis: verum
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, CARD_1:def_2;
then n - 1 <= Euler n by A5, A2, Th4;
hence Euler n = n - 1 by A6, XXREAL_0:1; ::_thesis: verum
end;
theorem :: EULER_1:21
for m, n being Nat st m > 1 & n > 1 & m,n are_relative_prime holds
Euler (m * n) = (Euler m) * (Euler n)
proof
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;
percases ( i > 0 or i = 0 ) ;
supposeA9: 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:29;
((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_10
.= ((m * y) + (n * x)) - ([\(((m * y) + (n * x)) / (m * n))/] * (m * n)) by INT_1:def_9 ;
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:1;
hence z in (Seg (m * n)) \/ {0} by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: 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:1; ::_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_3;
then (m + n) gcd m = 1 by Th7;
then A16: m,m + n are_relative_prime by INT_2:def_3;
(m + n) gcd n = 1 by A15, Th7;
then n,m + n are_relative_prime by INT_2:def_3;
then m * n,m + n are_relative_prime by A1, A16, Th14;
then A17: (m * n) gcd (m + n) = 1 by INT_2:def_3;
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, Th8;
then m * n,t are_relative_prime by A18, A19, INT_2:def_3;
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:51;
then n,a are_relative_prime by INT_2:def_3;
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:1; ::_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:29;
((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_10
.= ((m * y) + (n * x)) - ([\(((m * y) + (n * x)) / (m * n))/] * (m * n)) by INT_1:def_9 ;
hence ((m * y) + (n * x)) mod (m * n) <= m * n by A1, A2, A30, Lm1, XCMPLX_1:6; ::_thesis: verum
end;
percases ( 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_3;
hence z in { i where i is Element of NAT : ( m * n,i are_relative_prime & i >= 1 & i <= m * n ) } by A23, NEWTON:52; ::_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_3;
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, 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) * ((y0 div n) + (x0 div m))) by A37, A38;
then A39: (m * y0) + (n * x0) = ((m * y1) + (n * x1)) mod (m * n) by A36, Th12;
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 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:51;
then m,b are_relative_prime by INT_2:def_3;
hence b in B by A1, A44; ::_thesis: verum
end;
{0} c= NAT by ZFMISC_1:31;
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 H1( 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 H1(y,x) in C
proof
set l = n * m;
let y be Element of A; ::_thesis: for x being Element of B holds H1(y,x) in C
let x be Element of B; ::_thesis: H1(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, 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_relative_prime by INT_2:def_3;
j * n,m are_relative_prime 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_relative_prime by INT_2:def_3;
i * m <> 0 * m by A1, A48, XCMPLX_1:5;
then n * m,(m * i) + (n * j) are_relative_prime 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 (n * m)) gcd (n * m) = 1 by A55, Th8;
then n * m,q are_relative_prime by A56, INT_2:def_3;
hence H1(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) = H1(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= K208(C,f)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in C or z in K208(C,f) )
assume z in C ; ::_thesis: z in K208(C,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: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) * ((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 Th12; ::_thesis: verum
end;
A67: y <= n by A2, A64, NEWTON:65;
reconsider x = x, y = y as Element of NAT by A63, A64, INT_1:3, NEWTON:64;
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_10;
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_10
.= 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_3;
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:69;
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:3;
jj = 0
proof
assume not jj = 0 ; ::_thesis: contradiction
m * (n gcd jj) = 1 by A1, A2, A70, Th15;
hence contradiction by A1, NAT_1:15; ::_thesis: verum
end;
then (m * n) gcd 0 = 1 by A61, A62, A69, INT_2:def_3;
hence contradiction by A23, NEWTON:52; ::_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_10;
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_10
.= 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_3;
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:69;
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:3;
jj = 0
proof
assume not jj = 0 ; ::_thesis: contradiction
n * (m gcd jj) = 1 by A1, A2, A74, Th15;
hence contradiction by A2, NAT_1:15; ::_thesis: verum
end;
then (m * n) gcd 0 = 1 by A61, A62, A73, INT_2:def_3;
hence contradiction by A23, NEWTON:52; ::_thesis: verum
end;
A76: m,x0 are_relative_prime
proof
set p = m gcd x0;
m gcd x0 divides m by INT_2:21;
then consider i1 being Integer such that
A77: m = (m gcd x0) * i1 by INT_1:def_3;
m gcd x0 divides x0 by INT_2:21;
then consider i2 being Integer such that
A78: x0 = (m gcd x0) * i2 by INT_1:def_3;
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_10;
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:69;
hence contradiction by A4, A61, A77, A78, A81, INT_1:def_10; ::_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:3;
not i1 * n < 0
proof
assume i1 * n < 0 ; ::_thesis: contradiction
then p * (i1 * n) < 0 * (i1 * n) by A79, XREAL_1:69;
hence contradiction by A4, A77; ::_thesis: verum
end;
then reconsider jj = i1 * n as Element of NAT by INT_1:3;
A82: m * n = p * (i1 * n) by A77;
now__::_thesis:_p_=_1
percases ( ( p <> 0 & jj <> 0 & j <> 0 ) or ( p <> 0 & jj <> 0 & j = 0 ) ) by A1, A2, A82, XCMPLX_1:6;
supposeA83: ( p <> 0 & jj <> 0 & j <> 0 ) ; ::_thesis: p = 1
(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; ::_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_3;
then p * jj = 1 by NEWTON:52;
hence p = 1 by NAT_1:15; ::_thesis: verum
end;
end;
end;
hence m,x0 are_relative_prime by INT_2:def_3; ::_thesis: verum
end;
n,y0 are_relative_prime
proof
set p = n gcd y0;
n gcd y0 divides n by INT_2:21;
then consider i1 being Integer such that
A84: n = (n gcd y0) * i1 by INT_1:def_3;
n gcd y0 divides y0 by INT_2:21;
then consider i2 being Integer such that
A85: y0 = (n gcd y0) * i2 by INT_1:def_3;
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_10;
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:69;
hence contradiction by A4, A61, A84, A85, A88, INT_1:def_10; ::_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:3;
not i1 * m < 0
proof
assume i1 * m < 0 ; ::_thesis: contradiction
then p * (i1 * m) < 0 * (i1 * m) by A86, XREAL_1:69;
hence contradiction by A4, A84; ::_thesis: verum
end;
then reconsider jj = i1 * m as Element of NAT by INT_1:3;
A89: m * n = p * (i1 * m) by A84;
now__::_thesis:_p_=_1
percases ( ( p <> 0 & jj <> 0 & j <> 0 ) or ( p <> 0 & jj <> 0 & j = 0 ) ) by A1, A2, A89, XCMPLX_1:6;
supposeA90: ( p <> 0 & jj <> 0 & j <> 0 ) ; ::_thesis: p = 1
(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; ::_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_3;
then p * jj = 1 by NEWTON:52;
hence p = 1 by NAT_1:15; ::_thesis: verum
end;
end;
end;
hence n,y0 are_relative_prime by INT_2:def_3; ::_thesis: verum
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_relative_prime 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_relative_prime by A91, INT_2:def_3;
y >= 0 + 1 by A72, INT_1:7;
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:87;
hence z in rng f by A59, A96, A95, FUNCT_1:def_3; ::_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_4 ::_thesis: ( not x in dom f or not y in dom 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 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
A99: x = [xx1,xx2] by A98, DOMAIN_1:1;
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:1;
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_3;
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_3;
then A121: n divides x1 - y1 by A3, A119, INT_2:25;
A122: x1 - y1 = 0
proof
percases ( 0 <= x1 - y1 or x1 - y1 <= 0 ) ;
supposeA123: 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: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;
then n + (- 1) is Element of NAT by A123, INT_1:3;
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:25, NAT_D:7; ::_thesis: verum
end;
hence x1 - y1 = 0 by A124; ::_thesis: verum
end;
supposeA127: 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:10;
reconsider k = 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 A131: (- x1) + y1 <= n + (- 1) by A114, XREAL_1:7;
then n + (- 1) is Element of NAT by A128, A129, INT_1:3;
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:25;
x2 - y2 = 0
proof
percases ( 0 <= x2 - y2 or x2 - y2 <= 0 ) ;
supposeA134: 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:3;
k = 0
proof
set b = m + (- 1);
- y2 <= - 1 by A110, XREAL_1:24;
then A136: x2 + (- y2) <= m + (- 1) by A106, XREAL_1:7;
then m + (- 1) is Element of NAT by A134, INT_1:3;
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:25, NAT_D:7; ::_thesis: verum
end;
hence x2 - y2 = 0 by A135; ::_thesis: verum
end;
supposeA138: 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:10;
reconsider k = k as Element of NAT by A138, A139, INT_1:3;
k = 0
proof
set b = m + (- 1);
- x2 <= - 1 by A105, XREAL_1:24;
then A142: (- x2) + y2 <= m + (- 1) by A111, XREAL_1:7;
then m + (- 1) is Element of NAT by A139, A140, INT_1:3;
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 f is bijective by A58, FUNCT_2:def_4;
then card [:A,B:] = card C by Th11;
hence Euler (m * n) = (Euler m) * (Euler n) by A24, CARD_2:46; ::_thesis: verum
end;