int_1.miz



    begin

    reserve X for set,

x,y,z for object,

k,l,n for Nat,

r for Real;

    

     Lm1: z in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}) implies ex k st z = ( - k)

    proof

      

       A1: [: { 0 }, NAT :] c= [: { 0 }, REAL+ :] by ARYTM_2: 2, ZFMISC_1: 95;

      assume

       A2: z in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]});

      then

       A3: not z in { [ 0 , 0 ]} by XBOOLE_0:def 5;

      z in ( NAT \/ [: { 0 }, NAT :]) by A2, XBOOLE_0:def 3;

      then z in INT by A3, NUMBERS:def 4, XBOOLE_0:def 5;

      then

      reconsider z9 = z as Element of REAL by NUMBERS: 15;

      consider x,y be object such that x in { 0 } and

       A4: y in NAT and

       A5: z = [x, y] by A2, ZFMISC_1: 84;

      reconsider y as Element of REAL by A4, NUMBERS: 19;

      z in [: { 0 }, NAT :] by A2;

      then

      consider x9,y9 be Element of REAL+ such that

       A6: z9 = [ 0 , x9] and

       A7: y = y9 and

       A8: ( + (z9,y)) = (y9 - x9) by A4, A1, ARYTM_0:def 1, ARYTM_2: 2;

      x9 = y9 by A5, A6, A7, XTUPLE_0: 1;

      then

       A9: (y9 - x9) = 0 by ARYTM_1: 18;

      reconsider y as Element of NAT by A4;

      take y;

      consider x1,x2,y1,y2 be Element of REAL such that

       A10: z9 = [*x1, x2*] and

       A11: y = [*y1, y2*] and

       A12: (z9 + y) = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

      

       A13: x2 = 0 by A10, ARYTM_0: 24;

      then

       A14: ( + (x2,y2)) = 0 by A11, ARYTM_0: 11, ARYTM_0: 24;

      y2 = 0 by A11, ARYTM_0: 24;

      then

       A15: y = y1 by A11, ARYTM_0:def 5;

      z9 = x1 by A10, A13, ARYTM_0:def 5;

      then (z9 + y) = 0 by A12, A15, A8, A9, A14, ARYTM_0:def 5;

      hence thesis;

    end;

    

     Lm2: for k st x = ( - k) & k <> x holds x in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]})

    proof

      let k such that

       A1: x = ( - k) and

       A2: k <> x;

      reconsider r = x as Element of REAL by A1, XREAL_0:def 1;

      (r + k) = 0 by A1;

      then

      consider x1,x2,y1,y2 be Element of REAL such that

       A3: r = [*x1, x2*] and

       A4: k = [*y1, y2*] and

       A5: 0 = [*( + (x1,y1)), ( + (x2,y2))*] by XCMPLX_0:def 4;

      

       A6: k in NAT by ORDINAL1:def 12;

      then k in REAL by NUMBERS: 19;

      then

       A7: y2 = 0 by A4, ARYTM_0: 24;

      then

       A8: y1 = k by A4, ARYTM_0:def 5;

      ( + (x2,y2)) = ( In ( 0 , REAL )) by A5, ARYTM_0: 24;

      then

       A9: ( + (x1,y1)) = 0 by A5, ARYTM_0:def 5;

       A10:

      now

        assume x1 in REAL+ ;

        then

        consider x9,y9 be Element of REAL+ such that

         A11: x1 = x9 and

         A12: y1 = y9 and

         A13: 0 = (x9 + y9) by A6, A8, A9, ARYTM_0:def 1, ARYTM_2: 2;

        

         A14: y9 = 0 by A13, ARYTM_2: 5;

        x9 = 0 by A13, ARYTM_2: 5;

        hence contradiction by A2, A3, A4, A7, A11, A12, A14, ARYTM_0: 24;

      end;

      x2 = 0 by A3, ARYTM_0: 24;

      then

       A15: x1 = r by A3, ARYTM_0:def 5;

      r in ( REAL+ \/ [: { 0 }, REAL+ :]) by NUMBERS:def 1, XBOOLE_0:def 5;

      then x in [: { 0 }, REAL+ :] by A15, A10, XBOOLE_0:def 3;

      then

      consider x9,y9 be Element of REAL+ such that

       A16: x1 = [ 0 , x9] and

       A17: y1 = y9 and

       A18: 0 = (y9 - x9) by A6, A15, A8, A9, ARYTM_0:def 1, ARYTM_2: 2;

      

       A19: 0 in { 0 } by TARSKI:def 1;

      

       A20: not r in { [ 0 , 0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;

      x9 = y9 by A18, ARYTM_0: 6;

      then x in [: { 0 }, NAT :] by A15, A8, A16, A17, A19, ZFMISC_1: 87, A6;

      hence thesis by A20, XBOOLE_0:def 5;

    end;

    definition

      :: original: INT

      redefine

      :: INT_1:def1

      func INT means

      : Def1: x in it iff ex k st x = k or x = ( - k);

      compatibility

      proof

        let I be set;

        thus I = INT implies for x holds x in I iff ex k st x = k or x = ( - k)

        proof

          assume

           A1: I = INT ;

          let x;

          thus x in I implies ex k st x = k or x = ( - k)

          proof

            assume

             A2: x in I;

            then

             A3: not x in { [ 0 , 0 ]} by A1, NUMBERS:def 4, XBOOLE_0:def 5;

            per cases by A1, A2, NUMBERS:def 4, XBOOLE_0:def 3;

              suppose x in NAT ;

              hence thesis;

            end;

              suppose x in [: { 0 }, NAT :];

              then x in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}) by A3, XBOOLE_0:def 5;

              hence thesis by Lm1;

            end;

          end;

          given k such that

           A4: x = k or x = ( - k);

          per cases by A4;

            suppose x = k;

            then

             A5: x in NAT by ORDINAL1:def 12;

            then x in REAL by NUMBERS: 19;

            then

             A6: not x in { [ 0 , 0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;

            x in ( NAT \/ [: { 0 }, NAT :]) by XBOOLE_0:def 3, A5;

            hence thesis by A1, A6, NUMBERS:def 4, XBOOLE_0:def 5;

          end;

            suppose x = ( - k) & k <> x;

            then

             A7: x in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}) by Lm2;

            then

             A8: not x in { [ 0 , 0 ]} by XBOOLE_0:def 5;

            x in ( NAT \/ [: { 0 }, NAT :]) by A7, XBOOLE_0:def 3;

            hence thesis by A1, A8, NUMBERS:def 4, XBOOLE_0:def 5;

          end;

        end;

        assume

         A9: for x holds x in I iff ex k st x = k or x = ( - k);

        thus I c= INT

        proof

          let x be object;

          assume x in I;

          then

          consider k such that

           A10: x = k or x = ( - k) by A9;

          per cases by A10;

            suppose x = k;

            then

             A11: x in NAT by ORDINAL1:def 12;

            then x in REAL by NUMBERS: 19;

            then

             A12: not x in { [ 0 , 0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;

            x in ( NAT \/ [: { 0 }, NAT :]) by XBOOLE_0:def 3, A11;

            hence thesis by A12, NUMBERS:def 4, XBOOLE_0:def 5;

          end;

            suppose x = ( - k) & k <> x;

            then

             A13: x in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}) by Lm2;

            then

             A14: not x in { [ 0 , 0 ]} by XBOOLE_0:def 5;

            x in ( NAT \/ [: { 0 }, NAT :]) by A13, XBOOLE_0:def 3;

            hence thesis by A14, NUMBERS:def 4, XBOOLE_0:def 5;

          end;

        end;

        let x be object;

        assume

         A15: x in INT ;

        then

         A16: not x in { [ 0 , 0 ]} by NUMBERS:def 4, XBOOLE_0:def 5;

        per cases by A15, NUMBERS:def 4, XBOOLE_0:def 3;

          suppose x in NAT ;

          hence thesis by A9;

        end;

          suppose x in [: { 0 }, NAT :];

          then x in ( [: { 0 }, NAT :] \ { [ 0 , 0 ]}) by A16, XBOOLE_0:def 5;

          then ex k st x = k or x = ( - k) by Lm1;

          hence thesis by A9;

        end;

      end;

    end

    definition

      let i be Number;

      :: INT_1:def2

      attr i is integer means

      : Def2: i in INT ;

    end

    registration

      cluster integer for Real;

      existence

      proof

        take 0 ;

        thus 0 in INT by Def1;

      end;

      cluster integer for number;

      existence

      proof

        take 0 ;

        thus 0 in INT by Def1;

      end;

      cluster -> integer for Element of INT ;

      coherence ;

    end

    definition

      mode Integer is integer Number;

    end

    theorem :: INT_1:1

    

     Th1: for k be natural Number st r = k or r = ( - k) holds r is Integer

    proof

      let k be natural Number;

      

       A1: k is Nat by TARSKI: 1;

      assume r = k or r = ( - k);

      then r in INT by A1, Def1;

      hence thesis;

    end;

    theorem :: INT_1:2

    

     Th2: r is Integer implies ex k st r = k or r = ( - k)

    proof

      assume r is Integer;

      then r is Element of INT by Def2;

      hence thesis by Def1;

    end;

    registration

      cluster natural -> integer for object;

      coherence by Th1;

    end

    registration

      cluster integer -> real for object;

      coherence by NUMBERS: 15;

    end

    reserve i,i0,i1,i2,i3,i4,i5,i8,i9,j for Integer;

    registration

      let i1,i2 be Integer;

      cluster (i1 + i2) -> integer;

      coherence

      proof

        consider l such that

         A1: i2 = l or i2 = ( - l) by Th2;

        consider k such that

         A2: i1 = k or i1 = ( - k) by Th2;

         A3:

        now

           A4:

          now

            assume (l - k) <= 0 ;

            then l <= ( 0 + k) by XREAL_1: 20;

            then

            consider z be Nat such that

             A5: k = (l + z) by NAT_1: 10;

            ( - z) = (( - k) + l) by A5;

            hence (l - k) is Integer by Th1;

          end;

          assume that

           A6: i1 = ( - k) and

           A7: i2 = l;

          now

            assume 0 <= (l - k);

            then ( 0 + k) <= l by XREAL_1: 19;

            then ex z be Nat st l = (k + z) by NAT_1: 10;

            hence (l - k) is Integer;

          end;

          hence (i1 + i2) is Integer by A6, A7, A4;

        end;

         A8:

        now

           A9:

          now

            assume (k - l) <= 0 ;

            then k <= ( 0 + l) by XREAL_1: 20;

            then

            consider z be Nat such that

             A10: l = (k + z) by NAT_1: 10;

            ( - z) = (( - l) + k) by A10;

            hence (k - l) is Integer by Th1;

          end;

          assume that

           A11: i1 = k and

           A12: i2 = ( - l);

          now

            assume 0 <= (k - l);

            then ( 0 + l) <= k by XREAL_1: 19;

            then ex z be Nat st k = (l + z) by NAT_1: 10;

            hence (k - l) is Integer;

          end;

          hence (i1 + i2) is Integer by A11, A12, A9;

        end;

        now

          assume that

           A13: i1 = ( - k) and

           A14: i2 = ( - l);

          (i1 + i2) = ( - (k + l)) by A13, A14;

          hence (i1 + i2) is Integer by Th1;

        end;

        hence thesis by A2, A1, A8, A3;

      end;

      cluster (i1 * i2) -> integer;

      coherence

      proof

        consider l such that

         A15: i2 = l or i2 = ( - l) by Th2;

        consider k such that

         A16: i1 = k or i1 = ( - k) by Th2;

         A17:

        now

          assume that

           A18: i1 = ( - k) and

           A19: i2 = ( - l);

          (i1 * i2) = (k * l) by A18, A19;

          hence (i1 * i2) is Integer;

        end;

        now

          assume i1 = ( - k) & i2 = l or i1 = k & i2 = ( - l);

          then (i1 * i2) = ( - (k * l));

          hence (i1 * i2) is Integer by Th1;

        end;

        hence thesis by A16, A15, A17;

      end;

    end

    registration

      let i0 be Integer;

      cluster ( - i0) -> integer;

      coherence

      proof

        ex k st i0 = k or i0 = ( - k) by Th2;

        hence thesis by Th1;

      end;

    end

    registration

      let i1,i2 be Integer;

      cluster (i1 - i2) -> integer;

      coherence

      proof

        (i1 - i2) = (i1 + ( - i2));

        hence thesis;

      end;

    end

    theorem :: INT_1:3

    

     Th3: 0 <= i0 implies i0 in NAT

    proof

      consider k such that

       A1: i0 = k or i0 = ( - k) by Th2;

      assume 0 <= i0;

      then i0 = ( - k) implies i0 is Element of NAT ;

      hence thesis by A1, ORDINAL1:def 12;

    end;

    theorem :: INT_1:4

    r is Integer implies (r + 1) is Integer & (r - 1) is Integer;

    theorem :: INT_1:5

    

     Th5: i2 <= i1 implies (i1 - i2) in NAT

    proof

      assume i2 <= i1;

      then (i2 - i2) <= (i1 - i2) by XREAL_1: 9;

      hence thesis by Th3;

    end;

    theorem :: INT_1:6

    

     Th6: (i1 + k) = i2 implies i1 <= i2

    proof

      reconsider i0 = k as Integer;

      assume (i1 + k) = i2;

      then ( 0 + (i1 + k)) <= (k + i2) by XREAL_1: 6;

      then ((i1 + i0) - i0) <= ((i2 + i0) - i0) by XREAL_1: 9;

      hence thesis;

    end;

    

     Lm3: for j be Element of NAT holds j < 1 implies j = 0

    proof

      let j be Element of NAT ;

      assume j < 1;

      then j < ( 0 + 1);

      hence thesis by NAT_1: 13;

    end;

    

     Lm4: 0 < i1 implies 1 <= i1

    proof

      assume

       A1: 0 < i1;

      then

      reconsider i2 = i1 as Element of NAT by Th3;

       0 <> i2 by A1;

      hence thesis by Lm3;

    end;

    theorem :: INT_1:7

    

     Th7: i0 < i1 implies (i0 + 1) <= i1

    proof

      assume i0 < i1;

      then (i0 + ( - i0)) < (i1 + ( - i0)) by XREAL_1: 6;

      then 1 <= (i1 + ( - i0)) by Lm4;

      then (1 + i0) <= ((i1 + ( - i0)) + i0) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: INT_1:8

    

     Th8: i1 < 0 implies i1 <= ( - 1)

    proof

      assume i1 < 0 ;

      then 0 < ( - i1) by XREAL_1: 58;

      then 1 <= ( - i1) by Lm4;

      then ( - ( - i1)) <= ( - 1) by XREAL_1: 24;

      hence thesis;

    end;

    theorem :: INT_1:9

    

     Th9: (i1 * i2) = 1 iff i1 = 1 & i2 = 1 or i1 = ( - 1) & i2 = ( - 1)

    proof

      thus (i1 * i2) = 1 implies i1 = 1 & i2 = 1 or i1 = ( - 1) & i2 = ( - 1)

      proof

        assume

         A1: (i1 * i2) = 1;

        then

         A2: not i2 = 0 ;

         A3:

        now

          

           A4: (( - i1) * ( - i2)) = (i1 * i2);

          assume that

           A5: i1 < 0 and

           A6: i2 < 0 ;

          

           A7: ( - i2) is Element of NAT by A6, Th3;

          ( - i1) is Element of NAT by A5, Th3;

          then ( - ( - i1)) = ( - 1) by A1, A7, A4, NAT_1: 15;

          hence i1 = ( - 1) & i2 = ( - 1) by A1;

        end;

         A8:

        now

          assume that

           A9: 0 < i1 and

           A10: 0 < i2;

          

           A11: i2 is Element of NAT by A10, Th3;

          i1 is Element of NAT by A9, Th3;

          hence i1 = 1 & i2 = 1 by A1, A11, NAT_1: 15;

        end;

         not i1 = 0 by A1;

        hence thesis by A1, A2, A8, A3;

      end;

      thus thesis;

    end;

    theorem :: INT_1:10

    (i1 * i2) = ( - 1) iff i1 = ( - 1) & i2 = 1 or i1 = 1 & i2 = ( - 1)

    proof

      thus (i1 * i2) = ( - 1) implies i1 = ( - 1) & i2 = 1 or i1 = 1 & i2 = ( - 1)

      proof

        assume (i1 * i2) = ( - 1);

        then (( - i1) * i2) = 1;

        then ( - ( - i1)) = ( - 1) & i2 = 1 or ( - i1) = ( - 1) & i2 = ( - 1) by Th9;

        hence thesis;

      end;

      assume i1 = ( - 1) & i2 = 1 or i1 = 1 & i2 = ( - 1);

      hence thesis;

    end;

    

     Lm5: i0 <= i1 implies ex k st (i0 + k) = i1

    proof

      assume i0 <= i1;

      then

      reconsider k = (i1 - i0) as Element of NAT by Th5;

      (i0 + k) = i1;

      hence thesis;

    end;

    

     Lm6: i0 <= i1 implies ex k st (i1 - k) = i0

    proof

      assume i0 <= i1;

      then

      reconsider k = (i1 - i0) as Element of NAT by Th5;

      (i1 - k) = i0;

      hence thesis;

    end;

    scheme :: INT_1:sch1

    SepInt { P[ Integer] } :

