:: COMPLEX1 semantic presentation begin theorem Th1: :: COMPLEX1:1 for a, b being real number st (a ^2) + (b ^2) = 0 holds a = 0 proof let a, b be real number ; ::_thesis: ( (a ^2) + (b ^2) = 0 implies a = 0 ) ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63; hence ( (a ^2) + (b ^2) = 0 implies a = 0 ) ; ::_thesis: verum end; Lm1: for a, b being real number holds 0 <= (a ^2) + (b ^2) proof let a, b be real number ; ::_thesis: 0 <= (a ^2) + (b ^2) ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63; hence 0 <= (a ^2) + (b ^2) ; ::_thesis: verum end; definition let z be complex number ; func Re z -> set means :Def1: :: COMPLEX1:def 1 it = z if z in REAL otherwise ex f being Function of 2,REAL st ( z = f & it = f . 0 ); existence ( ( z in REAL implies ex b1 being set st b1 = z ) & ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st ( z = f & b1 = f . 0 ) ) ) proof thus ( z in REAL implies ex IT being set st IT = z ) ; ::_thesis: ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st ( z = f & b1 = f . 0 ) ) A1: z in COMPLEX by XCMPLX_0:def_2; assume not z in REAL ; ::_thesis: ex b1 being set ex f being Function of 2,REAL st ( z = f & b1 = f . 0 ) then z in (Funcs (2,REAL)) \ { x where x is Element of Funcs (2,REAL) : x . 1 = 0 } by A1, CARD_1:50, NUMBERS:def_2, XBOOLE_0:def_3; then reconsider f = z as Function of 2,REAL by FUNCT_2:66; take f . 0 ; ::_thesis: ex f being Function of 2,REAL st ( z = f & f . 0 = f . 0 ) take f ; ::_thesis: ( z = f & f . 0 = f . 0 ) thus ( z = f & f . 0 = f . 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being set holds ( ( z in REAL & b1 = z & b2 = z implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2,REAL st ( z = f & b1 = f . 0 ) & ex f being Function of 2,REAL st ( z = f & b2 = f . 0 ) implies b1 = b2 ) ) ; consistency for b1 being set holds verum ; func Im z -> set means :Def2: :: COMPLEX1:def 2 it = 0 if z in REAL otherwise ex f being Function of 2,REAL st ( z = f & it = f . 1 ); existence ( ( z in REAL implies ex b1 being set st b1 = 0 ) & ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st ( z = f & b1 = f . 1 ) ) ) proof thus ( z in REAL implies ex IT being set st IT = 0 ) ; ::_thesis: ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st ( z = f & b1 = f . 1 ) ) A2: z in COMPLEX by XCMPLX_0:def_2; assume not z in REAL ; ::_thesis: ex b1 being set ex f being Function of 2,REAL st ( z = f & b1 = f . 1 ) then z in (Funcs (2,REAL)) \ { x where x is Element of Funcs (2,REAL) : x . 1 = 0 } by A2, CARD_1:50, NUMBERS:def_2, XBOOLE_0:def_3; then reconsider f = z as Function of 2,REAL by FUNCT_2:66; take f . 1 ; ::_thesis: ex f being Function of 2,REAL st ( z = f & f . 1 = f . 1 ) take f ; ::_thesis: ( z = f & f . 1 = f . 1 ) thus ( z = f & f . 1 = f . 1 ) ; ::_thesis: verum end; uniqueness for b1, b2 being set holds ( ( z in REAL & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2,REAL st ( z = f & b1 = f . 1 ) & ex f being Function of 2,REAL st ( z = f & b2 = f . 1 ) implies b1 = b2 ) ) ; consistency for b1 being set holds verum ; end; :: deftheorem Def1 defines Re COMPLEX1:def_1_:_ for z being complex number for b2 being set holds ( ( z in REAL implies ( b2 = Re z iff b2 = z ) ) & ( not z in REAL implies ( b2 = Re z iff ex f being Function of 2,REAL st ( z = f & b2 = f . 0 ) ) ) ); :: deftheorem Def2 defines Im COMPLEX1:def_2_:_ for z being complex number for b2 being set holds ( ( z in REAL implies ( b2 = Im z iff b2 = 0 ) ) & ( not z in REAL implies ( b2 = Im z iff ex f being Function of 2,REAL st ( z = f & b2 = f . 1 ) ) ) ); registration let z be complex number ; cluster Re z -> real ; coherence Re z is real proof percases ( z in REAL or not z in REAL ) ; suppose z in REAL ; ::_thesis: Re z is real hence Re z is real by Def1; ::_thesis: verum end; suppose not z in REAL ; ::_thesis: Re z is real then consider f being Function of 2,REAL such that z = f and A1: Re z = f . 0 by Def1; 0 in 2 by CARD_1:50, TARSKI:def_2; then f . 0 in REAL by FUNCT_2:5; hence Re z is real by A1; ::_thesis: verum end; end; end; cluster Im z -> real ; coherence Im z is real proof percases ( z in REAL or not z in REAL ) ; suppose z in REAL ; ::_thesis: Im z is real hence Im z is real by Def2; ::_thesis: verum end; suppose not z in REAL ; ::_thesis: Im z is real then consider f being Function of 2,REAL such that z = f and A2: Im z = f . 1 by Def2; 1 in 2 by CARD_1:50, TARSKI:def_2; then f . 1 in REAL by FUNCT_2:5; hence Im z is real by A2; ::_thesis: verum end; end; end; end; definition let z be complex number ; :: original: Re redefine func Re z -> Real; coherence Re z is Real by XREAL_0:def_1; :: original: Im redefine func Im z -> Real; coherence Im z is Real by XREAL_0:def_1; end; theorem Th2: :: COMPLEX1:2 for f being Function of 2,REAL ex a, b being Element of REAL st f = (0,1) --> (a,b) proof let f be Function of 2,REAL; ::_thesis: ex a, b being Element of REAL st f = (0,1) --> (a,b) ( 0 in 2 & 1 in 2 ) by CARD_1:50, TARSKI:def_2; then reconsider a = f . 0, b = f . 1 as Element of REAL by FUNCT_2:5; take a ; ::_thesis: ex b being Element of REAL st f = (0,1) --> (a,b) take b ; ::_thesis: f = (0,1) --> (a,b) dom f = {0,1} by CARD_1:50, FUNCT_2:def_1; hence f = (0,1) --> (a,b) by FUNCT_4:66; ::_thesis: verum end; Lm2: for a, b being Element of REAL holds ( Re [*a,b*] = a & Im [*a,b*] = b ) proof let a, b be Element of REAL ; ::_thesis: ( Re [*a,b*] = a & Im [*a,b*] = b ) reconsider a9 = a, b9 = b as Element of REAL ; thus Re [*a,b*] = a ::_thesis: Im [*a,b*] = b proof percases ( b = 0 or b <> 0 ) ; suppose b = 0 ; ::_thesis: Re [*a,b*] = a then [*a,b*] = a by ARYTM_0:def_5; hence Re [*a,b*] = a by Def1; ::_thesis: verum end; suppose b <> 0 ; ::_thesis: Re [*a,b*] = a then A1: [*a,b*] = (0,1) --> (a9,b9) by ARYTM_0:def_5; then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:50; ( not [*a,b*] in REAL & f . 0 = a ) by A1, ARYTM_0:8, FUNCT_4:63; hence Re [*a,b*] = a by Def1; ::_thesis: verum end; end; end; percases ( b = 0 or b <> 0 ) ; supposeA2: b = 0 ; ::_thesis: Im [*a,b*] = b then [*a,b*] = a by ARYTM_0:def_5; hence Im [*a,b*] = b by A2, Def2; ::_thesis: verum end; suppose b <> 0 ; ::_thesis: Im [*a,b*] = b then A3: [*a,b*] = (0,1) --> (a9,b9) by ARYTM_0:def_5; then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:50; ( not [*a,b*] in REAL & f . 1 = b ) by A3, ARYTM_0:8, FUNCT_4:63; hence Im [*a,b*] = b by Def2; ::_thesis: verum end; end; end; Lm3: for z being complex number holds [*(Re z),(Im z)*] = z proof let z be complex number ; ::_thesis: [*(Re z),(Im z)*] = z A1: z in COMPLEX by XCMPLX_0:def_2; percases ( z in REAL or not z in REAL ) ; supposeA2: z in REAL ; ::_thesis: [*(Re z),(Im z)*] = z then Im z = 0 by Def2; hence [*(Re z),(Im z)*] = Re z by ARYTM_0:def_5 .= z by A2, Def1 ; ::_thesis: verum end; supposeA3: not z in REAL ; ::_thesis: [*(Re z),(Im z)*] = z then A4: ex f being Function of 2,REAL st ( z = f & Im z = f . 1 ) by Def2; then consider a, b being Element of REAL such that A5: z = (0,1) --> (a,b) by Th2; reconsider f = z as Element of Funcs (2,REAL) by A5, CARD_1:50, FUNCT_2:8; z in (Funcs (2,REAL)) \ { x where x is Element of Funcs (2,REAL) : x . 1 = 0 } by A1, A3, CARD_1:50, NUMBERS:def_2, XBOOLE_0:def_3; then not z in { x where x is Element of Funcs (2,REAL) : x . 1 = 0 } by XBOOLE_0:def_5; then f . 1 <> 0 ; then A6: b <> 0 by A5, FUNCT_4:63; ex f being Function of 2,REAL st ( z = f & Re z = f . 0 ) by A3, Def1; then A7: Re z = a by A5, FUNCT_4:63; Im z = b by A4, A5, FUNCT_4:63; hence [*(Re z),(Im z)*] = z by A5, A7, A6, ARYTM_0:def_5; ::_thesis: verum end; end; end; theorem Th3: :: COMPLEX1:3 for z1, z2 being complex number st Re z1 = Re z2 & Im z1 = Im z2 holds z1 = z2 proof let z1, z2 be complex number ; ::_thesis: ( Re z1 = Re z2 & Im z1 = Im z2 implies z1 = z2 ) assume ( Re z1 = Re z2 & Im z1 = Im z2 ) ; ::_thesis: z1 = z2 hence z1 = [*(Re z2),(Im z2)*] by Lm3 .= z2 by Lm3 ; ::_thesis: verum end; definition let z1, z2 be complex number ; redefine pred z1 = z2 means :: COMPLEX1:def 3 ( Re z1 = Re z2 & Im z1 = Im z2 ); compatibility ( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) ) by Th3; end; :: deftheorem defines = COMPLEX1:def_3_:_ for z1, z2 being complex number holds ( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) ); notation synonym 0c for 0 ; end; definition :: original: 0c redefine func 0c -> Element of COMPLEX ; correctness coherence 0c is Element of COMPLEX ; by XCMPLX_0:def_2; end; definition func 1r -> Element of COMPLEX equals :: COMPLEX1:def 4 1; correctness coherence 1 is Element of COMPLEX ; by XCMPLX_0:def_2; :: original: redefine func -> Element of COMPLEX ; coherence is Element of COMPLEX by XCMPLX_0:def_2; end; :: deftheorem defines 1r COMPLEX1:def_4_:_ 1r = 1; Lm4: 0 = [*0,0*] by ARYTM_0:def_5; Lm5: 1r = [*1,0*] by ARYTM_0:def_5; theorem Th4: :: COMPLEX1:4 ( Re 0 = 0 & Im 0 = 0 ) by Lm2, Lm4; theorem Th5: :: COMPLEX1:5 for z being complex number holds ( z = 0 iff ((Re z) ^2) + ((Im z) ^2) = 0 ) proof let z be complex number ; ::_thesis: ( z = 0 iff ((Re z) ^2) + ((Im z) ^2) = 0 ) set r = Re z; set i = Im z; thus ( z = 0 implies ((Re z) ^2) + ((Im z) ^2) = 0 ) by Th4; ::_thesis: ( ((Re z) ^2) + ((Im z) ^2) = 0 implies z = 0 ) assume 0 = ((Re z) ^2) + ((Im z) ^2) ; ::_thesis: z = 0 then ( Re z = 0 & Im z = 0 ) by Th1; hence z = 0 by Th3, Th4; ::_thesis: verum end; theorem Th6: :: COMPLEX1:6 ( Re 1r = 1 & Im 1r = 0 ) by Lm2, Lm5; Lm6: = [*0,1*] by ARYTM_0:def_5, XCMPLX_0:def_1; theorem Th7: :: COMPLEX1:7 ( Re = 0 & Im = 1 ) by Lm2, Lm6; Lm7: for x being real number for x1, x2 being Element of REAL st x = [*x1,x2*] holds ( x2 = 0 & x = x1 ) proof let x be real number ; ::_thesis: for x1, x2 being Element of REAL st x = [*x1,x2*] holds ( x2 = 0 & x = x1 ) let x1, x2 be Element of REAL ; ::_thesis: ( x = [*x1,x2*] implies ( x2 = 0 & x = x1 ) ) assume A1: x = [*x1,x2*] ; ::_thesis: ( x2 = 0 & x = x1 ) A2: x in REAL by XREAL_0:def_1; hereby ::_thesis: x = x1 assume x2 <> 0 ; ::_thesis: contradiction then x = (0,1) --> (x1,x2) by A1, ARYTM_0:def_5; hence contradiction by A2, ARYTM_0:8; ::_thesis: verum end; hence x = x1 by A1, ARYTM_0:def_5; ::_thesis: verum end; Lm8: for x9, y9 being Element of REAL for x, y being real number st x9 = x & y9 = y holds + (x9,y9) = x + y proof let x9, y9 be Element of REAL ; ::_thesis: for x, y being real number st x9 = x & y9 = y holds + (x9,y9) = x + y let x, y be real number ; ::_thesis: ( x9 = x & y9 = y implies + (x9,y9) = x + y ) assume A1: ( x9 = x & y9 = y ) ; ::_thesis: + (x9,y9) = x + y consider x1, x2, y1, y2 being Element of REAL such that A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4; ( x2 = 0 & y2 = 0 ) by A2, Lm7; then A4: + (x2,y2) = 0 by ARYTM_0:11; ( x = x1 & y = y1 ) by A2, Lm7; hence + (x9,y9) = x + y by A1, A3, A4, ARYTM_0:def_5; ::_thesis: verum end; Lm9: for x being Element of REAL holds opp x = - x proof let x be Element of REAL ; ::_thesis: opp x = - x + (x,(opp x)) = 0 by ARYTM_0:def_3; then x + (opp x) = 0 by Lm8; hence opp x = - x ; ::_thesis: verum end; Lm10: for x9, y9 being Element of REAL for x, y being real number st x9 = x & y9 = y holds * (x9,y9) = x * y proof let x9, y9 be Element of REAL ; ::_thesis: for x, y being real number st x9 = x & y9 = y holds * (x9,y9) = x * y let x, y be real number ; ::_thesis: ( x9 = x & y9 = y implies * (x9,y9) = x * y ) assume A1: ( x9 = x & y9 = y ) ; ::_thesis: * (x9,y9) = x * y consider x1, x2, y1, y2 being Element of REAL such that A2: x = [*x1,x2*] and A3: y = [*y1,y2*] and A4: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5; x2 = 0 by A2, Lm7; then A5: * (x2,y1) = 0 by ARYTM_0:12; A6: y2 = 0 by A3, Lm7; then * (x1,y2) = 0 by ARYTM_0:12; then A7: + ((* (x1,y2)),(* (x2,y1))) = 0 by A5, ARYTM_0:11; ( x = x1 & y = y1 ) by A2, A3, Lm7; hence * (x9,y9) = + ((* (x1,y1)),(* ((opp x2),y2))) by A1, A6, ARYTM_0:11, ARYTM_0:12 .= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15 .= x * y by A4, A7, ARYTM_0:def_5 ; ::_thesis: verum end; Lm11: for x, y, z being complex number st z = x + y holds Re z = (Re x) + (Re y) proof let x, y, z be complex number ; ::_thesis: ( z = x + y implies Re z = (Re x) + (Re y) ) assume A1: z = x + y ; ::_thesis: Re z = (Re x) + (Re y) consider x1, x2, y1, y2 being Element of REAL such that A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4; A4: ( Re x = x1 & Re y = y1 ) by A2, Lm2; thus Re z = + (x1,y1) by A1, A3, Lm2 .= (Re x) + (Re y) by A4, Lm8 ; ::_thesis: verum end; Lm12: for x, y, z being complex number st z = x + y holds Im z = (Im x) + (Im y) proof let x, y, z be complex number ; ::_thesis: ( z = x + y implies Im z = (Im x) + (Im y) ) assume A1: z = x + y ; ::_thesis: Im z = (Im x) + (Im y) consider x1, x2, y1, y2 being Element of REAL such that A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4; A4: ( Im x = x2 & Im y = y2 ) by A2, Lm2; thus Im z = + (x2,y2) by A1, A3, Lm2 .= (Im x) + (Im y) by A4, Lm8 ; ::_thesis: verum end; Lm13: for x, y, z being complex number st z = x * y holds Re z = ((Re x) * (Re y)) - ((Im x) * (Im y)) proof let x, y, z be complex number ; ::_thesis: ( z = x * y implies Re z = ((Re x) * (Re y)) - ((Im x) * (Im y)) ) assume A1: z = x * y ; ::_thesis: Re z = ((Re x) * (Re y)) - ((Im x) * (Im y)) consider x1, x2, y1, y2 being Element of REAL such that A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and A3: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5; A4: ( Re x = x1 & Re y = y1 ) by A2, Lm2; A5: ( Im x = x2 & Im y = y2 ) by A2, Lm2; thus Re z = + ((* (x1,y1)),(opp (* (x2,y2)))) by A1, A3, Lm2 .= (* (x1,y1)) + (opp (* (x2,y2))) by Lm8 .= (x1 * y1) + (opp (* (x2,y2))) by Lm10 .= (x1 * y1) + (- (* (x2,y2))) by Lm9 .= (x1 * y1) - (* (x2,y2)) .= ((Re x) * (Re y)) - ((Im x) * (Im y)) by A4, A5, Lm10 ; ::_thesis: verum end; Lm14: for x, y, z being complex number st z = x * y holds Im z = ((Re x) * (Im y)) + ((Im x) * (Re y)) proof let x, y, z be complex number ; ::_thesis: ( z = x * y implies Im z = ((Re x) * (Im y)) + ((Im x) * (Re y)) ) assume A1: z = x * y ; ::_thesis: Im z = ((Re x) * (Im y)) + ((Im x) * (Re y)) consider x1, x2, y1, y2 being Element of REAL such that A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and A3: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5; A4: ( Im x = x2 & Im y = y2 ) by A2, Lm2; A5: ( Re x = x1 & Re y = y1 ) by A2, Lm2; thus Im z = + ((* (x1,y2)),(* (x2,y1))) by A1, A3, Lm2 .= (* (x1,y2)) + (* (x2,y1)) by Lm8 .= (x1 * y2) + (* (x2,y1)) by Lm10 .= ((Re x) * (Im y)) + ((Im x) * (Re y)) by A4, A5, Lm10 ; ::_thesis: verum end; Lm15: for z1, z2 being complex number holds z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] proof let z1, z2 be complex number ; ::_thesis: z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] set z = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]; reconsider z9 = z1 + z2 as Element of COMPLEX by XCMPLX_0:def_2; A1: Im [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] = (Im z1) + (Im z2) by Lm2 .= Im z9 by Lm12 ; Re [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] = (Re z1) + (Re z2) by Lm2 .= Re z9 by Lm11 ; hence z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by A1, Th3; ::_thesis: verum end; Lm16: for z1, z2 being complex number holds z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] proof let z1, z2 be complex number ; ::_thesis: z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] set z = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*]; reconsider z9 = z1 * z2 as Element of COMPLEX by XCMPLX_0:def_2; A1: Im [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Lm2 .= Im z9 by Lm14 ; Re [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Lm2 .= Re z9 by Lm13 ; hence z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by A1, Th3; ::_thesis: verum end; Lm17: for z1, z2 being complex number holds ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) proof let z1, z2 be complex number ; ::_thesis: ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16; hence ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) by Lm2; ::_thesis: verum end; Lm18: for z1, z2 being complex number holds ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) proof let z1, z2 be complex number ; ::_thesis: ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15; hence ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) by Lm2; ::_thesis: verum end; Lm19: for x being Real holds Re (x * ) = 0 proof let x be Real; ::_thesis: Re (x * ) = 0 thus Re (x * ) = ((Re x) * (Re )) - ((Im x) * (Im )) by Lm17 .= ((Re x) * 0) - (0 * (Im )) by Def2, Th7 .= 0 ; ::_thesis: verum end; Lm20: for x being Real holds Im (x * ) = x proof let x be Real; ::_thesis: Im (x * ) = x thus Im (x * ) = ((Re x) * (Im )) + ((Im x) * (Re )) by Lm17 .= x by Def1, Th7 ; ::_thesis: verum end; Lm21: for x, y being Real holds [*x,y*] = x + (y * ) proof let x, y be Real; ::_thesis: [*x,y*] = x + (y * ) A1: Im (x + (y * )) = (Im x) + (Im (y * )) by Lm18 .= 0 + (Im (y * )) by Def2 .= y by Lm20 ; Re (x + (y * )) = (Re x) + (Re (y * )) by Lm18 .= (Re x) + 0 by Lm19 .= x by Def1 ; hence [*x,y*] = x + (y * ) by A1, Lm3; ::_thesis: verum end; definition let z1, z2 be Element of COMPLEX ; :: original: + redefine funcz1 + z2 -> Element of COMPLEX equals :: COMPLEX1:def 5 ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * ); coherence z1 + z2 is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = z1 + z2 iff b1 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * ) ) proof z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15; hence for b1 being Element of COMPLEX holds ( b1 = z1 + z2 iff b1 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * ) ) by Lm21; ::_thesis: verum end; end; :: deftheorem defines + COMPLEX1:def_5_:_ for z1, z2 being Element of COMPLEX holds z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * ); theorem Th8: :: COMPLEX1:8 for z1, z2 being complex number holds ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) proof let z1, z2 be complex number ; ::_thesis: ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15; hence ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) by Lm2; ::_thesis: verum end; definition let z1, z2 be Element of COMPLEX ; :: original: * redefine funcz1 * z2 -> Element of COMPLEX equals :: COMPLEX1:def 6 (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * ); coherence z1 * z2 is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = z1 * z2 iff b1 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * ) ) proof z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16; hence for b1 being Element of COMPLEX holds ( b1 = z1 * z2 iff b1 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * ) ) by Lm21; ::_thesis: verum end; end; :: deftheorem defines * COMPLEX1:def_6_:_ for z1, z2 being Element of COMPLEX holds z1 * z2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * ); theorem Th9: :: COMPLEX1:9 for z1, z2 being complex number holds ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) proof let z1, z2 be complex number ; ::_thesis: ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16; hence ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) by Lm2; ::_thesis: verum end; theorem :: COMPLEX1:10 for a being real number holds Re (a * ) = 0 proof let a be real number ; ::_thesis: Re (a * ) = 0 A1: a in REAL by XREAL_0:def_1; thus Re (a * ) = ((Re a) * (Re )) - ((Im a) * (Im )) by Th9 .= ((Re a) * 0) - (0 * (Im )) by Def2, Th7, A1 .= 0 ; ::_thesis: verum end; theorem :: COMPLEX1:11 for a being real number holds Im (a * ) = a proof let a be real number ; ::_thesis: Im (a * ) = a A1: a in REAL by XREAL_0:def_1; thus Im (a * ) = ((Re a) * (Im )) + ((Im a) * (Re )) by Th9 .= a by Def1, Th7, A1 ; ::_thesis: verum end; theorem Th12: :: COMPLEX1:12 for a, b being real number holds ( Re (a + (b * )) = a & Im (a + (b * )) = b ) proof let a, b be real number ; ::_thesis: ( Re (a + (b * )) = a & Im (a + (b * )) = b ) reconsider a = a, b = b as Real by XREAL_0:def_1; a + (b * ) = [*a,b*] by Lm21; hence ( Re (a + (b * )) = a & Im (a + (b * )) = b ) by Lm2; ::_thesis: verum end; theorem Th13: :: COMPLEX1:13 for z being complex number holds (Re z) + ((Im z) * ) = z proof let z be complex number ; ::_thesis: (Re z) + ((Im z) * ) = z [*(Re z),(Im z)*] = z by Lm3; hence (Re z) + ((Im z) * ) = z by Lm21; ::_thesis: verum end; theorem Th14: :: COMPLEX1:14 for z1, z2 being complex number st Im z1 = 0 & Im z2 = 0 holds ( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 ) proof let z1, z2 be complex number ; ::_thesis: ( Im z1 = 0 & Im z2 = 0 implies ( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 ) ) assume that A1: Im z1 = 0 and A2: Im z2 = 0 ; ::_thesis: ( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 ) thus Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Th9 .= (Re z1) * (Re z2) by A1 ; ::_thesis: Im (z1 * z2) = 0 thus Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Th9 .= 0 by A1, A2 ; ::_thesis: verum end; theorem Th15: :: COMPLEX1:15 for z1, z2 being complex number st Re z1 = 0 & Re z2 = 0 holds ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 ) proof let z1, z2 be complex number ; ::_thesis: ( Re z1 = 0 & Re z2 = 0 implies ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 ) ) assume that A1: Re z1 = 0 and A2: Re z2 = 0 ; ::_thesis: ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 ) thus Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Th9 .= - ((Im z1) * (Im z2)) by A1 ; ::_thesis: Im (z1 * z2) = 0 thus Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Th9 .= 0 by A1, A2 ; ::_thesis: verum end; theorem :: COMPLEX1:16 for z being complex number holds ( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) ) proof let z be complex number ; ::_thesis: ( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) ) thus Re (z * z) = ((Re z) ^2) - ((Im z) ^2) by Th9; ::_thesis: Im (z * z) = 2 * ((Re z) * (Im z)) thus Im (z * z) = ((Re z) * (Im z)) + ((Re z) * (Im z)) by Th9 .= 2 * ((Re z) * (Im z)) ; ::_thesis: verum end; definition let z be Element of COMPLEX ; :: original: - redefine func - z -> Element of COMPLEX equals :Def7: :: COMPLEX1:def 7 (- (Re z)) + ((- (Im z)) * ); coherence - z is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = - z iff b1 = (- (Re z)) + ((- (Im z)) * ) ) proof set z9 = [*(- (Re z)),(- (Im z))*]; [*(- (Re z)),(- (Im z))*] + z = [*((Re [*(- (Re z)),(- (Im z))*]) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm15 .= [*((- (Re z)) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm2 .= [*0,((- (Im z)) + (Im z))*] by Lm2 .= 0 by ARYTM_0:def_5 ; hence for b1 being Element of COMPLEX holds ( b1 = - z iff b1 = (- (Re z)) + ((- (Im z)) * ) ) by Lm21; ::_thesis: verum end; end; :: deftheorem Def7 defines - COMPLEX1:def_7_:_ for z being Element of COMPLEX holds - z = (- (Re z)) + ((- (Im z)) * ); theorem Th17: :: COMPLEX1:17 for z being complex number holds ( Re (- z) = - (Re z) & Im (- z) = - (Im z) ) proof let z be complex number ; ::_thesis: ( Re (- z) = - (Re z) & Im (- z) = - (Im z) ) z in COMPLEX by XCMPLX_0:def_2; then - z = (- (Re z)) + ((- (Im z)) * ) by Def7; hence ( Re (- z) = - (Re z) & Im (- z) = - (Im z) ) by Th12; ::_thesis: verum end; theorem :: COMPLEX1:18 * = - 1r ; definition let z1, z2 be Element of COMPLEX ; :: original: - redefine funcz1 - z2 -> Element of COMPLEX equals :Def8: :: COMPLEX1:def 8 ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * ); coherence z1 - z2 is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = z1 - z2 iff b1 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * ) ) proof A1: z1 = (Re z1) + ((Im z1) * ) by Th13; z1 - z2 = z1 + (- z2) .= z1 + ((- (Re z2)) + ((- (Im z2)) * )) by Def7 .= ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * ) by A1 ; hence for b1 being Element of COMPLEX holds ( b1 = z1 - z2 iff b1 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * ) ) ; ::_thesis: verum end; end; :: deftheorem Def8 defines - COMPLEX1:def_8_:_ for z1, z2 being Element of COMPLEX holds z1 - z2 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * ); theorem Th19: :: COMPLEX1:19 for z1, z2 being complex number holds ( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) ) proof let z1, z2 be complex number ; ::_thesis: ( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) ) A1: ( z1 in COMPLEX & z2 in COMPLEX ) by XCMPLX_0:def_2; hence Re (z1 - z2) = Re (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * )) by Def8 .= (Re z1) - (Re z2) by Th12 ; ::_thesis: Im (z1 - z2) = (Im z1) - (Im z2) thus Im (z1 - z2) = Im (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * )) by A1, Def8 .= (Im z1) - (Im z2) by Th12 ; ::_thesis: verum end; definition let z be Element of COMPLEX ; :: original: " redefine funcz " -> Element of COMPLEX equals :Def9: :: COMPLEX1:def 9 ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ); coherence z " is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = z " iff b1 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) ) proof reconsider z9 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) as Element of COMPLEX by XCMPLX_0:def_2; percases ( z = 0 or z <> 0 ) ; suppose z = 0 ; ::_thesis: for b1 being Element of COMPLEX holds ( b1 = z " iff b1 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) ) hence for b1 being Element of COMPLEX holds ( b1 = z " iff b1 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) ) by Th4; ::_thesis: verum end; supposeA1: z <> 0 ; ::_thesis: for b1 being Element of COMPLEX holds ( b1 = z " iff b1 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) ) then A2: ((Re z) ^2) + ((Im z) ^2) <> 0 by Th5; A3: Im z9 = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th12; then A4: ((Re z) * (Im z9)) + ((Re z9) * (Im z)) = (((Re z) / 1) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) + (((Re z) / (((Re z) ^2) + ((Im z) ^2))) * (Im z)) by Th12 .= (((Re z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) + ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) * (Im z)) / 1) by XCMPLX_1:76 .= (((Re z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) + ((((Im z) / 1) * (Re z)) / (((Re z) ^2) + ((Im z) ^2))) by XCMPLX_1:76 .= ((- ((Re z) * (Im z))) + ((Re z) * (Im z))) / (((Re z) ^2) + ((Im z) ^2)) by XCMPLX_1:62 .= 0 ; A5: ((Re z) * (Re z9)) - ((Im z) * (Im z9)) = (((Re z) / 1) * ((Re z) / (((Re z) ^2) + ((Im z) ^2)))) - ((Im z) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) by A3, Th12 .= (((Re z) * (Re z)) / (1 * (((Re z) ^2) + ((Im z) ^2)))) - (((Im z) / 1) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:76 .= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - (((Im z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:76 .= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - ((- ((Im z) ^2)) / (1 * (((Re z) ^2) + ((Im z) ^2)))) .= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - (- (((Im z) ^2) / (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:187 .= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) + (((Im z) ^2) / (1 * (((Re z) ^2) + ((Im z) ^2)))) .= (((Re z) ^2) + ((Im z) ^2)) / (((Re z) ^2) + ((Im z) ^2)) by XCMPLX_1:62 .= 1 by A2, XCMPLX_1:60 ; z * z9 = [*(((Re z) * (Re z9)) - ((Im z) * (Im z9))),(((Re z) * (Im z9)) + ((Re z9) * (Im z)))*] by Lm16 .= 1 by A5, A4, ARYTM_0:def_5 ; hence for b1 being Element of COMPLEX holds ( b1 = z " iff b1 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) ) by A1, XCMPLX_0:def_7; ::_thesis: verum end; end; end; end; :: deftheorem Def9 defines " COMPLEX1:def_9_:_ for z being Element of COMPLEX holds z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ); theorem Th20: :: COMPLEX1:20 for z being complex number holds ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) proof let z be complex number ; ::_thesis: ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) z in COMPLEX by XCMPLX_0:def_2; then z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * ) by Def9; hence ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) by Th12; ::_thesis: verum end; theorem :: COMPLEX1:21 " = - ; theorem Th22: :: COMPLEX1:22 for z being complex number st Re z <> 0 & Im z = 0 holds ( Re (z ") = (Re z) " & Im (z ") = 0 ) proof let z be complex number ; ::_thesis: ( Re z <> 0 & Im z = 0 implies ( Re (z ") = (Re z) " & Im (z ") = 0 ) ) assume that A1: Re z <> 0 and A2: Im z = 0 ; ::_thesis: ( Re (z ") = (Re z) " & Im (z ") = 0 ) Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20; hence Re (z ") = (1 * (Re z)) / ((Re z) * (Re z)) by A2 .= 1 / (Re z) by A1, XCMPLX_1:91 .= (Re z) " by XCMPLX_1:215 ; ::_thesis: Im (z ") = 0 Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th20; hence Im (z ") = 0 by A2; ::_thesis: verum end; theorem Th23: :: COMPLEX1:23 for z being complex number st Re z = 0 & Im z <> 0 holds ( Re (z ") = 0 & Im (z ") = - ((Im z) ") ) proof let z be complex number ; ::_thesis: ( Re z = 0 & Im z <> 0 implies ( Re (z ") = 0 & Im (z ") = - ((Im z) ") ) ) assume that A1: Re z = 0 and A2: Im z <> 0 ; ::_thesis: ( Re (z ") = 0 & Im (z ") = - ((Im z) ") ) Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20; hence Re (z ") = 0 by A1; ::_thesis: Im (z ") = - ((Im z) ") Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th20; hence Im (z ") = - ((1 * (Im z)) / ((Im z) * (Im z))) by A1, XCMPLX_1:187 .= - (1 / (Im z)) by A2, XCMPLX_1:91 .= - ((Im z) ") by XCMPLX_1:215 ; ::_thesis: verum end; definition let z1, z2 be complex number ; :: original: / redefine funcz1 / z2 -> Element of COMPLEX equals :Def10: :: COMPLEX1:def 10 ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * ); coherence z1 / z2 is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = z1 / z2 iff b1 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * ) ) proof reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def_2; set k = ((Re z2) ^2) + ((Im z2) ^2); A1: Re [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] = Re (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) + (((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))) * )) by Lm21 .= (Re z2) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; A2: Im [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] = Im (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) + (((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))) * )) by Lm21 .= (- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; z1 / z2 = z1 * (z2 ") by XCMPLX_0:def_9 .= z1 * [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] by Lm21 .= [*((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2) + ((Im z2) ^2)))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))),(((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1)))*] by A1, A2, Lm16 .= ((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2) + ((Im z2) ^2)))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * ) by Lm21 .= ((((Re z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2)))) - (((Im z1) / 1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * ) by XCMPLX_1:76 .= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) + (((((Re z1) / 1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * ) by XCMPLX_1:76 .= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((((Re z1) * (- (Im z2))) / (1 * (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * ((Im z1) / 1))) * ) by XCMPLX_1:76 .= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) * ) by XCMPLX_1:76 .= ((((Re z1) * (Re z2)) - ((Im z1) * (- (Im z2)))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) * ) by XCMPLX_1:120 .= ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + ((((- ((Re z1) * (Im z2))) + ((Im z1) * (Re z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * ) by XCMPLX_1:62 .= ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * ) ; hence for b1 being Element of COMPLEX holds ( b1 = z1 / z2 iff b1 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * ) ) ; ::_thesis: verum end; end; :: deftheorem Def10 defines / COMPLEX1:def_10_:_ for z1, z2 being complex number holds z1 / z2 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * ); theorem :: COMPLEX1:24 for z1, z2 being complex number holds ( Re (z1 / z2) = (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) & Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) ) proof let z1, z2 be complex number ; ::_thesis: ( Re (z1 / z2) = (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) & Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) ) thus Re (z1 / z2) = Re (((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * )) by Def10 .= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; ::_thesis: Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) thus Im (z1 / z2) = Im (((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * )) by Def10 .= (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; ::_thesis: verum end; theorem :: COMPLEX1:25 for z1, z2 being complex number st Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 holds ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 ) proof let z1, z2 be complex number ; ::_thesis: ( Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 ) ) assume that A1: Im z1 = 0 and A2: ( Im z2 = 0 & Re z2 <> 0 ) ; ::_thesis: ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 ) A3: ( z1 / z2 = z1 * (z2 ") & Im (z2 ") = 0 ) by A2, Th22, XCMPLX_0:def_9; hence Re (z1 / z2) = (Re z1) * (Re (z2 ")) by A1, Th14 .= (Re z1) * ((Re z2) ") by A2, Th22 .= (Re z1) / (Re z2) by XCMPLX_0:def_9 ; ::_thesis: Im (z1 / z2) = 0 thus Im (z1 / z2) = 0 by A1, A3, Th14; ::_thesis: verum end; theorem :: COMPLEX1:26 for z1, z2 being complex number st Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 holds ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 ) proof let z1, z2 be complex number ; ::_thesis: ( Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 implies ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 ) ) assume that A1: Re z1 = 0 and A2: ( Re z2 = 0 & Im z2 <> 0 ) ; ::_thesis: ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 ) A3: ( z1 / z2 = z1 * (z2 ") & Re (z2 ") = 0 ) by A2, Th23, XCMPLX_0:def_9; hence Re (z1 / z2) = - ((Im z1) * (Im (z2 "))) by A1, Th15 .= - ((Im z1) * (- ((Im z2) "))) by A2, Th23 .= - (- ((Im z1) * ((Im z2) "))) .= (Im z1) / (Im z2) by XCMPLX_0:def_9 ; ::_thesis: Im (z1 / z2) = 0 thus Im (z1 / z2) = 0 by A1, A3, Th15; ::_thesis: verum end; definition let z be complex number ; funcz *' -> complex number equals :: COMPLEX1:def 11 (Re z) - ((Im z) * ); correctness coherence (Re z) - ((Im z) * ) is complex number ; ; involutiveness for b1, b2 being complex number st b1 = (Re b2) - ((Im b2) * ) holds b2 = (Re b1) - ((Im b1) * ) proof let z, z9 be complex number ; ::_thesis: ( z = (Re z9) - ((Im z9) * ) implies z9 = (Re z) - ((Im z) * ) ) assume z = (Re z9) - ((Im z9) * ) ; ::_thesis: z9 = (Re z) - ((Im z) * ) then z = (Re z9) + ((- (Im z9)) * ) ; then ( Re z = Re z9 & - (Im z) = - (- (Im z9)) ) by Th12; hence z9 = (Re z) + ((- (Im z)) * ) by Th13 .= (Re z) - ((Im z) * ) ; ::_thesis: verum end; end; :: deftheorem defines *' COMPLEX1:def_11_:_ for z being complex number holds z *' = (Re z) - ((Im z) * ); definition let z be complex number ; :: original: *' redefine funcz *' -> Element of COMPLEX ; coherence z *' is Element of COMPLEX by XCMPLX_0:def_2; end; theorem Th27: :: COMPLEX1:27 for z being complex number holds ( Re (z *') = Re z & Im (z *') = - (Im z) ) proof let z be complex number ; ::_thesis: ( Re (z *') = Re z & Im (z *') = - (Im z) ) z *' = (Re z) + ((- (Im z)) * ) ; hence ( Re (z *') = Re z & Im (z *') = - (Im z) ) by Th12; ::_thesis: verum end; theorem :: COMPLEX1:28 0 *' = 0 by Th4; theorem :: COMPLEX1:29 for z being complex number st z *' = 0 holds z = 0 proof let z be complex number ; ::_thesis: ( z *' = 0 implies z = 0 ) assume z *' = 0 ; ::_thesis: z = 0 then 0 = (Re z) + ((- (Im z)) * ) ; hence ( Re z = Re 0 & Im z = Im 0 ) by Th4, Th12; :: according to COMPLEX1:def_3 ::_thesis: verum end; theorem :: COMPLEX1:30 1r *' = 1r by Th6; theorem :: COMPLEX1:31 *' = - by Th7; theorem Th32: :: COMPLEX1:32 for z1, z2 being complex number holds (z1 + z2) *' = (z1 *') + (z2 *') proof let z1, z2 be complex number ; ::_thesis: (z1 + z2) *' = (z1 *') + (z2 *') thus Re ((z1 + z2) *') = Re (z1 + z2) by Th27 .= (Re z1) + (Re z2) by Th8 .= (Re (z1 *')) + (Re z2) by Th27 .= (Re (z1 *')) + (Re (z2 *')) by Th27 .= Re ((z1 *') + (z2 *')) by Th8 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((z1 + z2) *') = Im ((z1 *') + (z2 *')) thus Im ((z1 + z2) *') = - (Im (z1 + z2)) by Th27 .= - ((Im z1) + (- (- (Im z2)))) by Th8 .= (- (Im z1)) + (- (Im z2)) .= (Im (z1 *')) + (- (Im z2)) by Th27 .= (Im (z1 *')) + (Im (z2 *')) by Th27 .= Im ((z1 *') + (z2 *')) by Th8 ; ::_thesis: verum end; theorem Th33: :: COMPLEX1:33 for z being complex number holds (- z) *' = - (z *') proof let z be complex number ; ::_thesis: (- z) *' = - (z *') thus Re ((- z) *') = Re (- z) by Th27 .= - (Re z) by Th17 .= - (Re (z *')) by Th27 .= Re (- (z *')) by Th17 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((- z) *') = Im (- (z *')) thus Im ((- z) *') = - (Im (- z)) by Th27 .= - (- (Im z)) by Th17 .= - (Im (z *')) by Th27 .= Im (- (z *')) by Th17 ; ::_thesis: verum end; theorem :: COMPLEX1:34 for z1, z2 being complex number holds (z1 - z2) *' = (z1 *') - (z2 *') proof let z1, z2 be complex number ; ::_thesis: (z1 - z2) *' = (z1 *') - (z2 *') thus (z1 - z2) *' = (z1 + (- z2)) *' .= (z1 *') + ((- z2) *') by Th32 .= (z1 *') + (- (z2 *')) by Th33 .= (z1 *') - (z2 *') ; ::_thesis: verum end; theorem Th35: :: COMPLEX1:35 for z1, z2 being complex number holds (z1 * z2) *' = (z1 *') * (z2 *') proof let z1, z2 be complex number ; ::_thesis: (z1 * z2) *' = (z1 *') * (z2 *') A1: ( Re (z1 *') = Re z1 & Re (z2 *') = Re z2 ) by Th27; A2: ( Im (z1 *') = - (Im z1) & Im (z2 *') = - (Im z2) ) by Th27; thus Re ((z1 * z2) *') = Re (z1 * z2) by Th27 .= ((Re (z1 *')) * (Re (z2 *'))) - ((- (Im (z1 *'))) * (- (Im (z2 *')))) by A1, A2, Th9 .= ((Re (z1 *')) * (Re (z2 *'))) - (- (- ((Im (z1 *')) * (Im (z2 *'))))) .= Re ((z1 *') * (z2 *')) by Th9 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((z1 * z2) *') = Im ((z1 *') * (z2 *')) thus Im ((z1 * z2) *') = - (Im (z1 * z2)) by Th27 .= - (((Re (z1 *')) * (- (Im (z2 *')))) + ((Re (z2 *')) * (- (Im (z1 *'))))) by A1, A2, Th9 .= ((Re (z2 *')) * (Im (z1 *'))) + (- (- ((Re (z1 *')) * (Im (z2 *'))))) .= Im ((z1 *') * (z2 *')) by Th9 ; ::_thesis: verum end; theorem Th36: :: COMPLEX1:36 for z being complex number holds (z ") *' = (z *') " proof let z be complex number ; ::_thesis: (z ") *' = (z *') " A1: ( Re z = Re (z *') & - (Im z) = Im (z *') ) by Th27; thus Re ((z ") *') = Re (z ") by Th27 .= (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20 .= Re ((z *') ") by A1, Th20 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((z ") *') = Im ((z *') ") thus Im ((z ") *') = - (Im (z ")) by Th27 .= - ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) by Th20 .= (- (Im (z *'))) / (((Re (z *')) ^2) + ((Im (z *')) ^2)) by A1, XCMPLX_1:187 .= Im ((z *') ") by Th20 ; ::_thesis: verum end; theorem :: COMPLEX1:37 for z1, z2 being complex number holds (z1 / z2) *' = (z1 *') / (z2 *') proof let z1, z2 be complex number ; ::_thesis: (z1 / z2) *' = (z1 *') / (z2 *') thus (z1 / z2) *' = (z1 * (z2 ")) *' by XCMPLX_0:def_9 .= (z1 *') * ((z2 ") *') by Th35 .= (z1 *') * ((z2 *') ") by Th36 .= (z1 *') / (z2 *') by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: COMPLEX1:38 for z being complex number st Im z = 0 holds z *' = z proof let z be complex number ; ::_thesis: ( Im z = 0 implies z *' = z ) ( Re (z *') = Re z & Im (z *') = - (Im z) ) by Th27; hence ( Im z = 0 implies z *' = z ) by Th3; ::_thesis: verum end; theorem :: COMPLEX1:39 for z being complex number st Re z = 0 holds z *' = - z proof let z be complex number ; ::_thesis: ( Re z = 0 implies z *' = - z ) A1: z in COMPLEX by XCMPLX_0:def_2; assume A2: Re z = 0 ; ::_thesis: z *' = - z hence z *' = (- 0) + ((- (Im z)) * ) .= - z by A1, A2, Def7 ; ::_thesis: verum end; theorem :: COMPLEX1:40 for z being complex number holds ( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 ) proof let z be complex number ; ::_thesis: ( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 ) thus Re (z * (z *')) = ((Re z) * (Re (z *'))) - ((Im z) * (Im (z *'))) by Th9 .= ((Re z) * (Re z)) - ((Im z) * (Im (z *'))) by Th27 .= ((Re z) * (Re z)) - ((Im z) * (- (Im z))) by Th27 .= ((Re z) ^2) + ((Im z) ^2) ; ::_thesis: Im (z * (z *')) = 0 thus Im (z * (z *')) = ((Re z) * (Im (z *'))) + ((Re (z *')) * (Im z)) by Th9 .= ((Re z) * (- (Im z))) + ((Re (z *')) * (Im z)) by Th27 .= (- ((Re z) * (Im z))) + ((Re z) * (Im z)) by Th27 .= 0 ; ::_thesis: verum end; theorem :: COMPLEX1:41 for z being complex number holds ( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 ) proof let z be complex number ; ::_thesis: ( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 ) thus Re (z + (z *')) = (Re z) + (Re (z *')) by Th8 .= (Re z) + (Re z) by Th27 .= 2 * (Re z) ; ::_thesis: Im (z + (z *')) = 0 thus Im (z + (z *')) = (Im z) + (Im (z *')) by Th8 .= (Im z) + (- (Im z)) by Th27 .= 0 ; ::_thesis: verum end; theorem :: COMPLEX1:42 for z being complex number holds ( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) ) proof let z be complex number ; ::_thesis: ( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) ) thus Re (z - (z *')) = (Re z) - (Re (z *')) by Th19 .= (Re z) - (Re z) by Th27 .= 0 ; ::_thesis: Im (z - (z *')) = 2 * (Im z) thus Im (z - (z *')) = (Im z) - (Im (z *')) by Th19 .= (Im z) - (- (Im z)) by Th27 .= 2 * (Im z) ; ::_thesis: verum end; definition let z be complex number ; func|.z.| -> real number equals :: COMPLEX1:def 12 sqrt (((Re z) ^2) + ((Im z) ^2)); coherence sqrt (((Re z) ^2) + ((Im z) ^2)) is real number ; projectivity for b1 being real number for b2 being complex number st b1 = sqrt (((Re b2) ^2) + ((Im b2) ^2)) holds b1 = sqrt (((Re b1) ^2) + ((Im b1) ^2)) proof let r be real number ; ::_thesis: for b1 being complex number st r = sqrt (((Re b1) ^2) + ((Im b1) ^2)) holds r = sqrt (((Re r) ^2) + ((Im r) ^2)) let z be complex number ; ::_thesis: ( r = sqrt (((Re z) ^2) + ((Im z) ^2)) implies r = sqrt (((Re r) ^2) + ((Im r) ^2)) ) assume A1: r = sqrt (((Re z) ^2) + ((Im z) ^2)) ; ::_thesis: r = sqrt (((Re r) ^2) + ((Im r) ^2)) then A2: Im r = 0 by Def2; ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63; then r >= 0 by A1, SQUARE_1:def_2; then A3: Re r >= 0 by A1, Def1; thus r = Re r by A1, Def1 .= sqrt (((Re r) ^2) + ((Im r) ^2)) by A3, A2, SQUARE_1:22 ; ::_thesis: verum end; end; :: deftheorem defines |. COMPLEX1:def_12_:_ for z being complex number holds |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2)); definition let z be complex number ; :: original: |. redefine func|.z.| -> Real; coherence |.z.| is Real ; end; theorem Th43: :: COMPLEX1:43 for a being real number st a >= 0 holds |.a.| = a proof let a be real number ; ::_thesis: ( a >= 0 implies |.a.| = a ) A1: a in REAL by XREAL_0:def_1; then A2: Im a = 0 by Def2; assume a >= 0 ; ::_thesis: |.a.| = a then Re a >= 0 by A1, Def1; hence |.a.| = Re a by A2, SQUARE_1:22 .= a by A1, Def1 ; ::_thesis: verum end; registration cluster|.0.| -> zero real ; coherence |.0.| is zero by Th4, SQUARE_1:17; end; theorem :: COMPLEX1:44 |.0.| = 0 ; registration let z be non zero complex number ; cluster|.z.| -> non zero real ; coherence not |.z.| is zero proof assume |.z.| is zero ; ::_thesis: contradiction then ((Re z) ^2) + ((Im z) ^2) = 0 by Lm1, SQUARE_1:24; hence contradiction by Th5; ::_thesis: verum end; end; theorem :: COMPLEX1:45 for z being complex number st |.z.| = 0 holds z = 0 ; registration let z be complex number ; cluster|.z.| -> real non negative ; coherence not |.z.| is negative proof 0 <= ((Re z) ^2) + ((Im z) ^2) by Lm1; hence not |.z.| is negative by SQUARE_1:def_2; ::_thesis: verum end; end; theorem :: COMPLEX1:46 for z being complex number holds 0 <= |.z.| ; theorem :: COMPLEX1:47 for z being complex number holds ( z <> 0 iff 0 < |.z.| ) ; theorem Th48: :: COMPLEX1:48 |.1r.| = 1 by Th6, SQUARE_1:18; theorem :: COMPLEX1:49 |..| = 1 by Th7, SQUARE_1:18; Lm22: for z being complex number holds |.(- z).| = |.z.| proof let z be complex number ; ::_thesis: |.(- z).| = |.z.| thus |.(- z).| = sqrt (((- (Re z)) ^2) + ((Im (- z)) ^2)) by Th17 .= sqrt (((- (Re z)) ^2) + ((- (Im z)) ^2)) by Th17 .= |.z.| ; ::_thesis: verum end; Lm23: for a being real number st a <= 0 holds |.a.| = - a proof let a be real number ; ::_thesis: ( a <= 0 implies |.a.| = - a ) assume a <= 0 ; ::_thesis: |.a.| = - a then |.(- a).| = - a by Th43; hence |.a.| = - a by Lm22; ::_thesis: verum end; Lm24: for a being real number holds sqrt (a ^2) = |.a.| proof let a be real number ; ::_thesis: sqrt (a ^2) = |.a.| percases ( 0 <= a or not 0 <= a ) ; supposeA1: 0 <= a ; ::_thesis: sqrt (a ^2) = |.a.| then sqrt (a ^2) = a by SQUARE_1:22; hence sqrt (a ^2) = |.a.| by A1, Th43; ::_thesis: verum end; supposeA2: not 0 <= a ; ::_thesis: sqrt (a ^2) = |.a.| then |.a.| = - a by Lm23; hence sqrt (a ^2) = |.a.| by A2, SQUARE_1:23; ::_thesis: verum end; end; end; theorem :: COMPLEX1:50 for z being complex number st Im z = 0 holds |.z.| = |.(Re z).| by Lm24; theorem :: COMPLEX1:51 for z being complex number st Re z = 0 holds |.z.| = |.(Im z).| by Lm24; theorem :: COMPLEX1:52 for z being complex number holds |.(- z).| = |.z.| by Lm22; theorem Th53: :: COMPLEX1:53 for z being complex number holds |.(z *').| = |.z.| proof let z be complex number ; ::_thesis: |.(z *').| = |.z.| thus |.(z *').| = sqrt (((Re z) ^2) + ((Im (z *')) ^2)) by Th27 .= sqrt (((Re z) ^2) + ((- (Im z)) ^2)) by Th27 .= |.z.| ; ::_thesis: verum end; Lm25: for a being real number holds ( - |.a.| <= a & a <= |.a.| ) proof let a be real number ; ::_thesis: ( - |.a.| <= a & a <= |.a.| ) ( a < 0 implies ( - |.a.| <= a & a <= |.a.| ) ) proof assume a < 0 ; ::_thesis: ( - |.a.| <= a & a <= |.a.| ) then |.a.| = - a by Lm23; hence ( - |.a.| <= a & a <= |.a.| ) ; ::_thesis: verum end; hence ( - |.a.| <= a & a <= |.a.| ) by Th43; ::_thesis: verum end; theorem :: COMPLEX1:54 for z being complex number holds Re z <= |.z.| proof let z be complex number ; ::_thesis: Re z <= |.z.| 0 <= (Im z) ^2 by XREAL_1:63; then A1: ((Re z) ^2) + 0 <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:7; 0 <= (Re z) ^2 by XREAL_1:63; then sqrt ((Re z) ^2) <= |.z.| by A1, SQUARE_1:26; then A2: |.(Re z).| <= |.z.| by Lm24; Re z <= |.(Re z).| by Lm25; hence Re z <= |.z.| by A2, XXREAL_0:2; ::_thesis: verum end; theorem :: COMPLEX1:55 for z being complex number holds Im z <= |.z.| proof let z be complex number ; ::_thesis: Im z <= |.z.| 0 <= (Re z) ^2 by XREAL_1:63; then A1: ((Im z) ^2) + 0 <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:7; 0 <= (Im z) ^2 by XREAL_1:63; then sqrt ((Im z) ^2) <= |.z.| by A1, SQUARE_1:26; then A2: |.(Im z).| <= |.z.| by Lm24; Im z <= |.(Im z).| by Lm25; hence Im z <= |.z.| by A2, XXREAL_0:2; ::_thesis: verum end; theorem Th56: :: COMPLEX1:56 for z1, z2 being complex number holds |.(z1 + z2).| <= |.z1.| + |.z2.| proof let z1, z2 be complex number ; ::_thesis: |.(z1 + z2).| <= |.z1.| + |.z2.| set r1 = Re z1; set r2 = Re z2; set i1 = Im z1; set i2 = Im z2; A1: (Im (z1 + z2)) ^2 = ((Im z1) + (Im z2)) ^2 by Th8 .= (((Im z1) ^2) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2) ; A2: 0 <= ((Re z1) ^2) + ((Im z1) ^2) by Lm1; ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = (((Re z1) * (Im z2)) - ((Im z1) * (Re z2))) ^2 ; then 0 <= ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) by XREAL_1:63; then A3: ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) + 0 <= (((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2)) by XREAL_1:19; ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= |.(((Re z1) * (Re z2)) + ((Im z1) * (Im z2))).| by Lm25; then A4: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) by Lm24; A5: 0 <= ((Re z2) ^2) + ((Im z2) ^2) by Lm1; then A6: (sqrt (((Re z2) ^2) + ((Im z2) ^2))) ^2 = ((Re z2) ^2) + ((Im z2) ^2) by SQUARE_1:def_2; 0 <= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 by XREAL_1:63; then sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) <= sqrt ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) by A3, SQUARE_1:26; then sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A2, A5, SQUARE_1:29; then A7: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A4, XXREAL_0:2; ((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) = 2 * (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ; then ((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) <= 2 * ((sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) by A7, XREAL_1:64; then A8: (((Re z1) ^2) + ((Im z1) ^2)) + (((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2))) <= (((Re z1) ^2) + ((Im z1) ^2)) + ((2 * (sqrt (((Re z1) ^2) + ((Im z1) ^2)))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) by XREAL_1:7; (Re (z1 + z2)) ^2 = ((Re z1) + (Re z2)) ^2 by Th8 .= (((Re z1) ^2) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2) ; then ((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2) = ((((Re z1) ^2) + ((Im z1) ^2)) + (((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)))) + (((Re z2) ^2) + ((Im z2) ^2)) by A1; then A9: ((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2) <= ((((Re z1) ^2) + ((Im z1) ^2)) + ((2 * (sqrt (((Re z1) ^2) + ((Im z1) ^2)))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))))) + (((Re z2) ^2) + ((Im z2) ^2)) by A8, XREAL_1:7; A10: 0 <= ((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2) by Lm1; (sqrt (((Re z1) ^2) + ((Im z1) ^2))) ^2 = ((Re z1) ^2) + ((Im z1) ^2) by A2, SQUARE_1:def_2; then sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) <= sqrt (((sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) ^2) by A6, A9, A10, SQUARE_1:26; hence |.(z1 + z2).| <= |.z1.| + |.z2.| by SQUARE_1:22; ::_thesis: verum end; theorem Th57: :: COMPLEX1:57 for z1, z2 being complex number holds |.(z1 - z2).| <= |.z1.| + |.z2.| proof let z1, z2 be complex number ; ::_thesis: |.(z1 - z2).| <= |.z1.| + |.z2.| |.(z1 - z2).| = |.(z1 + (- z2)).| ; then |.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th56; hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Lm22; ::_thesis: verum end; theorem :: COMPLEX1:58 for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 + z2).| proof let z1, z2 be complex number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 + z2).| z1 = (z1 + z2) - z2 ; then |.z1.| <= |.(z1 + z2).| + |.z2.| by Th57; hence |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:20; ::_thesis: verum end; theorem Th59: :: COMPLEX1:59 for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 - z2).| proof let z1, z2 be complex number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z2).| z1 = (z1 - z2) + z2 ; then |.z1.| <= |.(z1 - z2).| + |.z2.| by Th56; hence |.z1.| - |.z2.| <= |.(z1 - z2).| by XREAL_1:20; ::_thesis: verum end; theorem Th60: :: COMPLEX1:60 for z1, z2 being complex number holds |.(z1 - z2).| = |.(z2 - z1).| proof let z1, z2 be complex number ; ::_thesis: |.(z1 - z2).| = |.(z2 - z1).| thus |.(z1 - z2).| = |.(- (z2 - z1)).| .= |.(z2 - z1).| by Lm22 ; ::_thesis: verum end; theorem Th61: :: COMPLEX1:61 for z1, z2 being complex number holds ( |.(z1 - z2).| = 0 iff z1 = z2 ) proof let z1, z2 be complex number ; ::_thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 ) thus ( |.(z1 - z2).| = 0 implies z1 = z2 ) ::_thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 ) proof assume |.(z1 - z2).| = 0 ; ::_thesis: z1 = z2 then z1 - z2 = 0 ; hence z1 = z2 ; ::_thesis: verum end; thus ( z1 = z2 implies |.(z1 - z2).| = 0 ) ; ::_thesis: verum end; theorem :: COMPLEX1:62 for z1, z2 being complex number holds ( z1 <> z2 iff 0 < |.(z1 - z2).| ) proof let z1, z2 be complex number ; ::_thesis: ( z1 <> z2 iff 0 < |.(z1 - z2).| ) thus ( z1 <> z2 implies 0 < |.(z1 - z2).| ) ::_thesis: ( 0 < |.(z1 - z2).| implies z1 <> z2 ) proof assume z1 <> z2 ; ::_thesis: 0 < |.(z1 - z2).| then |.(z1 - z2).| <> 0 by Th61; hence 0 < |.(z1 - z2).| ; ::_thesis: verum end; thus ( 0 < |.(z1 - z2).| implies z1 <> z2 ) ; ::_thesis: verum end; theorem :: COMPLEX1:63 for z1, z2, z being complex number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| proof let z1, z2, z be complex number ; ::_thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| |.(z1 - z2).| = |.((z1 - z) + (z - z2)).| ; hence |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by Th56; ::_thesis: verum end; Lm26: for b, a being real number holds ( ( - b <= a & a <= b ) iff |.a.| <= b ) proof let b, a be real number ; ::_thesis: ( ( - b <= a & a <= b ) iff |.a.| <= b ) A1: ( |.a.| <= b implies ( - b <= a & a <= b ) ) proof assume A2: |.a.| <= b ; ::_thesis: ( - b <= a & a <= b ) ( a < - 0 implies ( - b <= a & a <= b ) ) proof assume A3: a < - 0 ; ::_thesis: ( - b <= a & a <= b ) then - a <= b by A2, Lm23; then - b <= - (- a) by XREAL_1:24; hence ( - b <= a & a <= b ) by A3; ::_thesis: verum end; hence ( - b <= a & a <= b ) by A2, Th43; ::_thesis: verum end; ( - b <= a & a <= b implies |.a.| <= b ) proof assume that A4: - b <= a and A5: a <= b ; ::_thesis: |.a.| <= b - a <= - (- b) by A4, XREAL_1:24; then ( a < 0 implies |.a.| <= b ) by Lm23; hence |.a.| <= b by A5, Th43; ::_thesis: verum end; hence ( ( - b <= a & a <= b ) iff |.a.| <= b ) by A1; ::_thesis: verum end; theorem :: COMPLEX1:64 for z1, z2 being complex number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| proof let z1, z2 be complex number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| |.z2.| - |.z1.| <= |.(z2 - z1).| by Th59; then - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th60; then A1: - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:24; |.z1.| - |.z2.| <= |.(z1 - z2).| by Th59; hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by A1, Lm26; ::_thesis: verum end; theorem Th65: :: COMPLEX1:65 for z1, z2 being complex number holds |.(z1 * z2).| = |.z1.| * |.z2.| proof let z1, z2 be complex number ; ::_thesis: |.(z1 * z2).| = |.z1.| * |.z2.| set r1 = Re z1; set r2 = Re z2; set i1 = Im z1; set i2 = Im z2; A1: ( 0 <= ((Re z1) ^2) + ((Im z1) ^2) & 0 <= ((Re z2) ^2) + ((Im z2) ^2) ) by Lm1; A2: (Im (z1 * z2)) ^2 = (((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) ^2 by Th9 .= ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) ^2) + (((Re z2) * (Im z1)) ^2)) ; (Re (z1 * z2)) ^2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) ^2 by Th9 .= ((((Re z1) * (Re z2)) ^2) + (((Im z1) * (Im z2)) ^2)) + (- ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2)))) ; then ((Re (z1 * z2)) ^2) + ((Im (z1 * z2)) ^2) = (((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2)) by A2; hence |.(z1 * z2).| = |.z1.| * |.z2.| by A1, SQUARE_1:29; ::_thesis: verum end; theorem Th66: :: COMPLEX1:66 for z being complex number holds |.(z ").| = |.z.| " proof let z be complex number ; ::_thesis: |.(z ").| = |.z.| " percases ( z <> 0 or z = 0 ) ; supposeA1: z <> 0 ; ::_thesis: |.(z ").| = |.z.| " set r2i2 = ((Re z) ^2) + ((Im z) ^2); A2: ((Re z) ^2) + ((Im z) ^2) <> 0 by A1, Th5; A3: 0 <= ((Re z) ^2) + ((Im z) ^2) by Lm1; thus |.(z ").| = sqrt ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) ^2) + ((Im (z ")) ^2)) by Th20 .= sqrt ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) ^2) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) ^2)) by Th20 .= sqrt ((((Re z) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2)) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) ^2)) by XCMPLX_1:76 .= sqrt ((((Re z) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2)) + (((- (Im z)) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2))) by XCMPLX_1:76 .= sqrt ((1 * (((Re z) ^2) + ((Im z) ^2))) / ((((Re z) ^2) + ((Im z) ^2)) * (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:62 .= sqrt (1 / (((Re z) ^2) + ((Im z) ^2))) by A2, XCMPLX_1:91 .= 1 / |.z.| by A3, SQUARE_1:18, SQUARE_1:30 .= |.z.| " by XCMPLX_1:215 ; ::_thesis: verum end; supposeA4: z = 0 ; ::_thesis: |.(z ").| = |.z.| " hence |.(z ").| = 0 " .= |.z.| " by A4 ; ::_thesis: verum end; end; end; theorem Th67: :: COMPLEX1:67 for z1, z2 being complex number holds |.z1.| / |.z2.| = |.(z1 / z2).| proof let z1, z2 be complex number ; ::_thesis: |.z1.| / |.z2.| = |.(z1 / z2).| thus |.z1.| / |.z2.| = |.z1.| * (|.z2.| ") by XCMPLX_0:def_9 .= |.z1.| * |.(z2 ").| by Th66 .= |.(z1 * (z2 ")).| by Th65 .= |.(z1 / z2).| by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: COMPLEX1:68 for z being complex number holds |.(z * z).| = ((Re z) ^2) + ((Im z) ^2) proof let z be complex number ; ::_thesis: |.(z * z).| = ((Re z) ^2) + ((Im z) ^2) ( 0 <= ((Re z) ^2) + ((Im z) ^2) & |.(z * z).| = |.z.| * |.z.| ) by Lm1, Th65; then |.(z * z).| = sqrt ((((Re z) ^2) + ((Im z) ^2)) ^2) by SQUARE_1:29; hence |.(z * z).| = ((Re z) ^2) + ((Im z) ^2) by Lm1, SQUARE_1:22; ::_thesis: verum end; theorem :: COMPLEX1:69 for z being complex number holds |.(z * z).| = |.(z * (z *')).| proof let z be complex number ; ::_thesis: |.(z * z).| = |.(z * (z *')).| thus |.(z * z).| = |.z.| * |.z.| by Th65 .= |.z.| * |.(z *').| by Th53 .= |.(z * (z *')).| by Th65 ; ::_thesis: verum end; theorem :: COMPLEX1:70 for a being real number st a <= 0 holds |.a.| = - a by Lm23; theorem Th71: :: COMPLEX1:71 for a being real number holds ( |.a.| = a or |.a.| = - a ) proof let a be real number ; ::_thesis: ( |.a.| = a or |.a.| = - a ) ( a >= 0 or a < 0 ) ; hence ( |.a.| = a or |.a.| = - a ) by Lm23, Th43; ::_thesis: verum end; theorem :: COMPLEX1:72 for a being real number holds sqrt (a ^2) = |.a.| by Lm24; theorem :: COMPLEX1:73 for a, b being real number holds min (a,b) = ((a + b) - |.(a - b).|) / 2 proof let a, b be real number ; ::_thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2 percases ( a <= b or b <= a ) ; supposeA1: a <= b ; ::_thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2 |.(a - b).| = |.(- (b - a)).| .= |.(b - a).| by Lm22 .= b - a by A1, Th43, XREAL_1:48 ; hence min (a,b) = ((a + b) - |.(a - b).|) / 2 by A1, XXREAL_0:def_9; ::_thesis: verum end; supposeA2: b <= a ; ::_thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2 hence min (a,b) = ((a + b) - (a - b)) / 2 by XXREAL_0:def_9 .= ((a + b) - |.(a - b).|) / 2 by A2, Th43, XREAL_1:48 ; ::_thesis: verum end; end; end; theorem :: COMPLEX1:74 for a, b being real number holds max (a,b) = ((a + b) + |.(a - b).|) / 2 proof let a, b be real number ; ::_thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2 percases ( b <= a or a <= b ) ; supposeA1: b <= a ; ::_thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2 hence max (a,b) = ((a + b) + (a - b)) / 2 by XXREAL_0:def_10 .= ((a + b) + |.(a - b).|) / 2 by A1, Th43, XREAL_1:48 ; ::_thesis: verum end; supposeA2: a <= b ; ::_thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2 then A3: 0 <= b - a by XREAL_1:48; thus max (a,b) = ((a + b) + (- (a - b))) / 2 by A2, XXREAL_0:def_10 .= ((a + b) + |.(- (a - b)).|) / 2 by A3, Th43 .= ((a + b) + |.(a - b).|) / 2 by Lm22 ; ::_thesis: verum end; end; end; theorem Th75: :: COMPLEX1:75 for a being real number holds |.a.| ^2 = a ^2 proof let a be real number ; ::_thesis: |.a.| ^2 = a ^2 ( |.a.| = a or |.a.| = - a ) by Th71; hence |.a.| ^2 = a ^2 ; ::_thesis: verum end; theorem :: COMPLEX1:76 for a being real number holds ( - |.a.| <= a & a <= |.a.| ) by Lm25; notation let z be complex number ; synonym abs z for |.z.|; end; definition let z be complex number ; :: original: |. redefine func abs z -> Real; coherence |.z.| is Real ; end; theorem :: COMPLEX1:77 for a, b, c, d being real number st a + (b * ) = c + (d * ) holds ( a = c & b = d ) proof let a, b, c, d be real number ; ::_thesis: ( a + (b * ) = c + (d * ) implies ( a = c & b = d ) ) assume A1: a + (b * ) = c + (d * ) ; ::_thesis: ( a = c & b = d ) then (a - c) + ((b - d) * ) = 0 ; then a - c = 0 by Th4, Th12; hence ( a = c & b = d ) by A1; ::_thesis: verum end; theorem :: COMPLEX1:78 for a, b being real number holds sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b) proof let a, b be real number ; ::_thesis: sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b) A1: (sqrt ((a ^2) + (b ^2))) ^2 >= 0 by XREAL_1:63; ( a ^2 >= 0 & b ^2 >= 0 ) by XREAL_1:63; then A2: (sqrt ((a ^2) + (b ^2))) ^2 = (a ^2) + (b ^2) by SQUARE_1:def_2; ( ((abs a) + (abs b)) ^2 = (((abs a) ^2) + ((2 * (abs a)) * (abs b))) + ((abs b) ^2) & (abs a) ^2 = a ^2 ) by Th75; then (((abs a) + (abs b)) ^2) - ((sqrt ((a ^2) + (b ^2))) ^2) = (((a ^2) + ((2 * (abs a)) * (abs b))) + (b ^2)) - ((a ^2) + (b ^2)) by A2, Th75 .= (2 * (abs a)) * (abs b) ; then ((abs a) + (abs b)) ^2 >= (sqrt ((a ^2) + (b ^2))) ^2 by XREAL_1:49; then sqrt (((abs a) + (abs b)) ^2) >= sqrt ((sqrt ((a ^2) + (b ^2))) ^2) by A1, SQUARE_1:26; hence sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b) by A2, SQUARE_1:22; ::_thesis: verum end; theorem :: COMPLEX1:79 for a, b being real number holds abs a <= sqrt ((a ^2) + (b ^2)) proof let a, b be real number ; ::_thesis: abs a <= sqrt ((a ^2) + (b ^2)) ( a ^2 >= 0 & (a ^2) + 0 <= (a ^2) + (b ^2) ) by XREAL_1:6, XREAL_1:63; then sqrt (a ^2) <= sqrt ((a ^2) + (b ^2)) by SQUARE_1:26; hence abs a <= sqrt ((a ^2) + (b ^2)) by Lm24; ::_thesis: verum end; theorem :: COMPLEX1:80 for z1 being complex number holds |.(1 / z1).| = 1 / |.z1.| by Th48, Th67;