:: by Czes{\l}aw Byli\'nski

::

:: Received March 1, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

:: Auxiliary theorems

Lm1: for a, b being real number holds 0 <= (a ^2) + (b ^2)

proof end;

:: Complex Numbers

definition

let z be complex number ;

( ( z in REAL implies ex b_{1} being set st b_{1} = z ) & ( not z in REAL implies ex b_{1} being set ex f being Function of 2,REAL st

( z = f & b_{1} = f . 0 ) ) )

for b_{1}, b_{2} being set holds

( ( z in REAL & b_{1} = z & b_{2} = z implies b_{1} = b_{2} ) & ( not z in REAL & ex f being Function of 2,REAL st

( z = f & b_{1} = f . 0 ) & ex f being Function of 2,REAL st

( z = f & b_{2} = f . 0 ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being set holds verum
;

( ( z in REAL implies ex b_{1} being set st b_{1} = 0 ) & ( not z in REAL implies ex b_{1} being set ex f being Function of 2,REAL st

( z = f & b_{1} = f . 1 ) ) )

for b_{1}, b_{2} being set holds

( ( z in REAL & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not z in REAL & ex f being Function of 2,REAL st

( z = f & b_{1} = f . 1 ) & ex f being Function of 2,REAL st

( z = f & b_{2} = f . 1 ) implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being set holds verum
;

end;
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 it = z if z in REAL

otherwise ex f being Function of 2,REAL st

( z = f & it = f . 0 );

( ( z in REAL implies ex b

( z = f & b

proof end;

uniqueness for b

( ( z in REAL & b

( z = f & b

( z = f & b

consistency

for b

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 it = 0 if z in REAL

otherwise ex f being Function of 2,REAL st

( z = f & it = f . 1 );

( ( z in REAL implies ex b

( z = f & b

proof end;

uniqueness for b

( ( z in REAL & b

( z = f & b

( z = f & b

consistency

for b

:: deftheorem Def1 defines Re COMPLEX1:def 1 :

for z being complex number

for b_{2} being set holds

( ( z in REAL implies ( b_{2} = Re z iff b_{2} = z ) ) & ( not z in REAL implies ( b_{2} = Re z iff ex f being Function of 2,REAL st

( z = f & b_{2} = f . 0 ) ) ) );

for z being complex number

for b

( ( z in REAL implies ( b

( z = f & b

:: deftheorem Def2 defines Im COMPLEX1:def 2 :

for z being complex number

for b_{2} being set holds

( ( z in REAL implies ( b_{2} = Im z iff b_{2} = 0 ) ) & ( not z in REAL implies ( b_{2} = Im z iff ex f being Function of 2,REAL st

( z = f & b_{2} = f . 1 ) ) ) );

for z being complex number

for b

( ( z in REAL implies ( b

( z = f & b

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

Lm2: for a, b being Element of REAL holds

( Re [*a,b*] = a & Im [*a,b*] = b )

proof end;

Lm3: for z being complex number holds [*(Re z),(Im z)*] = z

proof end;

definition

let z1, z2 be complex number ;

compatibility

( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) ) by Th3;

end;
compatibility

( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) ) by Th3;

:: deftheorem defines = COMPLEX1:def 3 :

for z1, z2 being complex number holds

( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) );

for z1, z2 being complex number holds

( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) );

definition

:: original: 0c

redefine func 0c -> Element of COMPLEX ;

correctness

coherence

0c is Element of COMPLEX ;

by XCMPLX_0:def 2;

end;
redefine func 0c -> Element of COMPLEX ;

correctness

coherence

0c is Element of COMPLEX ;

by XCMPLX_0:def 2;

definition

correctness

coherence

1 is Element of COMPLEX ;

by XCMPLX_0:def 2;

:: original: <i>

redefine func <i> -> Element of COMPLEX ;

coherence

<i> is Element of COMPLEX by XCMPLX_0:def 2;

end;
coherence

1 is Element of COMPLEX ;

by XCMPLX_0:def 2;

:: original: <i>

redefine func <i> -> Element of COMPLEX ;

coherence

<i> is Element of COMPLEX by XCMPLX_0:def 2;

Lm4: 0 = [*0,0*]

by ARYTM_0:def 5;

Lm5: 1r = [*1,0*]

by ARYTM_0:def 5;

Lm6: <i> = [*0,1*]

by ARYTM_0:def 5, XCMPLX_0:def 1;

Lm7: for x being real number

for x1, x2 being Element of REAL st x = [*x1,x2*] holds

( x2 = 0 & x = x1 )

proof 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 end;

Lm9: for x being Element of REAL holds opp x = - x

proof 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 end;

Lm11: for x, y, z being complex number st z = x + y holds

Re z = (Re x) + (Re y)

proof end;

Lm12: for x, y, z being complex number st z = x + y holds

Im z = (Im x) + (Im y)

proof 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 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 end;

Lm15: for z1, z2 being complex number holds z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]

proof 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 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 end;

Lm18: for z1, z2 being complex number holds

( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )

proof end;

Lm19: for x being Real holds Re (x * <i>) = 0

proof end;

Lm20: for x being Real holds Im (x * <i>) = x

proof end;

Lm21: for x, y being Real holds [*x,y*] = x + (y * <i>)

proof end;

definition

let z1, z2 be Element of COMPLEX ;

z1 + z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = z1 + z2 iff b_{1} = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>) )

end;
:: original: +

redefine func z1 + z2 -> Element of COMPLEX equals :: COMPLEX1:def 5

((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);

coherence redefine func z1 + z2 -> Element of COMPLEX equals :: COMPLEX1:def 5

((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);

z1 + z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof end;

:: deftheorem defines + COMPLEX1:def 5 :

for z1, z2 being Element of COMPLEX holds z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);

for z1, z2 being Element of COMPLEX holds z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);

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) )

( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )

proof end;

definition

let z1, z2 be Element of COMPLEX ;

z1 * z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = z1 * z2 iff b_{1} = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>) )

end;
:: original: *

redefine func z1 * z2 -> Element of COMPLEX equals :: COMPLEX1:def 6

(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>);

coherence redefine func z1 * z2 -> Element of COMPLEX equals :: COMPLEX1:def 6

(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>);

z1 * z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof 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))) * <i>);

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))) * <i>);

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)) )

( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )

proof 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 )

( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 )

proof 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 )

( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 )

proof 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)) )

( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) )

proof end;

definition

let z be Element of COMPLEX ;

- z is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = - z iff b_{1} = (- (Re z)) + ((- (Im z)) * <i>) )

end;
:: original: -

redefine func - z -> Element of COMPLEX equals :Def7: :: COMPLEX1:def 7

(- (Re z)) + ((- (Im z)) * <i>);

coherence redefine func - z -> Element of COMPLEX equals :Def7: :: COMPLEX1:def 7

(- (Re z)) + ((- (Im z)) * <i>);

- z is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof end;

:: deftheorem Def7 defines - COMPLEX1:def 7 :

for z being Element of COMPLEX holds - z = (- (Re z)) + ((- (Im z)) * <i>);

for z being Element of COMPLEX holds - z = (- (Re z)) + ((- (Im z)) * <i>);

definition

let z1, z2 be Element of COMPLEX ;

z1 - z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = z1 - z2 iff b_{1} = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) )

end;
:: original: -

redefine func z1 - z2 -> Element of COMPLEX equals :Def8: :: COMPLEX1:def 8

((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>);

coherence redefine func z1 - z2 -> Element of COMPLEX equals :Def8: :: COMPLEX1:def 8

((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>);

z1 - z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof 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)) * <i>);

for z1, z2 being Element of COMPLEX holds z1 - z2 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>);

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) )

( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) )

proof end;

definition

let z be Element of COMPLEX ;

z " is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = z " iff b_{1} = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) )

end;
:: original: "

redefine func z " -> Element of COMPLEX equals :Def9: :: COMPLEX1:def 9

((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>);

coherence redefine func z " -> Element of COMPLEX equals :Def9: :: COMPLEX1:def 9

((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>);

z " is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof 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))) * <i>);

for z being Element of COMPLEX holds z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>);

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)) )

( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) )

proof end;

definition

let z1, z2 be complex number ;

z1 / z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b_{1} being Element of COMPLEX holds

( b_{1} = z1 / z2 iff b_{1} = ((((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))) * <i>) )

end;
:: original: /

redefine func z1 / 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))) * <i>);

coherence redefine func z1 / 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))) * <i>);

z1 / z2 is Element of COMPLEX by XCMPLX_0:def 2;

compatibility

for b

( b

proof 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))) * <i>);

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))) * <i>);

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)) )

( 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 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 )

( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 )

proof 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 )

( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 )

proof end;

definition

let z be complex number ;

correctness

coherence

(Re z) - ((Im z) * <i>) is complex number ;

;

involutiveness

for b_{1}, b_{2} being complex number st b_{1} = (Re b_{2}) - ((Im b_{2}) * <i>) holds

b_{2} = (Re b_{1}) - ((Im b_{1}) * <i>)

end;
correctness

coherence

(Re z) - ((Im z) * <i>) is complex number ;

;

involutiveness

for b

b

proof end;

:: deftheorem defines *' COMPLEX1:def 11 :

for z being complex number holds z *' = (Re z) - ((Im z) * <i>);

for z being complex number holds z *' = (Re z) - ((Im z) * <i>);

definition

let z be complex number ;

:: original: *'

redefine func z *' -> Element of COMPLEX ;

coherence

z *' is Element of COMPLEX by XCMPLX_0:def 2;

end;
:: original: *'

redefine func z *' -> Element of COMPLEX ;

coherence

z *' is Element of COMPLEX by XCMPLX_0:def 2;

theorem :: COMPLEX1:40

for z being complex number holds

( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )

( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )

proof end;

definition

let z be complex number ;

coherence

sqrt (((Re z) ^2) + ((Im z) ^2)) is real number ;

projectivity

for b_{1} being real number

for b_{2} being complex number st b_{1} = sqrt (((Re b_{2}) ^2) + ((Im b_{2}) ^2)) holds

b_{1} = sqrt (((Re b_{1}) ^2) + ((Im b_{1}) ^2))

end;
coherence

sqrt (((Re z) ^2) + ((Im z) ^2)) is real number ;

projectivity

for b

for b

b

proof end;

:: deftheorem defines |. COMPLEX1:def 12 :

for z being complex number holds |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2));

for z being complex number holds |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2));

definition
end;

Lm22: for z being complex number holds |.(- z).| = |.z.|

proof end;

Lm23: for a being real number st a <= 0 holds

|.a.| = - a

proof end;

Lm24: for a being real number holds sqrt (a ^2) = |.a.|

proof end;

Lm25: for a being real number holds

( - |.a.| <= a & a <= |.a.| )

proof end;

Lm26: for b, a being real number holds

( ( - b <= a & a <= b ) iff |.a.| <= b )

proof end;

:: Originally from SQUARE_1

definition
end;

:: from JGRAPH_1, 29.12.2006, AK