ex X be Subset of INT st for x be Integer holds x in X iff P[x];

      defpred P1[ object] means ex i0 st i0 = $1 & P[i0];

      consider X such that

       A1: for y be object holds y in X iff y in INT & P1[y] from XBOOLE_0:sch 1;

      for y be object holds y in X implies y in INT by A1;

      then

      reconsider X as Subset of INT by TARSKI:def 3;

      take X;

      let i0;

      

       A2: i0 in X implies P[i0]

      proof

        assume i0 in X;

        then ex i1 st i0 = i1 & P[i1] by A1;

        hence thesis;

      end;

      P[i0] implies i0 in X by Def2, A1;

      hence thesis by A2;

    end;

    scheme :: INT_1:sch2

    IntIndUp { F() -> Integer , P[ Integer] } :

for i0 st F() <= i0 holds P[i0]

      provided

       A1: P[F()]

       and

       A2: for i2 st F() <= i2 holds P[i2] implies P[(i2 + 1)];

      defpred Q[ Nat] means for i2 st $1 = (i2 - F()) holds P[i2];

      

       A3: for k st Q[k] holds Q[(k + 1)]

      proof

        let k;

        reconsider i8 = k as Integer;

        assume

         A4: Q[k];

        let i2;

        assume

         A5: (k + 1) = (i2 - F());

        then (i2 - 1) = (i8 + F());

        then

         A6: F() <= (i2 - 1) by Th6;

        k = ((i2 - 1) - F()) by A5;

        then P[((i2 - 1) + 1)] by A2, A4, A6;

        hence thesis;

      end;

      let i0;

      assume F() <= i0;

      then

      reconsider l = (i0 - F()) as Element of NAT by Th5;

      

       A7: l = (i0 - F());

      

       A8: Q[ 0 ] by A1;

      for k holds Q[k] from NAT_1:sch 2( A8, A3);

      hence thesis by A7;

    end;

    scheme :: INT_1:sch3

    IntIndDown { F() -> Integer , P[ Integer] } :

