:: by Wenpai Chang, Yatsuka Nakamura and Piotr Rudnicki

::

:: Received May 29, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

theorem Th1: :: COMPLEX2:1

for a, b being Real st b > 0 holds

ex r being Real st

( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b )

ex r being Real st

( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b )

proof end;

theorem Th2: :: COMPLEX2:2

for a, b, c being Real st a > 0 & b >= 0 & c >= 0 & b < a & c < a holds

for i being Integer st b = c + (a * i) holds

b = c

for i being Integer st b = c + (a * i) holds

b = c

proof end;

theorem Th3: :: COMPLEX2:3

for a, b being Real holds

( sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b)) & cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b)) )

( sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b)) & cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b)) )

proof end;

theorem Th7: :: COMPLEX2:7

for a, b being Real st a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ holds

( a < b iff sin a > sin b )

( a < b iff sin a > sin b )

proof end;

theorem Th11: :: COMPLEX2:11

for a, b being Real st 0 <= a & a < 2 * PI & 0 <= b & b < 2 * PI & sin a = sin b & cos a = cos b holds

a = b

a = b

proof end;

Lm1: Arg 0 = 0

by COMPTRIG:35;

:: ALL these to be changed (mainly deleted) after the change in COMPTRIG

::$CT

theorem Th12: :: COMPLEX2:13

for z being Complex st z <> 0 holds

( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) )

( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) )

proof end;

::$CT

theorem Th23: :: COMPLEX2:25

for z being Element of COMPLEX st z <> 0 holds

( cos (Arg (- z)) = - (cos (Arg z)) & sin (Arg (- z)) = - (sin (Arg z)) )

( cos (Arg (- z)) = - (cos (Arg z)) & sin (Arg (- z)) = - (sin (Arg z)) )

proof end;

definition
end;

theorem Th27: :: COMPLEX2:29

for x, y being Complex holds x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>)

proof end;

theorem Th28: :: COMPLEX2:30

for z being Complex holds

( z .|. z = ((Re z) * (Re z)) + ((Im z) * (Im z)) & z .|. z = ((Re z) ^2) + ((Im z) ^2) )

( z .|. z = ((Re z) * (Re z)) + ((Im z) * (Im z)) & z .|. z = ((Re z) ^2) + ((Im z) ^2) )

proof end;

theorem :: COMPLEX2:40

theorem :: COMPLEX2:41

for a, b, x, y, z being Complex holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z))

proof end;

theorem :: COMPLEX2:48

for x, y being Complex holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)

proof end;

theorem Th47: :: COMPLEX2:49

for x, y being Complex holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y)

proof end;

Lm2: for z being Complex holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)

proof end;

theorem Th48: :: COMPLEX2:50

for x, y being Complex holds

( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) )

( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) )

proof end;

definition

let a be Complex;

let r be Real;

coherence

(|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

end;
let r be Real;

func Rotate (a,r) -> Element of COMPLEX equals :: COMPLEX2:def 2

(|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>);

correctness (|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>);

coherence

(|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

:: deftheorem defines Rotate COMPLEX2:def 2 :

for a being Complex

for r being Real holds Rotate (a,r) = (|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>);

for a being Complex

for r being Real holds Rotate (a,r) = (|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>);

theorem Th52: :: COMPLEX2:54

for r being Real

for a being Complex st a <> 0 holds

ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))

for a being Complex st a <> 0 holds

ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a))

proof end;

theorem Th54: :: COMPLEX2:56

for a being Complex

for r being Real holds

( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) )

for r being Real holds

( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) )

proof end;

definition

let a, b be Complex;

coherence

( ( ( Arg a = 0 or b <> 0 ) implies Arg (Rotate (b,(- (Arg a)))) is Real ) & ( Arg a = 0 or b <> 0 or (2 * PI) - (Arg a) is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
func angle (a,b) -> Real equals :Def3: :: COMPLEX2:def 3

Arg (Rotate (b,(- (Arg a)))) if ( Arg a = 0 or b <> 0 )

otherwise (2 * PI) - (Arg a);

correctness Arg (Rotate (b,(- (Arg a)))) if ( Arg a = 0 or b <> 0 )

otherwise (2 * PI) - (Arg a);

coherence

( ( ( Arg a = 0 or b <> 0 ) implies Arg (Rotate (b,(- (Arg a)))) is Real ) & ( Arg a = 0 or b <> 0 or (2 * PI) - (Arg a) is Real ) );

consistency

for b

;

:: deftheorem Def3 defines angle COMPLEX2:def 3 :

for a, b being Complex holds

( ( ( Arg a = 0 or b <> 0 ) implies angle (a,b) = Arg (Rotate (b,(- (Arg a)))) ) & ( Arg a = 0 or b <> 0 or angle (a,b) = (2 * PI) - (Arg a) ) );

for a, b being Complex holds

( ( ( Arg a = 0 or b <> 0 ) implies angle (a,b) = Arg (Rotate (b,(- (Arg a)))) ) & ( Arg a = 0 or b <> 0 or angle (a,b) = (2 * PI) - (Arg a) ) );

theorem Th60: :: COMPLEX2:62

for r being Real

for a, b being Complex st Arg a = Arg b & a <> 0 & b <> 0 holds

Arg (Rotate (a,r)) = Arg (Rotate (b,r))

for a, b being Complex st Arg a = Arg b & a <> 0 & b <> 0 holds

Arg (Rotate (a,r)) = Arg (Rotate (b,r))

proof end;

theorem Th63: :: COMPLEX2:65

for a, b being Complex

for r being Real st a <> 0 & b <> 0 holds

angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r)))

for r being Real st a <> 0 & b <> 0 holds

angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r)))

proof end;

