euler_1.miz



    begin

    reserve a,b,c,k,l,m,n for Nat,

i,j,x,y for Integer;

    

     Lm1: k <> 0 & ( [\(j / k)/] + 1) >= (j / k) implies k >= (j - ( [\(j / k)/] * k))

    proof

      assume that

       A1: k <> 0 and

       A2: ( [\(j / k)/] + 1) >= (j / k);

      (( [\(j / k)/] + 1) + ( - 1)) >= ((j / k) + ( - 1)) by A2, XREAL_1: 6;

      then ( [\(j / k)/] * k) >= (((j / k) - 1) * k) by XREAL_1: 64;

      then ( - (((j / k) - 1) * k)) >= ( - ( [\(j / k)/] * k)) by XREAL_1: 24;

      then (j + ( - (((j / k) - 1) * k))) >= (j + ( - ( [\(j / k)/] * k))) by XREAL_1: 6;

      then (j - (((j / k) * k) - (1 * k))) >= (j - ( [\(j / k)/] * k));

      then (j - (j - k)) >= (j - ( [\(j / k)/] * k)) by A1, XCMPLX_1: 87;

      hence thesis;

    end;

    

     Lm2: not 1 is prime by INT_2:def 4;

    theorem :: EULER_1:1

    

     Th1: (n,n) are_coprime iff n = 1

    proof

      (n gcd n) = n by NAT_D: 32;

      hence thesis by INT_2:def 3;

    end;

    theorem :: EULER_1:2

    

     Th2: for k,n be Nat holds k <> 0 & k < n & n is prime implies (k,n) are_coprime

    proof

      let k,n be Nat;

      assume that

       A1: k <> 0 & k < n and

       A2: n is prime;

      

       A3: (k gcd n) divides n by NAT_D:def 5;

      per cases by A2, A3, INT_2:def 4;

        suppose (k gcd n) = 1;

        hence thesis by INT_2:def 3;

      end;

        suppose (k gcd n) = n;

        then n divides k by NAT_D:def 5;

        hence thesis by A1, NAT_D: 7;

      end;

    end;

    theorem :: EULER_1:3

    

     Th3: n is prime & k in { kk where kk be Element of NAT : (n,kk) are_coprime & kk >= 1 & kk <= n } iff n is prime & k in ( Segm n) & not k in { 0 }

    proof

      set X = { kk where kk be Element of NAT : (n,kk) are_coprime & kk >= 1 & kk <= n };

      thus n is prime & k in X implies n is prime & k in ( Segm n) & not k in { 0 }

      proof

        assume that

         A1: n is prime and

         A2: k in X;

        

         A3: ex kk be Element of NAT st kk = k & (n,kk) are_coprime & kk >= 1 & kk <= n by A2;

        then k <> n by A1, Lm2, Th1;

        then k < n by A3, XXREAL_0: 1;

        hence thesis by A1, A3, NAT_1: 44, TARSKI:def 1;

      end;

      assume that

       A4: n is prime and

       A5: k in ( Segm n) and

       A6: not k in { 0 };

      

       A7: k <> 0 by A6, TARSKI:def 1;

      then

       A8: k >= 1 by NAT_1: 14;

      

       A9: k < n by A5, NAT_1: 44;

      then k in NAT & (k,n) are_coprime by A4, A7, Th2, ORDINAL1:def 12;

      hence thesis by A4, A9, A8;

    end;

    theorem :: EULER_1:4

    

     Th4: for A be finite set, x be set st x in A holds ( card (A \ {x})) = (( card A) - ( card {x})) by CARD_2: 44, ZFMISC_1: 31;

    theorem :: EULER_1:5

    

     Th5: (a gcd b) = 1 implies for c holds ((a * c) gcd (b * c)) = c

    proof

      assume

       A1: (a gcd b) = 1;

      let m;

      reconsider a9 = a, b9 = b as Integer;

      (a9,b9) are_coprime by A1, INT_2:def 3;

      

      hence ((a * m) gcd (b * m)) = |. |.m.|.| by INT_2: 24

      .= m by ABSVALUE:def 1;

    end;

    theorem :: EULER_1:6

    

     Th6: a <> 0 & c <> 0 & ((a * c) gcd (b * c)) = c implies (a,b) are_coprime

    proof

      assume that

       A1: a <> 0 and

       A2: c <> 0 and

       A3: ((a * c) gcd (b * c)) = c;

      (a * c) <> ( 0 * c) by A1, A2, XCMPLX_1: 5;

      then

      consider a1,b1 be Integer such that

       A4: (a * c) = (((a * c) gcd (b * c)) * a1) and

       A5: (b * c) = (((a * c) gcd (b * c)) * b1) & (a1,b1) are_coprime by INT_2: 23;

      a = a1 by A2, A3, A4, XCMPLX_1: 5;

      hence thesis by A2, A3, A5, XCMPLX_1: 5;

    end;

    theorem :: EULER_1:7

    

     Th7: (a gcd b) = 1 implies ((a + b) gcd b) = 1

    proof

      assume

       A1: (a gcd b) = 1;

      set n = ((a + b) gcd b);

      

       A2: n divides b by NAT_D:def 5;

      n divides (a + b) by NAT_D:def 5;

      then n divides a by A2, NAT_D: 10;

      then n divides (a gcd b) by A2, NEWTON: 50;

      then

       A3: n <= (1 + 0 ) by A1, NAT_D: 7;

      per cases by A3, NAT_1: 9;

        suppose n = 1;

        hence thesis;

      end;

        suppose n = 0 ;

        then b = 0 by INT_2: 5;

        hence thesis by A1;

      end;

    end;

    theorem :: EULER_1:8

    

     Th8: for a,b,c be Nat holds ((a + (b * c)) gcd b) = (a gcd b)

    proof

      let a,b,c be Nat;

      defpred P[ Nat] means ((a + (b * $1)) gcd b) = (a gcd b);

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let kk be Nat;

        assume

         A2: ((a + (b * kk)) gcd b) = (a gcd b);

        now

          per cases ;

            suppose b = 0 ;

            hence ((a + (b * (kk + 1))) gcd b) = (a gcd b);

          end;

            suppose

             A3: b > 0 ;

            set T = (a gcd b);

            

             A4: (a gcd b) > 0 by A3, NEWTON: 58;

            

             A5: (a gcd b) divides (a + (b * kk)) by A2, NAT_D:def 5;

            then

             A6: (a + (b * kk)) = ((a gcd b) * ((a + (b * kk)) div (a gcd b))) by NAT_D: 3;

            now

              per cases ;

                suppose

                 A7: (a + (b * kk)) = 0 ;

                

                then (a gcd b) = ( 0 gcd b) by NAT_1: 7

                .= b by NEWTON: 52;

                hence ((a + (b * (kk + 1))) gcd b) = (a gcd b) by A7, NAT_D: 32;

              end;

                suppose

                 A8: (a + (b * kk)) > 0 ;

                set T2 = (b div (a gcd b));

                set T1 = ((a + (b * kk)) div (a gcd b));

                

                 A9: ((a + (b * kk)) div (a gcd b)) <> 0 by A6, A8;

                (a gcd b) divides b by NAT_D:def 5;

                then

                 A10: b = ((a gcd b) * (b div (a gcd b))) by NAT_D: 3;

                then ((T1 * T) gcd (T2 * T)) = T by A2, A5, NAT_D: 3;

                then (T1,T2) are_coprime by A4, A9, Th6;

                then (T1 gcd T2) = 1 by INT_2:def 3;

                then

                 A11: ((T1 + T2) gcd T2) = 1 by Th7;

                ((a + (b * (kk + 1))) gcd b) = (((a + (b * kk)) + b) gcd b)

                .= (((T * T1) + (T * T2)) gcd (T * T2)) by A5, A10, NAT_D: 3

                .= ((T * (T1 + T2)) gcd (T * T2))

                .= (a gcd b) by A11, Th5;

                hence ((a + (b * (kk + 1))) gcd b) = (a gcd b);

              end;

            end;

            hence ((a + (b * (kk + 1))) gcd b) = (a gcd b);

          end;

        end;

        hence thesis;

      end;

      

       A12: P[ 0 ];

      for c be Nat holds P[c] from NAT_1:sch 2( A12, A1);

      hence thesis;

    end;

    theorem :: EULER_1:9

    

     Th9: (m,n) are_coprime implies ex k st (ex i0,j0 be Integer st k = ((i0 * m) + (j0 * n)) & k > 0 ) & for l st (ex i,j be Integer st l = ((i * m) + (j * n)) & l > 0 ) holds k <= l

    proof

      defpred P[ Nat] means ex i0,j0 be Integer st $1 = ((i0 * m) + (j0 * n)) & $1 > 0 ;

      assume

       A1: (m,n) are_coprime ;

      m > 0 or n > 0

      proof

        assume ( not m > 0 ) & not n > 0 ;

        then m = 0 & n = 0 ;

        then (m gcd n) <> 1 by NAT_D: 32;

        hence contradiction by A1, INT_2:def 3;

      end;

      then ((1 * m) + (1 * n)) > 0 ;

      then

       A2: ex k be Nat st P[k];

      consider k be Nat such that

       A3: P[k] and

       A4: for l be Nat st P[l] holds k <= l from NAT_1:sch 5( A2);

      take k;

      thus ex i0,j0 be Integer st k = ((i0 * m) + (j0 * n)) & k > 0 by A3;

      let l;

      thus thesis by A4;

    end;

    theorem :: EULER_1:10

    

     Th10: (m,n) are_coprime implies for k holds ex i, j st ((i * m) + (j * n)) = k

    proof

      reconsider a9 = 1, 09 = 0 as Integer;

      assume

       A1: (m,n) are_coprime ;

      then

      consider a such that

       A2: ex i0,j0 be Integer st a = ((i0 * m) + (j0 * n)) & a > 0 and

       A3: for c st (ex i, j st c = ((i * m) + (j * n)) & c > 0 ) holds a <= c by Th9;

      let k;

      consider i0,j0 be Integer such that

       A4: a = ((i0 * m) + (j0 * n)) and

       A5: a > 0 by A2;

      

       A6: for c st (ex i, j st c = ((i * m) + (j * n)) & c > 0 ) holds (c mod a) = 0

      proof

        let b;

        assume ex i, j st b = ((i * m) + (j * n)) & b > 0 ;

        then

        consider i, j such that

         A7: b = ((i * m) + (j * n)) and b > 0 ;

        set t2 = (j - ((b div a) * j0));

        set t1 = (i - ((b div a) * i0));

        

         A8: (((b mod a) + (a * (b div a))) - (a * (b div a))) = (b - (a * (b div a))) by A5, NAT_D: 2;

        then

        reconsider c = ((t1 * m) + (t2 * n)) as Element of NAT by A4, A7;

        assume

         A9: (b mod a) <> 0 ;

        c < a by A4, A5, A7, A8, NAT_D: 1;

        hence contradiction by A3, A4, A9, A7, A8;

      end;

      

       A10: a divides n

      proof

        per cases ;

          suppose n = 0 ;

          hence thesis by NAT_D: 6;

        end;

          suppose n > 0 ;

          then ((09 * m) + (a9 * n)) > 0 ;

          then (n mod a) = 0 by A6;

          then n = ((a * (n div a)) + 0 ) by A2, NAT_D: 2;

          hence thesis by NAT_D: 3;

        end;

      end;

      a divides m

      proof

        per cases ;

          suppose m = 0 ;

          hence thesis by NAT_D: 6;

        end;

          suppose m > 0 ;

          then ((a9 * m) + (09 * n)) > 0 ;

          then (m mod a) = 0 by A6;

          then m = ((a * (m div a)) + 0 ) by A2, NAT_D: 2;

          hence thesis by NAT_D: 3;

        end;

      end;

      then a divides (m gcd n) by A10, NAT_D:def 5;

      then a divides 1 by A1, INT_2:def 3;

      then ex b be Nat st 1 = (a * b) by NAT_D:def 3;

      then ((i0 * m) + (j0 * n)) = 1 by A4, NAT_1: 15;

      

      then k = (k * ((i0 * m) + (j0 * n)))

      .= (((k * i0) * m) + (k * (j0 * n)));

      then k = (((k * i0) * m) + ((k * j0) * n));

      hence thesis;

    end;

    theorem :: EULER_1:11

    

     Th11: for A be set, B be non empty set, f be Function of A, B st f is bijective holds ( card A) = ( card B)

    proof

      let A be set, B be non empty set, f be Function of A, B;

      assume f is bijective;

      then

       A1: f is one-to-one onto;

      

       A2: A = ( dom f) by FUNCT_2:def 1;

      B c= ( rng f) by A1;

      then

       A3: ( card B) c= ( card A) by A2, CARD_1: 12;

      ( card A) c= ( card B) by A2, A1, CARD_1: 10;

      hence thesis by A3;

    end;

    theorem :: EULER_1:12

    

     Th12: for i,k,n be Integer holds ((i + (k * n)) mod n) = (i mod n)

    proof

      let i,k,n be Integer;

      per cases ;

        suppose

         A1: n <> 0 ;

        

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

      end;

        suppose n = 0 ;

        hence thesis;

      end;

    end;

    theorem :: EULER_1:13

    

     Th13: c divides (a * b) & (a,c) are_coprime implies c divides b

    proof

      assume that

       A1: c divides (a * b) and

       A2: (a,c) are_coprime ;

      

       A3: c divides (c * b) by NAT_D: 9;

      (a gcd c) = 1 by A2, INT_2:def 3;

      then ((a * b) gcd (c * b)) = b by Th5;

      hence thesis by A1, A3, NEWTON: 50;

    end;

    theorem :: EULER_1:14

    

     Th14: a <> 0 & c <> 0 & (a,c) are_coprime & (b,c) are_coprime implies ((a * b),c) are_coprime

    proof

      assume that

       A1: a <> 0 and

       A2: c <> 0 and

       A3: (a,c) are_coprime and

       A4: (b,c) are_coprime ;

      

       A5: (a gcd c) = 1 by A3, INT_2:def 3;

      

       A6: ((a * b) gcd c) divides c by NAT_D:def 5;

      (((a * b) gcd c) gcd a) divides ((a * b) gcd c) by NAT_D:def 5;

      then (((a * b) gcd c) gcd a) divides a & (((a * b) gcd c) gcd a) divides c by A6, NAT_D: 4, 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_coprime by INT_2:def 3, NAT_D:def 5;

      then

       A8: ((a * b) gcd c) divides b by Th13;

      (b gcd c) = 1 by A4, INT_2:def 3;

      then ((a * b) gcd c) divides 1 by A6, A8, NEWTON: 50;

      then

       A9: ((a * b) gcd c) <= ( 0 + 1) by NAT_D: 7;

      ((a * b) gcd c) > 0 by A2, NEWTON: 58;

      then ((a * b) gcd c) = 1 by A9, NAT_1: 9;

      hence thesis by INT_2:def 3;

    end;

    theorem :: EULER_1:15

    

     Th15: x <> 0 & i >= 0 implies ((i * x) gcd (i * y)) = (i * (x gcd y))

    proof

      assume that

       A1: x <> 0 and

       A2: i >= 0 ;

      consider a2,b2 be Integer such that

       A3: x = ((x gcd y) * a2) & y = ((x gcd y) * b2) and

       A4: (a2,b2) are_coprime by A1, INT_2: 23;

      (i * x) = ((i * (x gcd y)) * a2) & (i * y) = ((i * (x gcd y)) * b2) by A3;

      

      then

       A5: ((i * x) gcd (i * y)) = |.(i * (x gcd y)).| by A4, INT_2: 24

      .= ( |.i.| * |.(x gcd y).|) by COMPLEX1: 65;

      i = |.i.| by A2, ABSVALUE:def 1;

      hence thesis by A5, ABSVALUE:def 1;

    end;

    theorem :: EULER_1:16

    

     Th16: for x st a <> 0 holds ((a + (x * b)) gcd b) = (a gcd b)

    proof

      let xx be Integer;

      set i = (a gcd b);

      

       A1: b = |.b.| by ABSVALUE:def 1;

      assume

       A2: a <> 0 ;

      

       A3: for m be Nat st m divides |.(a + (xx * b)).| & m divides |.b.| holds m divides i

      proof

        let mm be Nat;

        assume that

         A4: mm divides |.(a + (xx * b)).| and

         A5: mm divides |.b.|;

        consider n be Nat such that

         A6: b = (mm * n) by A1, A5, NAT_D:def 3;

        reconsider mm as Element of NAT by ORDINAL1:def 12;

        now

          per cases ;

            suppose (a + (xx * b)) >= 0 ;

            then |.(a + (xx * b)).| = (a + (xx * b)) by ABSVALUE:def 1;

            then

            consider t be Integer such that

             A7: (a + (xx * b)) = (mm * t) by A4, INT_1:def 3;

            

             A8: a = ((mm * t) - (mm * (xx * n))) by A6, A7, XCMPLX_1: 26

            .= (mm * (t - (xx * n)));

            then (t - (xx * n)) >= 0 by A2;

            then

            reconsider tt = (t - (xx * n)) as Element of NAT by INT_1: 3;

            a = (mm * tt) by A8;

            hence mm divides a by NAT_D:def 3;

          end;

            suppose (a + (xx * b)) < 0 ;

            then |.(a + (xx * b)).| = ( - (a + (xx * b))) by ABSVALUE:def 1;

            then

            consider t be Integer such that

             A9: ( - (a + (xx * b))) = (mm * t) by A4, INT_1:def 3;

            

             A10: a = (( - (mm * t)) - (mm * (xx * n))) by A6, A9, XCMPLX_1: 26

            .= (mm * (( - t) - (xx * n)));

            then (( - t) - (xx * n)) >= 0 by A2;

            then

            reconsider tt = (( - t) - (xx * n)) as Element of NAT by INT_1: 3;

            a = (mm * tt) by A10;

            hence mm divides a by NAT_D:def 3;

          end;

        end;

        hence thesis by A1, A5, NEWTON: 50;

      end;

      i divides a by NAT_D:def 5;

      then

       A11: a = (i * (a div i)) by NAT_D: 3;

      

       A12: i divides b by NAT_D:def 5;

      then

       A13: b = (i * (b div i)) by NAT_D: 3;

      i divides |.(a + (xx * b)).|

      proof

        per cases ;

          suppose (a + (xx * b)) < 0 ;

          then

           A14: |.(a + (xx * b)).| = ( - (a + (xx * b))) by ABSVALUE:def 1;

          ( - (a + (xx * b))) = (i * ( - ((a div i) + (xx * (b div i))))) by A11, A13;

          hence thesis by A14, INT_1:def 3;

        end;

          suppose (a + (xx * b)) >= 0 ;

          then

           A15: |.(a + (xx * b)).| = (a + (xx * b)) by ABSVALUE:def 1;

          (a + (xx * b)) = (i * ((a div i) + (xx * (b div i)))) by A11, A13;

          hence thesis by A15, INT_1:def 3;

        end;

      end;

      then ( |.(a + (xx * b)).| gcd |.b.|) = i by A1, A12, A3, NAT_D:def 5;

      hence thesis by INT_2: 34;

    end;

    begin

    definition

      let n be Nat;

      :: EULER_1:def1

      func Euler n -> Element of NAT equals ( card { k where k be Element of NAT : (n,k) are_coprime & k >= 1 & k <= n });

      coherence

      proof

        set X = { k where k be Element of NAT : (n,k) are_coprime & k >= 1 & k <= n };

        X c= ( Seg n)

        proof

          let x be object;

          assume x in X;

          then ex k be Element of NAT st k = x & (n,k) are_coprime & k >= 1 & k <= n;

          hence thesis by FINSEQ_1: 1;

        end;

        then

        reconsider X as finite set;

        ( card X) is Element of NAT ;

        hence thesis;

      end;

    end

    set X = { k where k be Element of NAT : (1,k) are_coprime & k >= 1 & k <= 1 };

    for x be object holds x in X iff x = 1

    proof

      let x be object;

      thus x in X implies x = 1

      proof

        assume x in X;

        then ex k be Element of NAT st k = x & (1,k) are_coprime & k >= 1 & k <= 1;

        hence thesis by XXREAL_0: 1;

      end;

      (1 gcd 1) = 1 by NAT_D: 32;

      then (1,1) are_coprime by INT_2:def 3;

      hence thesis;

    end;

    then

     Lm3: ( card {1}) = ( Euler 1) by TARSKI:def 1;

    theorem :: EULER_1:17

    ( Euler 1) = 1 by Lm3, CARD_1: 30;

    set X = { k where k be Element of NAT : (2,k) are_coprime & k >= 1 & k <= 2 };

    for x be object holds x in X iff x = 1

    proof

      let x be object;

      thus x in X implies x = 1

      proof

        assume x in X;

        then

        consider k be Element of NAT such that

         A1: k = x & (2,k) are_coprime and

         A2: k >= 1 & k <= 2;

        

         A3: (2 gcd 2) = 2 by NAT_D: 32;

        k = 0 or ... or k = 2 by A2;

        hence thesis by A1, A2, A3, INT_2:def 3;

      end;

      (2 gcd 1) = 1 by NEWTON: 51;

      then (2,1) are_coprime by INT_2:def 3;

      hence thesis;

    end;

    then

     Lm4: ( card {1}) = ( Euler 2) by TARSKI:def 1;

    theorem :: EULER_1:18

    ( Euler 2) = 1 by Lm4, CARD_1: 30;

    theorem :: EULER_1:19

    

     Th19: n > 1 implies ( Euler n) <= (n - 1)

    proof

      set X = { kk where kk be Element of NAT : (n,kk) are_coprime & kk >= 1 & kk <= n };

      X c= ( Seg n)

      proof

        let x be object;

        assume x in X;

        then ex k be Element of NAT st k = x & (n,k) are_coprime & k >= 1 & k <= n;

        hence thesis by FINSEQ_1: 1;

      end;

      then

      reconsider X as finite set;

      assume

       A1: n > 1;

      then 0 in { l where l be Nat : l < n };

      then 0 in n by AXIOMS: 4;

      then

       A2: ( card (n \ { 0 })) = (( card n) - ( card { 0 })) by Th4;

      

       A3: X c= (n \ { 0 })

      proof

        let x be object;

        assume x in X;

        then

        consider k be Element of NAT such that

         A4: k = x and

         A5: (n,k) are_coprime and

         A6: k >= 1 and

         A7: k <= n;

         not (n,n) are_coprime by A1, Th1;

        then k < n by A5, A7, XXREAL_0: 1;

        then k in { l where l be Nat : l < n };

        then

         A8: k in n by AXIOMS: 4;

         not k in { 0 } by A6, TARSKI:def 1;

        hence thesis by A4, A8, XBOOLE_0:def 5;

      end;

      ( card n) = n & ( card { 0 }) = 1 by CARD_1: 30;

      hence thesis by A3, A2, NAT_1: 43;

    end;

    theorem :: EULER_1:20

    n is prime implies ( Euler n) = (n - 1)

    proof

      set X = { kk where kk be Element of NAT : (n,kk) are_coprime & kk >= 1 & kk <= n };

      X c= ( Seg n)

      proof

        let x be object;

        assume x in X;

        then ex k be Element of NAT st k = x & (n,k) are_coprime & k >= 1 & k <= n;

        hence thesis by FINSEQ_1: 1;

      end;

      then

      reconsider X as finite set;

      assume

       A1: n is prime;

      n <> 0

      proof

        assume n = 0 ;

        then n in ( SetPrimenumber 2) by A1, NEWTON:def 7;

        hence contradiction;

      end;

      then 0 in { l where l be Nat : l < n };

      then

       A2: 0 in n by AXIOMS: 4;

      (( Segm n) \ { 0 }) c= X

      proof

        let x be object;

        assume

         A3: x in (( Segm n) \ { 0 });

        then

         A4: x in ( Segm n) by XBOOLE_0:def 5;

         not x in { 0 } by A3, XBOOLE_0:def 5;

        hence thesis by A1, Th3, A4;

      end;

      then

       A5: ( card (n \ { 0 })) <= ( card X) by NAT_1: 43;

      

       A6: ( Euler n) <= (n - 1) by A1, Th19, INT_2:def 4;

      ( card n) = n & ( card { 0 }) = 1 by CARD_1: 30;

      then (n - 1) <= ( Euler n) by A5, A2, Th4;

      hence thesis by A6, XXREAL_0: 1;

    end;

    theorem :: EULER_1:21

    m > 1 & n > 1 & (m,n) are_coprime implies ( Euler (m * n)) = (( Euler m) * ( Euler n))

    proof

      assume that

       A1: m > 1 and

       A2: n > 1 and

       A3: (m,n) are_coprime ;

      set X = { i where i be Element of NAT : ((m * n),i) are_coprime & i >= 1 & i <= (m * n) };

      set C = { i where i be Element of NAT : ex x,y be Integer st i = (((m * y) + (n * x)) mod (m * n)) & ((m * n),i) are_coprime & y <= n & x <= m & i >= 0 };

      

       A4: (m * n) <> 0 by A1, A2, XCMPLX_1: 6;

      

       A5: C c= (( Seg (m * n)) \/ { 0 })

      proof

        let z be object;

        assume z in C;

        then

        consider i be Element of NAT such that

         A6: i = z and

         A7: ex x,y be Integer st i = (((m * y) + (n * x)) mod (m * n)) & ((m * n),i) are_coprime & y <= n & x <= m & i >= 0 ;

        consider x,y be Integer such that

         A8: i = (((m * y) + (n * x)) mod (m * n)) and ((m * n),i) are_coprime and y <= n and x <= m and i >= 0 by A7;

        per cases ;

          suppose

           A9: i > 0 ;

          

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

          proof

            set i2 = (m * n);

            set i1 = ((m * y) + (n * x));

            

             A11: ( [\(i1 / i2)/] + 1) >= (i1 / i2) by INT_1: 29;

            (((m * y) + (n * x)) mod (m * n)) = (i1 - ((i1 div i2) * i2)) by A4, INT_1:def 10

            .= (i1 - ( [\(i1 / i2)/] * i2)) by INT_1:def 9;

            hence thesis by A1, A2, A11, Lm1, XCMPLX_1: 6;

          end;

          i >= 1 by A9, NAT_1: 14;

          then z in ( Seg (m * n)) by A6, A8, A10, FINSEQ_1: 1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A12: i = 0 ;

           0 in { 0 } by TARSKI:def 1;

          hence thesis by A6, A12, XBOOLE_0:def 3;

        end;

      end;

      then

      reconsider C as finite set;

      set A = { i where i be Element of NAT : (n,i) are_coprime & i >= 1 & i <= n };

      

       A13: A c= ( Seg n)

      proof

        let x be object;

        assume x in A;

        then ex i be Element of NAT st i = x & (n,i) are_coprime & i >= 1 & i <= n;

        hence thesis by FINSEQ_1: 1;

      end;

      

       A14: y = 1 & x = 1 implies (((m * y) + (n * x)) mod (m * n)) in C

      proof

        

         A15: (m gcd n) = 1 by A3, INT_2:def 3;

        then ((m + n) gcd m) = 1 by Th7;

        then

         A16: (m,(m + n)) are_coprime by INT_2:def 3;

        ((m + n) gcd n) = 1 by A15, Th7;

        then (n,(m + n)) are_coprime by INT_2:def 3;

        then ((m * n),(m + n)) are_coprime by A1, A16, Th14;

        then

         A17: ((m * n) gcd (m + n)) = 1 by INT_2:def 3;

        assume

         A18: y = 1 & x = 1;

        then

        reconsider y9 = y, x9 = x as Element of NAT ;

        (((m * y9) + (n * x9)) mod (m * n)) = (((m * y) + (n * x)) mod (m * n));

        then

        consider t be Element of NAT such that

         A19: t = (((m * y) + (n * x)) mod (m * n));

        ex d be Nat st (m + n) = (((m * n) * d) + ((m + n) mod (m * n))) & ((m + n) mod (m * n)) < (m * n) by A4, NAT_D:def 2;

        then (((m + n) mod (m * n)) gcd (m * n)) = 1 by A17, Th8;

        then ((m * n),t) are_coprime by A18, A19, INT_2:def 3;

        hence thesis by A1, A2, A18, A19;

      end;

      reconsider A as finite set by A13;

      

       A20: a = 1 implies a in A

      proof

        assume

         A21: a = 1;

        then (n gcd a) = 1 by NEWTON: 51;

        then (n,a) are_coprime by INT_2:def 3;

        hence thesis by A2, A21;

      end;

      set B = { i where i be Element of NAT : (m,i) are_coprime & i >= 1 & i <= m };

      

       A22: B c= ( Seg m)

      proof

        let x be object;

        assume x in B;

        then ex i be Element of NAT st i = x & (m,i) are_coprime & i >= 1 & i <= m;

        hence thesis by FINSEQ_1: 1;

      end;

      

       A23: (m * n) <> 1 by A1, NAT_1: 15;

      

       A24: C = X

      proof

        thus C c= X

        proof

          let z be object;

          assume z in C;

          then

          consider i be Element of NAT such that

           A25: i = z and

           A26: ex x,y be Integer st i = (((m * y) + (n * x)) mod (m * n)) & ((m * n),i) are_coprime & y <= n & x <= m & i >= 0 ;

          consider x,y be Integer such that

           A27: i = (((m * y) + (n * x)) mod (m * n)) and

           A28: ((m * n),i) are_coprime and y <= n and x <= m and i >= 0 by A26;

          

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

          proof

            set i2 = (m * n);

            set i1 = ((m * y) + (n * x));

            

             A30: ( [\(i1 / i2)/] + 1) >= (i1 / i2) by INT_1: 29;

            (((m * y) + (n * x)) mod (m * n)) = (i1 - ((i1 div i2) * i2)) by A4, INT_1:def 10

            .= (i1 - ( [\(i1 / i2)/] * i2)) by INT_1:def 9;

            hence thesis by A1, A2, A30, Lm1, XCMPLX_1: 6;

          end;

          per cases ;

            suppose i > 0 ;

            then i >= 1 by NAT_1: 14;

            hence thesis by A25, A27, A28, A29;

          end;

            suppose i = 0 ;

            then ((m * n) gcd 0 ) = 1 by A28, INT_2:def 3;

            hence thesis by A23, NEWTON: 52;

          end;

        end;

        let z be object;

        assume z in X;

        then

        consider i be Element of NAT such that

         A31: i = z and

         A32: ((m * n),i) are_coprime and i >= 1 and

         A33: i <= (m * n);

        i <> (m * n)

        proof

          assume i = (m * n);

          then ((m * n) gcd (m * n)) = 1 by A32, INT_2:def 3;

          then (m * n) = 1 by NAT_D: 32;

          hence contradiction by A1, NAT_1: 15;

        end;

        then

         A34: i < (m * n) by A33, XXREAL_0: 1;

        consider y0,x0 be 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 be Integer such that

         A37: x1 = (x0 mod m) and

         A38: y1 = (y0 mod n);

        (x0 mod m) = (x0 - ((x0 div m) * m)) & (y0 mod n) = (y0 - ((y0 div n) * n)) by A1, A2, INT_1:def 10;

        then ((m * y0) + (n * x0)) = (((m * y1) + (n * x1)) + ((m * n) * (k + j))) by A37, A38;

        then

         A39: ((m * y0) + (n * x0)) = (((m * y1) + (n * x1)) mod (m * n)) by A36, 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 thesis by A31, A32, A35, A42, A39;

      end;

      reconsider B as finite set by A22;

      

       A43: b = 1 implies b in B

      proof

        assume

         A44: b = 1;

        then (m gcd b) = 1 by NEWTON: 51;

        then (m,b) are_coprime by INT_2:def 3;

        hence thesis by A1, A44;

      end;

       { 0 } c= NAT by ZFMISC_1: 31;

      then (( Seg (m * n)) \/ { 0 }) c= NAT by XBOOLE_1: 8;

      then

      reconsider A, B, C as non empty finite Subset of NAT by A13, A22, A5, A20, A43, A14, XBOOLE_1: 1;

      deffunc F( Element of A, Element of B) = (((m * $1) + (n * $2)) mod (m * n));

      

       A45: for y be Element of A, x be Element of B holds F(y,x) in C

      proof

        set l = (n * m);

        let y be Element of A, x be Element of B;

        y in A;

        then

        consider i be Element of NAT such that

         A46: i = y and

         A47: (n,i) are_coprime and

         A48: i >= 1 and

         A49: i <= n;

        x in B;

        then

        consider j be Element of NAT such that

         A50: j = x and

         A51: (m,j) are_coprime and j >= 1 and

         A52: j <= m;

        ((i * m),n) are_coprime by A1, A2, A3, A47, Th14;

        then ((i * m) gcd n) = 1 by INT_2:def 3;

        then (((m * i) + (n * j)) gcd n) = 1 by Th8;

        then

         A53: (n,((m * i) + (n * j))) are_coprime by INT_2:def 3;

        ((j * n),m) are_coprime by A1, A2, A3, A51, Th14;

        then ((j * n) gcd m) = 1 by INT_2:def 3;

        then (((m * i) + (n * j)) gcd m) = 1 by Th8;

        then

         A54: (m,((m * i) + (n * j))) are_coprime by INT_2:def 3;

        (i * m) <> ( 0 * m) by A1, A48, XCMPLX_1: 5;

        then ((n * m),((m * i) + (n * j))) are_coprime by A1, A53, A54, Th14;

        then

         A55: ((n * m) gcd ((m * i) + (n * j))) = 1 by INT_2:def 3;

        reconsider ii = i, jj = j as Integer;

        (((m * ii) + (n * jj)) mod (m * n)) = (((m * i) + (n * j)) mod (m * n));

        then

        consider q be Element of NAT such that

         A56: q = (((m * ii) + (n * jj)) mod (m * n));

        ex t be Nat st ((m * i) + (n * j)) = (((n * m) * t) + (((m * i) + (n * j)) mod (n * m))) & (((m * i) + (n * j)) mod (n * m)) < (n * m) by A4, NAT_D:def 2;

        then ((((m * i) + (n * j)) mod l) gcd l) = 1 by A55, Th8;

        then (l,q) are_coprime by A56, INT_2:def 3;

        hence thesis by A46, A49, A50, A52, A56;

      end;

      consider f be Function of [:A, B:], C such that

       A57: for y be Element of A, x be Element of B holds (f . (y,x)) = F(y,x) from FUNCT_7:sch 1( A45);

      

       A58: f is onto

      proof

        thus ( rng f) c= C by RELAT_1:def 19;

        let z be object;

        assume z in C;

        then

        consider i be Element of NAT such that

         A59: i = z and

         A60: ex x0,y0 be Integer st i = (((m * y0) + (n * x0)) mod (m * n)) & ((m * n),i) are_coprime & y0 <= n & x0 <= m & i >= 0 ;

        consider x0,y0 be Integer such that

         A61: i = (((m * y0) + (n * x0)) mod (m * n)) and

         A62: ((m * n),i) are_coprime and y0 <= n and x0 <= m and i >= 0 by A60;

        consider x,y be Integer such that

         A63: x = (x0 mod m) and

         A64: y = (y0 mod n);

        

         A65: x <= m by A1, A63, NEWTON: 65;

        

         A66: (((m * y) + (n * x)) mod (m * n)) = (((m * y0) + (n * x0)) mod (m * n))

        proof

          set k = (y0 div n);

          set j = (x0 div m);

          (x0 mod m) = (x0 - ((x0 div m) * m)) & (y0 mod n) = (y0 - ((y0 div n) * n)) by A1, A2, INT_1:def 10;

          then ((m * y0) + (n * x0)) = (((m * y) + (n * x)) + ((m * n) * (k + j))) by A63, A64;

          hence thesis by Th12;

        end;

        

         A67: y <= n by A2, A64, NEWTON: 65;

        reconsider x, 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 * j)) - (n * ((m * (y0 + (n * j))) div (m * n))));

          assume x = 0 ;

          then (x0 - ((x0 div m) * m)) = 0 by A1, A63, INT_1:def 10;

          

          then

           A69: (((m * y0) + (n * x0)) mod (m * n)) = ((m * (y0 + (n * j))) - (((m * (y0 + (n * j))) div (m * n)) * (m * n))) by A4, INT_1:def 10

          .= (m * ((y0 + (n * j)) - (n * ((m * (y0 + (n * j))) div (m * n)))));

          then

          reconsider g = (m * jj) as Element of NAT by A61;

          

           A70: ((m * n) gcd (m * jj)) = 1 by A61, A62, A69, INT_2:def 3;

          

           A71: g > 0 or g = 0 ;

           not jj < 0

          proof

            assume jj < 0 ;

            then (m * jj) < ( 0 * jj) by A1, XREAL_1: 69;

            hence contradiction by A71;

          end;

          then

          reconsider jj as Element of NAT by INT_1: 3;

          (m * (n gcd jj)) = 1 by A2, A70, Th15;

          then jj = 0 by A1, NAT_1: 15;

          then ((m * n) gcd 0 ) = 1 by A61, A62, A69, INT_2:def 3;

          hence contradiction by A23, NEWTON: 52;

        end;

        

         A72: y <> 0

        proof

          set j = (y0 div n);

          set jj = (((m * j) + x0) - (m * ((n * ((m * j) + x0)) div (m * n))));

          assume y = 0 ;

          then (y0 - ((y0 div n) * n)) = 0 by A2, A64, INT_1:def 10;

          

          then

           A73: (((m * y0) + (n * x0)) mod (m * n)) = ((n * ((m * j) + x0)) - (((n * ((m * j) + x0)) div (m * n)) * (m * n))) by A4, INT_1:def 10

          .= (n * (((m * j) + x0) - (m * ((n * ((m * j) + x0)) div (m * n)))));

          then

          reconsider g = (n * jj) as Element of NAT by A61;

          

           A74: ((m * n) gcd (n * jj)) = 1 by A61, A62, A73, INT_2:def 3;

          

           A75: g > 0 or g = 0 ;

           not jj < 0

          proof

            assume jj < 0 ;

            then (n * jj) < ( 0 * jj) by A2, XREAL_1: 69;

            hence contradiction by A75;

          end;

          then

          reconsider jj as Element of NAT by INT_1: 3;

          (n * (m gcd jj)) = 1 by A1, A74, Th15;

          then jj = 0 by A2, NAT_1: 15;

          then ((m * n) gcd 0 ) = 1 by A61, A62, A73, INT_2:def 3;

          hence contradiction by A23, NEWTON: 52;

        end;

        

         A76: (m,x0) are_coprime

        proof

          set p = (m gcd x0);

          p divides m by INT_2: 21;

          then

          consider i1 be Integer such that

           A77: m = (p * i1) by INT_1:def 3;

          p divides x0 by INT_2: 21;

          then

          consider i2 be Integer such that

           A78: x0 = (p * i2) by INT_1:def 3;

          set jj = (i1 * n);

          set k = ((((p * i1) * y0) + (n * (p * i2))) div ((p * i1) * n));

          set j = (((i1 * y0) + (n * i2)) - ((i1 * k) * n));

          

           A79: p <> 0 by A1, A77;

          

           A80: (((m * y0) + (n * x0)) mod (m * n)) = ((((p * i1) * y0) + (n * (p * i2))) - (((((p * i1) * y0) + (n * (p * i2))) div ((p * i1) * n)) * ((p * i1) * n))) by A4, A77, A78, INT_1:def 10;

          

           A81: ((((p * i1) * y0) + (n * (p * i2))) - (k * ((p * i1) * n))) = (p * (((i1 * y0) + (n * i2)) - ((i1 * k) * n)));

           not j < 0

          proof

            assume j < 0 ;

            then (p * j) < ( 0 * j) by A79, XREAL_1: 69;

            hence contradiction by A4, A61, A77, A78, A81, INT_1:def 10;

          end;

          then

          reconsider p, j as Element of NAT by INT_1: 3;

           not jj < 0

          proof

            assume jj < 0 ;

            then (p * jj) < ( 0 * jj) by A79, XREAL_1: 69;

            hence contradiction by A4, A77;

          end;

          then

          reconsider jj as Element of NAT by INT_1: 3;

          

           A82: (m * n) = (p * (i1 * n)) by A77;

          now

            per cases by A1, A2, A82, XCMPLX_1: 6;

              suppose

               A83: p <> 0 & jj <> 0 & j <> 0 ;

              ((p * jj) gcd (p * j)) = 1 by A61, A62, A77, A80, INT_2:def 3;

              then (p * (jj gcd j)) = 1 by A83, Th15;

              hence p = 1 by NAT_1: 15;

            end;

              suppose p <> 0 & jj <> 0 & j = 0 ;

              then ((p * jj) gcd 0 ) = 1 by A61, A62, A77, A80, A81, INT_2:def 3;

              then (p * jj) = 1 by NEWTON: 52;

              hence p = 1 by NAT_1: 15;

            end;

          end;

          hence thesis by INT_2:def 3;

        end;

        (n,y0) are_coprime

        proof

          set p = (n gcd y0);

          p divides n by INT_2: 21;

          then

          consider i1 be Integer such that

           A84: n = (p * i1) by INT_1:def 3;

          p divides y0 by INT_2: 21;

          then

          consider i2 be Integer such that

           A85: y0 = (p * i2) by INT_1:def 3;

          set jj = (i1 * m);

          set k = (((m * (p * i2)) + ((p * i1) * x0)) div (m * (p * i1)));

          set j = (((m * i2) + (i1 * x0)) - ((i1 * k) * m));

          

           A86: p <> 0 by A2, A84;

          

           A87: (((m * y0) + (n * x0)) mod (m * n)) = (((m * (p * i2)) + ((p * i1) * x0)) - ((((m * (p * i2)) + ((p * i1) * x0)) div (m * (p * i1))) * (m * (p * i1)))) by A4, A84, A85, INT_1:def 10;

          

           A88: (((m * (p * i2)) + ((p * i1) * x0)) - (k * (m * (p * i1)))) = (p * (((m * i2) + (i1 * x0)) - ((i1 * k) * m)));

          j >= 0

          proof

            assume j < 0 ;

            then (p * j) < ( 0 * j) by A86, XREAL_1: 69;

            hence contradiction by A4, A61, A84, A85, A88, INT_1:def 10;

          end;

          then

          reconsider p, j as Element of NAT by INT_1: 3;

           not jj < 0

          proof

            assume jj < 0 ;

            then (p * jj) < ( 0 * jj) by A86, XREAL_1: 69;

            hence contradiction by A4, A84;

          end;

          then

          reconsider jj as Element of NAT by INT_1: 3;

          

           A89: (m * n) = (p * (i1 * m)) by A84;

          now

            per cases by A1, A2, A89, XCMPLX_1: 6;

              suppose

               A90: p <> 0 & jj <> 0 & j <> 0 ;

              ((p * jj) gcd (p * j)) = 1 by A61, A62, A84, A87, INT_2:def 3;

              then (p * (jj gcd j)) = 1 by A90, Th15;

              hence p = 1 by NAT_1: 15;

            end;

              suppose p <> 0 & jj <> 0 & j = 0 ;

              then ((p * jj) gcd 0 ) = 1 by A61, A62, A84, A87, A88, INT_2:def 3;

              then (p * jj) = 1 by NEWTON: 52;

              hence p = 1 by NAT_1: 15;

            end;

          end;

          hence thesis by INT_2:def 3;

        end;

        then

         A91: (y0 gcd n) = 1 by INT_2:def 3;

        x = (x0 - ((x0 div m) * m)) by A1, A63, INT_1:def 10;

        then (x0 gcd m) = ((x + ((x0 div m) * m)) gcd m);

        then (x0 gcd m) = (x gcd m) by A68, Th16;

        then (m gcd x) = 1 by A76, INT_2:def 3;

        then

         A92: (m,x) are_coprime by INT_2:def 3;

        x >= ( 0 + 1) by A68, INT_1: 7;

        then

         A93: x in B by A65, A92;

        y = (y0 - ((y0 div n) * n)) by A2, A64, INT_1:def 10;

        then (y0 gcd n) = ((y + ((y0 div n) * n)) gcd n);

        then (y0 gcd n) = (y gcd n) by A72, Th16;

        then

         A94: (n,y) are_coprime by A91, INT_2:def 3;

        y >= ( 0 + 1) by A72, INT_1: 7;

        then y in A by A67, A94;

        then

        reconsider y as Element of A;

        reconsider x as Element of B by A93;

        

         A95: i = (f . (y,x)) by A57, A61, A66;

        consider w be set such that

         A96: w = [y, x];

        ( dom f) = [:A, B:] by FUNCT_2:def 1;

        then w in ( dom f) by A96, ZFMISC_1: 87;

        hence z in ( rng f) by A59, A96, A95, FUNCT_1:def 3;

      end;

      

       A97: (m * n) >= 1 by A1, A2, NAT_1: 14, XCMPLX_1: 6;

      f is one-to-one

      proof

        let x,y be object;

        

         A98: ( dom f) = [:A, B:] by FUNCT_2:def 1;

        assume x in ( dom f);

        then

        consider xx1 be Element of A, xx2 be Element of B such that

         A99: x = [xx1, xx2] by A98, DOMAIN_1: 1;

        assume y in ( dom f);

        then

        consider yy1 be Element of A, yy2 be Element of B such that

         A100: y = [yy1, yy2] by A98, DOMAIN_1: 1;

        xx1 in A;

        then

        consider x1 be Element of NAT such that

         A101: xx1 = x1 and (n,x1) are_coprime and

         A102: x1 >= 1 and

         A103: x1 <= n;

        xx2 in B;

        then

        consider x2 be Element of NAT such that

         A104: xx2 = x2 and (m,x2) are_coprime and

         A105: x2 >= 1 and

         A106: x2 <= m;

        consider p be Integer such that

         A107: p = m;

        assume

         A108: (f . x) = (f . y);

        yy2 in B;

        then

        consider y2 be Element of NAT such that

         A109: yy2 = y2 and (m,y2) are_coprime and

         A110: y2 >= 1 and

         A111: y2 <= m;

        yy1 in A;

        then

        consider y1 be Element of NAT such that

         A112: yy1 = y1 and (n,y1) are_coprime and

         A113: y1 >= 1 and

         A114: y1 <= n;

        

         A115: (((x1 * m) + (x2 * n)) mod (m * n)) = (f . (xx1,xx2)) by A57, A101, A104

        .= (f . (yy1,yy2)) by A99, A100, A108

        .= (((y1 * m) + (y2 * n)) mod (m * n)) by A57, A112, A109;

        reconsider y1, y2, x1, x2 as Element of NAT ;

        set k = (((x1 * m) + (x2 * n)) mod (m * n));

        

         A116: (((x1 * m) + (x2 * n)) - ((y1 * m) + (y2 * n))) = ((m * (x1 - y1)) + (n * (x2 - y2))) & ((k + ((((x1 * m) + (x2 * n)) div (m * n)) * (m * n))) - (k + ((((y1 * m) + (y2 * n)) div (m * n)) * (m * n)))) = ((m * n) * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n))));

        set w = ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)));

        ((y1 * m) + (y2 * n)) = (k + ((((y1 * m) + (y2 * n)) div (m * n)) * (m * n))) by A97, A115, NAT_D: 2;

        then

         A117: ((m * (x1 - y1)) + (n * (x2 - y2))) = ((m * n) * w) by A97, A116, NAT_D: 2;

        then (n * (x2 - y2)) = (m * ((n * w) - (x1 - y1)));

        then

         A118: p divides (n * (x2 - y2)) by A107, INT_1:def 3;

        consider p be Integer such that

         A119: p = n;

        (m * (x1 - y1)) = (n * ((m * w) - (x2 - y2))) by A117;

        then

         A120: p divides (m * (x1 - y1)) by A119, INT_1:def 3;

        then

         A121: n divides (x1 - y1) by A3, A119, INT_2: 25;

        

         A122: (x1 - y1) = 0

        proof

          per cases ;

            suppose

             A123: 0 <= (x1 - y1);

            consider k be Integer such that

             A124: k = (x1 - y1);

            reconsider k as Element of NAT by A123, A124, INT_1: 3;

            k = 0

            proof

              set b = (n + ( - 1));

              ( - y1) <= ( - 1) by A113, XREAL_1: 24;

              then

               A125: (x1 + ( - y1)) <= (n + ( - 1)) by A103, XREAL_1: 7;

              

               A126: k < (b + 1) by A124, A125, NAT_1: 13;

              assume k <> 0 ;

              hence contradiction by A3, A119, A120, A124, A126, INT_2: 25, NAT_D: 7;

            end;

            hence thesis by A124;

          end;

            suppose

             A127: (x1 - y1) <= 0 ;

            consider k be Integer such that

             A128: k = ( - (x1 - y1));

            

             A129: n divides k by A121, A128, INT_2: 10;

            reconsider k as Element of NAT by A127, A128, INT_1: 3;

            k = 0

            proof

              set b = (n + ( - 1));

              ( - x1) <= ( - 1) by A102, XREAL_1: 24;

              then

               A130: (( - x1) + y1) <= (n + ( - 1)) by A114, XREAL_1: 7;

              

               A131: k < (b + 1) by A128, A130, NAT_1: 13;

              assume k <> 0 ;

              hence contradiction by A129, A131, NAT_D: 7;

            end;

            hence thesis by A128;

          end;

        end;

        

         A132: m divides (x2 - y2) by A3, A107, A118, INT_2: 25;

        (x2 - y2) = 0

        proof

          per cases ;

            suppose

             A133: 0 <= (x2 - y2);

            consider k be Integer such that

             A134: k = (x2 - y2);

            reconsider k as Element of NAT by A133, A134, INT_1: 3;

            k = 0

            proof

              set b = (m + ( - 1));

              ( - y2) <= ( - 1) by A110, XREAL_1: 24;

              then

               A135: (x2 + ( - y2)) <= (m + ( - 1)) by A106, XREAL_1: 7;

              

               A136: k < (b + 1) by A134, A135, NAT_1: 13;

              assume k <> 0 ;

              hence contradiction by A3, A107, A118, A134, A136, INT_2: 25, NAT_D: 7;

            end;

            hence thesis by A134;

          end;

            suppose

             A137: (x2 - y2) <= 0 ;

            consider k be Integer such that

             A138: k = ( - (x2 - y2));

            

             A139: m divides k by A132, A138, INT_2: 10;

            reconsider k as Element of NAT by A137, A138, INT_1: 3;

            k = 0

            proof

              set b = (m + ( - 1));

              ( - x2) <= ( - 1) by A105, XREAL_1: 24;

              then

               A140: (( - x2) + y2) <= (m + ( - 1)) by A111, XREAL_1: 7;

              

               A141: k < (b + 1) by A138, A140, NAT_1: 13;

              assume k <> 0 ;

              hence contradiction by A139, A141, NAT_D: 7;

            end;

            hence thesis by A138;

          end;

        end;

        hence thesis by A99, A101, A104, A100, A112, A109, A122;

      end;

      then f is bijective by A58;

      then ( card [:A, B:]) = ( card C) by Th11;

      hence thesis by A24, CARD_2: 46;

    end;