for i0 st i0 <= F() holds P[i0]

      provided

       A1: P[F()]

       and

       A2: for i2 st i2 <= F() holds P[i2] implies P[(i2 - 1)];

      defpred Q[ Integer] means for i2 st $1 = ( - i2) holds P[i2];

      

       A3: for i2 st ( - F()) <= i2 holds Q[i2] implies Q[(i2 + 1)]

      proof

        let i2;

        assume that

         A4: ( - F()) <= i2 and

         A5: Q[i2];

        let i3;

        assume

         A6: (i2 + 1) = ( - i3);

        then

         A7: i2 = ( - (i3 + 1));

        ( - (( - i3) - 1)) <= ( - ( - F())) by A4, A6, XREAL_1: 24;

        then P[((i3 + 1) - 1)] by A2, A5, A7;

        hence thesis;

      end;

      let i0;

      assume i0 <= F();

      then

       A8: ( - F()) <= ( - i0) by XREAL_1: 24;

      

       A9: Q[( - F())] by A1;

      for i2 st ( - F()) <= i2 holds Q[i2] from IntIndUp( A9, A3);

      hence thesis by A8;

    end;

    scheme :: INT_1:sch4

    IntIndFull { F() -> Integer , P[ Integer] } :

for i0 holds P[i0]

      provided

       A1: P[F()]

       and

       A2: for i2 holds P[i2] implies P[(i2 - 1)] & P[(i2 + 1)];

      let i0;

      

       A3: P[F()] by A1;

       A4:

      now

        

         A5: for i2 st i2 <= F() holds P[i2] implies P[(i2 - 1)] by A2;

        

         A6: for i2 st i2 <= F() holds P[i2] from IntIndDown( A3, A5);

        assume i0 <= F();

        hence thesis by A6;

      end;

      now

        

         A7: for i2 st F() <= i2 holds P[i2] implies P[(i2 + 1)] by A2;

        

         A8: for i2 st F() <= i2 holds P[i2] from IntIndUp( A3, A7);

        assume F() <= i0;

        hence thesis by A8;

      end;

      hence thesis by A4;

    end;

    scheme :: INT_1:sch5

    IntMin { F() -> Integer , P[ Integer] } :

ex i0 st P[i0] & for i1 st P[i1] holds i0 <= i1

      provided

       A1: for i1 st P[i1] holds F() <= i1

       and

       A2: ex i1 st P[i1];

      defpred Q[ Nat] means P[(F() + $1)];

      consider i1 such that

       A3: P[i1] by A2;

      ex k st (F() + k) = i1 by A1, A3, Lm5;

      then

       A4: ex k be Nat st Q[k] by A3;

      consider l be Nat such that

       A5: Q[l] & for n be Nat st Q[n] holds l <= n from NAT_1:sch 5( A4);

      take i0 = (F() + l);

      for i1 st P[i1] holds i0 <= i1

      proof

        let i1;

        assume

         A6: P[i1];

        then ex n st (F() + n) = i1 by A1, Lm5;

        then (i0 - F()) <= (i1 - F()) by A5, A6;

        hence thesis by XREAL_1: 9;

      end;

      hence thesis by A5;

    end;

    scheme :: INT_1:sch6

    IntMax { F() -> Integer , P[ Integer] } :

