:: ARITHM semantic presentation

begin

theorem Th1: :: ARITHM:1
for x being complex number holds x + 0 = x
proof
let x be complex number ; ::_thesis: x + 0 = x
 x in COMPLEX by XCMPLX_0:def_2;
then consider x1, x2 being Element of REAL  such that
A1: x = [*x1,x2*] by ARYTM_0:9;
 0 = [*0,0*] by ARYTM_0:def_5;
then x + 0 = [*(+ (x1,0)),(+ (x2,0))*] by A1, XCMPLX_0:def_4
.= [*x1,(+ (x2,0))*] by ARYTM_0:11
.= x by A1, ARYTM_0:11 ;
hence  x + 0 = x ; ::_thesis: verum
end;

Lm1:  - 0 = 0
proof
 0 + (- 0) = - 0 by Th1;
hence  - 0 = 0 by XCMPLX_0:def_6; ::_thesis: verum
end;

Lm2:  opp 0 = 0
proof
 + (0,0) = 0 by ARYTM_0:11;
hence  opp 0 = 0 by ARYTM_0:def_3; ::_thesis: verum
end;

theorem Th2: :: ARITHM:2
for x being complex number holds x * 0 = 0
proof
let x be complex number ; ::_thesis: x * 0 = 0
 x in COMPLEX by XCMPLX_0:def_2;
then consider x1, x2 being Element of REAL  such that
A1: x = [*x1,x2*] by ARYTM_0:9;
 0 = [*0,0*] by ARYTM_0:def_5;
then x * 0 = [*(+ ((* (x1,0)),(opp (* (x2,0))))),(+ ((* (x1,0)),(* (x2,0))))*] by A1, XCMPLX_0:def_5
.= [*(+ ((* (x1,0)),(opp 0))),(+ ((* (x1,0)),(* (x2,0))))*] by ARYTM_0:12
.= [*(+ ((* (x1,0)),(opp 0))),(+ ((* (x1,0)),0))*] by ARYTM_0:12
.= [*(+ (0,(opp 0))),(+ ((* (x1,0)),0))*] by ARYTM_0:12
.= [*(+ (0,(opp 0))),(+ (0,0))*] by ARYTM_0:12
.= [*(+ (0,(opp 0))),0*] by ARYTM_0:11
.= [*(opp 0),0*] by ARYTM_0:11
.= 0 by Lm2, ARYTM_0:def_5 ;
hence  x * 0 = 0 ; ::_thesis: verum
end;

theorem Th3: :: ARITHM:3
for x being complex number holds 1 * x = x
proof
let x be complex number ; ::_thesis: 1 * x = x
 x in COMPLEX by XCMPLX_0:def_2;
then consider x1, x2 being Element of REAL  such that
A1: x = [*x1,x2*] by ARYTM_0:9;
 1 = [*1,0*] by ARYTM_0:def_5;
then x * 1 = [*(+ ((* (x1,1)),(opp (* (x2,0))))),(+ ((* (x1,0)),(* (x2,1))))*] by A1, XCMPLX_0:def_5
.= [*(+ ((* (x1,1)),(opp 0))),(+ ((* (x1,0)),(* (x2,1))))*] by ARYTM_0:12
.= [*(+ (x1,(opp 0))),(+ ((* (x1,0)),(* (x2,1))))*] by ARYTM_0:19
.= [*(+ (x1,(opp 0))),(+ ((* (x1,0)),x2))*] by ARYTM_0:19
.= [*(+ (x1,0)),(+ (0,x2))*] by Lm2, ARYTM_0:12
.= [*x1,(+ (0,x2))*] by ARYTM_0:11
.= x by A1, ARYTM_0:11 ;
hence  1 * x = x ; ::_thesis: verum
end;

theorem :: ARITHM:4
for x being complex number holds x - 0 = x
proof
let x be complex number ; ::_thesis: x - 0 = x
 x - 0 = x + 0 by Lm1, XCMPLX_0:def_8;
hence  x - 0 = x by Th1; ::_thesis: verum
end;

theorem :: ARITHM:5
for x being complex number holds 0 / x = 0
proof
let x be complex number ; ::_thesis: 0 / x = 0
 0 / x = 0 * (x ") by XCMPLX_0:def_9;
hence  0 / x = 0 by Th2; ::_thesis: verum
end;

Lm3:  1 " = 1
proof
 1 * (1 ") = 1 " by Th3;
hence  1 " = 1 by XCMPLX_0:def_7; ::_thesis: verum
end;

theorem :: ARITHM:6
for x being complex number holds x / 1 = x
proof
let x be complex number ; ::_thesis: x / 1 = x
 x / 1 = x * 1 by Lm3, XCMPLX_0:def_9;
hence  x / 1 = x by Th3; ::_thesis: verum
end;