:: ARITHM semantic presentation

theorem E1: :: ARITHM:1
for b1 being complex number holds b1 + 0 = b1
proof
let c1 be complex number ;
c1 in COMPLEX by XCMPLX_0:def 2;
then consider c2, c3 being Element of REAL such that
E2: c1 = [*c2,c3*] by ARYTM_0:11;
0 = [*0,0*] by ARYTM_0:def 7;
then c1 + 0 = [*(+ c2,0),(+ c3,0)*] by E2, XCMPLX_0:def 4
.= [*c2,(+ c3,0)*] by ARYTM_0:13
.= c1 by E2, ARYTM_0:13 ;
hence c1 + 0 = c1 ;
end;

E2: - 0 = 0
proof
0 + (- 0) = - 0 by E1;
hence - 0 = 0 by XCMPLX_0:def 6;
end;

E3: opp 0 = 0
proof
+ 0,0 = 0 by ARYTM_0:13;
hence opp 0 = 0 by ARYTM_0:def 4;
end;

theorem E4: :: ARITHM:2
for b1 being complex number holds b1 * 0 = 0
proof
let c1 be complex number ;
c1 in COMPLEX by XCMPLX_0:def 2;
then consider c2, c3 being Element of REAL such that
E5: c1 = [*c2,c3*] by ARYTM_0:11;
0 = [*0,0*] by ARYTM_0:def 7;
then c1 * 0 = [*(+ (* c2,0),(opp (* c3,0))),(+ (* c2,0),(* c3,0))*] by E5, XCMPLX_0:def 5
.= [*(+ (* c2,0),(opp 0)),(+ (* c2,0),(* c3,0))*] by ARYTM_0:14
.= [*(+ (* c2,0),(opp 0)),(+ (* c2,0),0)*] by ARYTM_0:14
.= [*(+ 0,(opp 0)),(+ (* c2,0),0)*] by ARYTM_0:14
.= [*(+ 0,(opp 0)),(+ 0,0)*] by ARYTM_0:14
.= [*(+ 0,(opp 0)),0*] by ARYTM_0:13
.= [*(opp 0),0*] by ARYTM_0:13
.= 0 by E3, ARYTM_0:def 7 ;
hence c1 * 0 = 0 ;
end;

E5: one = succ 0 by ORDINAL2:def 4
.= 1 ;

theorem E6: :: ARITHM:3
for b1 being complex number holds 1 * b1 = b1
proof
let c1 be complex number ;
c1 in COMPLEX by XCMPLX_0:def 2;
then consider c2, c3 being Element of REAL such that
E7: c1 = [*c2,c3*] by ARYTM_0:11;
1 = [*1,0*] by ARYTM_0:def 7;
then c1 * 1 = [*(+ (* c2,1),(opp (* c3,0))),(+ (* c2,0),(* c3,1))*] by E7, XCMPLX_0:def 5
.= [*(+ (* c2,1),(opp 0)),(+ (* c2,0),(* c3,1))*] by ARYTM_0:14
.= [*(+ c2,(opp 0)),(+ (* c2,0),(* c3,1))*] by E5, ARYTM_0:21
.= [*(+ c2,(opp 0)),(+ (* c2,0),c3)*] by E5, ARYTM_0:21
.= [*(+ c2,0),(+ 0,c3)*] by E3, ARYTM_0:14
.= [*c2,(+ 0,c3)*] by ARYTM_0:13
.= c1 by E7, ARYTM_0:13 ;
hence 1 * c1 = c1 ;
end;

theorem :: ARITHM:4
for b1 being complex number holds b1 - 0 = b1
proof
let c1 be complex number ;
c1 - 0 = c1 + 0 by E2, XCMPLX_0:def 8;
hence c1 - 0 = c1 by E1;
end;

theorem :: ARITHM:5
for b1 being complex number holds 0 / b1 = 0
proof
let c1 be complex number ;
0 / c1 = 0 * (c1 " ) by XCMPLX_0:def 9;
hence 0 / c1 = 0 by E4;
end;

E7: 1 " = 1
proof
1 * (1 " ) = 1 " by E6;
hence 1 " = 1 by XCMPLX_0:def 7;
end;

theorem :: ARITHM:6
for b1 being complex number holds b1 / 1 = b1
proof
let c1 be complex number ;
c1 / 1 = c1 * 1 by E7, XCMPLX_0:def 9;
hence c1 / 1 = c1 by E6;
end;