ex i0 st P[i0] & for i1 st P[i1] holds i1 <= i0

      provided

       A1: for i1 st P[i1] holds i1 <= F()

       and

       A2: ex i1 st P[i1];

      defpred Q[ Nat] means P[(F() - $1)];

      consider i1 such that

       A3: P[i1] by A2;

      ex k st i1 = (F() - k) by A1, A3, Lm6;

      then

       A4: ex k be Nat st Q[k] by A3;

      consider l be Nat such that

       A5: Q[l] & for n be Nat st Q[n] holds l <= n from NAT_1:sch 5( A4);

      take i0 = (F() - l);

      for i1 st P[i1] holds i1 <= i0

      proof

        let i1;

        assume

         A6: P[i1];

        then

        consider n such that

         A7: (F() - n) = i1 by A1, Lm6;

        l <= n by A5, A6, A7;

        then ((F() + ( - i0)) - F()) <= ((F() - i1) - F()) by A7, XREAL_1: 9;

        then ( - i0) <= ((F() + ( - i1)) - F());

        hence thesis by XREAL_1: 24;

      end;

      hence thesis by A5;

    end;

    definition

      let i1,i2 be Integer;

      :: INT_1:def3

      pred i1 divides i2 means ex i3 st i2 = (i1 * i3);

      reflexivity

      proof

        let a be Integer;

        take 1;

        thus thesis;

      end;

    end

    definition

      let i1,i2,i3 be Integer;

      :: INT_1:def4

      pred i1,i2 are_congruent_mod i3 means i3 divides (i1 - i2);

    end

    definition

      let i1,i2,i3 be Integer;

      :: original: are_congruent_mod

      redefine

      :: INT_1:def5

      pred i1,i2 are_congruent_mod i3 means ex i4 st (i3 * i4) = (i1 - i2);

      compatibility

      proof

        thus (i1,i2) are_congruent_mod i3 implies ex i4 st (i3 * i4) = (i1 - i2)

        proof

          assume i3 divides (i1 - i2);

          hence thesis;

        end;

        given i4 such that

         A1: (i3 * i4) = (i1 - i2);

        take i4;

        thus thesis by A1;

      end;

    end

    theorem :: INT_1:11

    (i1,i1) are_congruent_mod i2

    proof

      (i2 * 0 ) = (i1 - i1);

      hence thesis;

    end;

    theorem :: INT_1:12

    (i1, 0 ) are_congruent_mod i1 & ( 0 ,i1) are_congruent_mod i1

    proof

      

       A1: (i1 * ( - 1)) = ( 0 - i1);

      thus thesis by A1;

    end;

    theorem :: INT_1:13

    (i1,i2) are_congruent_mod 1

    proof

      (i1 - i2) = (1 * (i1 - i2));

      hence thesis;

    end;

    theorem :: INT_1:14

    (i1,i2) are_congruent_mod i3 implies (i2,i1) are_congruent_mod i3

    proof

      assume (i1,i2) are_congruent_mod i3;

      then

      consider i0 such that

       A1: (i1 - i2) = (i3 * i0);

      (i2 - i1) = (i3 * ( - i0)) by A1;

      hence thesis;

    end;

    theorem :: INT_1:15

    (i1,i2) are_congruent_mod i5 & (i2,i3) are_congruent_mod i5 implies (i1,i3) are_congruent_mod i5

    proof

      assume that

       A1: (i1,i2) are_congruent_mod i5 and

       A2: (i2,i3) are_congruent_mod i5;

      consider i8 such that

       A3: (i5 * i8) = (i1 - i2) by A1;

      consider i9 such that

       A4: (i5 * i9) = (i2 - i3) by A2;

      (i5 * (i8 + i9)) = (i1 - i3) by A3, A4;

      hence thesis;

    end;

    theorem :: INT_1:16

    (i1,i2) are_congruent_mod i5 & (i3,i4) are_congruent_mod i5 implies ((i1 + i3),(i2 + i4)) are_congruent_mod i5

    proof

      assume that

       A1: (i1,i2) are_congruent_mod i5 and

       A2: (i3,i4) are_congruent_mod i5;

      consider i8 such that

       A3: (i5 * i8) = (i1 - i2) by A1;

      consider i9 such that

       A4: (i5 * i9) = (i3 - i4) by A2;

      (i5 * (i8 + i9)) = ((i1 + i3) - (i2 + i4)) by A3, A4;

      hence thesis;

    end;

    theorem :: INT_1:17

    (i1,i2) are_congruent_mod i5 & (i3,i4) are_congruent_mod i5 implies ((i1 - i3),(i2 - i4)) are_congruent_mod i5

    proof

      assume that

       A1: (i1,i2) are_congruent_mod i5 and

       A2: (i3,i4) are_congruent_mod i5;

      consider i8 such that

       A3: (i5 * i8) = (i1 - i2) by A1;

      consider i9 such that

       A4: (i5 * i9) = (i3 - i4) by A2;

      ((i1 - i3) - (i2 - i4)) = (i5 * (i8 - i9)) by A3, A4;

      hence thesis;

    end;

    theorem :: INT_1:18

    (i1,i2) are_congruent_mod i5 & (i3,i4) are_congruent_mod i5 implies ((i1 * i3),(i2 * i4)) are_congruent_mod i5

    proof

      assume that

       A1: (i1,i2) are_congruent_mod i5 and

       A2: (i3,i4) are_congruent_mod i5;

      consider i8 such that

       A3: (i5 * i8) = (i1 - i2) by A1;

      consider i9 such that

       A4: (i5 * i9) = (i3 - i4) by A2;

      ((i1 * i3) - (i2 * i4)) = (((i1 - i2) * i3) + ((i3 - i4) * i2))

      .= (((i5 * i8) * i3) + ((i5 * i9) * i2)) by A3, A4

      .= (i5 * ((i8 * i3) + (i9 * i2)));

      hence thesis;

    end;

    theorem :: INT_1:19

    ((i1 + i2),i3) are_congruent_mod i5 iff (i1,(i3 - i2)) are_congruent_mod i5;

    theorem :: INT_1:20

    (i4 * i5) = i3 implies ((i1,i2) are_congruent_mod i3 implies (i1,i2) are_congruent_mod i4)

    proof

      assume

       A1: (i4 * i5) = i3;

      assume (i1,i2) are_congruent_mod i3;

      then

      consider i0 such that

       A2: (i3 * i0) = (i1 - i2);

      (i1 - i2) = (i4 * (i5 * i0)) by A1, A2;

      hence thesis;

    end;

    theorem :: INT_1:21

    (i1,i2) are_congruent_mod i5 iff ((i1 + i5),i2) are_congruent_mod i5

    proof

      thus (i1,i2) are_congruent_mod i5 implies ((i1 + i5),i2) are_congruent_mod i5

      proof

        assume (i1,i2) are_congruent_mod i5;

        then

        consider i0 such that

         A1: (i5 * i0) = (i1 - i2);

        (i5 * (i0 + 1)) = ((i1 + i5) - i2) by A1;

        hence thesis;

      end;

      assume ((i1 + i5),i2) are_congruent_mod i5;

      then

      consider i0 such that

       A2: (i5 * i0) = ((i1 + i5) - i2);

      (i5 * (i0 - 1)) = (i1 - i2) by A2;

      hence thesis;

    end;

    theorem :: INT_1:22

    (i1,i2) are_congruent_mod i5 iff ((i1 - i5),i2) are_congruent_mod i5

    proof

      thus (i1,i2) are_congruent_mod i5 implies ((i1 - i5),i2) are_congruent_mod i5

      proof

        assume (i1,i2) are_congruent_mod i5;

        then

        consider i0 such that

         A1: (i5 * i0) = (i1 - i2);

        (i5 * (i0 - 1)) = ((i1 - i5) - i2) by A1;

        hence thesis;

      end;

      assume ((i1 - i5),i2) are_congruent_mod i5;

      then

      consider i0 such that

       A2: (i5 * i0) = ((i1 - i5) - i2);

      (i5 * (i0 + 1)) = (i1 - i2) by A2;

      hence thesis;

    end;

    theorem :: INT_1:23

    

     Th23: i1 <= r & (r - 1) < i1 & i2 <= r & (r - 1) < i2 implies i1 = i2

    proof

      assume that

       A1: i1 <= r and

       A2: (r - 1) < i1 and

       A3: i2 <= r and

       A4: (r - 1) < i2;

      i2 = (i1 + (i2 - i1));

      then

      consider i0 such that

       A5: i2 = (i1 + i0);

       A6:

      now

        assume that

         A7: 0 < i0 and i1 <> i2;

        1 <= i0 by A7, Lm4;

        then ((r - 1) + 1) < (i1 + i0) by A2, XREAL_1: 8;

        hence contradiction by A3, A5;

      end;

       A8:

      now

        assume that

         A9: i0 < 0 and i1 <> i2;

        i0 <= ( - 1) by A9, Th8;

        then (i1 + i0) <= (r + ( - 1)) by A1, XREAL_1: 7;

        hence contradiction by A4, A5;

      end;

      i0 = 0 implies i2 = i1 by A5;

      hence thesis by A8, A6;

    end;

    theorem :: INT_1:24

    

     Th24: r <= i1 & i1 < (r + 1) & r <= i2 & i2 < (r + 1) implies i1 = i2

    proof

      assume that

       A1: r <= i1 and

       A2: i1 < (r + 1) and

       A3: r <= i2 and

       A4: i2 < (r + 1);

      i2 = (i1 + (i2 - i1));

      then

      consider i0 such that

       A5: i2 = (i1 + i0);

       A6:

      now

        assume that

         A7: i0 < 0 and i1 <> i2;

        i0 <= ( - 1) by A7, Th8;

        then (i1 + i0) < ((r + 1) + ( - 1)) by A2, XREAL_1: 8;

        hence contradiction by A3, A5;

      end;

       A8:

      now

        assume that

         A9: 0 < i0 and i1 <> i2;

        1 <= i0 by A9, Lm4;

        hence contradiction by A1, A4, A5, XREAL_1: 7;

      end;

      i0 = 0 implies i2 = i1 by A5;

      hence thesis by A6, A8;

    end;

    reserve r1,p,p1,g,g1,g2 for Real,

