:: 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;