:: 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;