Y for Subset of REAL ;

    

     Lm7: for r holds ex n st r < n

    proof

      defpred P[ Real] means for r st r in NAT holds not $1 < r;

      let r;

      consider Y such that

       A1: for p1 be Element of REAL holds p1 in Y iff P[p1] from SUBSET_1:sch 3;

      reconsider N = NAT as Subset of REAL by NUMBERS: 19;

      for r, p1 st r in N & p1 in Y holds r <= p1 by A1;

      then

      consider g2 such that

       A2: for r, p st r in N & p in Y holds r <= g2 & g2 <= p by AXIOMS: 1;

      

       A3: (g2 + ( - 1)) < (g2 + 0 ) by XREAL_1: 6;

      for g holds ex r st r in NAT & g < r

      proof

        given g1 such that

         A4: for r st r in NAT holds not g1 < r;

        g1 in REAL by XREAL_0:def 1;

        then

         A5: g1 in Y by A1, A4;

        now

          reconsider g21 = (g2 - 1) as Element of REAL by XREAL_0:def 1;

          assume not (g2 - 1) in Y;

          then not P[g21] by A1;

          then

          consider r1 be Real such that

           A6: r1 in NAT and

           A7: (g2 - 1) < r1;

          

           A8: (r1 + 1) in NAT by A6, AXIOMS: 2;

          ((g2 - 1) + 1) < (r1 + 1) by A7, XREAL_1: 6;

          hence contradiction by A2, A5, A8;

        end;

        hence contradiction by A2, A3;

      end;

      then

      consider p such that

       A9: p in NAT and

       A10: r < p;

      reconsider p as Element of NAT by A9;

      take p;

      thus thesis by A10;

    end;

    definition

      let r be Real;

      :: INT_1:def6

      func [\r/] -> Integer means

      : Def6: it <= r & (r - 1) < it ;

      existence

      proof

        defpred P[ Integer] means r < $1;

        consider n such that

         A1: ( - r) < n by Lm7;

        

         A2: ( - n) < ( - ( - r)) by A1, XREAL_1: 24;

        

         A3: for i1 st P[i1] holds ( - n) <= i1

        proof

          let i1;

          assume r < i1;

          then (r + ( - n)) < (i1 + r) by A2, XREAL_1: 8;

          hence thesis by XREAL_1: 6;

        end;

        ex n st r < n by Lm7;

        then

         A4: ex i0 st P[i0];

        consider i1 such that

         A5: P[i1] & for i2 st P[i2] holds i1 <= i2 from IntMin( A3, A4);

        

         A6: (r - 1) < (i1 - 1) by A5, XREAL_1: 9;

        r < (i1 - 1) implies i1 <= (i1 - 1) by A5;

        hence thesis by A6, XREAL_1: 146;

      end;

      uniqueness by Th23;

      projectivity by XREAL_1: 44;

    end

    theorem :: INT_1:25

    

     Th25: [\r/] = r iff r is integer

    proof

      r is Integer implies [\r/] = r

      proof

        (r + 0 ) < (r + 1) by XREAL_1: 6;

        then

         A1: (r - 1) < ((r + 1) - 1) by XREAL_1: 9;

        assume r is Integer;

        hence thesis by A1, Def6;

      end;

      hence thesis;

    end;

    theorem :: INT_1:26

    

     Th26: [\r/] < r iff not r is integer

    proof

      now

        assume

         A1: not r is Integer;

         [\r/] <= r by Def6;

        hence [\r/] < r by A1, XXREAL_0: 1;

      end;

      hence thesis by Th25;

    end;

    theorem :: INT_1:27

    ( [\r/] - 1) < r & [\r/] < (r + 1)

    proof

       [\r/] <= r by Def6;

      then

       A1: ( [\r/] + 0 ) < (r + 1) by XREAL_1: 8;

      then ( [\r/] + ( - 1)) < ((r + 1) + ( - 1)) by XREAL_1: 6;

      hence thesis by A1;

    end;

    theorem :: INT_1:28

    

     Th28: ( [\r/] + i0) = [\(r + i0)/]

    proof

      (r - 1) < [\r/] by Def6;

      then ((r - 1) + i0) < ( [\r/] + i0) by XREAL_1: 6;

      then

       A1: ((r + i0) - 1) < ( [\r/] + i0);

       [\r/] <= r by Def6;

      then ( [\r/] + i0) <= (r + i0) by XREAL_1: 6;

      hence thesis by A1, Def6;

    end;

    theorem :: INT_1:29

    

     Th29: r < ( [\r/] + 1)

    proof

      (r - 1) < [\r/] by Def6;

      then ((r - 1) + 1) < ( [\r/] + 1) by XREAL_1: 6;

      hence thesis;

    end;

    definition

      let r be Real;

      :: INT_1:def7

      func [/r\] -> Integer means

      : Def7: r <= it & it < (r + 1);

      existence

      proof

         A1:

        now

          

           A2: (r + 0 ) < (r + 1) by XREAL_1: 6;

          assume r is Integer;

          hence r <= [\r/] & [\r/] < (r + 1) by A2, Th25;

        end;

         not r is Integer implies r <= ( [\r/] + 1) & ( [\r/] + 1) < (r + 1) by Th29, XREAL_1: 6, Th26;

        hence thesis by A1;

      end;

      uniqueness by Th24;

      projectivity by XREAL_1: 29;

    end

    theorem :: INT_1:30

    

     Th30: [/r\] = r iff r is integer

    proof

      (r + 0 ) < (r + 1) by XREAL_1: 6;

      hence thesis by Def7;

    end;

    theorem :: INT_1:31

    

     Th31: r < [/r\] iff not r is integer

    proof

      now

        assume

         A1: not r is Integer;

        r <= [/r\] by Def7;

        hence r < [/r\] by A1, XXREAL_0: 1;

      end;

      hence thesis by Th30;

    end;

    theorem :: INT_1:32

    (r - 1) < [/r\] & r < ( [/r\] + 1)

    proof

      r <= [/r\] by Def7;

      then

       A1: (r + 0 ) < ( [/r\] + 1) by XREAL_1: 8;

      then (r + ( - 1)) < (( [/r\] + 1) + ( - 1)) by XREAL_1: 6;

      hence thesis by A1;

    end;

    theorem :: INT_1:33

    ( [/r\] + i0) = [/(r + i0)\]

    proof

       [/r\] < (r + 1) by Def7;

      then ( [/r\] + i0) < ((r + 1) + i0) by XREAL_1: 6;

      then

       A1: ( [/r\] + i0) < ((r + i0) + 1);

      r <= [/r\] by Def7;

      then (r + i0) <= ( [/r\] + i0) by XREAL_1: 6;

      hence thesis by A1, Def7;

    end;

    theorem :: INT_1:34

    

     Th34: [\r/] = [/r\] iff r is integer

    proof

       A1:

      now

        assume

         A2: not r is Integer;

        then [\r/] < r by Th26;

        hence [\r/] <> [/r\] by A2, Th31;

      end;

      now

        assume r is Integer;

        hence [\r/] = r & r = [/r\] by Th25, Th30;

        hence [\r/] = [/r\];

      end;

      hence thesis by A1;

    end;

    theorem :: INT_1:35

    

     Th35: [\r/] < [/r\] iff not r is integer

    proof

      now

        assume

         A1: not r is Integer;

        then

         A2: r < [/r\] by Th31;

         [\r/] < r by A1, Th26;

        hence [\r/] < [/r\] by A2, XXREAL_0: 2;

      end;

      hence thesis by Th34;

    end;

    theorem :: INT_1:36

     [\r/] <= [/r\]

    proof

      

       A1: r <= [/r\] by Def7;

       [\r/] <= r by Def6;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: INT_1:37

     [\ [/r\]/] = [/r\] by Th25;

    ::$Canceled

    theorem :: INT_1:40

     [/ [\r/]\] = [\r/] by Th30;

    theorem :: INT_1:41

     [\r/] = [/r\] iff not ( [\r/] + 1) = [/r\]

    proof

      set Diff = ( [/r\] + ( - [\r/]));

       A1:

      now

        assume not r is Integer;

        then [\r/] < [/r\] by Th35;

        then ( [\r/] + ( - [\r/])) < Diff by XREAL_1: 6;

        then

         A2: 1 <= Diff by Lm4;

        (r - 1) < [\r/] by Def6;

        then

         A3: ( - [\r/]) < ( - (r - 1)) by XREAL_1: 24;

         [/r\] < (r + 1) by Def7;

        then Diff < ((r + 1) + ( - (r - 1))) by A3, XREAL_1: 8;

        then ((Diff + 1) + ( - 1)) <= ((1 + 1) + ( - 1)) by Th7;

        then ( [\r/] + 1) = ( [\r/] + Diff) by A2, XXREAL_0: 1;

        hence ( [\r/] + 1) = [/r\] & [\r/] <> [/r\];

      end;

      now

        assume r is Integer;

        then [\r/] = [/r\] by Th34;

        hence [\r/] = [/r\] & ( [\r/] + 1) <> [/r\];

      end;

      hence thesis by A1;

    end;

    definition

      let r be Real;

      :: INT_1:def8

      func frac r -> number equals (r - [\r/]);

      coherence ;

    end

    registration

      let r be Real;

      cluster ( frac r) -> real;

      coherence ;

    end

    theorem :: INT_1:42

    r = ( [\r/] + ( frac r));

    theorem :: INT_1:43

    

     Th41: ( frac r) < 1 & 0 <= ( frac r)

    proof

      (r - 1) < [\r/] by Def6;

      then (( frac r) + (r - 1)) < ((r - [\r/]) + [\r/]) by XREAL_1: 6;

      then (((( frac r) + ( - 1)) + r) - r) < (r - r) by XREAL_1: 9;

      then

       A1: ((( frac r) - 1) + 1) < ( 0 + 1) by XREAL_1: 6;

       [\r/] <= r by Def6;

      then ( [\r/] + (r - [\r/])) <= (r + ( frac r)) by XREAL_1: 6;

      then (r - r) <= ((r + ( frac r)) - r) by XREAL_1: 9;

      hence thesis by A1;

    end;

    theorem :: INT_1:44

     [\( frac r)/] = 0

    proof

       [\( frac r)/] = [\(r + ( - [\r/]))/]

      .= ( [\r/] + ( - [\r/])) by Th28

      .= 0 ;

      hence thesis;

    end;

    theorem :: INT_1:45

    

     Th43: ( frac r) = 0 iff r is integer

    proof

      now

        assume r is Integer;

        then r = [\r/] by Th25;

        hence ( frac r) = 0 ;

      end;

      hence thesis;

    end;

    theorem :: INT_1:46

     0 < ( frac r) iff not r is integer

    proof

      now

        assume not r is Integer;

        then 0 <> ( frac r);

        hence 0 < ( frac r) by Th41;

      end;

      hence thesis by Th43;

    end;

    definition

      let i1,i2 be Integer;

      :: INT_1:def9

      func i1 div i2 -> Integer equals [\(i1 / i2)/];

      correctness ;

    end

    definition

      let i1,i2 be Integer;

      :: INT_1:def10

      func i1 mod i2 -> Integer equals

      : Def10: (i1 - ((i1 div i2) * i2)) if i2 <> 0

      otherwise 0 ;

      correctness ;

    end

    theorem :: INT_1:47

    

     Th45: for r be Real st r <> 0 holds [\(r / r)/] = 1

    proof

      let r be Real;

      assume r <> 0 ;

      

      hence [\(r / r)/] = [\1/] by XCMPLX_1: 60

      .= 1 by Th25;

    end;

    theorem :: INT_1:48

    for i be Integer holds (i div 0 ) = 0

    proof

      let i be Integer;

      

       A1: (i / 0 ) = (i * ( 0 " )) by XCMPLX_0:def 9

      .= (i * 0 );

      ( 0 - 1) < 0 ;

      hence thesis by A1, Def6;

    end;

    theorem :: INT_1:49

    for i be Integer st i <> 0 holds (i div i) = 1 by Th45;

    theorem :: INT_1:50

    for i be Integer holds (i mod i) = 0

    proof

      let i be Integer;

      per cases ;

        suppose i = 0 ;

        hence thesis by Def10;

      end;

        suppose

         A1: i <> 0 ;

        

        hence (i mod i) = (i - ((i div i) * i)) by Def10

        .= (i - (1 * i)) by A1, Th45

        .= 0 ;

      end;

    end;

    begin

    theorem :: INT_1:51

    for k,i be Integer holds k < i implies ex j be Element of NAT st j = (i - k) & 1 <= j

    proof

      let k,i be Integer;

      assume k < i;

      then

       A1: (k - k) < (i - k) by XREAL_1: 9;

      then

      reconsider j = (i - k) as Element of NAT by Th3;

      reconsider j9 = j, Z9 = 0 as Integer;

      take j;

      thus j = (i - k);

      (Z9 + 1) <= j9 by A1, Th7;

      hence thesis;

    end;

    theorem :: INT_1:52

    

     Th50: for a,b be Integer st a < b holds a <= (b - 1)

    proof

      let a,b be Integer;

      assume a < b;

      then (a - 1) < (b - 1) by XREAL_1: 9;

      then ((a - 1) + 1) <= (b - 1) by Th7;

      hence thesis;

    end;

    theorem :: INT_1:53

    for r be Real st r >= 0 holds [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT

    proof

      let r be Real;

      assume

       A1: r >= 0 ;

      

       A2: r <= [/r\] by Def7;

      (r - 1) < [\r/] by Def6;

      then ((r - 1) + 1) < ( [\r/] + 1) by XREAL_1: 6;

      then ( 0 - 1) < (( [\r/] + 1) - 1) by A1, XREAL_1: 9;

      then [\r/] >= 0 by Th8;

      hence thesis by A1, A2, Th3;

    end;

    theorem :: INT_1:54

    

     Th52: for i be Integer, r be Real st i <= r holds i <= [\r/]

    proof

      let i be Integer;

      let r be Real;

      assume i <= r;

      then

       A1: (i - 1) <= (r - 1) by XREAL_1: 9;

      (r - 1) < [\r/] by Def6;

      then (i - 1) < [\r/] by A1, XXREAL_0: 2;

      then ((i - 1) + 1) <= [\r/] by Th7;

      hence thesis;

    end;

    theorem :: INT_1:55

    for m,n be Nat holds 0 <= (m qua Integer div n) by Th52;

    theorem :: INT_1:56

     0 < i & 1 < j implies (i div j) < i

    proof

      assume that

       A1: 0 < i and

       A2: 1 < j;

      assume

       A3: i <= (i div j);

      (i div j) <= (i / j) by Def6;

      then (j * (i div j)) <= (j * (i / j)) by A2, XREAL_1: 64;

      then (j * (i div j)) <= i by A2, XCMPLX_1: 87;

      then (j * (i div j)) <= (i div j) by A3, XXREAL_0: 2;

      then ((j * (i div j)) * ((i div j) " )) <= ((i div j) * ((i div j) " )) by A1, A3, XREAL_1: 64;

      then (j * ((i div j) * ((i div j) " ))) <= ((i div j) * ((i div j) " ));

      then (j * 1) <= ((i div j) * ((i div j) " )) by A1, A3, XCMPLX_0:def 7;

      hence contradiction by A1, A2, A3, XCMPLX_0:def 7;

    end;

    theorem :: INT_1:57

    i2 >= 0 implies (i1 mod i2) >= 0

    proof

      assume

       A1: i2 >= 0 ;

      per cases by A1;

        suppose

         A2: i2 > 0 ;

         [\(i1 / i2)/] <= (i1 / i2) by Def6;

        then ((i1 div i2) * i2) <= ((i1 / i2) * i2) by A2, XREAL_1: 64;

        then ((i1 div i2) * i2) <= i1 by A2, XCMPLX_1: 87;

        then (i1 - ((i1 div i2) * i2)) >= 0 by XREAL_1: 48;

        hence thesis by Def10;

      end;

        suppose i2 = 0 ;

        hence thesis by Def10;

      end;

    end;

    theorem :: INT_1:58

    i2 > 0 implies (i1 mod i2) < i2

    proof

      assume

       A1: i2 > 0 ;

      ((i1 / i2) - 1) < [\(i1 / i2)/] by Def6;

      then (((i1 / i2) - 1) * i2) < ((i1 div i2) * i2) by A1, XREAL_1: 68;

      then (((i1 / i2) * i2) - (1 * i2)) < ((i1 div i2) * i2);

      then (i1 - i2) < (((i1 div i2) * i2) - 0 ) by A1, XCMPLX_1: 87;

      then (i1 - ((i1 div i2) * i2)) < (i2 - 0 ) by XREAL_1: 17;

      hence thesis by A1, Def10;

    end;

    theorem :: INT_1:59

    i2 <> 0 implies i1 = (((i1 div i2) * i2) + (i1 mod i2))

    proof

      assume i2 <> 0 ;

      

      then (((i1 div i2) * i2) + (i1 mod i2)) = (((i1 div i2) * i2) + (i1 - ((i1 div i2) * i2))) by Def10

      .= i1;

      hence thesis;

    end;

    theorem :: INT_1:60

    for m,j be Integer holds ((m * j), 0 ) are_congruent_mod m;

    theorem :: INT_1:61

    i >= 0 & j >= 0 implies (i div j) >= 0

    proof

      assume that

       A1: i >= 0 and

       A2: j >= 0 ;

      

       A3: ((i / j) - 1) < [\(i / j)/] by Def6;

      ((i / j) - 1) >= ( 0 - 1) by A1, A2, XREAL_1: 9;

      then ( - 1) < [\(i / j)/] by A3, XXREAL_0: 2;

      hence thesis by Th8;

    end;

    theorem :: INT_1:62

    for n be Nat st n > 0 holds for a be Integer holds (a mod n) = 0 iff n divides a

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      let a be Integer;

       A2:

      now

        

         A3: (a mod n) = (a - ((a div n) * n)) by A1, Def10

        .= (a - ( [\(a / n)/] * n));

        assume n divides a;

        then

        consider k be Integer such that

         A4: (n * k) = a;

        ( - n) <> 0 by A1;

        then (( - n) + a) < ( 0 + a) by XREAL_1: 6;

        then ((( - n) + a) * (n " )) < ((n * k) * (n " )) by A1, A4, XREAL_1: 68;

        then ((( - n) * (n " )) + (a * (n " ))) < ((n * k) * (n " ));

        then ((( - n) * (n " )) + (a / n)) < ((n * (n " )) * k) by XCMPLX_0:def 9;

        then ((( - n) * (n " )) + (a / n)) < (1 * k) by A1, XCMPLX_0:def 7;

        then (( - (n * (n " ))) + (a / n)) < k;

        then (( - 1) + (a / n)) < k by A1, XCMPLX_0:def 7;

        then

         A5: ((a / n) - 1) < k;

        k <= (a / n)

        proof

          assume k > (a / n);

          then (k * n) > ((a / n) * n) by A1, XREAL_1: 68;

          then (k * n) > ((a * (n " )) * n) by XCMPLX_0:def 9;

          then (k * n) > (a * ((n " ) * n));

          then (n * k) > (a * 1) by A1, XCMPLX_0:def 7;

          hence thesis by A4;

        end;

        then [\(a / n)/] = k by A5, Def6;

        hence (a mod n) = 0 by A4, A3;

      end;

      now

        assume (a mod n) = 0 ;

        then 0 = (a - ((a div n) * n)) by A1, Def10;

        hence n divides a;

      end;

      hence thesis by A2;

    end;

    reserve r,s for Real;

    theorem :: INT_1:63

     not (r / s) is Integer implies ( - [\(r / s)/]) = ( [\(( - r) / s)/] + 1)

    proof

      ((r / s) - 1) < [\(r / s)/] by Def6;

      then ( - ((r / s) - 1)) > ( - [\(r / s)/]) by XREAL_1: 24;

      then (( - (r / s)) + 1) > ( - [\(r / s)/]);

      then ( - [\(r / s)/]) <= ((( - r) / s) + 1) by XCMPLX_1: 187;

      then

       A1: (( - [\(r / s)/]) - 1) <= (((( - r) / s) + 1) - 1) by XREAL_1: 9;

      assume not (r / s) is Integer;

      then [\(r / s)/] < (r / s) by Th26;

      then ( - (r / s)) < ( - [\(r / s)/]) by XREAL_1: 24;

      then (( - (r / s)) - 1) < (( - [\(r / s)/]) - 1) by XREAL_1: 9;

      then ((( - r) / s) - 1) < (( - [\(r / s)/]) - 1) by XCMPLX_1: 187;

      then ((( - [\(r / s)/]) - 1) + 1) = ( [\(( - r) / s)/] + 1) by A1, Def6;

      hence thesis;

    end;

    theorem :: INT_1:64

    (r / s) is Integer implies ( - [\(r / s)/]) = [\(( - r) / s)/]

    proof

      assume (r / s) is Integer;

      then

       A1: [\(r / s)/] = (r / s) by Th25;

      

       A2: ( - (r / s)) = (( - r) / s) by XCMPLX_1: 187;

      then ((( - r) / s) - 1) < (( - [\(r / s)/]) - 0 ) by A1, XREAL_1: 15;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: INT_1:65

    r <= i implies [/r\] <= i

    proof

      assume r <= i;

      then

       A1: (r + 1) <= (i + 1) by XREAL_1: 6;

       [/r\] < (r + 1) by Def7;

      then [/r\] < (i + 1) by A1, XXREAL_0: 2;

      then [/r\] <= ((i + 1) - 1) by Th50;

      hence thesis;

    end;

    scheme :: INT_1:sch7

    FinInd { M,N() -> Element of NAT , P[ Nat] } :

for i be Element of NAT st M() <= i & i <= N() holds P[i]

      provided

       A1: P[M()]

       and

       A2: for j be Element of NAT st M() <= j & j < N() holds P[j] implies P[(j + 1)];

      defpred Q[ Nat] means M() <= $1 & $1 <= N() & not P[$1];

      assume not (for i be Element of NAT st M() <= i & i <= N() holds P[i]);

      then

       A3: ex i be Nat st Q[i];

      consider k be Nat such that

       A4: Q[k] & for k9 be Nat st Q[k9] holds k <= k9 from NAT_1:sch 5( A3);

      per cases ;

        suppose k = M();

        hence thesis by A1, A4;

      end;

        suppose k <> M();

        then M() < k by A4, XXREAL_0: 1;

        then (M() + 1) <= k by NAT_1: 13;

        then

         A5: ((M() + 1) - 1) <= (k - 1) by XREAL_1: 9;

        then

        reconsider k9 = (k - 1) as Element of NAT by Th3;

        

         A6: k9 <> (k9 + 1);

        k9 <= (k9 + 1) by NAT_1: 11;

        then

         A7: k9 < k by A6, XXREAL_0: 1;

        then

         A8: k9 < N() by A4, XXREAL_0: 2;

        

         A9: ((k - 1) + 1) = (k + 0 );

         not Q[k9] by A4, A7;

        hence thesis by A2, A4, A5, A9, A8;

      end;

    end;

    scheme :: INT_1:sch8

    FinInd2 { M,N() -> Element of NAT , P[ Nat] } :

for i be Element of NAT st M() <= i & i <= N() holds P[i]

      provided

       A1: P[M()]

       and

       A2: for j be Element of NAT st M() <= j & j < N() holds (for j9 be Element of NAT st M() <= j9 & j9 <= j holds P[j9]) implies P[(j + 1)];

      defpred Q[ Element of NAT ] means for j be Element of NAT st M() <= j & j <= $1 holds P[j];

      

       A3: for j be Element of NAT st M() <= j & j < N() holds Q[j] implies Q[(j + 1)]

      proof

        let j be Element of NAT ;

        assume that

         A4: M() <= j and

         A5: j < N();

        assume

         A6: Q[j];

        thus Q[(j + 1)]

        proof

          let i be Element of NAT ;

          assume that

           A7: M() <= i and

           A8: i <= (j + 1);

          per cases ;

            suppose i = (j + 1);

            hence thesis by A2, A4, A5, A6;

          end;

            suppose i <> (j + 1);

            then i < (j + 1) by A8, XXREAL_0: 1;

            then i <= j by NAT_1: 13;

            hence thesis by A6, A7;

          end;

        end;

      end;

      

       A9: Q[M()] by A1, XXREAL_0: 1;

      for i be Element of NAT st M() <= i & i <= N() holds Q[i] from FinInd( A9, A3);

      hence thesis;

    end;

    reserve i for Integer,

a,b,r,s for Real;

    theorem :: INT_1:66

    ( frac (r + i)) = ( frac r)

    proof

      

      thus ( frac (r + i)) = ((r + i) - [\(r + i)/])

      .= ((r + i) - ( [\r/] + i)) by Th28

      .= (((r - [\r/]) + i) - i)

      .= ( frac r);

    end;

    theorem :: INT_1:67

    

     Th65: r <= a & a < ( [\r/] + 1) implies [\a/] = [\r/]

    proof

      assume

       A1: r <= a;

      assume a < ( [\r/] + 1);

      then

       A2: (a - 1) < (( [\r/] + 1) - 1) by XREAL_1: 9;

       [\r/] <= r by Def6;

      then [\r/] <= a by A1, XXREAL_0: 2;

      hence thesis by A2, Def6;

    end;

    theorem :: INT_1:68

    

     Th66: r <= a & a < ( [\r/] + 1) implies ( frac r) <= ( frac a)

    proof

      assume

       A1: r <= a;

      assume a < ( [\r/] + 1);

      then [\a/] = [\r/] by A1, Th65;

      hence thesis by A1, XREAL_1: 9;

    end;

    theorem :: INT_1:69

    r < a & a < ( [\r/] + 1) implies ( frac r) < ( frac a)

    proof

      assume

       A1: r < a;

      assume a < ( [\r/] + 1);

      then [\a/] = [\r/] by A1, Th65;

      hence thesis by A1, XREAL_1: 9;

    end;

    theorem :: INT_1:70

    

     Th68: a >= ( [\r/] + 1) & a <= (r + 1) implies [\a/] = ( [\r/] + 1)

    proof

      assume

       A1: a >= ( [\r/] + 1);

      assume a <= (r + 1);

      then (a - 1) <= ((r + 1) - 1) by XREAL_1: 9;

      then (a - 1) < ( [\r/] + 1) by Th29, XXREAL_0: 2;

      hence thesis by A1, Def6;

    end;

    theorem :: INT_1:71

    

     Th69: a >= ( [\r/] + 1) & a < (r + 1) implies ( frac a) < ( frac r)

    proof

      assume

       A1: a >= ( [\r/] + 1);

      assume

       A2: a < (r + 1);

      then (a - 1) < r by XREAL_1: 19;

      then

       A3: ( frac a) = (a - [\a/]) & ((a - 1) - [\r/]) < (r - [\r/]) by XREAL_1: 14;

       [\a/] = ( [\r/] + 1) by A1, A2, Th68;

      hence thesis by A3;

    end;

    theorem :: INT_1:72

    r <= a & a < (r + 1) & r <= b & b < (r + 1) & ( frac a) = ( frac b) implies a = b

    proof

      assume that

       A1: r <= a and

       A2: a < (r + 1) and

       A3: r <= b and

       A4: b < (r + 1) and

       A5: ( frac a) = ( frac b);

      

       A6: [\r/] <= r by Def6;

      then

       A7: [\r/] <= a by A1, XXREAL_0: 2;

      

       A8: [\r/] <= b by A3, A6, XXREAL_0: 2;

      per cases ;

        suppose

         A9: a < ( [\r/] + 1) & b >= ( [\r/] + 1);

        then ( frac a) >= ( frac r) by A1, Th66;

        hence thesis by A4, A5, A9, Th69;

      end;

        suppose

         A10: a >= ( [\r/] + 1) & b < ( [\r/] + 1);

        then ( frac a) < ( frac r) by A2, Th69;

        hence thesis by A3, A5, A10, Th66;

      end;

        suppose

         A11: a < ( [\r/] + 1) & b < ( [\r/] + 1);

        then (b - 1) < (( [\r/] + 1) - 1) by XREAL_1: 9;

        then

         A12: [\b/] = [\r/] by A8, Def6;

        (a - 1) < (( [\r/] + 1) - 1) by A11, XREAL_1: 9;

        then [\a/] = [\r/] by A7, Def6;

        hence thesis by A5, A12;

      end;

        suppose a >= ( [\r/] + 1) & b >= ( [\r/] + 1);

        then [\a/] = ( [\r/] + 1) & [\b/] = ( [\r/] + 1) by A2, A4, Th68;

        hence thesis by A5;

      end;

    end;

    registration

      let i be Integer;

      reduce ( In (i, INT )) to i;

      reducibility by Def2, SUBSET_1:def 8;

    end

    definition

      let x be Number;

      :: INT_1:def11

      attr x is dim-like means

      : Def11: x = ( - 1) or x is natural;

    end

    registration

      cluster natural -> dim-like for object;

      coherence ;

      cluster dim-like -> integer for object;

      coherence ;

      cluster ( - 1) -> dim-like;

      coherence ;

    end

    registration

      cluster dim-like for set;

      existence

      proof

        reconsider x = ( - 1) as set by TARSKI: 1;

        take x;

        thus thesis;

      end;

    end

    registration

      let d be dim-like object;

      cluster (d + 1) -> natural;

      coherence

      proof

        per cases by Def11;

          suppose d = ( - 1);

          then (d + 1) = 0 ;

          hence thesis;

        end;

          suppose d is natural;

          hence thesis;

        end;

      end;

    end

    registration

      let k be dim-like object, n be non zero natural Number;

      cluster (k + n) -> natural;

      coherence

      proof

        per cases by Def11;

          suppose

           A1: k = ( - 1);

          consider i be Nat such that

           A2: n = (i + 1) by NAT_1: 6;

          (k + n) = i by A2, A1;

          hence thesis;

        end;

          suppose k is natural;

          hence thesis;

        end;

      end;

    end

    theorem :: INT_1:73

    for i be Integer holds 0 = ( 0 mod i)

    proof

      let i be Integer;

      per cases ;

        suppose i = 0 ;

        hence thesis by Def10;

      end;

        suppose

         A1: i <> 0 ;

        ( 0 div i) = 0 by Th25;

        then ( 0 mod i) = ( 0 - (i * 0 qua Nat)) by A1, Def10;

        hence thesis;

      end;

    end;

    theorem :: INT_1:74

    for n be non zero Nat holds (n - 1) is Nat & 1 <= n

    proof

      let n be non zero Nat;

      

       A1: ( 0 + 1) <= n by NAT_1: 13;

      then (( 0 + 1) - 1) <= (n - 1) by XREAL_1: 9;

      then (n - 1) in NAT by Th3;

      hence (n - 1) is Nat;

      thus thesis by A1;

    end;