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