theorem :: COMPLEX2:66

for a, b being Complex

for r being Real st r < 0 & a <> 0 & b <> 0 holds

angle (a,b) = angle ((a * r),(b * r))

for r being Real st r < 0 & a <> 0 & b <> 0 holds

angle (a,b) = angle ((a * r),(b * r))

proof end;

theorem Th67: :: COMPLEX2:69

for a, b being Complex st a <> 0 & b <> 0 holds

( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) )

( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) )

proof end;

definition

let x, y, z be Complex;

coherence

( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies (Arg (z - y)) - (Arg (x - y)) is Real ) & ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) is Real ) );

consistency

for b_{1} being Real holds verum;

;

end;
func angle (x,y,z) -> Real equals :Def4: :: COMPLEX2:def 4

(Arg (z - y)) - (Arg (x - y)) if (Arg (z - y)) - (Arg (x - y)) >= 0

otherwise (2 * PI) + ((Arg (z - y)) - (Arg (x - y)));

correctness (Arg (z - y)) - (Arg (x - y)) if (Arg (z - y)) - (Arg (x - y)) >= 0

otherwise (2 * PI) + ((Arg (z - y)) - (Arg (x - y)));

coherence

( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies (Arg (z - y)) - (Arg (x - y)) is Real ) & ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) is Real ) );

consistency

for b

;

:: deftheorem Def4 defines angle COMPLEX2:def 4 :

for x, y, z being Complex holds

( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies angle (x,y,z) = (Arg (z - y)) - (Arg (x - y)) ) & ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) ) );

for x, y, z being Complex holds

( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies angle (x,y,z) = (Arg (z - y)) - (Arg (x - y)) ) & ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) ) );

theorem Th72: :: COMPLEX2:74

for x, y, z being Complex st angle (x,y,z) = 0 holds

( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 )

( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 )

proof end;

theorem Th73: :: COMPLEX2:75

for a, b being Complex st a <> 0 & b <> 0 holds

( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) )

( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) )

proof end;

theorem :: COMPLEX2:76

for a, b being Complex st a <> 0 & b <> 0 holds

( ( ( not Im (a .|. b) = |.a.| * |.b.| & not Im (a .|. b) = - (|.a.| * |.b.|) ) or angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) & ( ( not angle (a,0,b) = PI / 2 & not angle (a,0,b) = (3 / 2) * PI ) or Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) )

( ( ( not Im (a .|. b) = |.a.| * |.b.| & not Im (a .|. b) = - (|.a.| * |.b.|) ) or angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) & ( ( not angle (a,0,b) = PI / 2 & not angle (a,0,b) = (3 / 2) * PI ) or Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) )

proof end;

Lm3: for a, b, c being Complex st a <> b & c <> b holds

( Re ((a - b) .|. (c - b)) = 0 iff ( angle (a,b,c) = PI / 2 or angle (a,b,c) = (3 / 2) * PI ) )

proof end;

theorem :: COMPLEX2:77

for x, y, z being Complex st x <> y & z <> y & ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) holds

(|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2

(|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2

proof end;

theorem Th76: :: COMPLEX2:78

for a, b, c being Complex

for r being Real st a <> b & b <> c holds

angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

for r being Real st a <> b & b <> c holds

angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r)))

proof end;

Lm4: for x, y, z being Complex st angle (x,y,z) <> 0 holds

angle (z,y,x) = (2 * PI) - (angle (x,y,z))

proof end;

theorem Th78: :: COMPLEX2:80

for a, b, c being Complex holds

( angle (a,b,c) <> 0 iff (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI )

( angle (a,b,c) <> 0 iff (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI )

proof end;

theorem Th81: :: COMPLEX2:83

for a, b, c being Complex st a <> b & a <> c & b <> c & not angle (a,b,c) <> 0 & not angle (b,c,a) <> 0 holds

angle (c,a,b) <> 0

angle (c,a,b) <> 0

proof end;

Lm5: for a, b being Complex st Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI holds

( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI & 0 < angle (0c,b,a) & 0 < angle (b,a,0c) )

proof end;

theorem Th82: :: COMPLEX2:84

for a, b, c being Complex st a <> b & b <> c & 0 < angle (a,b,c) & angle (a,b,c) < PI holds

( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI & 0 < angle (b,c,a) & 0 < angle (c,a,b) )

( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI & 0 < angle (b,c,a) & 0 < angle (c,a,b) )

proof end;

theorem Th83: :: COMPLEX2:85

for a, b, c being Complex st a <> b & b <> c & angle (a,b,c) > PI holds

( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI )

( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI )

proof end;

Lm6: for a, b being Complex st Im a = 0 & Re a > 0 & Arg b = PI holds

( ((angle (a,0,b)) + (angle (0,b,a))) + (angle (b,a,0)) = PI & 0 = angle (0,b,a) & 0 = angle (b,a,0) )

proof end;

theorem Th84: :: COMPLEX2:86

for a, b, c being Complex st a <> b & b <> c & angle (a,b,c) = PI holds

( angle (b,c,a) = 0 & angle (c,a,b) = 0 )

( angle (b,c,a) = 0 & angle (c,a,b) = 0 )

proof end;

theorem Th85: :: COMPLEX2:87

for a, b, c being Complex st a <> b & a <> c & b <> c & angle (a,b,c) = 0 & not ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) holds

( angle (b,c,a) = PI & angle (c,a,b) = 0 )

( angle (b,c,a) = PI & angle (c,a,b) = 0 )

proof end;

theorem :: COMPLEX2:88

for a, b, c being Complex holds

( ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) iff ( a <> b & a <> c & b <> c ) )

( ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI or ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) iff ( a <> b & a <> c & b <> c ) )

proof end;