arithm.miz



    begin

    reserve x for Complex;

    theorem :: ARITHM:1

    

     Th1: (x + 0 ) = x

    proof

       0 in NAT ;

      then

      reconsider Z = 0 as Element of REAL by NUMBERS: 19;

      x in COMPLEX by XCMPLX_0:def 2;

      then

      consider x1,x2 be Element of REAL such that

       A1: x = [*x1, x2*] by ARYTM_0: 9;

       0 = [*Z, Z*] by ARYTM_0:def 5;

      

      then (x + 0 ) = [*( + (x1,Z)), ( + (x2,Z))*] by A1, XCMPLX_0:def 4

      .= [*x1, ( + (x2,Z))*] by ARYTM_0: 11

      .= x by A1, ARYTM_0: 11;

      hence thesis;

    end;

    

     Lm1: ( - 0 ) = 0

    proof

      ( 0 + ( - 0 )) = ( - 0 ) by Th1;

      hence thesis by XCMPLX_0:def 6;

    end;

    theorem :: ARITHM:2

    

     Th2: (x * 0 ) = 0

    proof

       0 in NAT ;

      then

      reconsider Z = 0 as Element of REAL by NUMBERS: 19;

      x in COMPLEX by XCMPLX_0:def 2;

      then

      consider x1,x2 be Element of REAL such that

       A1: x = [*x1, x2*] by ARYTM_0: 9;

      ( + (Z,Z)) = 0 by ARYTM_0: 11;

      then

       Lm2: ( opp Z) = 0 by ARYTM_0:def 3;

       0 = [*Z, Z*] by ARYTM_0:def 5;

      

      then (x * 0 ) = [*( + (( * (x1,Z)),( opp ( * (x2,Z))))), ( + (( * (x1,Z)),( * (x2,Z))))*] by A1, XCMPLX_0:def 5

      .= [*( + (( * (x1,Z)),( opp Z))), ( + (( * (x1,Z)),( * (x2,Z))))*] by ARYTM_0: 12

      .= [*( + (( * (x1,Z)),( opp Z))), ( + (( * (x1,Z)),Z))*] by ARYTM_0: 12

      .= [*( + (Z,( opp Z))), ( + (( * (x1,Z)),Z))*] by ARYTM_0: 12

      .= [*( + (Z,( opp Z))), ( + (Z,Z))*] by ARYTM_0: 12

      .= [*( + (Z,( opp Z))), Z*] by ARYTM_0: 11

      .= [*( opp Z), Z*] by ARYTM_0: 11

      .= 0 by Lm2, ARYTM_0:def 5;

      hence thesis;

    end;

    theorem :: ARITHM:3

    

     Th3: (1 * x) = x

    proof

       0 in NAT & 1 in NAT ;

      then

      reconsider Z = 0 , J = 1 as Element of REAL by NUMBERS: 19;

      ( + (Z,Z)) = 0 by ARYTM_0: 11;

      then

       Lm2: ( opp Z) = 0 by ARYTM_0:def 3;

      x in COMPLEX by XCMPLX_0:def 2;

      then

      consider x1,x2 be Element of REAL such that

       A1: x = [*x1, x2*] by ARYTM_0: 9;

      1 = [*J, Z*] by ARYTM_0:def 5;

      

      then (x * 1) = [*( + (( * (x1,J)),( opp ( * (x2,Z))))), ( + (( * (x1,Z)),( * (x2,J))))*] by A1, XCMPLX_0:def 5

      .= [*( + (( * (x1,J)),( opp Z))), ( + (( * (x1,Z)),( * (x2,J))))*] by ARYTM_0: 12

      .= [*( + (x1,( opp Z))), ( + (( * (x1,Z)),( * (x2,J))))*] by ARYTM_0: 19

      .= [*( + (x1,( opp Z))), ( + (( * (x1,Z)),x2))*] by ARYTM_0: 19

      .= [*( + (x1,Z)), ( + (Z,x2))*] by Lm2, ARYTM_0: 12

      .= [*x1, ( + (Z,x2))*] by ARYTM_0: 11

      .= x by A1, ARYTM_0: 11;

      hence thesis;

    end;

    theorem :: ARITHM:4

    (x - 0 ) = x

    proof

      (x - 0 ) = (x + 0 ) by Lm1, XCMPLX_0:def 8;

      hence thesis by Th1;

    end;

    theorem :: ARITHM:5

    ( 0 / x) = 0

    proof

      ( 0 / x) = ( 0 * (x " )) by XCMPLX_0:def 9;

      hence thesis by Th2;

    end;

    

     Lm3: (1 " ) = 1

    proof

      (1 * (1 " )) = (1 " ) by Th3;

      hence thesis by XCMPLX_0:def 7;

    end;

    theorem :: ARITHM:6

    (x / 1) = x

    proof

      (x / 1) = (x * 1) by Lm3, XCMPLX_0:def 9;

      hence thesis by Th3;

    end;