nat_2.miz



    begin

    reserve i,j,k,l,m,n,t for Nat;

    scheme :: NAT_2:sch1

    NonUniqPiFinRecExD { D() -> non empty set , A() -> Element of D() , N() -> Nat , P[ set, set, set] } :

ex p be FinSequence of D() st ( len p) = N() & ((p /. 1) = A() or N() = 0 ) & for n be Nat st 1 <= n & n < N() holds P[n, (p /. n), (p /. (n + 1))]

      provided

       A1: for n be Nat st 1 <= n & n < N() holds for x be Element of D() holds ex y be Element of D() st P[n, x, y];

      consider p be FinSequence of D() such that

       A2: ( len p) = N() and

       A3: (p . 1) = A() or N() = 0 and

       A4: for n be Nat st 1 <= n & n < N() holds P[n, (p . n), (p . (n + 1))] from RECDEF_1:sch 4( A1);

      take p;

      thus ( len p) = N() by A2;

      now

        assume N() <> 0 ;

        then N() >= ( 0 + 1) by NAT_1: 13;

        hence (p /. 1) = A() by A2, A3, FINSEQ_4: 15;

      end;

      hence (p /. 1) = A() or N() = 0 ;

      let n be Nat;

      assume that

       A5: 1 <= n and

       A6: n < N();

      (n + 1) <= N() by A6, NAT_1: 13;

      then

       A7: (p . (n + 1)) = (p /. (n + 1)) by A2, FINSEQ_4: 15, NAT_1: 11;

      n in NAT & (p . n) = (p /. n) by A2, A5, A6, FINSEQ_4: 15, ORDINAL1:def 12;

      hence thesis by A4, A5, A6, A7;

    end;

    theorem :: NAT_2:1

    for x,y be Real st x >= 0 & y > 0 holds (x / ( [\(x / y)/] + 1)) < y

    proof

      let x,y be Real such that

       A1: x >= 0 and

       A2: y > 0 ;

      ((x / y) * y) < (( [\(x / y)/] + 1) * y) by A2, INT_1: 29, XREAL_1: 68;

      then

       A3: x < (( [\(x / y)/] + 1) * y) by A2, XCMPLX_1: 87;

       [\(x / y)/] >= 0 by A1, A2, INT_1: 53;

      hence thesis by A3, XREAL_1: 83;

    end;

    begin

    theorem :: NAT_2:2

    

     Th2: ( 0 div n) = 0

    proof

      now

        per cases by NAT_D:def 1;

          suppose

           A1: ex t be Nat st 0 = ((n * ( 0 div n)) + t) & t < n;

          then (n * ( 0 div n)) = 0 ;

          hence thesis by A1, XCMPLX_1: 6;

        end;

          suppose ( 0 div n) = 0 & n = 0 ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: NAT_2:3

    for n be non zero Nat holds (n div n) = 1

    proof

      let n be non zero Nat;

      ((n * 1) div n) = 1 by NAT_D: 18;

      hence thesis;

    end;

    theorem :: NAT_2:4

    (n div 1) = n

    proof

      n = ((1 * n) + 0 );

      hence thesis by NAT_D:def 1;

    end;

    theorem :: NAT_2:5

    i <= j & k <= j & i = ((j -' k) + l) implies k = ((j -' i) + l)

    proof

      assume that

       A1: i <= j and

       A2: k <= j & i = ((j -' k) + l);

      (i - l) = (j - k) by A2, XREAL_1: 233;

      

      hence k = ((j - i) + l)

      .= ((j -' i) + l) by A1, XREAL_1: 233;

    end;

    theorem :: NAT_2:6

    i in ( Seg n) implies ((n -' i) + 1) in ( Seg n)

    proof

      

       A1: 1 <= ((n -' i) + 1) by NAT_1: 11;

      assume

       A2: i in ( Seg n);

      then 1 <= i by FINSEQ_1: 1;

      then (n - i) <= (n - 1) by XREAL_1: 13;

      then

       A3: ((n - i) + 1) <= n by XREAL_1: 19;

      i <= n by A2, FINSEQ_1: 1;

      then ((n -' i) + 1) <= n by A3, XREAL_1: 233;

      hence thesis by A1, FINSEQ_1: 1;

    end;

    theorem :: NAT_2:7

    j < i implies ((i -' (j + 1)) + 1) = (i -' j)

    proof

      assume

       A1: j < i;

      then (j + 1) <= i by NAT_1: 13;

      

      hence ((i -' (j + 1)) + 1) = ((i - (j + 1)) + 1) by XREAL_1: 233

      .= (i - j)

      .= (i -' j) by A1, XREAL_1: 233;

    end;

    theorem :: NAT_2:8

    

     Th8: i >= j implies (j -' i) = 0

    proof

      assume

       A1: i >= j;

      per cases by A1, XXREAL_0: 1;

        suppose i = j;

        hence thesis by XREAL_1: 232;

      end;

        suppose i > j;

        then (j - i) < 0 by XREAL_1: 49;

        hence thesis by XREAL_0:def 2;

      end;

    end;

    theorem :: NAT_2:9

    

     Th9: for i,j be non zero Nat holds (i -' j) < i

    proof

      let i,j be non zero Nat;

      per cases ;

        suppose

         A1: j <= i;

        (i - j) < (i - 0 ) by XREAL_1: 15;

        hence thesis by A1, XREAL_1: 233;

      end;

        suppose j > i;

        hence thesis by Th8;

      end;

    end;

    theorem :: NAT_2:10

    

     Th10: k <= n implies (2 to_power n) = ((2 to_power k) * (2 to_power (n -' k)))

    proof

      assume k <= n;

      then n = (k + (n -' k)) by XREAL_1: 235;

      hence thesis by POWER: 27;

    end;

    theorem :: NAT_2:11

    k <= n implies (2 to_power k) divides (2 to_power n)

    proof

      assume k <= n;

      then

       A2: (2 to_power n) = ((2 to_power k) * (2 to_power (n -' k))) by Th10;

      reconsider a = (2 to_power (n -' k)) as Nat by TARSKI: 1;

      take a;

      thus thesis by A2;

    end;

    theorem :: NAT_2:12

    

     Th12: k > 0 & (n div k) = 0 implies n < k

    proof

      assume that

       A1: k > 0 and

       A2: (n div k) = 0 ;

      ex t be Nat st n = ((k * (n div k)) + t) & t < k by A1, NAT_D:def 1;

      hence thesis by A2;

    end;

    theorem :: NAT_2:13

    k > 0 & k <= n implies (n div k) >= 1

    proof

      assume k > 0 & k <= n;

      then (n div k) <> 0 by Th12;

      then (n div k) >= ( 0 + 1) by NAT_1: 13;

      hence thesis;

    end;

    theorem :: NAT_2:14

    k <> 0 implies ((n + k) div k) = ((n div k) + 1)

    proof

      assume k <> 0 ;

      then

      consider t be Nat such that

       A1: n = ((k * (n div k)) + t) and

       A2: t < k by NAT_D:def 1;

      (n + k) = ((k * ((n div k) + 1)) + t) by A1;

      hence thesis by A2, NAT_D:def 1;

    end;

    theorem :: NAT_2:15

    k divides n & 1 <= n & 1 <= i & i <= k implies ((n -' i) div k) = ((n div k) - 1)

    proof

      assume that

       A1: k divides n and

       A2: 1 <= n and

       A3: 1 <= i and

       A4: i <= k;

      

       A5: (k -' i) < k by A3, A4, Th9;

      

       A6: k <= n by A1, A2, NAT_D: 7;

      then (i + k) <= (k + n) by A4, XREAL_1: 7;

      then

       A7: i <= n by XREAL_1: 6;

      (n div k) > 0

      proof

        assume not (n div k) > 0 ;

        then (n div k) = 0 ;

        hence contradiction by A3, A4, A6, Th12;

      end;

      then (n div k) >= ( 0 + 1) by NAT_1: 13;

      then

       A8: ((n div k) -' 1) = ((n div k) - 1) by XREAL_1: 233;

      n = (k * (n div k)) by A1, NAT_D: 3;

      

      then (n -' i) = ((((k * (n div k)) - (k * 1)) + k) - i) by A7, XREAL_1: 233

      .= ((k * ((n div k) -' 1)) + (k - i)) by A8

      .= ((k * ((n div k) -' 1)) + (k -' i)) by A4, XREAL_1: 233;

      hence thesis by A8, A5, NAT_D:def 1;

    end;

    theorem :: NAT_2:16

    k <= n implies ((2 to_power n) div (2 to_power k)) = (2 to_power (n -' k))

    proof

      assume k <= n;

      then (2 to_power k) > 0 & (2 to_power n) = ((2 to_power k) * (2 to_power (n -' k))) by Th10, POWER: 34;

      hence thesis by NAT_D: 18;

    end;

    theorem :: NAT_2:17

    n > 0 implies ((2 to_power n) mod 2) = 0

    proof

      assume n > 0 ;

      then

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

      (2 to_power n) = (2 to_power ((n - 1) + 1))

      .= (2 to_power ((n -' 1) + 1)) by A1, XREAL_1: 233

      .= ((2 to_power (n -' 1)) * (2 to_power 1)) by POWER: 27

      .= ((2 to_power (n -' 1)) * 2) by POWER: 25;

      hence thesis by NAT_D: 13;

    end;

    theorem :: NAT_2:18

    n > 0 implies ((n mod 2) = 0 iff ((n -' 1) mod 2) = 1)

    proof

      assume

       A1: n > 0 ;

      thus (n mod 2) = 0 implies ((n -' 1) mod 2) = 1

      proof

        consider t be Nat such that

         A2: n = ((2 * t) + (n mod 2)) and (n mod 2) < 2 by NAT_D:def 2;

        assume

         A3: (n mod 2) = 0 ;

        then t > 0 by A1, A2;

        then

         A4: t >= ( 0 + 1) by NAT_1: 13;

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

        

        then (n -' 1) = ((2 * ((t - 1) + 1)) - 1) by A3, A2, XREAL_1: 233

        .= ((2 * (t - 1)) + ((1 + 1) - 1))

        .= ((2 * (t -' 1)) + 1) by A4, XREAL_1: 233;

        hence thesis by NAT_D:def 2;

      end;

      assume ((n -' 1) mod 2) = 1;

      then

      consider t be Nat such that

       A5: (n -' 1) = ((2 * t) + 1) and 1 < 2 by NAT_D:def 2;

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

      

      then n = (((2 * t) + 1) + 1) by A5, XREAL_1: 235

      .= ((2 * (t + 1)) + 0 );

      hence thesis by NAT_D:def 2;

    end;

    theorem :: NAT_2:19

    for n be non zero Nat st n <> 1 holds n > 1

    proof

      let n be non zero Nat;

      

       A1: n >= 1 by NAT_1: 14;

      assume n <> 1;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: NAT_2:20

    n <= k & k < (n + n) implies (k div n) = 1

    proof

      assume that

       A1: n <= k and

       A2: k < (n + n);

      

       A3: k = (n + (k - n))

      .= ((n * 1) + (k -' n)) by A1, XREAL_1: 233;

      (k - n) < ((n + n) - n) by A2, XREAL_1: 9;

      hence thesis by A3, NAT_D:def 1;

    end;

    theorem :: NAT_2:21

    

     Th21: n is even iff (n mod 2) = 0

    proof

      thus n is even implies (n mod 2) = 0

      proof

        assume n is even;

        then

        consider k be Nat such that

         A1: n = (2 * k) by ABIAN:def 2;

        n = ((2 * k) + 0 ) by A1;

        hence thesis by NAT_D:def 2;

      end;

      assume (n mod 2) = 0 ;

      then ex k be Nat st n = ((2 * k) + 0 ) & 0 < 2 by NAT_D:def 2;

      hence thesis;

    end;

    theorem :: NAT_2:22

    n is odd iff (n mod 2) = 1 by Th21, NAT_D: 12;

    theorem :: NAT_2:23

    1 <= t & k <= n & (2 * t) divides k implies ((n div t) is even iff ((n -' k) div t) is even)

    proof

      assume that

       A1: 1 <= t and

       A2: k <= n and

       A3: (2 * t) divides k;

      consider r be Nat such that

       A4: k = ((2 * t) * r) by A3, NAT_D:def 3;

      thus (n div t) is even implies ((n -' k) div t) is even

      proof

        assume (n div t) is even;

        then

        consider p be Nat such that

         A5: (n div t) = (2 * p) by ABIAN:def 2;

        consider q be Nat such that

         A6: n = ((t * (2 * p)) + q) and

         A7: q < t by A1, A5, NAT_D:def 1;

        (1 * t) < (2 * t) by A1, XREAL_1: 68;

        then (t + q) < ((2 * t) + t) by A7, XREAL_1: 8;

        then q < (2 * t) by XREAL_1: 6;

        then (q / (2 * t)) < 1 by XREAL_1: 189;

        then

         A8: (p + (q / (2 * t))) < (p + 1) by XREAL_1: 6;

        consider r be Nat such that

         A9: k = ((2 * t) * r) by A3, NAT_D:def 3;

        

         A10: (2 * t) <> 0 by A1;

        then ((2 * t) * r) <= (((2 * t) * p) + ((q / (2 * t)) * (2 * t))) by A2, A6, A9, XCMPLX_1: 87;

        then ((2 * t) * r) <= ((2 * t) * (p + (q / (2 * t))));

        then r <= (p + (q / (2 * t))) by A10, XREAL_1: 68;

        then ((p + (q / (2 * t))) + r) < ((p + 1) + (p + (q / (2 * t)))) by A8, XREAL_1: 8;

        then r < (p + 1) by XREAL_1: 6;

        then

         A11: r <= p by NAT_1: 13;

        (n -' k) = (((t * (2 * p)) + q) - ((2 * t) * r)) by A2, A6, A9, XREAL_1: 233

        .= ((t * (2 * (p - r))) + q)

        .= ((t * (2 * (p -' r))) + q) by A11, XREAL_1: 233;

        hence thesis by A7, NAT_D:def 1;

      end;

      assume ((n -' k) div t) is even;

      then

      consider p be Nat such that

       A12: ((n -' k) div t) = (2 * p) by ABIAN:def 2;

      consider q be Nat such that

       A13: (n -' k) = ((t * (2 * p)) + q) and

       A14: q < t by A1, A12, NAT_D:def 1;

      (n - k) = ((t * (2 * p)) + q) by A2, A13, XREAL_1: 233;

      then n = ((t * (2 * (p + r))) + q) by A4;

      hence thesis by A14, NAT_D:def 1;

    end;

    theorem :: NAT_2:24

    

     Th24: n <= m implies (n div k) <= (m div k)

    proof

      assume that

       A1: n <= m and

       A2: (n div k) > (m div k);

      set r = ((n div k) -' (m div k));

      

       A3: r = ((n div k) - (m div k)) by A2, XREAL_1: 233;

      then r > ((m div k) - (m div k)) by A2, XREAL_1: 9;

      then r >= ( 0 + 1) by NAT_1: 13;

      then (k * r) >= (k * 1) by XREAL_1: 64;

      then

       A4: ((k * r) + (k * (m div k))) >= (k + (k * (m div k))) by XREAL_1: 6;

      per cases ;

        suppose

         A5: k <> 0 ;

        then ex t2 be Nat st m = ((k * (m div k)) + t2) & t2 < k by NAT_D:def 1;

        then m < (k + (k * (m div k))) by XREAL_1: 6;

        then (m - (k * (n div k))) < ((k + (k * (m div k))) - (k + (k * (m div k)))) by A3, A4, XREAL_1: 14;

        then

         A6: (m - (k * (n div k))) < 0 ;

        ex t1 be Nat st n = ((k * (n div k)) + t1) & t1 < k by A5, NAT_D:def 1;

        then (k * (n div k)) <= n by NAT_1: 11;

        then (m - n) < ((k * (n div k)) - (k * (n div k))) by A6, XREAL_1: 13;

        then m < ( 0 + n) by XREAL_1: 19;

        hence contradiction by A1;

      end;

        suppose k = 0 ;

        hence contradiction by A2, NAT_D:def 1;

      end;

    end;

    theorem :: NAT_2:25

    k <= (2 * n) implies ((k + 1) div 2) <= n

    proof

      assume k <= (2 * n);

      then (k + 1) <= ((2 * n) + 1) by XREAL_1: 6;

      then ((k + 1) div 2) <= (((2 * n) + 1) div 2) by Th24;

      hence thesis by NAT_D:def 1;

    end;

    theorem :: NAT_2:26

    n is even implies (n div 2) = ((n + 1) div 2)

    proof

      assume

       A1: n is even;

      n = ((2 * (n div 2)) + (n mod 2)) by NAT_D: 2

      .= ((2 * (n div 2)) + 0 ) by A1, Th21;

      hence thesis by NAT_D:def 1;

    end;

    theorem :: NAT_2:27

    ((n div k) div i) = (n div (k * i))

    proof

      now

        per cases ;

          suppose

           A1: i = 0 ;

          

          hence ((n div k) div i) = 0 by NAT_D:def 1

          .= (n div (k * i)) by A1, NAT_D:def 1;

        end;

          suppose

           A2: i <> 0 ;

          now

            per cases ;

              suppose

               A3: k = 0 ;

              then (n div k) = 0 by NAT_D:def 1;

              hence thesis by A3, Th2;

            end;

              suppose

               A4: k <> 0 ;

              consider t2 be Nat such that

               A5: (n div k) = ((i * ((n div k) div i)) + t2) and

               A6: t2 < i by A2, NAT_D:def 1;

              (t2 + 1) <= i by A6, NAT_1: 13;

              then

               A7: (k * (t2 + 1)) <= (k * i) by XREAL_1: 64;

              consider t1 be Nat such that

               A8: n = ((k * (n div k)) + t1) and

               A9: t1 < k by A4, NAT_D:def 1;

              ((k * t2) + t1) < ((k * t2) + (k * 1)) by A9, XREAL_1: 6;

              then (((k * t2) + t1) - (k * i)) < ((k * (t2 + 1)) - (k * (t2 + 1))) by A7, XREAL_1: 14;

              then

               A10: ((k * t2) + t1) < ( 0 + (k * i)) by XREAL_1: 19;

              n = (((k * i) * ((n div k) div i)) + ((k * t2) + t1)) by A8, A5;

              hence thesis by A10, NAT_D:def 1;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    definition

      let n be Nat;

      :: original: trivial

      redefine

      :: NAT_2:def1

      attr n is trivial means

      : Def1: n = 0 or n = 1;

      compatibility

      proof

        thus n is trivial implies n = 0 or n = 1

        proof

          assume

           A1: n is trivial;

          assume that

           A2: n <> 0 and

           A3: n <> 1;

          

           A4: n > (1 + 0 ) by A2, A3, NAT_1: 25;

          reconsider n as Nat;

          consider x be object such that

           A5: n = {x} by A1, A2, ZFMISC_1: 131;

          

           A6: n = { k where k be Nat : k < n } by AXIOMS: 4;

          then

           A7: 1 in n by A4;

           0 in n by A2, A6;

          then 0 = x by A5, TARSKI:def 1;

          hence contradiction by A7, A5, TARSKI:def 1;

        end;

        assume n = 0 or n = 1;

        hence thesis by CARD_1: 49;

      end;

    end

    registration

      cluster non trivial for Nat;

      existence

      proof

        take 2;

        thus thesis;

      end;

    end

    theorem :: NAT_2:28

    k is non trivial iff k is non empty & k <> 1;

    theorem :: NAT_2:29

    for k be non trivial Nat holds k >= 2

    proof

      let k be non trivial Nat;

      k >= 1 by NAT_1: 14;

      then k > 1 or k = 1 by XXREAL_0: 1;

      then k >= (1 + 1) by Def1, NAT_1: 13;

      hence thesis;

    end;

    scheme :: NAT_2:sch2

    Indfrom2 { P[ set] } :

for k be non trivial Nat holds P[k]

      provided

       A1: P[2]

       and

       A2: for k be non trivial Nat st P[k] holds P[(k + 1)];

      defpred P[ non zero Nat] means $1 is non trivial implies P[$1];

       A3:

      now

        let k be non zero Nat;

        assume

         A4: P[k];

        now

          assume (k + 1) is non trivial;

          per cases ;

            suppose k = 1;

            hence P[(k + 1)] by A1;

          end;

            suppose k <> 1;

            then k is non trivial;

            hence P[(k + 1)] by A2, A4;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A5: P[1] by Def1;

      for k be non zero Nat holds P[k] from NAT_1:sch 10( A5, A3);

      hence thesis;

    end;

    begin

    theorem :: NAT_2:30

    ((i -' j) -' k) = (i -' (j + k))

    proof

      per cases ;

        suppose

         A1: i <= j;

        

        hence ((i -' j) -' k) = ( 0 -' k) by Th8

        .= 0 by Th8

        .= (i -' (j + k)) by A1, Th8, NAT_1: 12;

      end;

        suppose

         A2: j <= i & (i - j) <= k;

        then

         A3: i <= (j + k) by XREAL_1: 20;

        (i -' j) = (i - j) by A2, XREAL_1: 233;

        

        hence ((i -' j) -' k) = 0 by A2, Th8

        .= (i -' (j + k)) by A3, Th8;

      end;

        suppose

         A4: j <= i & k <= (i - j);

        then

         A5: (k + j) <= i by XREAL_1: 19;

        (i -' j) = (i - j) by A4, XREAL_1: 233;

        

        hence ((i -' j) -' k) = ((i - j) - k) by A4, XREAL_1: 233

        .= (i - (j + k))

        .= (i -' (j + k)) by A5, XREAL_1: 233;

      end;

    end;