arytm_1.miz

    begin

    reserve x,y,z for Element of REAL+ ;

    theorem :: ARYTM_1:1



     Th1: (x + y) = y implies x = {}

    proof

      reconsider o = {} as Element of REAL+ by ARYTM_2: 20;

      assume (x + y) = y;

      then (x + y) = (y + o) by ARYTM_2:def 8;

      hence thesis by ARYTM_2: 11;

    end;



     Lm1: (x *' y) = (x *' z) & x <> {} implies y = z

    proof

      assume

       A1: (x *' y) = (x *' z);

      assume x <> {} ;

      then

      consider x1 be Element of REAL+ such that

       A2: (x *' x1) = one by ARYTM_2: 14;



      thus y = ((x *' x1) *' y) by A2, ARYTM_2: 15

      .= (x1 *' (x *' z)) by A1, ARYTM_2: 12

      .= ((x *' x1) *' z) by ARYTM_2: 12

      .= z by A2, ARYTM_2: 15;

    end;

    theorem :: ARYTM_1:2

    (x *' y) = {} implies x = {} or y = {}

    proof

      assume

       A1: (x *' y) = {} ;

      assume x <> {} ;

      then

      consider x1 be Element of REAL+ such that

       A2: (x *' x1) = one by ARYTM_2: 14;



      thus y = ((x *' x1) *' y) by A2, ARYTM_2: 15

      .= ((x *' y) *' x1) by ARYTM_2: 12

      .= {} by A1, ARYTM_2: 4;

    end;

    theorem :: ARYTM_1:3



     Th3: x <=' y & y <=' z implies x <=' z

    proof

      assume x <=' y;

      then

      consider z1 be Element of REAL+ such that

       A1: (x + z1) = y by ARYTM_2: 9;

      assume y <=' z;

      then

      consider z2 be Element of REAL+ such that

       A2: (y + z2) = z by ARYTM_2: 9;

      z = (x + (z1 + z2)) by A1, A2, ARYTM_2: 6;

      hence thesis by ARYTM_2: 19;

    end;

    theorem :: ARYTM_1:4



     Th4: x <=' y & y <=' x implies x = y

    proof

      assume x <=' y;

      then

      consider z1 be Element of REAL+ such that

       A1: (x + z1) = y by ARYTM_2: 9;

      assume y <=' x;

      then

      consider z2 be Element of REAL+ such that

       A2: (y + z2) = x by ARYTM_2: 9;

      x = (x + (z1 + z2)) by A1, A2, ARYTM_2: 6;

      then z1 = {} by Th1, ARYTM_2: 5;

      hence thesis by A1, ARYTM_2:def 8;

    end;

    theorem :: ARYTM_1:5



     Th5: x <=' y & y = {} implies x = {}

    proof

      assume x <=' y;

      then ex z be Element of REAL+ st (x + z) = y by ARYTM_2: 9;

      hence thesis by ARYTM_2: 5;

    end;

    theorem :: ARYTM_1:6



     Th6: x = {} implies x <=' y

    proof

      assume x = {} ;

      then (x + y) = y by ARYTM_2:def 8;

      hence thesis by ARYTM_2: 19;

    end;

    theorem :: ARYTM_1:7



     Th7: x <=' y iff (x + z) <=' (y + z)

    proof

      thus x <=' y implies (x + z) <=' (y + z)

      proof

        assume x <=' y;

        then

        consider z0 be Element of REAL+ such that

         A1: (x + z0) = y by ARYTM_2: 9;

        ((x + z) + z0) = (y + z) by A1, ARYTM_2: 6;

        hence thesis by ARYTM_2: 19;

      end;

      assume (x + z) <=' (y + z);

      then

      consider z0 be Element of REAL+ such that

       A2: ((x + z) + z0) = (y + z) by ARYTM_2: 9;

      (y + z) = ((x + z0) + z) by A2, ARYTM_2: 6;

      hence thesis by ARYTM_2: 11, ARYTM_2: 19;

    end;

    theorem :: ARYTM_1:8



     Th8: x <=' y implies (x *' z) <=' (y *' z)

    proof

      assume x <=' y;

      then

      consider z0 be Element of REAL+ such that

       A1: (x + z0) = y by ARYTM_2: 9;

      (y *' z) = ((x *' z) + (z0 *' z)) by A1, ARYTM_2: 13;

      hence thesis by ARYTM_2: 19;

    end;



     Lm2: (x *' y) <=' (x *' z) & x <> {} implies y <=' z

    proof

      reconsider u = one as Element of REAL+ by ARYTM_2: 20;

      assume (x *' y) <=' (x *' z);

      then

      consider z0 be Element of REAL+ such that

       A1: ((x *' y) + z0) = (x *' z) by ARYTM_2: 9;

      assume

       A2: x <> {} ;

      then

      consider x1 be Element of REAL+ such that

       A3: (x *' x1) = one by ARYTM_2: 14;

      (x *' z) = ((x *' y) + (u *' z0)) by A1, ARYTM_2: 15

      .= ((x *' y) + (x *' (x1 *' z0))) by A3, ARYTM_2: 12

      .= (x *' (y + (x1 *' z0))) by ARYTM_2: 13;

      hence thesis by A2, Lm1, ARYTM_2: 19;

    end;

    definition

      let x,y be Element of REAL+ ;

      :: ARYTM_1:def1

      func x -' y -> Element of REAL+ means

      : Def1: (it + y) = x if y <=' x

      otherwise it = {} ;

      existence

      proof

        hereby

          assume y <=' x;

          then ex IT be Element of REAL+ st (y + IT) = x by ARYTM_2: 9;

          hence ex IT be Element of REAL+ st (IT + y) = x;

        end;

        thus thesis by ARYTM_2: 20;

      end;

      correctness by ARYTM_2: 11;

    end



     Lm3: (x -' x) = {}

    proof

      x <=' x;

      then ((x -' x) + x) = x by Def1;

      hence thesis by Th1;

    end;

    theorem :: ARYTM_1:9



     Th9: x <=' y or (x -' y) <> {}

    proof

      assume

       A1: not x <=' y;

      assume

       A2: (x -' y) = {} ;

      ((x -' y) + y) = x by A1, Def1;

      then x = y by A2, ARYTM_2:def 8;

      hence contradiction by A1;

    end;

    theorem :: ARYTM_1:10

    x <=' y & (y -' x) = {} implies x = y

    proof

      assume

       A1: x <=' y;

      assume (y -' x) = {} ;

      then y <=' x by Th9;

      hence thesis by A1, Th4;

    end;

    theorem :: ARYTM_1:11



     Th11: (x -' y) <=' x

    proof

      per cases ;

        suppose y <=' x;

        then ((x -' y) + y) = x by Def1;

        hence thesis by ARYTM_2: 19;

      end;

        suppose not y <=' x;

        then (x -' y) = {} by Def1;

        hence thesis by Th6;

      end;

    end;



     Lm4: x = {} implies (y -' x) = y

    proof

      assume

       A1: x = {} ;

      then

       A2: x <=' y by Th6;



      thus (y -' x) = ((y -' x) + x) by A1, ARYTM_2:def 8

      .= y by A2, Def1;

    end;



     Lm5: ((x + y) -' y) = x

    proof

      y <=' (x + y) by ARYTM_2: 19;

      hence thesis by Def1;

    end;



     Lm6: x <=' y implies (y -' (y -' x)) = x

    proof

      assume

       A1: x <=' y;

      (y -' x) <=' y by Th11;



      then ((y -' (y -' x)) + (y -' x)) = y by Def1

      .= ((y -' x) + x) by A1, Def1;

      hence thesis by ARYTM_2: 11;

    end;



     Lm7: (z -' y) <=' x iff z <=' (x + y)

    proof

      per cases ;

        suppose y <=' z;

        then ((z -' y) + y) = z by Def1;

        hence thesis by Th7;

      end;

        suppose

         A1: not y <=' z;



         A2: y <=' (x + y) by ARYTM_2: 19;

        (z -' y) = {} by A1, Def1;

        hence thesis by A1, A2, Th3, Th6;

      end;

    end;



     Lm8: y <=' x implies ((z + y) <=' x iff z <=' (x -' y))

    proof

      assume y <=' x;

      then ((x -' y) + y) = x by Def1;

      hence thesis by Th7;

    end;



     Lm9: ((z -' y) -' x) = (z -' (x + y))

    proof

      per cases ;

        suppose

         A1: (x + y) <=' z;

        y <=' (x + y) by ARYTM_2: 19;

        then

         A2: y <=' z by A1, Th3;

        then

         A3: x <=' (z -' y) by A1, Lm8;

        (((z -' y) -' x) + (x + y)) = ((((z -' y) -' x) + x) + y) by ARYTM_2: 6

        .= ((z -' y) + y) by A3, Def1

        .= z by A2, Def1;

        hence thesis by A1, Def1;

      end;

        suppose

         A4: x = {} ;



        hence ((z -' y) -' x) = (z -' y) by Lm4

        .= (z -' (x + y)) by A4, ARYTM_2:def 8;

      end;

        suppose that

         A5: not y <=' z and

         A6: x <> {} ;

        y <=' (y + x) by ARYTM_2: 19;

        then

         A7: not (x + y) <=' z by A5, Th3;

        now

          assume

           A8: x <=' (z -' y);

          (z -' y) = {} by A5, Def1;

          hence contradiction by A6, A8, Th5;

        end;



        hence ((z -' y) -' x) = {} by Def1

        .= (z -' (x + y)) by A7, Def1;

      end;

        suppose that

         A9: not (x + y) <=' z and

         A10: y <=' z;

         not x <=' (z -' y) by A9, A10, Lm8;



        hence ((z -' y) -' x) = {} by Def1

        .= (z -' (x + y)) by A9, Def1;

      end;

    end;



     Lm10: ((y -' z) -' x) = ((y -' x) -' z)

    proof



      thus ((y -' z) -' x) = (y -' (x + z)) by Lm9

      .= ((y -' x) -' z) by Lm9;

    end;

    theorem :: ARYTM_1:12

    y <=' x & y <=' z implies (x + (z -' y)) = ((x -' y) + z)

    proof

      assume that

       A1: y <=' x and

       A2: y <=' z;

      ((x + (z -' y)) + y) = (x + ((z -' y) + y)) by ARYTM_2: 6

      .= (x + z) by A2, Def1

      .= (((x -' y) + y) + z) by A1, Def1

      .= (((x -' y) + z) + y) by ARYTM_2: 6;

      hence thesis by ARYTM_2: 11;

    end;

    theorem :: ARYTM_1:13



     Th13: z <=' y implies (x + (y -' z)) = ((x + y) -' z)

    proof

      assume

       A1: z <=' y;

      y <=' (x + y) by ARYTM_2: 19;

      then

       A2: z <=' (x + y) by A1, Th3;

      ((x + (y -' z)) + z) = (x + ((y -' z) + z)) by ARYTM_2: 6

      .= (x + y) by A1, Def1

      .= (((x + y) -' z) + z) by A2, Def1;

      hence thesis by ARYTM_2: 11;

    end;



     Lm11: y <=' z implies (x -' (z -' y)) = ((x + y) -' z)

    proof

      assume

       A1: y <=' z;

      per cases ;

        suppose

         A2: (z -' y) <=' x;

        then

         A3: z <=' (x + y) by Lm7;

        ((x -' (z -' y)) + (z -' y)) = x by A2, Def1

        .= ((x + z) -' z) by Lm5

        .= ((x + (y + (z -' y))) -' z) by A1, Def1

        .= (((x + y) + (z -' y)) -' z) by ARYTM_2: 6

        .= (((x + y) -' z) + (z -' y)) by A3, Th13;

        hence thesis by ARYTM_2: 11;

      end;

        suppose

         A4: not (z -' y) <=' x;

        then

         A5: not z <=' (x + y) by Lm7;



        thus (x -' (z -' y)) = {} by A4, Def1

        .= ((x + y) -' z) by A5, Def1;

      end;

    end;



     Lm12: z <=' x & y <=' z implies (x -' (z -' y)) = ((x -' z) + y)

    proof

      assume that

       A1: z <=' x and

       A2: y <=' z;



      thus (x -' (z -' y)) = ((x + y) -' z) by A2, Lm11

      .= ((x -' z) + y) by A1, Th13;

    end;



     Lm13: x <=' z & y <=' z implies (x -' (z -' y)) = (y -' (z -' x))

    proof

      assume that

       A1: x <=' z and

       A2: y <=' z;



      thus (x -' (z -' y)) = ((x + y) -' z) by A2, Lm11

      .= (y -' (z -' x)) by A1, Lm11;

    end;

    theorem :: ARYTM_1:14

    z <=' x & y <=' z implies ((x -' z) + y) = (x -' (z -' y))

    proof

      assume that

       A1: z <=' x and

       A2: y <=' z;



      thus (x -' (z -' y)) = ((x + y) -' z) by A2, Lm11

      .= ((x -' z) + y) by A1, Th13;

    end;

    theorem :: ARYTM_1:15

    y <=' x & y <=' z implies ((z -' y) + x) = ((x -' y) + z)

    proof

      assume that

       A1: y <=' x and

       A2: y <=' z;

      (((z -' y) + x) + y) = (((z -' y) + y) + x) by ARYTM_2: 6

      .= (z + x) by A2, Def1

      .= (((x -' y) + y) + z) by A1, Def1

      .= (((x -' y) + z) + y) by ARYTM_2: 6;

      hence thesis by ARYTM_2: 11;

    end;

    theorem :: ARYTM_1:16

    x <=' y implies (z -' y) <=' (z -' x)

    proof

      assume

       A1: x <=' y;

      per cases ;

        suppose

         A2: y <=' z;

        ((z -' y) + x) <=' ((z -' y) + y) by A1, Th7;

        then

         A3: ((z -' y) + x) <=' z by A2, Def1;

        x <=' z by A1, A2, Th3;

        then ((z -' y) + x) <=' ((z -' x) + x) by A3, Def1;

        hence thesis by Th7;

      end;

        suppose not y <=' z;

        then (z -' y) = {} by Def1;

        hence thesis by Th6;

      end;

    end;

    theorem :: ARYTM_1:17

    x <=' y implies (x -' z) <=' (y -' z)

    proof

      assume

       A1: x <=' y;

      per cases ;

        suppose

         A2: z <=' x;

        then z <=' y by A1, Th3;

        then

         A3: ((y -' z) + z) = y by Def1;

        ((x -' z) + z) = x by A2, Def1;

        hence thesis by A1, A3, Th7;

      end;

        suppose not z <=' x;

        then (x -' z) = {} by Def1;

        hence thesis by Th6;

      end;

    end;



     Lm14: (x *' (y -' z)) = ((x *' y) -' (x *' z))

    proof

      per cases ;

        suppose

         A1: z <=' y;

        then

         A2: (x *' z) <=' (x *' y) by Th8;

        ((x *' (y -' z)) + (x *' z)) = (x *' ((y -' z) + z)) by ARYTM_2: 13

        .= (x *' y) by A1, Def1

        .= (((x *' y) -' (x *' z)) + (x *' z)) by A2, Def1;

        hence thesis by ARYTM_2: 11;

      end;

        suppose

         A3: x = {} ;

        then (x *' y) = {} by ARYTM_2: 4;



        hence (x *' (y -' z)) = (x *' y) by A3, ARYTM_2: 4

        .= ((x *' y) -' (x *' z)) by A3, Lm4, ARYTM_2: 4;

      end;

        suppose

         A4: not z <=' y & x <> {} ;

        then

         A5: not (x *' z) <=' (x *' y) by Lm2;

        (y -' z) = {} by A4, Def1;



        hence (x *' (y -' z)) = {} by ARYTM_2: 4

        .= ((x *' y) -' (x *' z)) by A5, Def1;

      end;

    end;

    definition

      let x,y be Element of REAL+ ;

      :: ARYTM_1:def2

      func x - y -> set equals

      : Def2: (x -' y) if y <=' x

      otherwise [ {} , (y -' x)];

      correctness by TARSKI: 1;

    end

    theorem :: ARYTM_1:18

    (x - x) = {}

    proof

      x <=' x;

      then (x - x) = (x -' x) by Def2;

      hence thesis by Lm3;

    end;

    theorem :: ARYTM_1:19

    x = {} & y <> {} implies (x - y) = [ {} , y]

    proof

      assume that

       A1: x = {} and

       A2: y <> {} ;

      x <=' y by A1, Th6;

      then not y <=' x by A1, A2, Th4;



      hence (x - y) = [ {} , (y -' x)] by Def2

      .= [ {} , y] by A1, Lm4;

    end;

    theorem :: ARYTM_1:20

    z <=' y implies (x + (y -' z)) = ((x + y) - z)

    proof

      assume

       A1: z <=' y;

      y <=' (x + y) by ARYTM_2: 19;

      then z <=' (x + y) by A1, Th3;

      then ((x + y) - z) = ((x + y) -' z) by Def2;

      hence thesis by A1, Th13;

    end;

    theorem :: ARYTM_1:21

     not z <=' y implies (x - (z -' y)) = ((x + y) - z)

    proof

      assume

       A1: not z <=' y;

      per cases ;

        suppose

         A2: (z -' y) <=' x;

        then z <=' (x + y) by Lm7;

        then

         A3: ((x + y) - z) = ((x + y) -' z) by Def2;

        (x - (z -' y)) = (x -' (z -' y)) by A2, Def2;

        hence thesis by A1, A3, Lm11;

      end;

        suppose

         A4: not (z -' y) <=' x;

        then

         A5: not z <=' (x + y) by Lm7;

        ((z -' y) -' x) = (z -' (x + y)) by Lm9;



        hence (x - (z -' y)) = [ {} , (z -' (x + y))] by A4, Def2

        .= ((x + y) - z) by A5, Def2;

      end;

    end;

    theorem :: ARYTM_1:22

    y <=' x & not y <=' z implies (x - (y -' z)) = ((x -' y) + z)

    proof

      assume that

       A1: y <=' x and

       A2: not y <=' z;

      (y -' z) <=' y by Th11;

      then (y -' z) <=' x by A1, Th3;

      then (x - (y -' z)) = (x -' (y -' z)) by Def2;

      hence thesis by A1, A2, Lm12;

    end;

    theorem :: ARYTM_1:23

     not y <=' x & not y <=' z implies (x - (y -' z)) = (z - (y -' x))

    proof

      assume

       A1: ( not y <=' x) & not y <=' z;

      per cases ;

        suppose

         A2: y <=' (x + z);

        then (y -' x) <=' z by Lm7;

        then

         A3: (z - (y -' x)) = (z -' (y -' x)) by Def2;

        (y -' z) <=' x by A2, Lm7;

        then (x - (y -' z)) = (x -' (y -' z)) by Def2;

        hence thesis by A1, A3, Lm13;

      end;

        suppose

         A4: not y <=' (x + z);

        then

         A5: not (y -' x) <=' z by Lm7;



         A6: ((y -' z) -' x) = ((y -' x) -' z) by Lm10;

         not (y -' z) <=' x by A4, Lm7;



        hence (x - (y -' z)) = [ {} , ((y -' x) -' z)] by A6, Def2

        .= (z - (y -' x)) by A5, Def2;

      end;

    end;

    theorem :: ARYTM_1:24

    y <=' x implies (x - (y + z)) = ((x -' y) - z)

    proof

      assume

       A1: y <=' x;

      per cases ;

        suppose

         A2: (y + z) <=' x;

        then z <=' (x -' y) by A1, Lm8;

        then

         A3: ((x -' y) - z) = ((x -' y) -' z) by Def2;

        (x - (y + z)) = (x -' (y + z)) by A2, Def2;

        hence thesis by A3, Lm9;

      end;

        suppose that

         A4: not (y + z) <=' x and

         A5: x <=' y;



         A6: not z <=' (x -' y) by A1, A4, Lm8;



         A7: ((x + z) -' x) = z by Lm5

        .= (z -' (x -' x)) by Lm3, Lm4;

        x = y by A1, A5, Th4;



        hence (x - (y + z)) = [ {} , (z -' (x -' y))] by A4, A7, Def2

        .= ((x -' y) - z) by A6, Def2;

      end;

        suppose that

         A8: not (y + z) <=' x and

         A9: not x <=' y;



         A10: not z <=' (x -' y) by A1, A8, Lm8;

        ((y + z) -' x) = (z -' (x -' y)) by A9, Lm11;



        hence (x - (y + z)) = [ {} , (z -' (x -' y))] by A8, Def2

        .= ((x -' y) - z) by A10, Def2;

      end;

    end;

    theorem :: ARYTM_1:25

    x <=' y & z <=' y implies ((y -' z) - x) = ((y -' x) - z)

    proof

      assume that

       A1: x <=' y and

       A2: z <=' y;

      per cases ;

        suppose

         A3: (x + z) <=' y;

        then z <=' (y -' x) by A1, Lm8;

        then

         A4: ((y -' x) -' z) = ((y -' x) - z) by Def2;

        x <=' (y -' z) by A2, A3, Lm8;

        then ((y -' z) -' x) = ((y -' z) - x) by Def2;

        hence thesis by A4, Lm10;

      end;

        suppose that

         A5: not (x + z) <=' y and

         A6: y <=' x;



         A7: not x <=' (y -' z) by A2, A5, Lm8;



         A8: not z <=' (y -' x) by A1, A5, Lm8;



         A9: x = y by A1, A6, Th4;



        then (x -' (x -' z)) = z by A2, Lm6

        .= (z -' (x -' x)) by Lm3, Lm4;



        hence ((y -' z) - x) = [ {} , (z -' (y -' x))] by A7, A9, Def2

        .= ((y -' x) - z) by A8, Def2;

      end;

        suppose that

         A10: not (x + z) <=' y and

         A11: y <=' z;



         A12: not x <=' (y -' z) by A2, A10, Lm8;



         A13: not z <=' (y -' x) by A1, A10, Lm8;



         A14: z = y by A2, A11, Th4;

        (x -' (z -' z)) = x by Lm3, Lm4

        .= (z -' (z -' x)) by A1, A14, Lm6;



        hence ((y -' z) - x) = [ {} , (z -' (y -' x))] by A12, A14, Def2

        .= ((y -' x) - z) by A13, Def2;

      end;

        suppose that

         A15: not (x + z) <=' y and

         A16: not y <=' x & not y <=' z;



         A17: not z <=' (y -' x) by A1, A15, Lm8;

        ( not x <=' (y -' z)) & (x -' (y -' z)) = (z -' (y -' x)) by A15, A16, Lm8, Lm13;



        hence ((y -' z) - x) = [ {} , (z -' (y -' x))] by Def2

        .= ((y -' x) - z) by A17, Def2;

      end;

    end;

    theorem :: ARYTM_1:26

    z <=' y implies (x *' (y -' z)) = ((x *' y) - (x *' z))

    proof

      assume z <=' y;

      then (x *' z) <=' (x *' y) by Th8;

      then ((x *' y) - (x *' z)) = ((x *' y) -' (x *' z)) by Def2;

      hence thesis by Lm14;

    end;

    theorem :: ARYTM_1:27



     Th27: not z <=' y & x <> {} implies [ {} , (x *' (z -' y))] = ((x *' y) - (x *' z))

    proof

      assume ( not z <=' y) & x <> {} ;

      then

       A1: not (x *' z) <=' (x *' y) by Lm2;



      thus [ {} , (x *' (z -' y))] = [ {} , ((x *' z) -' (x *' y))] by Lm14

      .= ((x *' y) - (x *' z)) by A1, Def2;

    end;

    theorem :: ARYTM_1:28

    (y -' z) <> {} & z <=' y & x <> {} implies ((x *' z) - (x *' y)) = [ {} , (x *' (y -' z))]

    proof

      assume (y -' z) <> {} ;

      then

       A1: y <> z by Lm3;

      assume z <=' y;

      then not y <=' z by A1, Th4;

      hence thesis by Th27;

    end;