:: XCMPLX_0 semantic presentation begin definition func -> set equals :: XCMPLX_0:def 1 (0,1) --> (0,1); coherence (0,1) --> (0,1) is set ; let c be number ; attrc is complex means :Def2: :: XCMPLX_0:def 2 c in COMPLEX ; end; :: deftheorem defines XCMPLX_0:def_1_:_ = (0,1) --> (0,1); :: deftheorem Def2 defines complex XCMPLX_0:def_2_:_ for c being number holds ( c is complex iff c in COMPLEX ); registration cluster -> complex ; coherence is complex proof set X = { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ; A1: now__::_thesis:_not__in__{__x_where_x_is_Element_of_Funcs_({0,1},REAL)_:_x_._1_=_0__}_ assume in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ; ::_thesis: contradiction then ex x being Element of Funcs ({0,1},REAL) st ( = x & x . 1 = 0 ) ; hence contradiction by FUNCT_4:63; ::_thesis: verum end; in Funcs ({0,1},REAL) by FUNCT_2:8; then in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by A1, XBOOLE_0:def_5; hence in COMPLEX by NUMBERS:def_2, XBOOLE_0:def_3; :: according to XCMPLX_0:def_2 ::_thesis: verum end; end; registration cluster complex for set ; existence ex b1 being number st b1 is complex proof take ; ::_thesis: is complex thus is complex ; ::_thesis: verum end; end; registration complex number ex b1 being set st for b2 being complex number holds b2 in b1 proof take COMPLEX ; ::_thesis: for b1 being complex number holds b1 in COMPLEX thus for b1 being complex number holds b1 in COMPLEX by Def2; ::_thesis: verum end; end; notation let x be complex number ; synonym zero x for empty ; end; definition let x be complex number ; redefine attr x is empty means :: XCMPLX_0:def 3 x = 0 ; compatibility ( x is zero iff x = 0 ) ; end; :: deftheorem defines zero XCMPLX_0:def_3_:_ for x being complex number holds ( x is zero iff x = 0 ); definition let x, y be complex number ; x in COMPLEX by Def2; then consider x1, x2 being Element of REAL such that A1: x = [*x1,x2*] by ARYTM_0:9; y in COMPLEX by Def2; then consider y1, y2 being Element of REAL such that A2: y = [*y1,y2*] by ARYTM_0:9; funcx + y -> set means :Def4: :: XCMPLX_0:def 4 ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & it = [*(+ (x1,y1)),(+ (x2,y2))*] ); existence ex b1 being set ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) proof take [*(+ (x1,y1)),(+ (x2,y2))*] ; ::_thesis: ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ (x1,y1)),(+ (x2,y2))*] = [*(+ (x1,y1)),(+ (x2,y2))*] ) thus ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ (x1,y1)),(+ (x2,y2))*] = [*(+ (x1,y1)),(+ (x2,y2))*] ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b2 = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds b1 = b2 proof let c1, c2 be number ; ::_thesis: ( ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & c1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) & ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & c2 = [*(+ (x1,y1)),(+ (x2,y2))*] ) implies c1 = c2 ) given x1, x2, y1, y2 being Element of REAL such that A3: x = [*x1,x2*] and A4: y = [*y1,y2*] and A5: c1 = [*(+ (x1,y1)),(+ (x2,y2))*] ; ::_thesis: ( for x1, x2, y1, y2 being Element of REAL holds ( not x = [*x1,x2*] or not y = [*y1,y2*] or not c2 = [*(+ (x1,y1)),(+ (x2,y2))*] ) or c1 = c2 ) given x19, x29, y19, y29 being Element of REAL such that A6: x = [*x19,x29*] and A7: y = [*y19,y29*] and A8: c2 = [*(+ (x19,y19)),(+ (x29,y29))*] ; ::_thesis: c1 = c2 A9: ( x1 = x19 & x2 = x29 ) by A3, A6, ARYTM_0:10; y1 = y19 by A4, A7, ARYTM_0:10; hence c1 = c2 by A4, A5, A7, A8, A9, ARYTM_0:10; ::_thesis: verum end; commutativity for b1 being set for x, y being complex number st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) holds ex x1, x2, y1, y2 being Element of REAL st ( y = [*x1,x2*] & x = [*y1,y2*] & b1 = [*(+ (x1,y1)),(+ (x2,y2))*] ) ; funcx * y -> set means :Def5: :: XCMPLX_0:def 5 ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & it = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ); existence ex b1 being set ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) proof take [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ; ::_thesis: ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) thus ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) & ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds b1 = b2 proof let c1, c2 be number ; ::_thesis: ( ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & c1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) & ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & c2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) implies c1 = c2 ) given x1, x2, y1, y2 being Element of REAL such that A10: x = [*x1,x2*] and A11: y = [*y1,y2*] and A12: c1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ; ::_thesis: ( for x1, x2, y1, y2 being Element of REAL holds ( not x = [*x1,x2*] or not y = [*y1,y2*] or not c2 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) or c1 = c2 ) given x19, x29, y19, y29 being Element of REAL such that A13: x = [*x19,x29*] and A14: y = [*y19,y29*] and A15: c2 = [*(+ ((* (x19,y19)),(opp (* (x29,y29))))),(+ ((* (x19,y29)),(* (x29,y19))))*] ; ::_thesis: c1 = c2 A16: ( x1 = x19 & x2 = x29 ) by A10, A13, ARYTM_0:10; ( y1 = y19 & y2 = y29 ) by A11, A14, ARYTM_0:10; hence c1 = c2 by A12, A15, A16; ::_thesis: verum end; commutativity for b1 being set for x, y being complex number st ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) holds ex x1, x2, y1, y2 being Element of REAL st ( y = [*x1,x2*] & x = [*y1,y2*] & b1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) ; end; :: deftheorem Def4 defines + XCMPLX_0:def_4_:_ for x, y being complex number for b3 being set holds ( b3 = x + y iff ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b3 = [*(+ (x1,y1)),(+ (x2,y2))*] ) ); :: deftheorem Def5 defines * XCMPLX_0:def_5_:_ for x, y being complex number for b3 being set holds ( b3 = x * y iff ex x1, x2, y1, y2 being Element of REAL st ( x = [*x1,x2*] & y = [*y1,y2*] & b3 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) ); Lm1: 0 = [*0,0*] by ARYTM_0:def_5; reconsider j = 1 as Element of REAL ; Lm2: for x, y, z being Element of REAL st + (x,y) = 0 & + (x,z) = 0 holds y = z proof let x, y, z be Element of REAL ; ::_thesis: ( + (x,y) = 0 & + (x,z) = 0 implies y = z ) assume that A1: + (x,y) = 0 and A2: + (x,z) = 0 ; ::_thesis: y = z percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & z in REAL+ & y in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ) ; suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; ::_thesis: y = z then ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A1, A2, ARYTM_0:def_1; hence y = z by ARYTM_2:11; ::_thesis: verum end; supposethat A3: x in REAL+ and A4: y in REAL+ and A5: z in [:{0},REAL+:] ; ::_thesis: y = z A6: ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & 0 = x9 + y9 ) by A1, A3, A4, ARYTM_0:def_1; consider x99, y99 being Element of REAL+ such that A7: x = x99 and A8: ( z = [0,y99] & 0 = x99 - y99 ) by A2, A3, A5, ARYTM_0:def_1; A9: x99 = 0 by A6, A7, ARYTM_2:5; [{},{}] in {[{},{}]} by TARSKI:def_1; then A10: not [{},{}] in REAL by NUMBERS:def_1, XBOOLE_0:def_5; z in REAL ; hence y = z by A8, A9, A10, ARYTM_1:19; ::_thesis: verum end; supposethat A11: x in REAL+ and A12: z in REAL+ and A13: y in [:{0},REAL+:] ; ::_thesis: y = z A14: ex x9, z9 being Element of REAL+ st ( x = x9 & z = z9 & 0 = x9 + z9 ) by A2, A11, A12, ARYTM_0:def_1; consider x99, y9 being Element of REAL+ such that A15: x = x99 and A16: ( y = [0,y9] & 0 = x99 - y9 ) by A1, A11, A13, ARYTM_0:def_1; A17: x99 = 0 by A14, A15, ARYTM_2:5; [0,0] in {[0,0]} by TARSKI:def_1; then A18: not [0,0] in REAL by NUMBERS:def_1, XBOOLE_0:def_5; y in REAL ; hence y = z by A16, A17, A18, ARYTM_1:19; ::_thesis: verum end; supposethat A19: x in REAL+ and A20: y in [:{0},REAL+:] and A21: z in [:{0},REAL+:] ; ::_thesis: y = z consider x9, y9 being Element of REAL+ such that A22: x = x9 and A23: y = [0,y9] and A24: 0 = x9 - y9 by A1, A19, A20, ARYTM_0:def_1; consider x99, z9 being Element of REAL+ such that A25: x = x99 and A26: z = [0,z9] and A27: 0 = x99 - z9 by A2, A19, A21, ARYTM_0:def_1; y9 = x9 by A24, ARYTM_0:6 .= z9 by A22, A25, A27, ARYTM_0:6 ; hence y = z by A23, A26; ::_thesis: verum end; supposethat A28: z in REAL+ and A29: y in REAL+ and A30: x in [:{0},REAL+:] ; ::_thesis: y = z consider x9, y9 being Element of REAL+ such that A31: x = [0,x9] and A32: y = y9 and A33: 0 = y9 - x9 by A1, A29, A30, ARYTM_0:def_1; consider x99, z9 being Element of REAL+ such that A34: x = [0,x99] and A35: z = z9 and A36: 0 = z9 - x99 by A2, A28, A30, ARYTM_0:def_1; x9 = x99 by A31, A34, XTUPLE_0:1; then z9 = x9 by A36, ARYTM_0:6 .= y9 by A33, ARYTM_0:6 ; hence y = z by A32, A35; ::_thesis: verum end; suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) ; ::_thesis: y = z then ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A1, ARYTM_0:def_1; hence y = z ; ::_thesis: verum end; suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ; ::_thesis: y = z then ex x9, z9 being Element of REAL+ st ( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A2, ARYTM_0:def_1; hence y = z ; ::_thesis: verum end; end; end; registration let z, z9 be complex number ; clusterz + z9 -> complex ; coherence z + z9 is complex proof ex x1, x2, y1, y2 being Element of REAL st ( z = [*x1,x2*] & z9 = [*y1,y2*] & z + z9 = [*(+ (x1,y1)),(+ (x2,y2))*] ) by Def4; hence z + z9 in COMPLEX ; :: according to XCMPLX_0:def_2 ::_thesis: verum end; clusterz * z9 -> complex ; coherence z * z9 is complex proof ex x1, x2, y1, y2 being Element of REAL st ( z = [*x1,x2*] & z9 = [*y1,y2*] & z * z9 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] ) by Def5; hence z * z9 in COMPLEX ; :: according to XCMPLX_0:def_2 ::_thesis: verum end; end; definition let z be complex number ; z in COMPLEX by Def2; then consider x, y being Element of REAL such that A1: z = [*x,y*] by ARYTM_0:9; func - z -> complex number means :Def6: :: XCMPLX_0:def 6 z + it = 0 ; existence ex b1 being complex number st z + b1 = 0 proof reconsider z9 = [*(opp x),(opp y)*] as complex number by Def2; take z9 ; ::_thesis: z + z9 = 0 ( 0 = + (x,(opp x)) & 0 = + (y,(opp y)) ) by ARYTM_0:def_3; hence z + z9 = 0 by A1, Def4, Lm1; ::_thesis: verum end; uniqueness for b1, b2 being complex number st z + b1 = 0 & z + b2 = 0 holds b1 = b2 proof let c1, c2 be complex number ; ::_thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 ) assume that A2: z + c1 = 0 and A3: z + c2 = 0 ; ::_thesis: c1 = c2 consider x1, x2, y1, y2 being Element of REAL such that A4: z = [*x1,x2*] and A5: c1 = [*y1,y2*] and A6: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by A2, Def4; consider x19, x29, y19, y29 being Element of REAL such that A7: z = [*x19,x29*] and A8: c2 = [*y19,y29*] and A9: 0 = [*(+ (x19,y19)),(+ (x29,y29))*] by A3, Def4; A10: x1 = x19 by A4, A7, ARYTM_0:10; A11: x2 = x29 by A4, A7, ARYTM_0:10; A12: + (x1,y1) = 0 by A6, Lm1, ARYTM_0:10; + (x1,y19) = 0 by A9, A10, Lm1, ARYTM_0:10; then A13: y1 = y19 by A12, Lm2; A14: + (x2,y2) = 0 by A6, Lm1, ARYTM_0:10; + (x2,y29) = 0 by A9, A11, Lm1, ARYTM_0:10; hence c1 = c2 by A5, A8, A13, A14, Lm2; ::_thesis: verum end; involutiveness for b1, b2 being complex number st b2 + b1 = 0 holds b1 + b2 = 0 ; funcz " -> complex number means :Def7: :: XCMPLX_0:def 7 z * it = 1 if z <> 0 otherwise it = 0 ; existence ( ( z <> 0 implies ex b1 being complex number st z * b1 = 1 ) & ( not z <> 0 implies ex b1 being complex number st b1 = 0 ) ) proof thus ( z <> 0 implies ex z9 being complex number st z * z9 = 1 ) ::_thesis: ( not z <> 0 implies ex b1 being complex number st b1 = 0 ) proof set y1 = * (x,(inv (+ ((* (x,x)),(* (y,y)))))); set y2 = * ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))); set z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]; reconsider z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] as complex number by Def2; assume A15: z <> 0 ; ::_thesis: ex z9 being complex number st z * z9 = 1 take z9 ; ::_thesis: z * z9 = 1 A16: opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))) = opp (* (y,(opp (* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:15 .= opp (opp (* (y,(* (y,(inv (+ ((* (x,x)),(* (y,y)))))))))) by ARYTM_0:15 .= * ((* (y,y)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:13 ; A17: * (x,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((* (x,x)),(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:13; A18: now__::_thesis:_not_+_((*_(x,x)),(*_(y,y)))_=_0 assume + ((* (x,x)),(* (y,y))) = 0 ; ::_thesis: contradiction then ( x = 0 & y = 0 ) by ARYTM_0:17; hence contradiction by A1, A15, ARYTM_0:def_5; ::_thesis: verum end; * (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))) = * ((opp y),(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))) by ARYTM_0:13 .= opp (* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))) by ARYTM_0:15 ; then + ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))) = 0 by ARYTM_0:def_3; then [*(+ ((* (x,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))),(opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))))))),(+ ((* (x,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))),(* (y,(* (x,(inv (+ ((* (x,x)),(* (y,y)))))))))))*] = + ((* (x,(* (x,(inv (+ ((* (x,x)),(* (y,y))))))))),(opp (* (y,(* ((opp y),(inv (+ ((* (x,x)),(* (y,y))))))))))) by ARYTM_0:def_5 .= * ((+ ((* (x,x)),(* (y,y)))),(inv (+ ((* (x,x)),(* (y,y)))))) by A16, A17, ARYTM_0:14 .= 1 by A18, ARYTM_0:def_4 ; hence z * z9 = 1 by A1, Def5; ::_thesis: verum end; assume z = 0 ; ::_thesis: ex b1 being complex number st b1 = 0 hence ex b1 being complex number st b1 = 0 ; ::_thesis: verum end; uniqueness for b1, b2 being complex number holds ( ( z <> 0 & z * b1 = 1 & z * b2 = 1 implies b1 = b2 ) & ( not z <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let c1, c2 be complex number ; ::_thesis: ( ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) & ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) ) thus ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) ::_thesis: ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) proof assume that A19: z <> 0 and A20: z * c1 = 1 and A21: z * c2 = 1 ; ::_thesis: c1 = c2 A22: for z9 being complex number st z * z9 = 1 holds z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] proof let z9 be complex number ; ::_thesis: ( z * z9 = 1 implies z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] ) assume A23: z * z9 = 1 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] consider x1, x2, x9, y9 being Element of REAL such that A24: z = [*x1,x2*] and A25: z9 = [*x9,y9*] and A26: 1 = [*(+ ((* (x1,x9)),(opp (* (x2,y9))))),(+ ((* (x1,y9)),(* (x2,x9))))*] by A23, Def5; A27: ( x = x1 & y = x2 ) by A1, A24, ARYTM_0:10; percases ( ( x = 0 & y <> 0 ) or ( opp y = 0 & x <> 0 ) or ( opp y <> 0 & x <> 0 ) ) by A1, A19, ARYTM_0:def_5; supposethat A28: x = 0 and A29: y <> 0 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] + (y,(opp y)) = 0 by ARYTM_0:def_3; then A30: opp y <> 0 by A29, ARYTM_0:11; ( * (x,y9) = 0 & * (x,x9) = 0 ) by A28, ARYTM_0:12; then A31: 1 = [*(opp (* (y,y9))),(+ (0,(* (y,x9))))*] by A26, A27, ARYTM_0:11 .= [*(opp (* (y,y9))),(* (y,x9))*] by ARYTM_0:11 ; A32: 1 = [*j,0*] by ARYTM_0:def_5; * ((opp y),y9) = opp (* (y,y9)) by ARYTM_0:15 .= 1 by A31, A32, ARYTM_0:10 ; then A33: y9 = inv (opp y) by A30, ARYTM_0:def_4; A34: * (x,x) = 0 by A28, ARYTM_0:12; * ((opp y),(opp (inv y))) = opp (* (y,(opp (inv y)))) by ARYTM_0:15 .= opp (opp (* (y,(inv y)))) by ARYTM_0:15 .= 1 by A29, ARYTM_0:def_4 ; then A35: inv (opp y) = opp (inv y) by A30, ARYTM_0:def_4; * (y,x9) = 0 by A31, A32, ARYTM_0:10; hence z9 = [*0,(inv (opp y))*] by A25, A29, A33, ARYTM_0:21 .= [*0,(opp (* (j,(inv y))))*] by A35, ARYTM_0:19 .= [*0,(opp (* ((* (y,(inv y))),(inv y))))*] by A29, ARYTM_0:def_4 .= [*0,(opp (* (y,(* ((inv y),(inv y))))))*] by ARYTM_0:13 .= [*0,(* ((opp y),(* ((inv y),(inv y)))))*] by ARYTM_0:15 .= [*0,(* ((opp y),(inv (* (y,y)))))*] by ARYTM_0:22 .= [*0,(* ((opp y),(inv (+ (0,(* (y,y)))))))*] by ARYTM_0:11 .= [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A28, A34, ARYTM_0:12 ; ::_thesis: verum end; supposethat A36: opp y = 0 and A37: x <> 0 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] + (y,(opp y)) = 0 by ARYTM_0:def_3; then A38: y = 0 by A36, ARYTM_0:11; then A39: * (y,x9) = 0 by ARYTM_0:12; opp (* (y,y9)) = * ((opp y),y9) by ARYTM_0:15 .= 0 by A36, ARYTM_0:12 ; then A40: 1 = [*(* (x,x9)),(+ ((* (x,y9)),0))*] by A26, A27, A39, ARYTM_0:11 .= [*(* (x,x9)),(* (x,y9))*] by ARYTM_0:11 ; A41: 1 = [*j,0*] by ARYTM_0:def_5; then * (x,x9) = 1 by A40, ARYTM_0:10; then A42: x9 = inv x by A37, ARYTM_0:def_4; * (x,y9) = 0 by A40, A41, ARYTM_0:10; then A43: y9 = 0 by A37, ARYTM_0:21; A44: * (y,y) = 0 by A38, ARYTM_0:12; x9 = * (j,(inv x)) by A42, ARYTM_0:19 .= * ((* (x,(inv x))),(inv x)) by A37, ARYTM_0:def_4 .= * (x,(* ((inv x),(inv x)))) by ARYTM_0:13 .= * (x,(inv (* (x,x)))) by ARYTM_0:22 .= * (x,(inv (+ ((* (x,x)),0)))) by ARYTM_0:11 ; hence z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A25, A36, A43, A44, ARYTM_0:12; ::_thesis: verum end; supposethat A45: opp y <> 0 and A46: x <> 0 ; ::_thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] A47: now__::_thesis:_not_+_((*_((*_(x,x)),(inv_(opp_y)))),(opp_y))_=_0 assume + ((* ((* (x,x)),(inv (opp y)))),(opp y)) = 0 ; ::_thesis: contradiction then + ((* ((* (x,x)),(inv (opp y)))),(* ((opp y),j))) = 0 by ARYTM_0:19; then + ((* ((* (x,x)),(inv (opp y)))),(* ((opp y),(* ((opp y),(inv (opp y))))))) = 0 by A45, ARYTM_0:def_4; then + ((* ((* (x,x)),(inv (opp y)))),(* ((* ((opp y),(opp y))),(inv (opp y))))) = 0 by ARYTM_0:13; then A48: * ((inv (opp y)),(+ ((* (x,x)),(* ((opp y),(opp y)))))) = 0 by ARYTM_0:14; + ((* (x,x)),(* ((opp y),(opp y)))) <> 0 by A46, ARYTM_0:17; then A49: inv (opp y) = 0 by A48, ARYTM_0:21; * ((opp y),(inv (opp y))) = 1 by A45, ARYTM_0:def_4; hence contradiction by A49, ARYTM_0:12; ::_thesis: verum end; reconsider j = 1 as Element of REAL ; A50: 1 = [*j,0*] by ARYTM_0:def_5; then + ((* (x1,y9)),(* (x2,x9))) = 0 by A26, ARYTM_0:10; then * (x,y9) = opp (* (y,x9)) by A27, ARYTM_0:def_3; then * (x,y9) = * ((opp y),x9) by ARYTM_0:15; then A51: x9 = * ((* (x,y9)),(inv (opp y))) by A45, ARYTM_0:20 .= * (x,(* (y9,(inv (opp y))))) by ARYTM_0:13 ; then + ((* (x,(* (x,(* (y9,(inv (opp y)))))))),(opp (* (y,y9)))) = 1 by A26, A27, A50, ARYTM_0:10; then + ((* ((* (x,x)),(* (y9,(inv (opp y)))))),(opp (* (y,y9)))) = 1 by ARYTM_0:13; then + ((* ((* (x,x)),(* (y9,(inv (opp y)))))),(* ((opp y),y9))) = 1 by ARYTM_0:15; then + ((* (y9,(* ((* (x,x)),(inv (opp y)))))),(* ((opp y),y9))) = 1 by ARYTM_0:13; then * (y9,(+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))) = 1 by ARYTM_0:14; then A52: y9 = inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))) by A47, ARYTM_0:def_4; then A53: x9 = * (x,(inv (* ((+ ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp y))))) by A51, ARYTM_0:22 .= * (x,(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(* ((opp y),(opp y))))))) by ARYTM_0:14 .= * (x,(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (* (y,(opp y)))))))) by ARYTM_0:15 .= * (x,(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (opp (* (y,y)))))))) by ARYTM_0:15 .= * (x,(inv (+ ((* ((* (x,x)),(* ((inv (opp y)),(opp y))))),(* (y,y)))))) by ARYTM_0:13 .= * (x,(inv (+ ((* ((* (x,x)),j)),(* (y,y)))))) by A45, ARYTM_0:def_4 .= * (x,(inv (+ ((* (x,x)),(* (y,y)))))) by ARYTM_0:19 ; y9 = * (j,(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))) by A52, ARYTM_0:19 .= * ((* ((opp y),(inv (opp y)))),(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))) by A45, ARYTM_0:def_4 .= * ((opp y),(* ((inv (opp y)),(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))))) by ARYTM_0:13 .= * ((opp y),(inv (* ((opp y),(+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))))) by ARYTM_0:22 .= * ((opp y),(inv (+ ((* ((opp y),(* ((* (x,x)),(inv (opp y)))))),(* ((opp y),(opp y))))))) by ARYTM_0:14 .= * ((opp y),(inv (+ ((* ((* (x,x)),(* ((opp y),(inv (opp y)))))),(* ((opp y),(opp y))))))) by ARYTM_0:13 .= * ((opp y),(inv (+ ((* ((* (x,x)),j)),(* ((opp y),(opp y))))))) by A45, ARYTM_0:def_4 .= * ((opp y),(inv (+ ((* (x,x)),(* ((opp y),(opp y))))))) by ARYTM_0:19 .= * ((opp y),(inv (+ ((* (x,x)),(opp (* (y,(opp y)))))))) by ARYTM_0:15 .= * ((opp y),(inv (+ ((* (x,x)),(opp (opp (* (y,y)))))))) by ARYTM_0:15 .= * ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))) ; hence z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A25, A53; ::_thesis: verum end; end; end; hence c1 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] by A20 .= c2 by A21, A22 ; ::_thesis: verum end; thus ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) ; ::_thesis: verum end; consistency for b1 being complex number holds verum ; involutiveness for b1, b2 being complex number st ( b2 <> 0 implies b2 * b1 = 1 ) & ( not b2 <> 0 implies b1 = 0 ) holds ( ( b1 <> 0 implies b1 * b2 = 1 ) & ( not b1 <> 0 implies b2 = 0 ) ) proof let z, z9 be complex number ; ::_thesis: ( ( z9 <> 0 implies z9 * z = 1 ) & ( not z9 <> 0 implies z = 0 ) implies ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) ) ) assume that A54: ( z9 <> 0 implies z9 * z = 1 ) and A55: ( z9 = 0 implies z = 0 ) ; ::_thesis: ( ( z <> 0 implies z * z9 = 1 ) & ( not z <> 0 implies z9 = 0 ) ) thus ( z <> 0 implies z * z9 = 1 ) by A54, A55; ::_thesis: ( not z <> 0 implies z9 = 0 ) assume A56: z = 0 ; ::_thesis: z9 = 0 assume z9 <> 0 ; ::_thesis: contradiction then consider x1, x2, y1, y2 being Element of REAL such that A57: z = [*x1,x2*] and z9 = [*y1,y2*] and A58: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by A54, Def5; A59: z = [*0,0*] by A56, ARYTM_0:def_5; then A60: x1 = 0 by A57, ARYTM_0:10; A61: x2 = 0 by A57, A59, ARYTM_0:10; A62: * (x1,y1) = 0 by A60, ARYTM_0:12; * (x2,y2) = 0 by A61, ARYTM_0:12; then A63: + ((* (x1,y1)),(opp (* (x2,y2)))) = 0 by A62, ARYTM_0:def_3; A64: * (x1,y2) = 0 by A60, ARYTM_0:12; * (x2,y1) = 0 by A61, ARYTM_0:12; then + ((* (x1,y2)),(* (x2,y1))) = 0 by A64, ARYTM_0:11; hence contradiction by A58, A63, ARYTM_0:def_5; ::_thesis: verum end; end; :: deftheorem Def6 defines - XCMPLX_0:def_6_:_ for z, b2 being complex number holds ( b2 = - z iff z + b2 = 0 ); :: deftheorem Def7 defines " XCMPLX_0:def_7_:_ for z, b2 being complex number holds ( ( z <> 0 implies ( b2 = z " iff z * b2 = 1 ) ) & ( not z <> 0 implies ( b2 = z " iff b2 = 0 ) ) ); definition let x, y be complex number ; funcx - y -> set equals :: XCMPLX_0:def 8 x + (- y); coherence x + (- y) is set ; funcx / y -> set equals :: XCMPLX_0:def 9 x * (y "); coherence x * (y ") is set ; end; :: deftheorem defines - XCMPLX_0:def_8_:_ for x, y being complex number holds x - y = x + (- y); :: deftheorem defines / XCMPLX_0:def_9_:_ for x, y being complex number holds x / y = x * (y "); registration let x, y be complex number ; clusterx - y -> complex ; coherence x - y is complex ; clusterx / y -> complex ; coherence x / y is complex ; end; Lm3: for x, y, z being complex number holds x * (y * z) = (x * y) * z proof let x, y, z be complex number ; ::_thesis: x * (y * z) = (x * y) * z consider x1, x2, y1, y2 being Element of REAL such that A1: x = [*x1,x2*] and A2: y = [*y1,y2*] and A3: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def5; consider y3, y4, z1, z2 being Element of REAL such that A4: y = [*y3,y4*] and A5: z = [*z1,z2*] and A6: y * z = [*(+ ((* (y3,z1)),(opp (* (y4,z2))))),(+ ((* (y3,z2)),(* (y4,z1))))*] by Def5; A7: y1 = y3 by A2, A4, ARYTM_0:10; A8: y2 = y4 by A2, A4, ARYTM_0:10; consider x3, x4, yz1, yz2 being Element of REAL such that A9: x = [*x3,x4*] and A10: y * z = [*yz1,yz2*] and A11: x * (y * z) = [*(+ ((* (x3,yz1)),(opp (* (x4,yz2))))),(+ ((* (x3,yz2)),(* (x4,yz1))))*] by Def5; A12: x1 = x3 by A1, A9, ARYTM_0:10; A13: x2 = x4 by A1, A9, ARYTM_0:10; consider xy1, xy2, z3, z4 being Element of REAL such that A14: x * y = [*xy1,xy2*] and A15: z = [*z3,z4*] and A16: (x * y) * z = [*(+ ((* (xy1,z3)),(opp (* (xy2,z4))))),(+ ((* (xy1,z4)),(* (xy2,z3))))*] by Def5; A17: z1 = z3 by A5, A15, ARYTM_0:10; A18: z2 = z4 by A5, A15, ARYTM_0:10; A19: xy1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A3, A14, ARYTM_0:10; A20: xy2 = + ((* (x1,y2)),(* (x2,y1))) by A3, A14, ARYTM_0:10; A21: yz1 = + ((* (y3,z1)),(opp (* (y4,z2)))) by A6, A10, ARYTM_0:10; A22: yz2 = + ((* (y3,z2)),(* (y4,z1))) by A6, A10, ARYTM_0:10; + ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))) = + ((* ((opp x4),(* (y4,z1)))),(* ((* ((opp x2),y1)),z4))) by A7, A13, A18, ARYTM_0:13 .= + ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))) by A8, A13, A17, ARYTM_0:13 ; then A23: + ((* (x3,(* ((opp y4),z2)))),(+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))))) = + ((* ((* (x1,(opp y2))),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by A8, A12, A18, ARYTM_0:13 .= + ((* ((opp (* (x1,y2))),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:15 .= + ((* ((* ((opp x1),y2)),z4)),(+ ((* ((* ((opp x2),y2)),z3)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:15 .= + ((* ((* ((opp x2),y2)),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:23 ; A24: + ((* (x3,yz1)),(opp (* (x4,yz2)))) = + ((* (x3,yz1)),(* ((opp x4),yz2))) by ARYTM_0:15 .= + ((* (x3,(+ ((* (y3,z1)),(* ((opp y4),z2)))))),(* ((opp x4),yz2))) by A21, ARYTM_0:15 .= + ((+ ((* (x3,(* (y3,z1)))),(* (x3,(* ((opp y4),z2)))))),(* ((opp x4),(+ ((* (y3,z2)),(* (y4,z1))))))) by A22, ARYTM_0:14 .= + ((+ ((* (x3,(* (y3,z1)))),(* (x3,(* ((opp y4),z2)))))),(+ ((* ((opp x4),(* (y3,z2)))),(* ((opp x4),(* (y4,z1))))))) by ARYTM_0:14 .= + ((* (x3,(* (y3,z1)))),(+ ((* ((* ((opp x2),y2)),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))))) by A23, ARYTM_0:23 .= + ((+ ((* (x3,(* (y3,z1)))),(* ((* ((opp x2),y2)),z3)))),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:23 .= + ((+ ((* ((* (x1,y1)),z3)),(* ((* ((opp x2),y2)),z3)))),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by A7, A12, A17, ARYTM_0:13 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((* ((opp x2),y1)),z4))))) by ARYTM_0:14 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(* ((opp (* (x2,y1))),z4))))) by ARYTM_0:15 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((* ((opp x1),y2)),z4)),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((* ((opp (* (x1,y2))),z4)),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(+ ((opp (* ((* (x1,y2)),z4))),(opp (* ((* (x2,y1)),z4)))))) by ARYTM_0:15 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(opp (+ ((* ((* (x1,y2)),z4)),(* ((* (x2,y1)),z4)))))) by ARYTM_0:25 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(opp (* ((+ ((* (x1,y2)),(* (x2,y1)))),z4)))) by ARYTM_0:14 .= + ((* ((+ ((* (x1,y1)),(* ((opp x2),y2)))),z3)),(* ((opp xy2),z4))) by A20, ARYTM_0:15 .= + ((* (xy1,z3)),(* ((opp xy2),z4))) by A19, ARYTM_0:15 .= + ((* (xy1,z3)),(opp (* (xy2,z4)))) by ARYTM_0:15 ; A25: + ((* ((opp (* (x2,y2))),z4)),(* ((* (x2,y1)),z3))) = + ((opp (* ((* (x2,y2)),z4))),(* ((* (x2,y1)),z3))) by ARYTM_0:15 .= + ((* (x4,(* (y3,z1)))),(opp (* ((* (x2,y2)),z4)))) by A7, A13, A17, ARYTM_0:13 .= + ((* (x4,(* (y3,z1)))),(opp (* (x4,(* (y4,z2)))))) by A8, A13, A18, ARYTM_0:13 .= + ((* (x4,(* (y3,z1)))),(* (x4,(opp (* (y4,z2)))))) by ARYTM_0:15 ; A26: + ((* ((opp (* (x2,y2))),z4)),(* (xy2,z3))) = + ((* ((opp (* (x2,y2))),z4)),(+ ((* ((* (x1,y2)),z3)),(* ((* (x2,y1)),z3))))) by A20, ARYTM_0:14 .= + ((* ((* (x1,y2)),z3)),(+ ((* ((opp (* (x2,y2))),z4)),(* ((* (x2,y1)),z3))))) by ARYTM_0:23 .= + ((* (x3,(* (y4,z1)))),(+ ((* (x4,(* (y3,z1)))),(* (x4,(opp (* (y4,z2)))))))) by A8, A12, A17, A25, ARYTM_0:13 .= + ((* (x3,(* (y4,z1)))),(* (x4,yz1))) by A21, ARYTM_0:14 ; + ((* (xy1,z4)),(* (xy2,z3))) = + ((+ ((* ((* (x1,y1)),z4)),(* ((opp (* (x2,y2))),z4)))),(* (xy2,z3))) by A19, ARYTM_0:14 .= + ((* ((* (x1,y1)),z4)),(+ ((* ((opp (* (x2,y2))),z4)),(* (xy2,z3))))) by ARYTM_0:23 .= + ((* (x3,(* (y3,z2)))),(+ ((* (x3,(* (y4,z1)))),(* (x4,yz1))))) by A7, A12, A18, A26, ARYTM_0:13 .= + ((+ ((* (x3,(* (y3,z2)))),(* (x3,(* (y4,z1)))))),(* (x4,yz1))) by ARYTM_0:23 .= + ((* (x3,yz2)),(* (x4,yz1))) by A22, ARYTM_0:14 ; hence x * (y * z) = (x * y) * z by A11, A16, A24; ::_thesis: verum end; registration cluster non zero complex for set ; existence not for b1 being complex number holds b1 is zero proof ( REAL c= COMPLEX & 1 in REAL ) by NUMBERS:def_2, XBOOLE_1:7; then 1 is complex number by Def2; hence not for b1 being complex number holds b1 is zero ; ::_thesis: verum end; end; Lm4: REAL c= COMPLEX by NUMBERS:def_2, XBOOLE_1:7; registration let x be non zero complex number ; cluster - x -> non zero complex ; coherence not - x is zero proof assume A1: - x = 0 ; :: according to XCMPLX_0:def_3 ::_thesis: contradiction x + (- x) = 0 by Def6; then consider x1, x2, y1, y2 being Element of REAL such that A2: x = [*x1,x2*] and A3: - x = [*y1,y2*] and A4: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by Def4; A5: + (x2,y2) = 0 by A4, ARYTM_0:24; then A6: + (x1,y1) = 0 by A4, ARYTM_0:def_5; y2 = 0 by A1, A3, ARYTM_0:24; then A7: y1 = 0 by A1, A3, ARYTM_0:def_5; x2 = 0 by A1, A3, A5, ARYTM_0:11, ARYTM_0:24; then x = x1 by A2, ARYTM_0:def_5 .= 0 by A6, A7, ARYTM_0:11 ; hence contradiction ; ::_thesis: verum end; clusterx " -> non zero complex ; coherence not x " is zero proof assume A8: x " = 0 ; :: according to XCMPLX_0:def_3 ::_thesis: contradiction x * (x ") = 1 by Def7; then consider x1, x2, y1, y2 being Element of REAL such that x = [*x1,x2*] and A9: x " = [*y1,y2*] and A10: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by Def5; y2 = 0 by A8, A9, ARYTM_0:24; then A11: y1 = 0 by A8, A9, ARYTM_0:def_5; + ((* (x1,y2)),(* (x2,y1))) = 0 by A10, ARYTM_0:24; then 1 = + ((* (x1,y1)),(opp (* (x2,y2)))) by A10, ARYTM_0:def_5 .= + ((* (x1,y1)),(* ((opp x2),y2))) by ARYTM_0:15 .= * ((opp x2),y2) by A11, ARYTM_0:11, ARYTM_0:12 ; hence contradiction by A8, A9, ARYTM_0:12, ARYTM_0:24; ::_thesis: verum end; let y be non zero complex number ; clusterx * y -> non zero ; coherence not x * y is zero proof 1 in REAL ; then reconsider j = 1 as complex number by Def2, Lm4; consider u1, u2, v1, v2 being Element of REAL such that A12: j = [*u1,u2*] and A13: ( y = [*v1,v2*] & j * y = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] ) by Def5; A14: u2 = 0 by A12, ARYTM_0:24; then A15: + ((* (u1,v2)),(* (u2,v1))) = * (u1,v2) by ARYTM_0:11, ARYTM_0:12; A16: u1 = 1 by A12, A14, ARYTM_0:def_5; + (0,(opp 0)) = 0 by ARYTM_0:def_3; then A17: opp 0 = 0 by ARYTM_0:11; A18: + ((* (u1,v1)),(opp (* (u2,v2)))) = + (v1,(opp (* (u2,v2)))) by A16, ARYTM_0:19 .= + (v1,(* ((opp u2),v2))) by ARYTM_0:15 .= + (v1,(* (0,v2))) by A12, A17, ARYTM_0:24 .= v1 by ARYTM_0:11, ARYTM_0:12 ; 0 in REAL ; then reconsider z = 0 as complex number by Def2, Lm4; consider u1, u2, v1, v2 being Element of REAL such that x " = [*u1,u2*] and A19: z = [*v1,v2*] and A20: (x ") * z = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] by Def5; v2 = 0 by A19, ARYTM_0:24; then A21: v1 = 0 by A19, ARYTM_0:def_5; then A22: + ((* (u1,v1)),(opp (* (u2,v2)))) = opp (* (u2,v2)) by ARYTM_0:11, ARYTM_0:12 .= 0 by A17, A19, ARYTM_0:12, ARYTM_0:24 ; A23: + ((* (u1,v2)),(* (u2,v1))) = + (0,(* (u2,v1))) by A19, ARYTM_0:12, ARYTM_0:24 .= * (u2,v1) by ARYTM_0:11 .= 0 by A21, ARYTM_0:12 ; assume A24: x * y = 0 ; :: according to XCMPLX_0:def_3 ::_thesis: contradiction A25: ((x ") * x) * y = (x ") * (x * y) by Lm3 .= 0 by A20, A22, A23, A24, ARYTM_0:def_5 ; ((x ") * x) * y = j * y by Def7 .= y by A13, A15, A16, A18, ARYTM_0:19 ; hence contradiction by A25; ::_thesis: verum end; end; registration let x, y be non zero complex number ; clusterx / y -> non zero ; coherence not x / y is zero ; end; registration cluster -> complex for Element of REAL ; coherence for b1 being Element of REAL holds b1 is complex proof let n be Element of REAL ; ::_thesis: n is complex n in REAL ; hence n is complex by Def2, Lm4; ::_thesis: verum end; end; registration cluster natural -> complex for set ; coherence for b1 being number st b1 is natural holds b1 is complex proof let n be set ; ::_thesis: ( n is natural implies n is complex ) assume n is natural ; ::_thesis: n is complex then n in NAT by ORDINAL1:def_12; hence n is complex ; ::_thesis: verum end; end; registration cluster -> complex for Element of COMPLEX ; coherence for b1 being Element of COMPLEX holds b1 is complex by Def2; end;