:: COMPLEX2 semantic presentation begin theorem Th1: :: COMPLEX2:1 for a, b being real number st b > 0 holds ex r being real number st ( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b ) proof let a, b be real number ; ::_thesis: ( b > 0 implies ex r being real number st ( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b ) ) assume A1: b > 0 ; ::_thesis: ex r being real number st ( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b ) set ab = [\(a / b)/]; set i = - [\(a / b)/]; take r = (b * (- [\(a / b)/])) + a; ::_thesis: ( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b ) thus r = (b * (- [\(a / b)/])) + a ; ::_thesis: ( 0 <= r & r < b ) [\(a / b)/] <= a / b by INT_1:def_6; then [\(a / b)/] * b <= (a / b) * b by A1, XREAL_1:64; then [\(a / b)/] * b <= a by A1, XCMPLX_1:87; then - ([\(a / b)/] * b) >= - a by XREAL_1:24; then (b * (- [\(a / b)/])) + a >= a + (- a) by XREAL_1:6; hence 0 <= r ; ::_thesis: r < b (a / b) - 1 < [\(a / b)/] by INT_1:def_6; then - ((a / b) - 1) > - [\(a / b)/] by XREAL_1:24; then ((- (a / b)) + 1) * b > (- [\(a / b)/]) * b by A1, XREAL_1:68; then (- ((a / b) * b)) + b > (- [\(a / b)/]) * b ; then (- a) + b > (- [\(a / b)/]) * b by A1, XCMPLX_1:87; then ((- a) + b) + a > r by XREAL_1:8; hence r < b ; ::_thesis: verum end; theorem Th2: :: COMPLEX2:2 for a, b, c being real number st a > 0 & b >= 0 & c >= 0 & b < a & c < a holds for i being Integer st b = c + (a * i) holds b = c proof let a, b, c be real number ; ::_thesis: ( a > 0 & b >= 0 & c >= 0 & b < a & c < a implies for i being Integer st b = c + (a * i) holds b = c ) assume that A1: a > 0 and A2: b >= 0 and A3: c >= 0 and A4: b < a and A5: c < a ; ::_thesis: for i being Integer st b = c + (a * i) holds b = c A6: 0 + a <= c + a by A3, XREAL_1:7; let i be Integer; ::_thesis: ( b = c + (a * i) implies b = c ) assume A7: b = c + (a * i) ; ::_thesis: b = c percases ( i < 0 or i = 0 or i > 0 ) ; suppose i < 0 ; ::_thesis: b = c then i <= - 1 by INT_1:8; then a * i <= a * (- 1) by A1, XREAL_1:64; then c + (a * i) <= c - a by XREAL_1:7; hence b = c by A2, A5, A7, XREAL_1:49; ::_thesis: verum end; suppose i = 0 ; ::_thesis: b = c hence b = c by A7; ::_thesis: verum end; suppose i > 0 ; ::_thesis: b = c then 0 + 1 <= i by INT_1:7; then a * i >= a by A1, XREAL_1:151; then c + (a * i) >= c + a by XREAL_1:7; hence b = c by A4, A7, A6, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th3: :: COMPLEX2:3 for a, b being real number holds ( sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b)) & cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b)) ) proof let th1, th2 be real number ; ::_thesis: ( sin (th1 - th2) = ((sin th1) * (cos th2)) - ((cos th1) * (sin th2)) & cos (th1 - th2) = ((cos th1) * (cos th2)) + ((sin th1) * (sin th2)) ) thus sin (th1 - th2) = sin . (th1 + (- th2)) by SIN_COS:def_17 .= ((sin . th1) * (cos . (- th2))) + ((cos . th1) * (sin . (- th2))) by SIN_COS:74 .= ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . (- th2))) by SIN_COS:30 .= ((sin . th1) * (cos . th2)) + ((cos . th1) * (- (sin . th2))) by SIN_COS:30 .= ((sin th1) * (cos . th2)) - ((cos . th1) * (sin . th2)) by SIN_COS:def_17 .= ((sin th1) * (cos th2)) - ((cos . th1) * (sin . th2)) by SIN_COS:def_19 .= ((sin th1) * (cos th2)) - ((cos th1) * (sin . th2)) by SIN_COS:def_19 .= ((sin th1) * (cos th2)) - ((cos th1) * (sin th2)) by SIN_COS:def_17 ; ::_thesis: cos (th1 - th2) = ((cos th1) * (cos th2)) + ((sin th1) * (sin th2)) thus cos (th1 - th2) = cos . (th1 + (- th2)) by SIN_COS:def_19 .= ((cos . th1) * (cos . (- th2))) - ((sin . th1) * (sin . (- th2))) by SIN_COS:74 .= ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . (- th2))) by SIN_COS:30 .= ((cos . th1) * (cos . th2)) - ((sin . th1) * (- (sin . th2))) by SIN_COS:30 .= ((cos th1) * (cos . th2)) + ((sin . th1) * (sin . th2)) by SIN_COS:def_19 .= ((cos th1) * (cos th2)) + ((sin . th1) * (sin . th2)) by SIN_COS:def_19 .= ((cos th1) * (cos th2)) + ((sin th1) * (sin . th2)) by SIN_COS:def_17 .= ((cos th1) * (cos th2)) + ((sin th1) * (sin th2)) by SIN_COS:def_17 ; ::_thesis: verum end; theorem :: COMPLEX2:4 for a being real number holds ( sin . (a - PI) = - (sin . a) & cos . (a - PI) = - (cos . a) ) proof let th be real number ; ::_thesis: ( sin . (th - PI) = - (sin . th) & cos . (th - PI) = - (cos . th) ) thus sin . (th - PI) = ((sin . th) * (cos . (- PI))) + ((cos . th) * (sin . (- PI))) by SIN_COS:74 .= ((sin . th) * (cos . PI)) + ((cos . th) * (sin . (- PI))) by SIN_COS:30 .= ((sin . th) * (cos . PI)) + ((cos . th) * (- (sin . PI))) by SIN_COS:30 .= - (sin . th) by SIN_COS:76 ; ::_thesis: cos . (th - PI) = - (cos . th) thus cos . (th - PI) = ((cos . th) * (cos . (- PI))) - ((sin . th) * (sin . (- PI))) by SIN_COS:74 .= ((cos . th) * (cos . PI)) - ((sin . th) * (sin . (- PI))) by SIN_COS:30 .= ((cos . th) * (cos . PI)) - ((sin . th) * (- (sin . PI))) by SIN_COS:30 .= - (cos . th) by SIN_COS:76 ; ::_thesis: verum end; theorem Th5: :: COMPLEX2:5 for a being real number holds ( sin (a - PI) = - (sin a) & cos (a - PI) = - (cos a) ) proof let r be real number ; ::_thesis: ( sin (r - PI) = - (sin r) & cos (r - PI) = - (cos r) ) thus sin (r - PI) = ((sin r) * (cos PI)) - ((cos r) * (sin PI)) by Th3 .= - (sin r) by SIN_COS:77 ; ::_thesis: cos (r - PI) = - (cos r) thus cos (r - PI) = ((cos r) * (cos PI)) + ((sin r) * (sin PI)) by Th3 .= - (cos r) by SIN_COS:77 ; ::_thesis: verum end; theorem Th6: :: COMPLEX2:6 for a, b being real number st a in ].0,(PI / 2).[ & b in ].0,(PI / 2).[ holds ( a < b iff sin a < sin b ) proof let a, b be real number ; ::_thesis: ( a in ].0,(PI / 2).[ & b in ].0,(PI / 2).[ implies ( a < b iff sin a < sin b ) ) assume ( a in ].0,(PI / 2).[ & b in ].0,(PI / 2).[ ) ; ::_thesis: ( a < b iff sin a < sin b ) then A1: ( a in ].0,(PI / 2).[ /\ (dom sin) & b in ].0,(PI / 2).[ /\ (dom sin) ) by SIN_COS:24, XBOOLE_0:def_4; A2: ( sin a = sin . a & sin b = sin . b ) by SIN_COS:def_17; hence ( a < b implies sin a < sin b ) by A1, RFUNCT_2:20, SIN_COS2:2; ::_thesis: ( sin a < sin b implies a < b ) assume A3: sin a < sin b ; ::_thesis: a < b assume a >= b ; ::_thesis: contradiction then a > b by A3, XXREAL_0:1; hence contradiction by A2, A1, A3, RFUNCT_2:20, SIN_COS2:2; ::_thesis: verum end; theorem Th7: :: COMPLEX2:7 for a, b being real number st a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ holds ( a < b iff sin a > sin b ) proof let a, b be real number ; ::_thesis: ( a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ implies ( a < b iff sin a > sin b ) ) assume ( a in ].(PI / 2),PI.[ & b in ].(PI / 2),PI.[ ) ; ::_thesis: ( a < b iff sin a > sin b ) then A1: ( a in ].(PI / 2),PI.[ /\ (dom sin) & b in ].(PI / 2),PI.[ /\ (dom sin) ) by SIN_COS:24, XBOOLE_0:def_4; A2: ( sin a = sin . a & sin b = sin . b ) by SIN_COS:def_17; hence ( a < b implies sin a > sin b ) by A1, RFUNCT_2:21, SIN_COS2:3; ::_thesis: ( sin a > sin b implies a < b ) assume A3: sin a > sin b ; ::_thesis: a < b assume a >= b ; ::_thesis: contradiction then a > b by A3, XXREAL_0:1; hence contradiction by A2, A1, A3, RFUNCT_2:21, SIN_COS2:3; ::_thesis: verum end; theorem Th8: :: COMPLEX2:8 for a being real number for i being Integer holds sin a = sin (((2 * PI) * i) + a) proof let r be real number ; ::_thesis: for i being Integer holds sin r = sin (((2 * PI) * i) + r) let i be Integer; ::_thesis: sin r = sin (((2 * PI) * i) + r) A1: sin . r = sin r by SIN_COS:def_17; A2: sin . (((2 * PI) * i) + r) = sin (((2 * PI) * i) + r) by SIN_COS:def_17; A3: sin . (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) = sin (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) by SIN_COS:def_17; percases ( i >= 0 or i < 0 ) ; suppose i >= 0 ; ::_thesis: sin r = sin (((2 * PI) * i) + r) then reconsider iN = i as Element of NAT by INT_1:3; sin r = sin (((2 * PI) * iN) + r) by A1, A2, SIN_COS2:10; hence sin r = sin (((2 * PI) * i) + r) ; ::_thesis: verum end; suppose i < 0 ; ::_thesis: sin r = sin (((2 * PI) * i) + r) then reconsider iN = - i as Element of NAT by INT_1:3; reconsider aa = ((2 * PI) * i) + r as Real ; sin aa = sin (((2 * PI) * iN) + aa) by A2, A3, SIN_COS2:10; hence sin r = sin (((2 * PI) * i) + r) ; ::_thesis: verum end; end; end; theorem Th9: :: COMPLEX2:9 for a being real number for i being Integer holds cos a = cos (((2 * PI) * i) + a) proof let r be real number ; ::_thesis: for i being Integer holds cos r = cos (((2 * PI) * i) + r) let i be Integer; ::_thesis: cos r = cos (((2 * PI) * i) + r) A1: cos . r = cos r by SIN_COS:def_19; A2: cos . (((2 * PI) * i) + r) = cos (((2 * PI) * i) + r) by SIN_COS:def_19; A3: cos . (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) = cos (((2 * PI) * (- i)) + (((2 * PI) * i) + r)) by SIN_COS:def_19; percases ( i >= 0 or i < 0 ) ; suppose i >= 0 ; ::_thesis: cos r = cos (((2 * PI) * i) + r) then reconsider iN = i as Element of NAT by INT_1:3; cos r = cos (((2 * PI) * iN) + r) by A1, A2, SIN_COS2:11; hence cos r = cos (((2 * PI) * i) + r) ; ::_thesis: verum end; suppose i < 0 ; ::_thesis: cos r = cos (((2 * PI) * i) + r) then reconsider iN = - i as Element of NAT by INT_1:3; reconsider aa = ((2 * PI) * i) + r as Real ; cos aa = cos (((2 * PI) * iN) + aa) by A2, A3, SIN_COS2:11; hence cos r = cos (((2 * PI) * i) + r) ; ::_thesis: verum end; end; end; theorem Th10: :: COMPLEX2:10 for a being real number st sin a = 0 holds cos a <> 0 proof let a be real number ; ::_thesis: ( sin a = 0 implies cos a <> 0 ) assume that A1: sin a = 0 and A2: cos a = 0 ; ::_thesis: contradiction consider r being real number such that A3: r = ((2 * PI) * (- [\(a / (2 * PI))/])) + a and A4: ( 0 <= r & r < 2 * PI ) by Th1, COMPTRIG:5; A5: cos a = cos r by A3, Th9; sin a = sin r by A3, Th8; then ( r = 0 or r = PI ) by A4, A1, COMPTRIG:17; hence contradiction by A5, A2, COMPTRIG:5, COMPTRIG:18; ::_thesis: verum end; theorem Th11: :: COMPLEX2:11 for a, b being real number st 0 <= a & a < 2 * PI & 0 <= b & b < 2 * PI & sin a = sin b & cos a = cos b holds a = b proof let r, s be real number ; ::_thesis: ( 0 <= r & r < 2 * PI & 0 <= s & s < 2 * PI & sin r = sin s & cos r = cos s implies r = s ) assume that A1: 0 <= r and A2: ( r < 2 * PI & 0 <= s ) and A3: s < 2 * PI and A4: ( sin r = sin s & cos r = cos s ) ; ::_thesis: r = s A5: cos (r - s) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by Th3 .= 1 by A4, SIN_COS:29 ; A6: sin (r - s) = ((sin r) * (cos s)) - ((cos r) * (sin s)) by Th3 .= 0 by A4 ; A7: cos (s - r) = ((cos r) * (cos s)) + ((sin r) * (sin s)) by Th3 .= 1 by A4, SIN_COS:29 ; A8: sin (s - r) = ((sin s) * (cos r)) - ((cos s) * (sin r)) by Th3 .= 0 by A4 ; percases ( r > s or r < s or r = s ) by XXREAL_0:1; supposeA9: r > s ; ::_thesis: r = s r + 0 < (2 * PI) + s by A2, XREAL_1:8; then A10: r - s < 2 * PI by XREAL_1:19; r > s + 0 by A9; then 0 <= r - s by XREAL_1:20; then ( r - s = 0 or r - s = PI ) by A6, A10, COMPTRIG:17; hence r = s by A5, SIN_COS:77; ::_thesis: verum end; suppose r < s ; ::_thesis: r = s then s > r + 0 ; then A11: 0 <= s - r by XREAL_1:20; s + 0 < (2 * PI) + r by A1, A3, XREAL_1:8; then s - r < 2 * PI by XREAL_1:19; then ( s - r = 0 or s - r = PI ) by A8, A11, COMPTRIG:17; hence r = s by A7, SIN_COS:77; ::_thesis: verum end; suppose r = s ; ::_thesis: r = s hence r = s ; ::_thesis: verum end; end; end; begin theorem Th12: :: COMPLEX2:12 for z being complex number holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) proof let a be complex number ; ::_thesis: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) percases ( a <> 0 or a = 0c ) ; suppose a <> 0 ; ::_thesis: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) hence a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) by COMPTRIG:def_1; ::_thesis: verum end; suppose a = 0c ; ::_thesis: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) hence a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) by COMPLEX1:44; ::_thesis: verum end; end; end; Lm1: Arg 0 = 0 by COMPTRIG:35; theorem Th13: :: COMPLEX2:13 for z being complex number st z <> 0 holds ( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) ) proof let z be complex number ; ::_thesis: ( z <> 0 implies ( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) ) ) assume A1: z <> 0 ; ::_thesis: ( ( Arg z < PI implies Arg (- z) = (Arg z) + PI ) & ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) ) then A2: |.z.| <> 0 by COMPLEX1:45; z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) by Th12; then A3: - z = (- (|.z.| * (cos (Arg z)))) + ((- (|.z.| * (sin (Arg z)))) * ) ; Arg z < 2 * PI by COMPTRIG:34; then (Arg z) + 0 < (2 * PI) + PI by COMPTRIG:5, XREAL_1:8; then A4: (Arg z) - PI < 2 * PI by XREAL_1:19; A5: - z = (|.(- z).| * (cos (Arg (- z)))) + ((|.(- z).| * (sin (Arg (- z)))) * ) by Th12; A6: |.z.| = |.(- z).| by COMPLEX1:52; then |.z.| * (sin (Arg (- z))) = |.z.| * (- (sin (Arg z))) by A5, A3, COMPLEX1:77; then A7: sin (Arg (- z)) = - (sin (Arg z)) by A2, XCMPLX_1:5; then A8: sin (Arg (- z)) = sin ((Arg z) + PI) by SIN_COS:79; |.z.| * (cos (Arg (- z))) = |.z.| * (- (cos (Arg z))) by A5, A3, A6, COMPLEX1:77; then A9: cos (Arg (- z)) = - (cos (Arg z)) by A2, XCMPLX_1:5; then A10: cos (Arg (- z)) = cos ((Arg z) + PI) by SIN_COS:79; hereby ::_thesis: ( Arg z >= PI implies Arg (- z) = (Arg z) - PI ) assume Arg z < PI ; ::_thesis: Arg (- z) = (Arg z) + PI then A11: (Arg z) + PI < PI + PI by XREAL_1:8; 0 <= Arg z by COMPTRIG:34; hence Arg (- z) = (Arg z) + PI by A1, A5, A10, A8, A11, COMPTRIG:5, COMPTRIG:def_1; ::_thesis: verum end; assume Arg z >= PI ; ::_thesis: Arg (- z) = (Arg z) - PI then A12: (Arg z) - PI >= PI - PI by XREAL_1:9; A13: sin (Arg (- z)) = sin ((Arg z) - PI) by A7, Th5; cos (Arg (- z)) = cos ((Arg z) - PI) by A9, Th5; hence Arg (- z) = (Arg z) - PI by A1, A5, A13, A12, A4, COMPTRIG:def_1; ::_thesis: verum end; theorem Th14: :: COMPLEX2:14 for r being Real st r >= 0 holds Arg r = 0 proof let r be Real; ::_thesis: ( r >= 0 implies Arg r = 0 ) assume A1: r >= 0 ; ::_thesis: Arg r = 0 A2: |.r.| = r by A1, ABSVALUE:def_1; A3: ( r = r + (0 * ) & r = (|.r.| * (cos (Arg r))) + ((|.r.| * (sin (Arg r))) * ) ) by Th12; then A4: r = |.r.| * (cos (Arg r)) by COMPLEX1:77; percases ( r = 0 or r > 0 ) by A1; suppose r = 0 ; ::_thesis: Arg r = 0 hence Arg r = 0 by COMPTRIG:35; ::_thesis: verum end; supposeA5: r > 0 ; ::_thesis: Arg r = 0 A6: ( 0 <= Arg r & Arg r < 2 * PI ) by COMPTRIG:34; ( cos (Arg r) = 1 & sin (Arg r) = 0 ) by A2, A3, A4, A5, XCMPLX_1:7; hence Arg r = 0 by A6, Th11, SIN_COS:31; ::_thesis: verum end; end; end; theorem Th15: :: COMPLEX2:15 for z being complex number holds ( Arg z = 0 iff z = |.z.| ) proof let z be complex number ; ::_thesis: ( Arg z = 0 iff z = |.z.| ) hereby ::_thesis: ( z = |.z.| implies Arg z = 0 ) assume Arg z = 0 ; ::_thesis: z = |.z.| then z = (|.z.| * (cos 0)) + ((|.z.| * (sin 0)) * ) by Th12; hence z = |.z.| by SIN_COS:31; ::_thesis: verum end; assume z = |.z.| ; ::_thesis: Arg z = 0 hence Arg z = 0 by Th14, COMPLEX1:46; ::_thesis: verum end; theorem Th16: :: COMPLEX2:16 for z being complex number st z <> 0 holds ( Arg z < PI iff Arg (- z) >= PI ) proof let z be complex number ; ::_thesis: ( z <> 0 implies ( Arg z < PI iff Arg (- z) >= PI ) ) assume A1: z <> 0 ; ::_thesis: ( Arg z < PI iff Arg (- z) >= PI ) thus ( Arg z < PI implies Arg (- z) >= PI ) ::_thesis: ( Arg (- z) >= PI implies Arg z < PI ) proof Arg z >= 0 by COMPTRIG:34; then A2: PI + 0 <= PI + (Arg z) by XREAL_1:7; assume Arg z < PI ; ::_thesis: Arg (- z) >= PI hence Arg (- z) >= PI by A1, A2, Th13; ::_thesis: verum end; thus ( Arg (- z) >= PI implies Arg z < PI ) ::_thesis: verum proof 2 * PI > Arg (- z) by COMPTRIG:34; then A3: (PI + PI) - PI > (Arg (- z)) - PI by XREAL_1:9; assume Arg (- z) >= PI ; ::_thesis: Arg z < PI then Arg (- (- z)) = (Arg (- z)) - PI by A1, Th13; hence Arg z < PI by A3; ::_thesis: verum end; end; theorem Th17: :: COMPLEX2:17 for x, y being complex number st ( x <> y or x - y <> 0 ) holds ( Arg (x - y) < PI iff Arg (y - x) >= PI ) proof let z1, z2 be complex number ; ::_thesis: ( ( z1 <> z2 or z1 - z2 <> 0 ) implies ( Arg (z1 - z2) < PI iff Arg (z2 - z1) >= PI ) ) assume ( z1 <> z2 or z1 - z2 <> 0 ) ; ::_thesis: ( Arg (z1 - z2) < PI iff Arg (z2 - z1) >= PI ) then z1 - z2 <> 0c ; then ( Arg (z1 - z2) < PI iff Arg (- (z1 - z2)) >= PI ) by Th16; hence ( Arg (z1 - z2) < PI iff Arg (z2 - z1) >= PI ) ; ::_thesis: verum end; theorem Th18: :: COMPLEX2:18 for z being complex number holds ( Arg z in ].0,PI.[ iff Im z > 0 ) proof let z be complex number ; ::_thesis: ( Arg z in ].0,PI.[ iff Im z > 0 ) thus ( Arg z in ].0,PI.[ implies Im z > 0 ) ::_thesis: ( Im z > 0 implies Arg z in ].0,PI.[ ) proof assume Arg z in ].0,PI.[ ; ::_thesis: Im z > 0 then A1: ( 0 < Arg z & Arg z < PI ) by XXREAL_1:4; A2: ( Arg z < PI / 2 or Arg z = PI / 2 or Arg z > PI / 2 ) by XXREAL_0:1; now__::_thesis:_(_(_Arg_z_in_].0,(PI_/_2).[_&_Im_z_>_0_)_or_(_Arg_z_=_PI_/_2_&_Im_z_>_0_)_or_(_Arg_z_in_].(PI_/_2),PI.[_&_Im_z_>_0_)_) percases ( Arg z in ].0,(PI / 2).[ or Arg z = PI / 2 or Arg z in ].(PI / 2),PI.[ ) by A1, A2, XXREAL_1:4; case Arg z in ].0,(PI / 2).[ ; ::_thesis: Im z > 0 hence Im z > 0 by COMPTRIG:41; ::_thesis: verum end; case Arg z = PI / 2 ; ::_thesis: Im z > 0 hence Im z > 0 by COMPTRIG:48, SIN_COS:77; ::_thesis: verum end; case Arg z in ].(PI / 2),PI.[ ; ::_thesis: Im z > 0 hence Im z > 0 by COMPTRIG:42; ::_thesis: verum end; end; end; hence Im z > 0 ; ::_thesis: verum end; A3: ].(PI / 2),PI.[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; A4: ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; thus ( Im z > 0 implies Arg z in ].0,PI.[ ) ::_thesis: verum proof assume A5: Im z > 0 ; ::_thesis: Arg z in ].0,PI.[ now__::_thesis:_(_(_Re_z_>_0_&_Arg_z_in_].0,PI.[_)_or_(_Re_z_=_0_&_Arg_z_in_].0,PI.[_)_or_(_Re_z_<_0_&_Arg_z_in_].0,PI.[_)_) percases ( Re z > 0 or Re z = 0 or Re z < 0 ) ; case Re z > 0 ; ::_thesis: Arg z in ].0,PI.[ then Arg z in ].0,(PI / 2).[ by A5, COMPTRIG:41; hence Arg z in ].0,PI.[ by A4; ::_thesis: verum end; case Re z = 0 ; ::_thesis: Arg z in ].0,PI.[ then z = 0 + ((Im z) * ) by COMPLEX1:13; then Arg z = PI / 2 by A5, COMPTRIG:37; hence Arg z in ].0,PI.[ by COMPTRIG:5, XXREAL_1:4; ::_thesis: verum end; case Re z < 0 ; ::_thesis: Arg z in ].0,PI.[ then Arg z in ].(PI / 2),PI.[ by A5, COMPTRIG:42; hence Arg z in ].0,PI.[ by A3; ::_thesis: verum end; end; end; hence Arg z in ].0,PI.[ ; ::_thesis: verum end; end; theorem :: COMPLEX2:19 for z being complex number st Arg z <> 0 holds ( Arg z < PI iff sin (Arg z) > 0 ) proof let z be complex number ; ::_thesis: ( Arg z <> 0 implies ( Arg z < PI iff sin (Arg z) > 0 ) ) A1: Arg z >= 0 by COMPTRIG:34; assume A2: Arg z <> 0 ; ::_thesis: ( Arg z < PI iff sin (Arg z) > 0 ) hereby ::_thesis: ( sin (Arg z) > 0 implies Arg z < PI ) assume Arg z < PI ; ::_thesis: sin (Arg z) > 0 then Arg z in ].0,PI.[ by A2, A1, XXREAL_1:4; then Im z > 0 by Th18; hence sin (Arg z) > 0 by COMPTRIG:45; ::_thesis: verum end; A3: ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; thus ( sin (Arg z) > 0 implies Arg z < PI ) ::_thesis: verum proof assume A4: sin (Arg z) > 0 ; ::_thesis: Arg z < PI then A5: Im z > 0 by COMPTRIG:48; now__::_thesis:_Arg_z_<_PI percases ( Re z > 0 or Re z = 0 or Re z < 0 ) ; suppose Re z > 0 ; ::_thesis: Arg z < PI then Arg z in ].0,(PI / 2).[ by A5, COMPTRIG:41; hence Arg z < PI by A3, XXREAL_1:4; ::_thesis: verum end; suppose Re z = 0 ; ::_thesis: Arg z < PI then z = 0 + ((Im z) * ) by COMPLEX1:13; hence Arg z < PI by A4, COMPTRIG:5, COMPTRIG:37, COMPTRIG:48; ::_thesis: verum end; suppose Re z < 0 ; ::_thesis: Arg z < PI then Arg z in ].(PI / 2),PI.[ by A5, COMPTRIG:42; hence Arg z < PI by XXREAL_1:4; ::_thesis: verum end; end; end; hence Arg z < PI ; ::_thesis: verum end; end; theorem :: COMPLEX2:20 for x, y being complex number st Arg x < PI & Arg y < PI holds Arg (x + y) < PI proof let z1, z2 be complex number ; ::_thesis: ( Arg z1 < PI & Arg z2 < PI implies Arg (z1 + z2) < PI ) assume that A1: Arg z1 < PI and A2: Arg z2 < PI ; ::_thesis: Arg (z1 + z2) < PI A3: |.z2.| = |.z2.| + (0 * ) ; A4: |.z1.| = |.z1.| + (0 * ) ; percases ( Arg z1 = 0 or Arg z1 > 0 ) by COMPTRIG:34; supposeA5: Arg z1 = 0 ; ::_thesis: Arg (z1 + z2) < PI then z1 = |.z1.| by Th15; then A6: Im z1 = 0 by A4, COMPLEX1:12; percases ( Arg z2 = 0 or Arg z2 > 0 ) by COMPTRIG:34; suppose Arg z2 = 0 ; ::_thesis: Arg (z1 + z2) < PI then z2 = |.z2.| by Th15; then A7: z1 + z2 = (|.z1.| + |.z2.|) + (0 * ) by A5, Th15; ( 0 <= |.z1.| & 0 <= |.z2.| ) by COMPLEX1:46; hence Arg (z1 + z2) < PI by A7, COMPTRIG:5, COMPTRIG:35; ::_thesis: verum end; suppose Arg z2 > 0 ; ::_thesis: Arg (z1 + z2) < PI then Arg z2 in ].0,PI.[ by A2, XXREAL_1:4; then A8: Im z2 > 0 by Th18; Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:8; then Arg (z1 + z2) in ].0,PI.[ by A6, A8, Th18; hence Arg (z1 + z2) < PI by XXREAL_1:4; ::_thesis: verum end; end; end; suppose Arg z1 > 0 ; ::_thesis: Arg (z1 + z2) < PI then Arg z1 in ].0,PI.[ by A1, XXREAL_1:4; then A9: Im z1 > 0 by Th18; percases ( Arg z2 = 0 or Arg z2 > 0 ) by COMPTRIG:34; suppose Arg z2 = 0 ; ::_thesis: Arg (z1 + z2) < PI then z2 = |.z2.| by Th15; then A10: Im z2 = 0 by A3, COMPLEX1:12; Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:8; then Arg (z1 + z2) in ].0,PI.[ by A9, A10, Th18; hence Arg (z1 + z2) < PI by XXREAL_1:4; ::_thesis: verum end; suppose Arg z2 > 0 ; ::_thesis: Arg (z1 + z2) < PI then Arg z2 in ].0,PI.[ by A2, XXREAL_1:4; then A11: Im z2 > 0 by Th18; Im (z1 + z2) = (Im z1) + (Im z2) by COMPLEX1:8; then Arg (z1 + z2) in ].0,PI.[ by A9, A11, Th18; hence Arg (z1 + z2) < PI by XXREAL_1:4; ::_thesis: verum end; end; end; end; end; theorem Th21: :: COMPLEX2:21 for z being complex number holds ( Arg z = 0 iff ( Re z >= 0 & Im z = 0 ) ) proof let z be complex number ; ::_thesis: ( Arg z = 0 iff ( Re z >= 0 & Im z = 0 ) ) A1: |.z.| = |.z.| + (0 * ) ; hereby ::_thesis: ( Re z >= 0 & Im z = 0 implies Arg z = 0 ) assume Arg z = 0 ; ::_thesis: ( Re z >= 0 & Im z = 0 ) then A2: z = |.z.| by Th15; then Re z = |.z.| by A1, COMPLEX1:12; hence ( Re z >= 0 & Im z = 0 ) by A1, A2, COMPLEX1:12, COMPLEX1:46; ::_thesis: verum end; assume that A3: Re z >= 0 and A4: Im z = 0 ; ::_thesis: Arg z = 0 z = (Re z) + (0 * ) by A4, COMPLEX1:13; hence Arg z = 0 by A3, COMPTRIG:35; ::_thesis: verum end; theorem Th22: :: COMPLEX2:22 for z being complex number holds ( Arg z = PI iff ( Re z < 0 & Im z = 0 ) ) proof let z be complex number ; ::_thesis: ( Arg z = PI iff ( Re z < 0 & Im z = 0 ) ) hereby ::_thesis: ( Re z < 0 & Im z = 0 implies Arg z = PI ) assume A1: Arg z = PI ; ::_thesis: ( Re z < 0 & Im z = 0 ) percases ( z <> 0 or z = 0 ) ; suppose z <> 0 ; ::_thesis: ( Re z < 0 & Im z = 0 ) then ( z = (|.z.| * (cos PI)) + ((|.z.| * (sin PI)) * ) & - (- |.z.|) > 0 ) by A1, COMPLEX1:47, COMPTRIG:def_1; hence ( Re z < 0 & Im z = 0 ) by COMPLEX1:def_1, COMPLEX1:def_2, SIN_COS:77; ::_thesis: verum end; suppose z = 0 ; ::_thesis: ( Re z < 0 & Im z = 0 ) hence ( Re z < 0 & Im z = 0 ) by A1, COMPTRIG:5, COMPTRIG:35; ::_thesis: verum end; end; end; assume that A2: Re z < 0 and A3: Im z = 0 ; ::_thesis: Arg z = PI z = (Re z) + (0 * ) by A3, COMPLEX1:13; hence Arg z = PI by A2, COMPTRIG:36; ::_thesis: verum end; theorem Th23: :: COMPLEX2:23 for z being complex number holds ( Im z = 0 iff ( Arg z = 0 or Arg z = PI ) ) proof let z be complex number ; ::_thesis: ( Im z = 0 iff ( Arg z = 0 or Arg z = PI ) ) hereby ::_thesis: ( ( Arg z = 0 or Arg z = PI ) implies Im z = 0 ) A1: ( Arg ((Re z) + (0 * )) = 0 or Arg ((Re z) + (0 * )) = PI ) by COMPTRIG:35, COMPTRIG:36; assume Im z = 0 ; ::_thesis: ( Arg z = 0 or Arg z = PI ) hence ( Arg z = 0 or Arg z = PI ) by A1, COMPLEX1:13; ::_thesis: verum end; assume ( Arg z = 0 or Arg z = PI ) ; ::_thesis: Im z = 0 hence Im z = 0 by Th21, Th22; ::_thesis: verum end; theorem Th24: :: COMPLEX2:24 for z being complex number st Arg z <= PI holds Im z >= 0 proof let z be complex number ; ::_thesis: ( Arg z <= PI implies Im z >= 0 ) assume A1: Arg z <= PI ; ::_thesis: Im z >= 0 percases ( Arg z = PI or Arg z = 0 or ( 0 < Arg z & Arg z < PI ) ) by A1, COMPTRIG:34, XXREAL_0:1; suppose ( Arg z = PI or Arg z = 0 ) ; ::_thesis: Im z >= 0 hence Im z >= 0 by Th23; ::_thesis: verum end; suppose ( 0 < Arg z & Arg z < PI ) ; ::_thesis: Im z >= 0 then Arg z in ].0,PI.[ by XXREAL_1:4; hence Im z >= 0 by Th18; ::_thesis: verum end; end; end; theorem Th25: :: COMPLEX2:25 for z being Element of COMPLEX st z <> 0 holds ( cos (Arg (- z)) = - (cos (Arg z)) & sin (Arg (- z)) = - (sin (Arg z)) ) proof let a be Element of COMPLEX ; ::_thesis: ( a <> 0 implies ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) ) A1: |.(- a).| = |.a.| by COMPLEX1:52; assume a <> 0 ; ::_thesis: ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) then A2: |.a.| <> 0 by COMPLEX1:45; ( a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) & - a = (|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * ) ) by Th12; then A3: 0 + (0 * ) = ((|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a))))) + (((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * ) by A1; then |.a.| * ((sin (Arg a)) + (sin (Arg (- a)))) = 0 by COMPLEX1:4, COMPLEX1:12; then A4: (sin (Arg a)) + (- (- (sin (Arg (- a))))) = 0 by A2; |.a.| * ((cos (Arg a)) + (cos (Arg (- a)))) = 0 by A3, COMPLEX1:4, COMPLEX1:12; then (cos (Arg a)) + (- (- (cos (Arg (- a))))) = 0 by A2; hence ( cos (Arg (- a)) = - (cos (Arg a)) & sin (Arg (- a)) = - (sin (Arg a)) ) by A4; ::_thesis: verum end; theorem Th26: :: COMPLEX2:26 for a being complex number st a <> 0 holds ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) proof let a be complex number ; ::_thesis: ( a <> 0 implies ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) ) a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) by Th12; then A1: ( Re a = |.a.| * (cos (Arg a)) & Im a = |.a.| * (sin (Arg a)) ) by COMPLEX1:12; assume a <> 0 ; ::_thesis: ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) hence ( cos (Arg a) = (Re a) / |.a.| & sin (Arg a) = (Im a) / |.a.| ) by A1, COMPLEX1:45, XCMPLX_1:89; ::_thesis: verum end; theorem Th27: :: COMPLEX2:27 for a being complex number for r being Real st r > 0 holds Arg (a * r) = Arg a proof let a be complex number ; ::_thesis: for r being Real st r > 0 holds Arg (a * r) = Arg a let r be Real; ::_thesis: ( r > 0 implies Arg (a * r) = Arg a ) assume A1: r > 0 ; ::_thesis: Arg (a * r) = Arg a percases ( a = 0 or a <> 0 ) ; suppose a = 0 ; ::_thesis: Arg (a * r) = Arg a hence Arg (a * r) = Arg a ; ::_thesis: verum end; supposeA2: a <> 0 ; ::_thesis: Arg (a * r) = Arg a then A3: sin (Arg a) = (Im a) / |.a.| by Th26; set b = a * r; A4: |.(a * r).| = |.a.| * (abs r) by COMPLEX1:65 .= |.a.| * r by A1, ABSVALUE:def_1 ; A5: cos (Arg a) = (Re a) / |.a.| by A2, Th26; A6: ( 0 <= Arg a & Arg a < 2 * PI ) by COMPTRIG:34; r = r + (0 * ) ; then A7: ( Re r = r & Im r = 0 ) by COMPLEX1:12; then A8: Im (a * r) = ((Re a) * 0) + (r * (Im a)) by COMPLEX1:9 .= r * (Im a) ; A9: sin (Arg (a * r)) = (Im (a * r)) / |.(a * r).| by A1, A2, Th26 .= sin (Arg a) by A1, A8, A4, A3, XCMPLX_1:91 ; A10: ( 0 <= Arg (a * r) & Arg (a * r) < 2 * PI ) by COMPTRIG:34; A11: Re (a * r) = ((Re a) * r) - (0 * (Im a)) by A7, COMPLEX1:9 .= r * (Re a) ; cos (Arg (a * r)) = (Re (a * r)) / |.(a * r).| by A1, A2, Th26 .= cos (Arg a) by A1, A11, A4, A5, XCMPLX_1:91 ; hence Arg (a * r) = Arg a by A9, A10, A6, Th11; ::_thesis: verum end; end; end; theorem Th28: :: COMPLEX2:28 for a being complex number for r being Real st r < 0 holds Arg (a * r) = Arg (- a) proof let a be complex number ; ::_thesis: for r being Real st r < 0 holds Arg (a * r) = Arg (- a) let r be Real; ::_thesis: ( r < 0 implies Arg (a * r) = Arg (- a) ) assume A1: r < 0 ; ::_thesis: Arg (a * r) = Arg (- a) percases ( a = 0 or a <> 0 ) ; suppose a = 0 ; ::_thesis: Arg (a * r) = Arg (- a) hence Arg (a * r) = Arg (- a) ; ::_thesis: verum end; supposeA2: a <> 0 ; ::_thesis: Arg (a * r) = Arg (- a) then A3: cos (Arg a) = (Re a) / |.a.| by Th26; A4: ( 0 <= Arg (- a) & Arg (- a) < 2 * PI ) by COMPTRIG:34; A5: sin (Arg a) = (Im a) / |.a.| by A2, Th26; set b = a * r; A6: a in COMPLEX by XCMPLX_0:def_2; A7: ( 0 <= Arg (a * r) & Arg (a * r) < 2 * PI ) by COMPTRIG:34; A8: |.(a * r).| = |.a.| * (abs r) by COMPLEX1:65 .= |.a.| * (- r) by A1, ABSVALUE:def_1 ; r = r + (0 * ) ; then A9: ( Re r = r & Im r = 0 ) by COMPLEX1:12; then Im (a * r) = ((Re a) * 0) + (r * (Im a)) by COMPLEX1:9 .= r * (Im a) ; then A10: sin (Arg (a * r)) = (r * (Im a)) / (- (|.a.| * r)) by A1, A2, A8, Th26 .= - ((r * (Im a)) / (|.a.| * r)) by XCMPLX_1:188 .= - (sin (Arg a)) by A1, A5, XCMPLX_1:91 .= sin (Arg (- a)) by A2, A6, Th25 ; Re (a * r) = ((Re a) * r) - (0 * (Im a)) by A9, COMPLEX1:9 .= r * (Re a) ; then cos (Arg (a * r)) = (r * (Re a)) / (- (|.a.| * r)) by A1, A2, A8, Th26 .= - ((r * (Re a)) / (|.a.| * r)) by XCMPLX_1:188 .= - (cos (Arg a)) by A1, A3, XCMPLX_1:91 .= cos (Arg (- a)) by A2, A6, Th25 ; hence Arg (a * r) = Arg (- a) by A10, A7, A4, Th11; ::_thesis: verum end; end; end; begin definition let x, y be complex number ; funcx .|. y -> Element of COMPLEX equals :: COMPLEX2:def 1 x * (y *'); correctness coherence x * (y *') is Element of COMPLEX ; by XCMPLX_0:def_2; end; :: deftheorem defines .|. COMPLEX2:def_1_:_ for x, y being complex number holds x .|. y = x * (y *'); theorem Th29: :: COMPLEX2:29 for x, y being Element of COMPLEX holds x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * ) proof let x, y be Element of COMPLEX ; ::_thesis: x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * ) ( x = (Re x) + ((Im x) * ) & y *' = (Re y) - ((Im y) * ) ) by COMPLEX1:13, COMPLEX1:def_11; hence x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * ) ; ::_thesis: verum end; theorem Th30: :: COMPLEX2:30 for z being Element of COMPLEX holds ( z .|. z = ((Re z) * (Re z)) + ((Im z) * (Im z)) & z .|. z = ((Re z) ^2) + ((Im z) ^2) ) proof let z be Element of COMPLEX ; ::_thesis: ( z .|. z = ((Re z) * (Re z)) + ((Im z) * (Im z)) & z .|. z = ((Re z) ^2) + ((Im z) ^2) ) thus z .|. z = (((Re z) * (Re z)) + ((Im z) * (Im z))) + (((- ((Im z) * (Re z))) + ((Im z) * (Re z))) * ) by Th29 .= ((Re z) * (Re z)) + ((Im z) * (Im z)) ; ::_thesis: z .|. z = ((Re z) ^2) + ((Im z) ^2) hence z .|. z = ((Re z) ^2) + ((Im z) ^2) ; ::_thesis: verum end; theorem Th31: :: COMPLEX2:31 for z being Element of COMPLEX holds ( z .|. z = |.z.| ^2 & |.z.| ^2 = Re (z .|. z) ) proof let z be Element of COMPLEX ; ::_thesis: ( z .|. z = |.z.| ^2 & |.z.| ^2 = Re (z .|. z) ) A1: ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63; A2: |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2)) by COMPLEX1:def_12; thus A3: z .|. z = ((Re z) ^2) + ((Im z) ^2) by Th30 .= |.z.| ^2 by A1, A2, SQUARE_1:def_2 ; ::_thesis: |.z.| ^2 = Re (z .|. z) |.z.| ^2 = (|.z.| ^2) + (0 * ) ; hence |.z.| ^2 = Re (z .|. z) by A3, COMPLEX1:12; ::_thesis: verum end; theorem Th32: :: COMPLEX2:32 for x, y being Element of COMPLEX holds |.(x .|. y).| = |.x.| * |.y.| proof let x, y be Element of COMPLEX ; ::_thesis: |.(x .|. y).| = |.x.| * |.y.| thus |.(x .|. y).| = |.x.| * |.(y *').| by COMPLEX1:65 .= |.x.| * |.y.| by COMPLEX1:53 ; ::_thesis: verum end; theorem :: COMPLEX2:33 for x being Element of COMPLEX st x .|. x = 0 holds x = 0 proof let x be Element of COMPLEX ; ::_thesis: ( x .|. x = 0 implies x = 0 ) assume x .|. x = 0 ; ::_thesis: x = 0 then ((Re x) ^2) + ((Im x) ^2) = 0 by Th30; hence x = 0 by COMPLEX1:5; ::_thesis: verum end; theorem Th34: :: COMPLEX2:34 for y, x being Element of COMPLEX holds y .|. x = (x .|. y) *' proof let y, x be Element of COMPLEX ; ::_thesis: y .|. x = (x .|. y) *' thus y .|. x = ((y * (x *')) *') *' .= (((x *') *') * (y *')) *' by COMPLEX1:35 .= (x .|. y) *' ; ::_thesis: verum end; theorem :: COMPLEX2:35 for x, y, z being Element of COMPLEX holds (x + y) .|. z = (x .|. z) + (y .|. z) ; theorem Th36: :: COMPLEX2:36 for x, y, z being Element of COMPLEX holds x .|. (y + z) = (x .|. y) + (x .|. z) proof let x, y, z be Element of COMPLEX ; ::_thesis: x .|. (y + z) = (x .|. y) + (x .|. z) thus x .|. (y + z) = x * ((y *') + (z *')) by COMPLEX1:32 .= (x .|. y) + (x .|. z) ; ::_thesis: verum end; theorem :: COMPLEX2:37 for a, x, y being Element of COMPLEX holds (a * x) .|. y = a * (x .|. y) ; theorem Th38: :: COMPLEX2:38 for x, a, y being Element of COMPLEX holds x .|. (a * y) = (a *') * (x .|. y) proof let x, a, y be Element of COMPLEX ; ::_thesis: x .|. (a * y) = (a *') * (x .|. y) thus x .|. (a * y) = x * ((a *') * (y *')) by COMPLEX1:35 .= (a *') * (x .|. y) ; ::_thesis: verum end; theorem :: COMPLEX2:39 for a, x, y being Element of COMPLEX holds (a * x) .|. y = x .|. ((a *') * y) proof let a, x, y be Element of COMPLEX ; ::_thesis: (a * x) .|. y = x .|. ((a *') * y) thus (a * x) .|. y = x * (((a *') *') * (y *')) .= x .|. ((a *') * y) by COMPLEX1:35 ; ::_thesis: verum end; theorem :: COMPLEX2:40 for a, x, b, y, z being Element of COMPLEX holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) ; theorem :: COMPLEX2:41 for x, a, y, b, z being Element of COMPLEX holds x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) proof let x, a, y, b, z be Element of COMPLEX ; ::_thesis: x .|. ((a * y) + (b * z)) = ((a *') * (x .|. y)) + ((b *') * (x .|. z)) thus x .|. ((a * y) + (b * z)) = (x .|. (a * y)) + (x .|. (b * z)) by Th36 .= ((a *') * (x .|. y)) + (x .|. (b * z)) by Th38 .= ((a *') * (x .|. y)) + ((b *') * (x .|. z)) by Th38 ; ::_thesis: verum end; theorem Th42: :: COMPLEX2:42 for x, y being Element of COMPLEX holds (- x) .|. y = x .|. (- y) proof let x, y be Element of COMPLEX ; ::_thesis: (- x) .|. y = x .|. (- y) thus (- x) .|. y = (- (1r *')) * (x .|. y) by COMPLEX1:30, COMPLEX1:def_4 .= ((- 1r) *') * (x .|. y) by COMPLEX1:33 .= x .|. ((- 1r) * y) by Th38 .= x .|. (- y) by COMPLEX1:def_4 ; ::_thesis: verum end; theorem :: COMPLEX2:43 for x, y being Element of COMPLEX holds (- x) .|. y = - (x .|. y) ; theorem Th44: :: COMPLEX2:44 for x, y being Element of COMPLEX holds - (x .|. y) = x .|. (- y) proof let x, y be Element of COMPLEX ; ::_thesis: - (x .|. y) = x .|. (- y) thus - (x .|. y) = (- x) .|. y .= x .|. (- y) by Th42 ; ::_thesis: verum end; theorem :: COMPLEX2:45 for x, y being Element of COMPLEX holds (- x) .|. (- y) = x .|. y proof let x, y be Element of COMPLEX ; ::_thesis: (- x) .|. (- y) = x .|. y (- x) .|. (- y) = - (x .|. (- y)) .= - (- (x .|. y)) by Th44 ; hence (- x) .|. (- y) = x .|. y ; ::_thesis: verum end; theorem :: COMPLEX2:46 for x, y, z being Element of COMPLEX holds (x - y) .|. z = (x .|. z) - (y .|. z) ; theorem Th47: :: COMPLEX2:47 for x, y, z being Element of COMPLEX holds x .|. (y - z) = (x .|. y) - (x .|. z) proof let x, y, z be Element of COMPLEX ; ::_thesis: x .|. (y - z) = (x .|. y) - (x .|. z) thus x .|. (y - z) = x * ((y *') - (z *')) by COMPLEX1:34 .= (x .|. y) - (x .|. z) ; ::_thesis: verum end; theorem :: COMPLEX2:48 for x, y being Element of COMPLEX holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) proof let x, y be Element of COMPLEX ; ::_thesis: (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) (x + y) .|. (x + y) = (x .|. (x + y)) + (y .|. (x + y)) .= ((x .|. x) + (x .|. y)) + (y .|. (x + y)) by Th36 .= ((x .|. x) + (x .|. y)) + ((y .|. x) + (y .|. y)) by Th36 .= (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) ; hence (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) ; ::_thesis: verum end; theorem Th49: :: COMPLEX2:49 for x, y being Element of COMPLEX holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) proof let x, y be Element of COMPLEX ; ::_thesis: (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) (x - y) .|. (x - y) = (x .|. (x - y)) - (y .|. (x - y)) .= ((x .|. x) - (x .|. y)) - (y .|. (x - y)) by Th47 .= ((x .|. x) - (x .|. y)) - ((y .|. x) - (y .|. y)) by Th47 .= (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ; hence (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) ; ::_thesis: verum end; Lm2: for z being Element of COMPLEX holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) proof let z be Element of COMPLEX ; ::_thesis: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) thus |.z.| ^2 = |.(z * z).| by COMPLEX1:65 .= ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:68 ; ::_thesis: verum end; theorem Th50: :: COMPLEX2:50 for x, y being Element of COMPLEX holds ( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) ) proof let x, y be Element of COMPLEX ; ::_thesis: ( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) ) hereby ::_thesis: ( ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) implies Re (x .|. y) = 0 ) assume A1: Re (x .|. y) = 0 ; ::_thesis: ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) (|.x.| * |.y.|) ^2 = |.(x .|. y).| ^2 by Th32 .= (0 ^2) + ((Im (x .|. y)) ^2) by A1, Lm2 .= (Im (x .|. y)) ^2 ; hence ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) by SQUARE_1:40; ::_thesis: verum end; hereby ::_thesis: verum assume ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) ; ::_thesis: Re (x .|. y) = 0 then (Im (x .|. y)) ^2 = (|.x.| * |.y.|) ^2 .= |.(x .|. y).| ^2 by Th32 .= ((Re (x .|. y)) ^2) + ((Im (x .|. y)) ^2) by Lm2 ; hence Re (x .|. y) = 0 ; ::_thesis: verum end; end; begin definition let a be complex number ; 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)))) * ); correctness coherence (|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * ) is Element of COMPLEX ; by XCMPLX_0:def_2; end; :: deftheorem defines Rotate COMPLEX2:def_2_:_ for a being complex number for r being Real holds Rotate (a,r) = (|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * ); theorem :: COMPLEX2:51 for a being Element of COMPLEX holds Rotate (a,0) = a by Th12; theorem Th52: :: COMPLEX2:52 for r being Real for a being complex number holds ( Rotate (a,r) = 0 iff a = 0 ) proof let r be Real; ::_thesis: for a being complex number holds ( Rotate (a,r) = 0 iff a = 0 ) let a be complex number ; ::_thesis: ( Rotate (a,r) = 0 iff a = 0 ) hereby ::_thesis: ( a = 0 implies Rotate (a,r) = 0 ) assume Rotate (a,r) = 0 ; ::_thesis: a = 0 then A1: Rotate (a,r) = 0 + (0 * ) ; percases ( |.a.| = 0 or ( cos (r + (Arg a)) = 0 & sin (r + (Arg a)) = 0 ) ) by A1, COMPLEX1:77; suppose |.a.| = 0 ; ::_thesis: a = 0 hence a = 0 by COMPLEX1:45; ::_thesis: verum end; suppose ( cos (r + (Arg a)) = 0 & sin (r + (Arg a)) = 0 ) ; ::_thesis: a = 0 hence a = 0 by Th10; ::_thesis: verum end; end; end; assume a = 0 ; ::_thesis: Rotate (a,r) = 0 hence Rotate (a,r) = 0 by COMPLEX1:44; ::_thesis: verum end; theorem Th53: :: COMPLEX2:53 for r being Real for a being complex number holds |.(Rotate (a,r)).| = |.a.| proof let r be Real; ::_thesis: for a being complex number holds |.(Rotate (a,r)).| = |.a.| let a be complex number ; ::_thesis: |.(Rotate (a,r)).| = |.a.| ( Re (Rotate (a,r)) = |.a.| * (cos (r + (Arg a))) & Im (Rotate (a,r)) = |.a.| * (sin (r + (Arg a))) ) by COMPLEX1:12; hence |.(Rotate (a,r)).| = sqrt (((|.a.| * (cos (r + (Arg a)))) ^2) + ((|.a.| * (sin (r + (Arg a)))) ^2)) by COMPLEX1:def_12 .= sqrt ((|.a.| ^2) * (((cos (r + (Arg a))) ^2) + ((sin (r + (Arg a))) ^2))) .= sqrt ((|.a.| ^2) * 1) by SIN_COS:29 .= |.a.| by COMPLEX1:46, SQUARE_1:22 ; ::_thesis: verum end; theorem Th54: :: COMPLEX2:54 for r being Real for a being complex number st a <> 0 holds ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a)) proof let r be Real; ::_thesis: for a being complex number st a <> 0 holds ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a)) let a be complex number ; ::_thesis: ( a <> 0 implies ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a)) ) A1: |.a.| = |.(Rotate (a,r)).| by Th53; assume a <> 0 ; ::_thesis: ex i being Integer st Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a)) then A2: Rotate (a,r) <> 0c by Th52; take - [\((r + (Arg a)) / (2 * PI))/] ; ::_thesis: Arg (Rotate (a,r)) = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a)) consider AR being real number such that A3: AR = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a)) and A4: ( 0 <= AR & AR < 2 * PI ) by Th1, COMPTRIG:5; reconsider ar = AR as Real by XREAL_0:def_1; ( cos (r + (Arg a)) = cos ar & sin (r + (Arg a)) = sin ar ) by A3, Th8, Th9; hence Arg (Rotate (a,r)) = ((2 * PI) * (- [\((r + (Arg a)) / (2 * PI))/])) + (r + (Arg a)) by A2, A1, A3, A4, COMPTRIG:def_1; ::_thesis: verum end; theorem :: COMPLEX2:55 for a being Element of COMPLEX holds Rotate (a,(- (Arg a))) = |.a.| by SIN_COS:31; theorem Th56: :: COMPLEX2:56 for a being Element of 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)) ) proof let a be Element of COMPLEX ; ::_thesis: 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)) ) let r be Real; ::_thesis: ( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) ) a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) by Th12; then A1: ( Re a = |.a.| * (cos (Arg a)) & Im a = |.a.| * (sin (Arg a)) ) by COMPLEX1:12; thus Re (Rotate (a,r)) = |.a.| * (cos (r + (Arg a))) by COMPLEX1:12 .= |.a.| * (((cos r) * (cos (Arg a))) - ((sin r) * (sin (Arg a)))) by SIN_COS:75 .= ((Re a) * (cos r)) - ((Im a) * (sin r)) by A1 ; ::_thesis: Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) thus Im (Rotate (a,r)) = |.a.| * (sin (r + (Arg a))) by COMPLEX1:12 .= |.a.| * (((sin r) * (cos (Arg a))) + ((cos r) * (sin (Arg a)))) by SIN_COS:75 .= ((Re a) * (sin r)) + ((Im a) * (cos r)) by A1 ; ::_thesis: verum end; theorem Th57: :: COMPLEX2:57 for a, b being Element of COMPLEX for r being Real holds Rotate ((a + b),r) = (Rotate (a,r)) + (Rotate (b,r)) proof let a, b be Element of COMPLEX ; ::_thesis: for r being Real holds Rotate ((a + b),r) = (Rotate (a,r)) + (Rotate (b,r)) let r be Real; ::_thesis: Rotate ((a + b),r) = (Rotate (a,r)) + (Rotate (b,r)) set ab = a + b; set rab = Rotate ((a + b),r); set ra = Rotate (a,r); set rb = Rotate (b,r); A1: ( Re (a + b) = (Re a) + (Re b) & Im (a + b) = (Im a) + (Im b) ) by COMPLEX1:8; A2: Im (Rotate ((a + b),r)) = ((Re (a + b)) * (sin r)) + ((Im (a + b)) * (cos r)) by Th56; ( Im (Rotate (a,r)) = ((Re a) * (sin r)) + ((Im a) * (cos r)) & Im (Rotate (b,r)) = ((Re b) * (sin r)) + ((Im b) * (cos r)) ) by Th56; then A3: Im ((Rotate (a,r)) + (Rotate (b,r))) = (((Re a) * (sin r)) + ((Im a) * (cos r))) + (((Re b) * (sin r)) + ((Im b) * (cos r))) by COMPLEX1:8 .= Im (Rotate ((a + b),r)) by A2, A1 ; A4: Re (Rotate ((a + b),r)) = ((Re (a + b)) * (cos r)) - ((Im (a + b)) * (sin r)) by Th56; ( Re (Rotate (a,r)) = ((Re a) * (cos r)) - ((Im a) * (sin r)) & Re (Rotate (b,r)) = ((Re b) * (cos r)) - ((Im b) * (sin r)) ) by Th56; then Re ((Rotate (a,r)) + (Rotate (b,r))) = (((Re a) * (cos r)) - ((Im a) * (sin r))) + (((Re b) * (cos r)) - ((Im b) * (sin r))) by COMPLEX1:8 .= Re (Rotate ((a + b),r)) by A4, A1 ; hence Rotate ((a + b),r) = (Rotate (a,r)) + (Rotate (b,r)) by A3, COMPLEX1:3; ::_thesis: verum end; theorem Th58: :: COMPLEX2:58 for a being Element of COMPLEX for r being Real holds Rotate ((- a),r) = - (Rotate (a,r)) proof let a be Element of COMPLEX ; ::_thesis: for r being Real holds Rotate ((- a),r) = - (Rotate (a,r)) let r be Real; ::_thesis: Rotate ((- a),r) = - (Rotate (a,r)) percases ( a <> 0c or a = 0c ) ; supposeA1: a <> 0c ; ::_thesis: Rotate ((- a),r) = - (Rotate (a,r)) A2: ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) proof percases ( Arg a < PI or Arg a >= PI ) ; suppose Arg a < PI ; ::_thesis: ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) then Arg (- a) = PI + (Arg a) by A1, Th13; then r + (Arg (- a)) = PI + (r + (Arg a)) ; hence ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) by SIN_COS:79; ::_thesis: verum end; suppose Arg a >= PI ; ::_thesis: ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) then Arg (- a) = (Arg a) - PI by A1, Th13; then r + (Arg (- a)) = ((Arg a) + r) - PI ; hence ( cos (r + (Arg (- a))) = - (cos (r + (Arg a))) & sin (r + (Arg (- a))) = - (sin (r + (Arg a))) ) by Th5; ::_thesis: verum end; end; end; |.a.| = |.(- a).| by COMPLEX1:52; hence Rotate ((- a),r) = - (Rotate (a,r)) by A2; ::_thesis: verum end; supposeA3: a = 0c ; ::_thesis: Rotate ((- a),r) = - (Rotate (a,r)) hence Rotate ((- a),r) = - 0 by Th52 .= - (Rotate (a,r)) by A3, Th52 ; ::_thesis: verum end; end; end; theorem Th59: :: COMPLEX2:59 for a, b being Element of COMPLEX for r being Real holds Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r)) proof let a, b be Element of COMPLEX ; ::_thesis: for r being Real holds Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r)) let r be Real; ::_thesis: Rotate ((a - b),r) = (Rotate (a,r)) - (Rotate (b,r)) thus Rotate ((a - b),r) = (Rotate (a,r)) + (Rotate ((- b),r)) by Th57 .= (Rotate (a,r)) - (Rotate (b,r)) by Th58 ; ::_thesis: verum end; theorem Th60: :: COMPLEX2:60 for a being Element of COMPLEX holds Rotate (a,PI) = - a proof let a be Element of COMPLEX ; ::_thesis: Rotate (a,PI) = - a A1: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) by Th12; A2: |.a.| * (- (sin (Arg a))) = - (|.a.| * (sin (Arg a))) .= - (Im a) by A1, COMPLEX1:12 ; A3: |.a.| * (- (cos (Arg a))) = - (|.a.| * (cos (Arg a))) .= - (Re a) by A1, COMPLEX1:12 ; thus Rotate (a,PI) = (|.a.| * (- (cos (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * ) by SIN_COS:79 .= (|.a.| * (- (cos (Arg a)))) + ((|.a.| * (- (sin (Arg a)))) * ) by SIN_COS:79 .= - a by A3, A2, COMPLEX1:def_7 ; ::_thesis: verum end; begin definition let a, b be complex number ; 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 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 b1 being Real holds verum; ; end; :: deftheorem Def3 defines angle COMPLEX2:def_3_:_ for a, b being complex number 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 Th61: :: COMPLEX2:61 for r being Real for a being complex number st r >= 0 holds angle (r,a) = Arg a proof let r be Real; ::_thesis: for a being complex number st r >= 0 holds angle (r,a) = Arg a let a be complex number ; ::_thesis: ( r >= 0 implies angle (r,a) = Arg a ) assume r >= 0 ; ::_thesis: angle (r,a) = Arg a then Arg r = 0 by Th14; hence angle (r,a) = Arg (Rotate (a,(- 0))) by Def3 .= Arg a by Th12 ; ::_thesis: verum end; theorem Th62: :: COMPLEX2:62 for r being Real for a, b being complex number st Arg a = Arg b & a <> 0 & b <> 0 holds Arg (Rotate (a,r)) = Arg (Rotate (b,r)) proof let r be Real; ::_thesis: for a, b being complex number st Arg a = Arg b & a <> 0 & b <> 0 holds Arg (Rotate (a,r)) = Arg (Rotate (b,r)) let a, b be complex number ; ::_thesis: ( Arg a = Arg b & a <> 0 & b <> 0 implies Arg (Rotate (a,r)) = Arg (Rotate (b,r)) ) assume that A1: Arg a = Arg b and A2: a <> 0 and A3: b <> 0 ; ::_thesis: Arg (Rotate (a,r)) = Arg (Rotate (b,r)) consider i being Integer such that A4: Arg (Rotate (a,r)) = ((2 * PI) * i) + (r + (Arg a)) by A2, Th54; consider j being Integer such that A5: Arg (Rotate (b,r)) = ((2 * PI) * j) + (r + (Arg b)) by A3, Th54; A6: ( 0 <= Arg (Rotate (a,r)) & 0 <= Arg (Rotate (b,r)) ) by COMPTRIG:34; A7: ( Arg (Rotate (a,r)) < 2 * PI & Arg (Rotate (b,r)) < 2 * PI ) by COMPTRIG:34; Arg (Rotate (b,r)) = ((2 * PI) * (j - i)) + (Arg (Rotate (a,r))) by A1, A4, A5; hence Arg (Rotate (a,r)) = Arg (Rotate (b,r)) by A6, A7, Th2; ::_thesis: verum end; theorem Th63: :: COMPLEX2:63 for a, b being Element of COMPLEX for r being Real st r > 0 holds angle (a,b) = angle ((a * r),(b * r)) proof let a, b be Element of COMPLEX ; ::_thesis: for r being Real st r > 0 holds angle (a,b) = angle ((a * r),(b * r)) let r be Real; ::_thesis: ( r > 0 implies angle (a,b) = angle ((a * r),(b * r)) ) assume A1: r > 0 ; ::_thesis: angle (a,b) = angle ((a * r),(b * r)) then A2: Arg (a * r) = Arg a by Th27; percases ( b <> 0 or b = 0 ) ; supposeA3: b <> 0 ; ::_thesis: angle (a,b) = angle ((a * r),(b * r)) hence angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by Def3 .= Arg (Rotate ((b * r),(- (Arg (a * r))))) by A1, A2, A3, Th27, Th62 .= angle ((a * r),(b * r)) by A1, A3, Def3 ; ::_thesis: verum end; supposeA4: b = 0 ; ::_thesis: angle (a,b) = angle ((a * r),(b * r)) thus angle (a,b) = angle ((a * r),(b * r)) ::_thesis: verum proof percases ( Arg a = 0 or Arg a <> 0 ) ; supposeA5: Arg a = 0 ; ::_thesis: angle (a,b) = angle ((a * r),(b * r)) hence angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by Def3 .= Arg 0c by A4, Th52 .= Arg (Rotate ((b * r),(- (Arg (a * r))))) by A4, Th52 .= angle ((a * r),(b * r)) by A2, A5, Def3 ; ::_thesis: verum end; supposeA6: Arg a <> 0 ; ::_thesis: angle (a,b) = angle ((a * r),(b * r)) hence angle (a,b) = (2 * PI) - (Arg a) by A4, Def3 .= angle ((a * r),(b * r)) by A2, A4, A6, Def3 ; ::_thesis: verum end; end; end; end; end; end; theorem Th64: :: COMPLEX2:64 for a, b being Element of COMPLEX st a <> 0 & b <> 0 & Arg a = Arg b holds Arg (- a) = Arg (- b) proof let a, b be Element of COMPLEX ; ::_thesis: ( a <> 0 & b <> 0 & Arg a = Arg b implies Arg (- a) = Arg (- b) ) assume ( a <> 0 & b <> 0 & Arg a = Arg b ) ; ::_thesis: Arg (- a) = Arg (- b) then Arg (Rotate (a,PI)) = Arg (Rotate (b,PI)) by Th62; then Arg (- a) = Arg (Rotate (b,PI)) by Th60; hence Arg (- a) = Arg (- b) by Th60; ::_thesis: verum end; theorem Th65: :: COMPLEX2:65 for a, b being Element of COMPLEX for r being Real st a <> 0 & b <> 0 holds angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r))) proof let a, b be Element of COMPLEX ; ::_thesis: for r being Real st a <> 0 & b <> 0 holds angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r))) let r be Real; ::_thesis: ( a <> 0 & b <> 0 implies angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r))) ) assume that A1: a <> 0 and A2: b <> 0 ; ::_thesis: angle (a,b) = angle ((Rotate (a,r)),(Rotate (b,r))) consider i being Integer such that A3: Arg (Rotate (b,(- (Arg a)))) = ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) by A2, Th54; consider l being Integer such that A4: Arg (Rotate (b,r)) = ((2 * PI) * l) + (r + (Arg b)) by A2, Th54; consider k being Integer such that A5: Arg (Rotate (a,r)) = ((2 * PI) * k) + (r + (Arg a)) by A1, Th54; A6: ( 0 <= Arg (Rotate ((Rotate (b,r)),(- (Arg (Rotate (a,r)))))) & Arg (Rotate ((Rotate (b,r)),(- (Arg (Rotate (a,r)))))) < 2 * PI ) by COMPTRIG:34; A7: ( 0 <= Arg (Rotate (b,(- (Arg a)))) & Arg (Rotate (b,(- (Arg a)))) < 2 * PI ) by COMPTRIG:34; A8: Rotate (b,r) <> 0 by A2, Th52; then consider j being Integer such that A9: Arg (Rotate ((Rotate (b,r)),(- (Arg (Rotate (a,r)))))) = ((2 * PI) * j) + ((- (Arg (Rotate (a,r)))) + (Arg (Rotate (b,r)))) by Th54; A10: Arg (Rotate ((Rotate (b,r)),(- (Arg (Rotate (a,r)))))) = ((2 * PI) * (((j - k) + l) - i)) + (Arg (Rotate (b,(- (Arg a))))) by A3, A9, A5, A4; thus angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by A2, Def3 .= Arg (Rotate ((Rotate (b,r)),(- (Arg (Rotate (a,r)))))) by A10, A7, A6, Th2 .= angle ((Rotate (a,r)),(Rotate (b,r))) by A8, Def3 ; ::_thesis: verum end; theorem :: COMPLEX2:66 for a, b being Element of COMPLEX for r being Real st r < 0 & a <> 0 & b <> 0 holds angle (a,b) = angle ((a * r),(b * r)) proof let a, b be Element of COMPLEX ; ::_thesis: for r being Real st r < 0 & a <> 0 & b <> 0 holds angle (a,b) = angle ((a * r),(b * r)) let r be Real; ::_thesis: ( r < 0 & a <> 0 & b <> 0 implies angle (a,b) = angle ((a * r),(b * r)) ) assume that A1: r < 0 and A2: a <> 0 and A3: b <> 0 ; ::_thesis: angle (a,b) = angle ((a * r),(b * r)) consider i being Integer such that A4: Arg (Rotate ((- b),(- (Arg (- a))))) = ((2 * PI) * i) + ((- (Arg (- a))) + (Arg (- b))) by A3, Th54; set br = b * r; set ar = a * r; ( Arg (b * r) = Arg (- b) & Arg (a * r) = Arg (- a) ) by A1, Th28; then consider j being Integer such that A5: Arg (Rotate ((b * r),(- (Arg (a * r))))) = ((2 * PI) * j) + ((- (Arg (- a))) + (Arg (- b))) by A1, A3, Th54; A6: Arg (Rotate ((b * r),(- (Arg (a * r))))) = ((2 * PI) * (j - i)) + (Arg (Rotate ((- b),(- (Arg (- a)))))) by A4, A5; A7: ( 0 <= Arg (Rotate ((b * r),(- (Arg (a * r))))) & Arg (Rotate ((b * r),(- (Arg (a * r))))) < 2 * PI ) by COMPTRIG:34; A8: ( 0 <= Arg (Rotate ((- b),(- (Arg (- a))))) & Arg (Rotate ((- b),(- (Arg (- a))))) < 2 * PI ) by COMPTRIG:34; thus angle (a,b) = angle ((Rotate (a,PI)),(Rotate (b,PI))) by A2, A3, Th65 .= angle ((- a),(Rotate (b,PI))) by Th60 .= angle ((- a),(- b)) by Th60 .= Arg (Rotate ((- b),(- (Arg (- a))))) by A3, Def3 .= Arg (Rotate ((b * r),(- (Arg (a * r))))) by A6, A7, A8, Th2 .= angle ((a * r),(b * r)) by A1, A3, Def3 ; ::_thesis: verum end; theorem :: COMPLEX2:67 for a, b being Element of COMPLEX st a <> 0 & b <> 0 holds angle (a,b) = angle ((- a),(- b)) proof let a, b be Element of COMPLEX ; ::_thesis: ( a <> 0 & b <> 0 implies angle (a,b) = angle ((- a),(- b)) ) assume ( a <> 0 & b <> 0 ) ; ::_thesis: angle (a,b) = angle ((- a),(- b)) hence angle (a,b) = angle ((Rotate (a,PI)),(Rotate (b,PI))) by Th65 .= angle ((- a),(Rotate (b,PI))) by Th60 .= angle ((- a),(- b)) by Th60 ; ::_thesis: verum end; theorem :: COMPLEX2:68 for b, a being Element of COMPLEX st b <> 0 & angle (a,b) = 0 holds angle (a,(- b)) = PI proof let b, a be Element of COMPLEX ; ::_thesis: ( b <> 0 & angle (a,b) = 0 implies angle (a,(- b)) = PI ) assume that A1: b <> 0 and A2: angle (a,b) = 0 ; ::_thesis: angle (a,(- b)) = PI A3: Arg (Rotate (b,(- (Arg a)))) = 0 by A1, A2, Def3; A4: Arg (Rotate ((- b),(- (Arg a)))) = Arg (- (Rotate (b,(- (Arg a))))) by Th58; Rotate (b,(- (Arg a))) <> 0 by A1, Th52; then Arg (- (Rotate (b,(- (Arg a))))) = (Arg (Rotate (b,(- (Arg a))))) + PI by A3, Th13, COMPTRIG:5 .= PI by A3 ; hence angle (a,(- b)) = PI by A1, A4, Def3; ::_thesis: verum end; theorem Th69: :: COMPLEX2:69 for a, b being Element of 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.|)) ) proof let a, b be Element of COMPLEX ; ::_thesis: ( a <> 0 & b <> 0 implies ( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) ) ) assume that A1: a <> 0 and A2: b <> 0 ; ::_thesis: ( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) ) A3: ( |.a.| <> 0 & |.b.| <> 0 ) by A1, A2, COMPLEX1:45; set ra = Rotate (a,(- (Arg a))); set rb = Rotate (b,(- (Arg a))); set r = - (Arg a); set mabi = (|.a.| * |.b.|) " ; A4: ( |.a.| >= 0 & |.b.| >= 0 ) by COMPLEX1:46; angle (a,b) = angle ((Rotate (a,(- (Arg a)))),(Rotate (b,(- (Arg a))))) by A1, A2, Th65; then A5: angle (a,b) = angle ((|.a.| * ((|.a.| * |.b.|) ")),((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "))) by A3, A4, Th63, SIN_COS:31 .= Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) by A4, Th61 ; A6: a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * ) by Th12; then Re a = |.a.| * (cos (Arg a)) by COMPLEX1:12; then A7: cos (Arg a) = (Re a) / |.a.| by A1, COMPLEX1:45, XCMPLX_1:89; Im a = |.a.| * (sin (Arg a)) by A6, COMPLEX1:12; then A8: sin (Arg a) = (Im a) / |.a.| by A1, COMPLEX1:45, XCMPLX_1:89; A9: a .|. b = (((Re a) * (Re b)) + ((Im a) * (Im b))) + (((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * ) by Th29; then A10: Re (a .|. b) = ((Re a) * (Re b)) + ((Im a) * (Im b)) by COMPLEX1:12; Re (Rotate (b,(- (Arg a)))) = ((Re b) * (cos (- (Arg a)))) - ((Im b) * (sin (- (Arg a)))) by Th56; then A11: Re (Rotate (b,(- (Arg a)))) = ((Re b) * (cos (- (Arg a)))) - ((Im b) * (- (sin (Arg a)))) by SIN_COS:31 .= ((Re b) * ((Re a) / |.a.|)) + ((Im b) * ((Im a) / |.a.|)) by A7, A8, SIN_COS:31 .= (Re (a .|. b)) / |.a.| by A10 ; A12: (Im (Rotate (b,(- (Arg a))))) ^2 >= 0 by XREAL_1:63; Im (Rotate (b,(- (Arg a)))) = ((Re b) * (sin (- (Arg a)))) + ((Im b) * (cos (- (Arg a)))) by Th56; then A13: Im (Rotate (b,(- (Arg a)))) = ((Re b) * (- (sin (Arg a)))) + ((Im b) * (cos (- (Arg a)))) by SIN_COS:31 .= ((- (Re b)) * ((Im a) / |.a.|)) + ((Im b) * ((Re a) / |.a.|)) by A7, A8, SIN_COS:31 .= - ((- (((- (Re b)) * (Im a)) + ((Im b) * (Re a)))) / |.a.|) .= - ((Im (a .|. b)) / |.a.|) by A9, COMPLEX1:12 ; set IT = (Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "); set mab = |.a.| * |.b.|; A14: ( ((|.a.| * |.b.|) ") ^2 >= 0 & (Re (Rotate (b,(- (Arg a))))) ^2 >= 0 ) by XREAL_1:63; (|.a.| * |.b.|) " = ((|.a.| * |.b.|) ") + (0 * ) ; then A15: ( Re ((|.a.| * |.b.|) ") = (|.a.| * |.b.|) " & Im ((|.a.| * |.b.|) ") = 0 ) by COMPLEX1:12; then A16: Re ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) = ((Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) - ((Im (Rotate (b,(- (Arg a))))) * 0) by COMPLEX1:9 .= (Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ") ; A17: Im ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) = ((Re (Rotate (b,(- (Arg a))))) * 0) + ((Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) by A15, COMPLEX1:9 .= (Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ") ; then A18: |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| = sqrt ((((Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) ^2) + (((Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) ^2)) by A16, COMPLEX1:def_12 .= sqrt ((((|.a.| * |.b.|) ") ^2) * (((Re (Rotate (b,(- (Arg a))))) ^2) + ((Im (Rotate (b,(- (Arg a))))) ^2))) .= (sqrt (((|.a.| * |.b.|) ") ^2)) * (sqrt (((Re (Rotate (b,(- (Arg a))))) ^2) + ((Im (Rotate (b,(- (Arg a))))) ^2))) by A14, A12, SQUARE_1:29 .= ((|.a.| * |.b.|) ") * (sqrt (((Re (Rotate (b,(- (Arg a))))) ^2) + ((Im (Rotate (b,(- (Arg a))))) ^2))) by A4, SQUARE_1:22 .= ((|.a.| * |.b.|) ") * |.(Rotate (b,(- (Arg a)))).| by COMPLEX1:def_12 .= ((|.a.| * |.b.|) ") * |.b.| by Th53 ; A19: (Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ") = (|.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (cos (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "))))) + ((|.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "))))) * ) by Th12; then |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (cos (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")))) = (Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ") by A16, COMPLEX1:12; hence cos (angle (a,b)) = ((Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| by A3, A5, A18, XCMPLX_1:89 .= (Re (Rotate (b,(- (Arg a))))) * (((|.a.| * |.b.|) ") / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).|) .= ((Re (a .|. b)) / |.a.|) * ((((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.|) by A11, A18, XCMPLX_1:78 .= ((Re (a .|. b)) / |.a.|) * (1 / |.b.|) by A3, XCMPLX_1:60 .= ((Re (a .|. b)) * 1) / (|.a.| * |.b.|) by XCMPLX_1:76 .= (Re (a .|. b)) / (|.a.| * |.b.|) ; ::_thesis: sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")))) = (Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ") by A19, A17, COMPLEX1:12; hence sin (angle (a,b)) = ((Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| by A3, A5, A18, XCMPLX_1:89 .= (Im (Rotate (b,(- (Arg a))))) * (((|.a.| * |.b.|) ") / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).|) .= (- ((Im (a .|. b)) / |.a.|)) * ((((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.|) by A13, A18, XCMPLX_1:78 .= ((- (Im (a .|. b))) / |.a.|) * (1 / |.b.|) by A3, XCMPLX_1:60 .= ((- (Im (a .|. b))) * 1) / (|.a.| * |.b.|) by XCMPLX_1:76 .= - ((Im (a .|. b)) / (|.a.| * |.b.|)) ; ::_thesis: verum end; definition let x, y, z be complex number ; func angle (x,y,z) -> real number 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 coherence ( ( (Arg (z - y)) - (Arg (x - y)) >= 0 implies (Arg (z - y)) - (Arg (x - y)) is real number ) & ( not (Arg (z - y)) - (Arg (x - y)) >= 0 implies (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) is real number ) ); consistency for b1 being real number holds verum; ; end; :: deftheorem Def4 defines angle COMPLEX2:def_4_:_ for x, y, z being complex number 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 Th70: :: COMPLEX2:70 for x, y, z being Element of COMPLEX holds ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) proof let x, y, z be Element of COMPLEX ; ::_thesis: ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) now__::_thesis:_(_(_(Arg_(z_-_y))_-_(Arg_(x_-_y))_>=_0_&_0_<=_angle_(x,y,z)_&_angle_(x,y,z)_<_2_*_PI_)_or_(_(Arg_(z_-_y))_-_(Arg_(x_-_y))_<_0_&_0_<=_angle_(x,y,z)_&_angle_(x,y,z)_<_2_*_PI_)_) percases ( (Arg (z - y)) - (Arg (x - y)) >= 0 or (Arg (z - y)) - (Arg (x - y)) < 0 ) ; caseA1: (Arg (z - y)) - (Arg (x - y)) >= 0 ; ::_thesis: ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) Arg (x - y) >= 0 by COMPTRIG:34; then (Arg (z - y)) + 0 <= (Arg (z - y)) + (Arg (x - y)) by XREAL_1:7; then A2: ( Arg (z - y) < 2 * PI & (Arg (z - y)) - (Arg (x - y)) <= Arg (z - y) ) by COMPTRIG:34, XREAL_1:20; angle (x,y,z) = (Arg (z - y)) - (Arg (x - y)) by A1, Def4; hence ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) by A1, A2, XXREAL_0:2; ::_thesis: verum end; caseA3: (Arg (z - y)) - (Arg (x - y)) < 0 ; ::_thesis: ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) Arg (z - y) >= 0 by COMPTRIG:34; then (Arg (x - y)) + 0 <= (Arg (x - y)) + (Arg (z - y)) by XREAL_1:7; then ( Arg (x - y) < 2 * PI & (Arg (x - y)) - (Arg (z - y)) <= Arg (x - y) ) by COMPTRIG:34, XREAL_1:20; then (Arg (x - y)) - (Arg (z - y)) < 2 * PI by XXREAL_0:2; then A4: (2 * PI) - ((Arg (x - y)) - (Arg (z - y))) > 0 by XREAL_1:50; ((Arg (z - y)) - (Arg (x - y))) + (2 * PI) < 0 + (2 * PI) by A3, XREAL_1:8; hence ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) by A3, A4, Def4; ::_thesis: verum end; end; end; hence ( 0 <= angle (x,y,z) & angle (x,y,z) < 2 * PI ) ; ::_thesis: verum end; theorem Th71: :: COMPLEX2:71 for x, y, z being Element of COMPLEX holds angle (x,y,z) = angle ((x - y),0,(z - y)) proof let x, y, z be Element of COMPLEX ; ::_thesis: angle (x,y,z) = angle ((x - y),0,(z - y)) now__::_thesis:_(_(_(Arg_((z_-_y)_-_0c))_-_(Arg_((x_-_y)_-_0c))_>=_0_&_angle_((x_-_y),0c,(z_-_y))_=_angle_(x,y,z)_)_or_(_(Arg_((z_-_y)_-_0c))_-_(Arg_((x_-_y)_-_0c))_<_0_&_angle_((x_-_y),0c,(z_-_y))_=_angle_(x,y,z)_)_) percases ( (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) >= 0 or (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) < 0 ) ; caseA1: (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) >= 0 ; ::_thesis: angle ((x - y),0c,(z - y)) = angle (x,y,z) then angle ((x - y),0c,(z - y)) = (Arg (z - y)) - (Arg (x - y)) by Def4; hence angle ((x - y),0c,(z - y)) = angle (x,y,z) by A1, Def4; ::_thesis: verum end; caseA2: (Arg ((z - y) - 0c)) - (Arg ((x - y) - 0c)) < 0 ; ::_thesis: angle ((x - y),0c,(z - y)) = angle (x,y,z) then angle ((x - y),0c,(z - y)) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) by Def4; hence angle ((x - y),0c,(z - y)) = angle (x,y,z) by A2, Def4; ::_thesis: verum end; end; end; hence angle (x,y,z) = angle ((x - y),0,(z - y)) ; ::_thesis: verum end; theorem Th72: :: COMPLEX2:72 for a, b, c, d being Element of COMPLEX holds angle (a,b,c) = angle ((a + d),(b + d),(c + d)) proof let a, b, c, d be Element of COMPLEX ; ::_thesis: angle (a,b,c) = angle ((a + d),(b + d),(c + d)) thus angle (a,b,c) = angle ((a - b),0c,(c - b)) by Th71 .= angle (((a + d) - (b + d)),0c,((c + d) - (b + d))) .= angle ((a + d),(b + d),(c + d)) by Th71 ; ::_thesis: verum end; theorem Th73: :: COMPLEX2:73 for a, b being Element of COMPLEX holds angle (a,b) = angle (a,0,b) proof let a, b be Element of COMPLEX ; ::_thesis: angle (a,b) = angle (a,0,b) set ab2 = angle (a,b); A1: ( 0 <= Arg (Rotate (b,(- (Arg a)))) & Arg (Rotate (b,(- (Arg a)))) < 2 * PI ) by COMPTRIG:34; percases ( b <> 0 or b = 0 ) ; supposeA2: b <> 0 ; ::_thesis: angle (a,b) = angle (a,0,b) then A3: angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by Def3; thus angle (a,b) = angle (a,0,b) ::_thesis: verum proof percases ( (Arg (b - 0c)) - (Arg (a - 0c)) >= 0 or (Arg (b - 0c)) - (Arg (a - 0c)) < 0 ) ; suppose (Arg (b - 0c)) - (Arg (a - 0c)) >= 0 ; ::_thesis: angle (a,b) = angle (a,0,b) then A4: angle (a,0c,b) = (- (Arg a)) + (Arg b) by Def4; A5: angle (a,0c,b) < 2 * PI by Th70; ( ex i being Integer st Arg (Rotate (b,(- (Arg a)))) = ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) & 0 <= angle (a,0c,b) ) by A2, Th54, Th70; hence angle (a,b) = angle (a,0,b) by A1, A3, A4, A5, Th2; ::_thesis: verum end; supposeA6: (Arg (b - 0c)) - (Arg (a - 0c)) < 0 ; ::_thesis: angle (a,b) = angle (a,0,b) consider i being Integer such that A7: Arg (Rotate (b,(- (Arg a)))) = ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) by A2, Th54; A8: ((2 * PI) * i) + ((- (Arg a)) + (Arg b)) = ((2 * PI) * (i - 1)) + ((2 * PI) + ((- (Arg a)) + (Arg b))) ; A9: angle (a,0c,b) = (2 * PI) + ((Arg b) + (- (Arg a))) by A6, Def4; then ( 0 <= (2 * PI) + ((- (Arg a)) + (Arg b)) & (2 * PI) + ((- (Arg a)) + (Arg b)) < 2 * PI ) by Th70; hence angle (a,b) = angle (a,0,b) by A1, A3, A9, A7, A8, Th2; ::_thesis: verum end; end; end; end; supposeA10: b = 0 ; ::_thesis: angle (a,b) = angle (a,0,b) thus angle (a,b) = angle (a,0,b) ::_thesis: verum proof percases ( Arg a = 0 or Arg a <> 0 ) ; supposeA11: Arg a = 0 ; ::_thesis: angle (a,b) = angle (a,0,b) then A12: (Arg (b - 0c)) - (Arg (a - 0c)) = 0 by A10, COMPTRIG:35; angle (a,b) = Arg (Rotate (b,(- (Arg a)))) by A11, Def3 .= 0 by A10, Lm1, Th52 ; hence angle (a,b) = angle (a,0,b) by A12, Def4; ::_thesis: verum end; supposeA13: Arg a <> 0 ; ::_thesis: angle (a,b) = angle (a,0,b) then A14: 0 < - (- (Arg a)) by COMPTRIG:34; (Arg (b - 0c)) - (Arg (a - 0c)) = - (Arg a) by A10, Lm1; then angle (a,0c,b) = (2 * PI) - (Arg a) by A14, Def4; hence angle (a,b) = angle (a,0,b) by A10, A13, Def3; ::_thesis: verum end; end; end; end; end; end; theorem Th74: :: COMPLEX2:74 for x, y, z being Element of COMPLEX st angle (x,y,z) = 0 holds ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) proof let x, y, z be Element of COMPLEX ; ::_thesis: ( angle (x,y,z) = 0 implies ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) ) assume A1: angle (x,y,z) = 0 ; ::_thesis: ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) now__::_thesis:_(_(_(Arg_(z_-_y))_-_(Arg_(x_-_y))_>=_0_&_Arg_(x_-_y)_=_Arg_(z_-_y)_&_angle_(z,y,x)_=_0_)_or_(_(Arg_(z_-_y))_-_(Arg_(x_-_y))_<_0_&_contradiction_)_) percases ( (Arg (z - y)) - (Arg (x - y)) >= 0 or (Arg (z - y)) - (Arg (x - y)) < 0 ) ; case (Arg (z - y)) - (Arg (x - y)) >= 0 ; ::_thesis: ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) then (Arg (z - y)) - (Arg (x - y)) = 0 by A1, Def4; hence ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) by Def4; ::_thesis: verum end; caseA2: (Arg (z - y)) - (Arg (x - y)) < 0 ; ::_thesis: contradiction then - ((Arg (z - y)) - (Arg (x - y))) > 0 ; then A3: angle (z,y,x) = (Arg (x - y)) - (Arg (z - y)) by Def4; angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) by A2, Def4; hence contradiction by A1, A3, Th70; ::_thesis: verum end; end; end; hence ( Arg (x - y) = Arg (z - y) & angle (z,y,x) = 0 ) ; ::_thesis: verum end; theorem Th75: :: COMPLEX2:75 for a, b being Element of 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 ) ) proof let a, b be Element of COMPLEX ; ::_thesis: ( a <> 0 & b <> 0 implies ( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) ) ) A1: - ((Im (a .|. b)) / (|.a.| * |.b.|)) = (- (Im (a .|. b))) / (|.a.| * |.b.|) ; assume A2: ( a <> 0 & b <> 0 ) ; ::_thesis: ( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) ) then A3: ( |.a.| <> 0 & |.b.| <> 0 ) by COMPLEX1:45; A4: ( angle (a,b) = angle (a,0c,b) & 0 <= angle (a,0c,b) ) by Th70, Th73; A5: ( angle (a,0c,b) < 2 * PI & PI / 2 < 2 * PI ) by Th70, COMPTRIG:5, XXREAL_0:2; A6: cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) by A2, Th69; A7: sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) by A2, Th69; hereby ::_thesis: ( ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) implies Re (a .|. b) = 0 ) assume A8: Re (a .|. b) = 0 ; ::_thesis: ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) then ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) by Th50; then ( sin (angle (a,b)) = 1 or sin (angle (a,b)) = - 1 ) by A7, A3, A1, XCMPLX_1:60; hence ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) by A6, A4, A5, A8, Th11, COMPTRIG:5, SIN_COS:77; ::_thesis: verum end; assume ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) ; ::_thesis: Re (a .|. b) = 0 hence Re (a .|. b) = 0 by A6, A3, Th73, SIN_COS:77; ::_thesis: verum end; theorem :: COMPLEX2:76 for a, b being Element of 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.|) ) ) proof let a, b be Element of COMPLEX ; ::_thesis: ( a <> 0 & b <> 0 implies ( ( ( 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.|) ) ) ) assume A1: ( a <> 0 & b <> 0 ) ; ::_thesis: ( ( ( 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.|) ) ) hereby ::_thesis: ( ( 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.|) ) assume ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) ; ::_thesis: ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) then Re (a .|. b) = 0 by Th50; hence ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) by A1, Th75; ::_thesis: verum end; hereby ::_thesis: verum assume ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) ; ::_thesis: ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) then Re (a .|. b) = 0 by A1, Th75; hence ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) by Th50; ::_thesis: verum end; end; Lm3: for a, b, c being Element of 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 let x, y, z be Element of COMPLEX ; ::_thesis: ( x <> y & z <> y implies ( Re ((x - y) .|. (z - y)) = 0 iff ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) ) ) assume ( x <> y & z <> y ) ; ::_thesis: ( Re ((x - y) .|. (z - y)) = 0 iff ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) ) then A1: ( x - y <> 0c & z - y <> 0c ) ; angle (x,y,z) = angle ((x - y),0c,(z - y)) by Th71; hence ( Re ((x - y) .|. (z - y)) = 0 iff ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) ) by A1, Th75; ::_thesis: verum end; theorem :: COMPLEX2:77 for x, y, z being Element of 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 proof let x, y, z be Element of COMPLEX ; ::_thesis: ( x <> y & z <> y & ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) implies (|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2 ) assume A1: ( x <> y & z <> y & ( angle (x,y,z) = PI / 2 or angle (x,y,z) = (3 / 2) * PI ) ) ; ::_thesis: (|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2 set x3 = x - z; A2: (|.(x - y).| ^2) + (|.(z - y).| ^2) = (Re ((x - y) .|. (x - y))) + (|.(z - y).| ^2) by Th31 .= (Re ((x - y) .|. (x - y))) + (Re ((z - y) .|. (z - y))) by Th31 .= Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) by COMPLEX1:8 ; x - z = (x - y) - (z - y) ; then (x - z) .|. (x - z) = ((((x - y) .|. (x - y)) - ((x - y) .|. (z - y))) - ((z - y) .|. (x - y))) + ((z - y) .|. (z - y)) by Th49; then Re ((x - z) .|. (x - z)) = Re ((((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) - (((x - y) .|. (z - y)) + ((z - y) .|. (x - y)))) .= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (Re (((x - y) .|. (z - y)) + ((z - y) .|. (x - y)))) by COMPLEX1:19 .= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re ((z - y) .|. (x - y)))) by COMPLEX1:8 .= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re (((x - y) .|. (z - y)) *'))) by Th34 .= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - ((Re ((x - y) .|. (z - y))) + (Re ((x - y) .|. (z - y)))) by COMPLEX1:27 .= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - (0 + (Re ((x - y) .|. (z - y)))) by A1, Lm3 .= (Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y)))) - 0 by A1, Lm3 .= Re (((x - y) .|. (x - y)) + ((z - y) .|. (z - y))) ; hence (|.(x - y).| ^2) + (|.(z - y).| ^2) = |.(x - z).| ^2 by A2, Th31; ::_thesis: verum end; theorem Th78: :: COMPLEX2:78 for a, b, c being Element of 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))) proof let a, b, c be Element of COMPLEX ; ::_thesis: for r being Real st a <> b & b <> c holds angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) let r be Real; ::_thesis: ( a <> b & b <> c implies angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) ) set cb = c - b; set ab = a - b; set rc = Rotate (c,r); set rb = Rotate (b,r); set ra = Rotate (a,r); set rcb = (Rotate (c,r)) - (Rotate (b,r)); set rab = (Rotate (a,r)) - (Rotate (b,r)); assume that A1: a <> b and A2: b <> c ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) A3: ( 0 <= angle (a,b,c) & angle (a,b,c) < 2 * PI ) by Th70; c - b <> 0 by A2; then consider cbi being Integer such that A4: Arg (Rotate ((c - b),r)) = ((2 * PI) * cbi) + (r + (Arg (c - b))) by Th54; a - b <> 0 by A1; then consider abi being Integer such that A5: Arg (Rotate ((a - b),r)) = ((2 * PI) * abi) + (r + (Arg (a - b))) by Th54; A6: ( 0 <= angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) & angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) < 2 * PI ) by Th70; (Rotate (a,r)) - (Rotate (b,r)) = Rotate ((a - b),r) by Th59; then A7: (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) = ((((2 * PI) * cbi) + r) + (Arg (c - b))) - ((((2 * PI) * abi) + r) + (Arg (a - b))) by A5, A4, Th59 .= ((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi)) ; percases ( (Arg (c - b)) - (Arg (a - b)) >= 0 or (Arg (c - b)) - (Arg (a - b)) < 0 ) ; suppose (Arg (c - b)) - (Arg (a - b)) >= 0 ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) then A8: angle (a,b,c) = (Arg (c - b)) - (Arg (a - b)) by Def4; thus angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) ::_thesis: verum proof percases ( (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 or (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ) ; suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) by Def4; hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A7, A8, Th2; ::_thesis: verum end; suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = (((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))) + (2 * PI) by A7, Def4 .= ((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * ((cbi - abi) + 1)) ; hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A8, Th2; ::_thesis: verum end; end; end; end; suppose (Arg (c - b)) - (Arg (a - b)) < 0 ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) then A9: angle (a,b,c) = (2 * PI) + ((Arg (c - b)) - (Arg (a - b))) by Def4; thus angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) ::_thesis: verum proof percases ( (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 or (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ) ; suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) >= 0 ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = ((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * ((cbi - abi) + (- 1))) by A7, Def4; hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A9, Th2; ::_thesis: verum end; suppose (Arg ((Rotate (c,r)) - (Rotate (b,r)))) - (Arg ((Rotate (a,r)) - (Rotate (b,r)))) < 0 ; ::_thesis: angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) then angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) = (((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (cbi - abi))) + (2 * PI) by A7, Def4 .= ((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * (cbi - abi)) ; hence angle (a,b,c) = angle ((Rotate (a,r)),(Rotate (b,r)),(Rotate (c,r))) by A3, A6, A9, Th2; ::_thesis: verum end; end; end; end; end; end; theorem Th79: :: COMPLEX2:79 for a, b being Element of COMPLEX holds angle (a,b,a) = 0 proof let a, b be Element of COMPLEX ; ::_thesis: angle (a,b,a) = 0 (Arg (a - b)) - (Arg (a - b)) = 0 ; hence angle (a,b,a) = 0 by Def4; ::_thesis: verum end; Lm4: for x, y, z being Element of COMPLEX st angle (x,y,z) <> 0 holds angle (z,y,x) = (2 * PI) - (angle (x,y,z)) proof let x, y, z be Element of COMPLEX ; ::_thesis: ( angle (x,y,z) <> 0 implies angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ) assume A1: angle (x,y,z) <> 0 ; ::_thesis: angle (z,y,x) = (2 * PI) - (angle (x,y,z)) now__::_thesis:_(_(_(Arg_(x_-_y))_-_(Arg_(z_-_y))_>_0_&_angle_(z,y,x)_=_(2_*_PI)_-_(angle_(x,y,z))_)_or_(_(Arg_(x_-_y))_-_(Arg_(z_-_y))_<=_0_&_angle_(z,y,x)_=_(2_*_PI)_-_(angle_(x,y,z))_)_) percases ( (Arg (x - y)) - (Arg (z - y)) > 0 or (Arg (x - y)) - (Arg (z - y)) <= 0 ) ; caseA2: (Arg (x - y)) - (Arg (z - y)) > 0 ; ::_thesis: angle (z,y,x) = (2 * PI) - (angle (x,y,z)) then - (- ((Arg (x - y)) - (Arg (z - y)))) > 0 ; then angle (x,y,z) = (2 * PI) + ((Arg (z - y)) - (Arg (x - y))) by Def4 .= (2 * PI) - ((Arg (x - y)) - (Arg (z - y))) ; hence angle (z,y,x) = (2 * PI) - (angle (x,y,z)) by A2, Def4; ::_thesis: verum end; caseA3: (Arg (x - y)) - (Arg (z - y)) <= 0 ; ::_thesis: angle (z,y,x) = (2 * PI) - (angle (x,y,z)) (Arg (x - y)) - (Arg (z - y)) <> 0 by A1, Def4; then A4: angle (z,y,x) = (2 * PI) - ((Arg (z - y)) - (Arg (x - y))) by A3, Def4; - (- ((Arg (x - y)) - (Arg (z - y)))) <= 0 by A3; then (angle (x,y,z)) + (angle (z,y,x)) = ((2 * PI) - ((Arg (z - y)) - (Arg (x - y)))) + ((Arg (z - y)) - (Arg (x - y))) by A4, Def4 .= 2 * PI ; hence angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ; ::_thesis: verum end; end; end; hence angle (z,y,x) = (2 * PI) - (angle (x,y,z)) ; ::_thesis: verum end; theorem Th80: :: COMPLEX2:80 for a, b, c being Element of COMPLEX holds ( angle (a,b,c) <> 0 iff (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI ) proof let a, b, c be Element of COMPLEX ; ::_thesis: ( angle (a,b,c) <> 0 iff (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI ) hereby ::_thesis: ( (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI implies angle (a,b,c) <> 0 ) assume angle (a,b,c) <> 0 ; ::_thesis: (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI then angle (c,b,a) = (2 * PI) - (angle (a,b,c)) by Lm4; hence (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI ; ::_thesis: verum end; assume ( (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI & angle (a,b,c) = 0 ) ; ::_thesis: contradiction hence contradiction by Th70; ::_thesis: verum end; theorem :: COMPLEX2:81 for a, b, c being Element of COMPLEX st angle (a,b,c) <> 0 holds angle (c,b,a) <> 0 proof let a, b, c be Element of COMPLEX ; ::_thesis: ( angle (a,b,c) <> 0 implies angle (c,b,a) <> 0 ) assume angle (a,b,c) <> 0 ; ::_thesis: angle (c,b,a) <> 0 then A1: (angle (a,b,c)) + (angle (c,b,a)) = 2 * PI by Th80; assume not angle (c,b,a) <> 0 ; ::_thesis: contradiction hence contradiction by A1, Th70; ::_thesis: verum end; theorem :: COMPLEX2:82 for a, b, c being Element of COMPLEX st angle (a,b,c) = PI holds angle (c,b,a) = PI proof let a, b, c be Element of COMPLEX ; ::_thesis: ( angle (a,b,c) = PI implies angle (c,b,a) = PI ) assume A1: angle (a,b,c) = PI ; ::_thesis: angle (c,b,a) = PI then (angle (a,b,c)) + (angle (c,b,a)) = 0 + (2 * PI) by Th80, COMPTRIG:5; hence angle (c,b,a) = PI by A1; ::_thesis: verum end; theorem Th83: :: COMPLEX2:83 for a, b, c being Element of 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 proof let a, b, c be Element of COMPLEX ; ::_thesis: ( a <> b & a <> c & b <> c & not angle (a,b,c) <> 0 & not angle (b,c,a) <> 0 implies angle (c,a,b) <> 0 ) assume that A1: ( a <> b & a <> c ) and A2: b <> c ; ::_thesis: ( angle (a,b,c) <> 0 or angle (b,c,a) <> 0 or angle (c,a,b) <> 0 ) A3: ( b - a <> 0 & a - c <> 0 ) by A1; c - b <> 0 by A2; then A4: ( Arg (c - b) < PI iff Arg (- (c - b)) >= PI ) by Th16; A5: ( - (b - a) = a - b & - (a - c) = c - a ) ; A6: - (c - a) = a - c ; assume A7: ( not angle (a,b,c) <> 0 & not angle (b,c,a) <> 0 & not angle (c,a,b) <> 0 ) ; ::_thesis: contradiction then A8: Arg (a - c) = Arg (b - c) by Th74; Arg (b - a) = Arg (c - a) by A7, Th74; then Arg (a - b) = Arg (a - c) by A3, A5, A6, Th64; hence contradiction by A7, A8, A4, Th74; ::_thesis: verum end; Lm5: for a, b being Element of 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 let a, b be Element of COMPLEX ; ::_thesis: ( Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI implies ( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI & 0 < angle (0c,b,a) & 0 < angle (b,a,0c) ) ) assume that A1: Im a = 0 and A2: Re a > 0 and A3: 0 < Arg b and A4: Arg b < PI ; ::_thesis: ( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI & 0 < angle (0c,b,a) & 0 < angle (b,a,0c) ) a = (Re a) + (0 * ) by A1, COMPLEX1:13; then A5: Arg a = 0 by A2, COMPTRIG:35; then A6: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI) by A2, Th13, COMPLEX1:4, COMPTRIG:5 .= - PI ; (Arg (b - 0c)) - (Arg (a - 0c)) >= 0 by A3, A5; then A7: angle (a,0c,b) = (Arg b) - (Arg a) by Def4; Arg b in ].0,PI.[ by A3, A4, XXREAL_1:4; then A8: Im b > 0 by Th18; then A9: (Arg b) - (Arg (- b)) = (Arg b) - ((Arg b) + PI) by A4, Th13, COMPLEX1:4 .= - PI ; A10: Im (a - b) = (Im a) - (Im b) by COMPLEX1:19 .= - (Im b) by A1 ; then A11: Arg (a - b) > PI by A8, Th24; then Arg (b - a) <= PI by A8, A10, Th17, COMPLEX1:4; then A12: - (Arg (b - a)) >= - PI by XREAL_1:24; A13: (Arg (a - b)) - (Arg (b - a)) = (Arg (a - b)) - (Arg (- (a - b))) .= (Arg (a - b)) - ((Arg (a - b)) - PI) by A8, A10, A11, Th13, COMPLEX1:4 .= PI ; Arg (- a) = (Arg a) + PI by A2, A5, Th13, COMPLEX1:4, COMPTRIG:5 .= PI by A5 ; then (Arg (- a)) + (- (Arg (b - a))) >= (0 - PI) + PI by A12, XREAL_1:7; then A14: angle (b,a,0c) = (Arg (0c - a)) - (Arg (b - a)) by Def4; now__::_thesis:_for_a,_b_being_Element_of_COMPLEX_st_Im_a_=_0_&_Re_a_>_0_&_0_<_Arg_b_&_Arg_b_<_PI_holds_ (Arg_(b_-_a))_-_(Arg_b)_>_0 let a, b be Element of COMPLEX ; ::_thesis: ( Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI implies (Arg (b2 - b1)) - (Arg b2) > 0 ) assume that A15: Im a = 0 and A16: Re a > 0 and A17: ( 0 < Arg b & Arg b < PI ) ; ::_thesis: (Arg (b2 - b1)) - (Arg b2) > 0 A18: (Re b) + (- (Re a)) < (Re b) + 0 by A16, XREAL_1:8; set ba = b - a; set B = Arg b; set BA = Arg (b - a); set mb = |.b.|; set mba = |.(b - a).|; A19: Re (b - a) = (Re b) - (Re a) by COMPLEX1:19; ( b - a = (|.(b - a).| * (cos (Arg (b - a)))) + ((|.(b - a).| * (sin (Arg (b - a)))) * ) & b - a = (Re (b - a)) + ((Im (b - a)) * ) ) by Th12, COMPLEX1:13; then A20: Im (b - a) = |.(b - a).| * (sin (Arg (b - a))) by COMPLEX1:77; set Rb = Re b; set Rba = Re (b - a); set Ib = Im b; set Iba = Im (b - a); A21: Im (b - a) = (Im b) - (Im a) by COMPLEX1:19 .= Im b by A15 ; then A22: ( |.b.| = sqrt (((Re b) ^2) + ((Im b) ^2)) & |.(b - a).| = sqrt (((Re (b - a)) ^2) + ((Im b) ^2)) ) by COMPLEX1:def_12; A23: ( (Re b) ^2 >= 0 & (Im b) ^2 >= 0 ) by XREAL_1:63; A24: ( (Re (b - a)) ^2 >= 0 & (Im b) ^2 >= 0 ) by XREAL_1:63; Arg b in ].0,PI.[ by A17, XXREAL_1:4; then A25: Im b > 0 by Th18; then A26: |.b.| >= 0 by COMPLEX1:4, COMPLEX1:47; A27: |.(b - a).| >= 0 by A25, A21, COMPLEX1:4, COMPLEX1:47; A28: sin (Arg (b - a)) > 0 by A25, A21, COMPTRIG:45; A29: |.b.| <> 0 by A25, COMPLEX1:4, COMPLEX1:47; ( b = (|.b.| * (cos (Arg b))) + ((|.b.| * (sin (Arg b))) * ) & b = (Re b) + ((Im b) * ) ) by Th12, COMPLEX1:13; then Im b = |.b.| * (sin (Arg b)) by COMPLEX1:77; then A30: |.(b - a).| / |.b.| = (sin (Arg b)) / (sin (Arg (b - a))) by A21, A20, A29, A28, XCMPLX_1:94; percases ( 0 < Re (b - a) or 0 = Re (b - a) or 0 > Re (b - a) ) ; supposeA31: 0 < Re (b - a) ; ::_thesis: (Arg (b2 - b1)) - (Arg b2) > 0 then (Re b) ^2 > (Re (b - a)) ^2 by A19, A18, SQUARE_1:16; then ((Re b) ^2) + ((Im b) ^2) > ((Re (b - a)) ^2) + ((Im b) ^2) by XREAL_1:8; then |.b.| > |.(b - a).| by A22, A24, SQUARE_1:27; then |.(b - a).| / |.b.| < 1 by A27, XREAL_1:189; then ((sin (Arg b)) / (sin (Arg (b - a)))) * (sin (Arg (b - a))) < 1 * (sin (Arg (b - a))) by A28, A30, XREAL_1:68; then A32: sin (Arg b) < 1 * (sin (Arg (b - a))) by A28, XCMPLX_1:87; ( Arg b in ].0,(PI / 2).[ & Arg (b - a) in ].0,(PI / 2).[ ) by A25, A21, A19, A18, A31, COMPTRIG:41; then Arg (b - a) > Arg b by A32, Th6; then (Arg (b - a)) + (- (Arg b)) > (Arg b) + (- (Arg b)) by XREAL_1:8; hence (Arg (b - a)) - (Arg b) > 0 ; ::_thesis: verum end; supposeA33: 0 = Re (b - a) ; ::_thesis: (Arg (b2 - b1)) - (Arg b2) > 0 then b - a = 0 + ((Im (b - a)) * ) by COMPLEX1:13; then A34: Arg (b - a) = PI / 2 by A25, A21, COMPTRIG:37; Arg b in ].0,(PI / 2).[ by A16, A25, A19, A33, COMPTRIG:41; then Arg b < Arg (b - a) by A34, XXREAL_1:4; then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:8; hence (Arg (b - a)) - (Arg b) > 0 ; ::_thesis: verum end; supposeA35: 0 > Re (b - a) ; ::_thesis: (Arg (b2 - b1)) - (Arg b2) > 0 thus (Arg (b - a)) - (Arg b) > 0 ::_thesis: verum proof percases ( 0 < Re b or 0 = Re b or 0 > Re b ) ; suppose 0 < Re b ; ::_thesis: (Arg (b - a)) - (Arg b) > 0 then Arg b in ].0,(PI / 2).[ by A25, COMPTRIG:41; then A36: Arg b < PI / 2 by XXREAL_1:4; Arg (b - a) in ].(PI / 2),PI.[ by A25, A21, A35, COMPTRIG:42; then Arg (b - a) > PI / 2 by XXREAL_1:4; then Arg (b - a) > Arg b by A36, XXREAL_0:2; then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:8; hence (Arg (b - a)) - (Arg b) > 0 ; ::_thesis: verum end; suppose 0 = Re b ; ::_thesis: (Arg (b - a)) - (Arg b) > 0 then b = 0 + ((Im b) * ) by COMPLEX1:13; then A37: Arg b = PI / 2 by A25, COMPTRIG:37; Arg (b - a) in ].(PI / 2),PI.[ by A25, A21, A35, COMPTRIG:42; then Arg b < Arg (b - a) by A37, XXREAL_1:4; then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:8; hence (Arg (b - a)) - (Arg b) > 0 ; ::_thesis: verum end; supposeA38: 0 > Re b ; ::_thesis: (Arg (b - a)) - (Arg b) > 0 then (Re b) ^2 < (Re (b - a)) ^2 by A19, A18, SQUARE_1:44; then ((Re b) ^2) + ((Im b) ^2) < ((Re (b - a)) ^2) + ((Im b) ^2) by XREAL_1:8; then |.b.| < |.(b - a).| by A22, A23, SQUARE_1:27; then |.(b - a).| / |.b.| > 1 by A26, A29, XREAL_1:187; then ((sin (Arg b)) / (sin (Arg (b - a)))) * (sin (Arg (b - a))) > 1 * (sin (Arg (b - a))) by A28, A30, XREAL_1:68; then A39: sin (Arg b) > 1 * (sin (Arg (b - a))) by A28, XCMPLX_1:87; A40: Arg b in ].(PI / 2),PI.[ by A25, A38, COMPTRIG:42; Arg (b - a) in ].(PI / 2),PI.[ by A25, A21, A35, COMPTRIG:42; then Arg (b - a) > Arg b by A40, A39, Th7; then (Arg (b - a)) + (- (Arg b)) > (Arg b) + (- (Arg b)) by XREAL_1:8; hence (Arg (b - a)) - (Arg b) > 0 ; ::_thesis: verum end; end; end; end; end; end; then (Arg (b - a)) - (Arg b) > 0 by A1, A2, A3, A4; then (Arg (- (a - b))) - (Arg b) > 0 ; then ((Arg (a - b)) - PI) - (Arg b) > 0 by A8, A10, A11, Th13, COMPLEX1:4; then A41: (Arg (a - b)) - ((Arg b) + PI) > 0 ; then (Arg (a - b)) - (Arg (- b)) > 0 by A4, A8, Th13, COMPLEX1:4; then angle (0c,b,a) = (Arg (a - b)) - (Arg (0c - b)) by Def4; hence ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = ((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a))) by A7, A14 .= PI by A9, A6, A13 ; ::_thesis: ( 0 < angle (0c,b,a) & 0 < angle (b,a,0c) ) (Arg (a - b)) - (Arg (0c - b)) > 0 by A4, A8, A41, Th13, COMPLEX1:4; hence 0 < angle (0c,b,a) by Def4; ::_thesis: 0 < angle (b,a,0c) A42: Arg a >= 0 by COMPTRIG:34; 2 * PI > 0 + (Arg (a - b)) by COMPTRIG:34; then A43: (2 * PI) - (Arg (a - b)) > 0 by XREAL_1:20; (Arg (- a)) - ((Arg (a - b)) - PI) = (Arg a) + ((2 * PI) - (Arg (a - b))) by A6; hence 0 < angle (b,a,0c) by A14, A13, A43, A42; ::_thesis: verum end; theorem Th84: :: COMPLEX2:84 for a, b, c being Element of 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) ) proof let a, b, c be Element of COMPLEX ; ::_thesis: ( a <> b & b <> c & 0 < angle (a,b,c) & angle (a,b,c) < PI implies ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI & 0 < angle (b,c,a) & 0 < angle (c,a,b) ) ) assume that A1: a <> b and A2: b <> c and A3: 0 < angle (a,b,c) and A4: angle (a,b,c) < PI ; ::_thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI & 0 < angle (b,c,a) & 0 < angle (c,a,b) ) A5: c - b <> 0 by A2; set r = - (Arg (a + (- b))); set A = Rotate ((a + (- b)),(- (Arg (a + (- b))))); set B = Rotate ((c + (- b)),(- (Arg (a + (- b))))); A6: Rotate (0c,(- (Arg (a + (- b))))) = 0c by Th52; A7: c + (- b) <> a + (- b) by A3, Th79; A8: angle (b,c,a) = angle ((b + (- b)),(c + (- b)),(a + (- b))) by Th72 .= angle (0c,(Rotate ((c + (- b)),(- (Arg (a + (- b)))))),(Rotate ((a + (- b)),(- (Arg (a + (- b))))))) by A6, A7, A5, Th78 ; A9: angle ((a + (- b)),0c,(c + (- b))) = angle ((a + (- b)),(b + (- b)),(c + (- b))) .= angle (a,b,c) by Th72 ; A10: a - b <> 0 by A1; then A11: angle ((a + (- b)),0c,(c + (- b))) = angle ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c,(Rotate ((c + (- b)),(- (Arg (a + (- b))))))) by A6, A5, Th78; a + (- b) <> 0c by A1; then |.(a + (- b)).| > 0 by COMPLEX1:47; then A12: ( Im (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0 & Re (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) > 0 ) by COMPLEX1:12, SIN_COS:31; then A13: Arg (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0c by Th21; then (Arg ((Rotate ((c + (- b)),(- (Arg (a + (- b)))))) - 0c)) - (Arg ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))) - 0c)) >= 0 by COMPTRIG:34; then A14: angle (a,b,c) = Arg (Rotate ((c + (- b)),(- (Arg (a + (- b)))))) by A9, A11, A13, Def4; A15: angle (c,a,b) = angle ((c + (- b)),(a + (- b)),(b + (- b))) by Th72 .= angle ((Rotate ((c + (- b)),(- (Arg (a + (- b)))))),(Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c) by A6, A10, A7, Th78 ; hence ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI by A3, A4, A9, A11, A12, A14, A8, Lm5; ::_thesis: ( 0 < angle (b,c,a) & 0 < angle (c,a,b) ) thus 0 < angle (b,c,a) by A3, A4, A12, A14, A8, Lm5; ::_thesis: 0 < angle (c,a,b) thus 0 < angle (c,a,b) by A3, A4, A12, A14, A15, Lm5; ::_thesis: verum end; theorem Th85: :: COMPLEX2:85 for a, b, c being Element of 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 ) proof let a, b, c be Element of COMPLEX ; ::_thesis: ( a <> b & b <> c & angle (a,b,c) > PI implies ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI ) ) assume that A1: ( a <> b & b <> c ) and A2: angle (a,b,c) > PI ; ::_thesis: ( ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI & angle (b,c,a) > PI & angle (c,a,b) > PI ) A3: angle (c,b,a) < PI proof assume not angle (c,b,a) < PI ; ::_thesis: contradiction then (angle (a,b,c)) + (angle (c,b,a)) > PI + PI by A2, XREAL_1:8; hence contradiction by A2, Th80, COMPTRIG:5; ::_thesis: verum end; A4: (angle (a,b,c)) + (angle (c,b,a)) = (2 * PI) + 0 by A2, Th80, COMPTRIG:5; then A5: angle (c,b,a) <> 0 by Th70; A6: 0 <= angle (c,b,a) by Th70; then angle (b,a,c) > 0 by A1, A5, A3, Th84; then A7: (angle (c,a,b)) + (angle (b,a,c)) = (2 * PI) + 0 by Th80; angle (a,c,b) > 0 by A1, A6, A5, A3, Th84; then (angle (b,c,a)) + (angle (a,c,b)) = (2 * PI) + 0 by Th80; then ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = (((2 * PI) + (2 * PI)) + (2 * PI)) - (((angle (c,b,a)) + (angle (b,a,c))) + (angle (a,c,b))) by A4, A7; hence A8: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = ((((2 * PI) + (2 * PI)) + PI) + PI) - PI by A1, A6, A5, A3, Th84 .= 5 * PI ; ::_thesis: ( angle (b,c,a) > PI & angle (c,a,b) > PI ) A9: angle (a,b,c) < 2 * PI by Th70; angle (b,c,a) < 2 * PI by Th70; then A10: ( ((2 * PI) + (2 * PI)) + PI = 5 * PI & (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + (2 * PI) ) by A9, XREAL_1:8; A11: ((2 * PI) + PI) + (2 * PI) = 5 * PI ; hereby ::_thesis: angle (c,a,b) > PI assume angle (b,c,a) <= PI ; ::_thesis: contradiction then A12: (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + PI by A9, XREAL_1:8; angle (c,a,b) < 2 * PI by Th70; hence contradiction by A8, A11, A12, XREAL_1:8; ::_thesis: verum end; assume angle (c,a,b) <= PI ; ::_thesis: contradiction hence contradiction by A8, A10, XREAL_1:8; ::_thesis: verum end; Lm6: for a, b being Element of 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 let a, b be Element of COMPLEX ; ::_thesis: ( Im a = 0 & Re a > 0 & Arg b = PI implies ( ((angle (a,0,b)) + (angle (0,b,a))) + (angle (b,a,0)) = PI & 0 = angle (0,b,a) & 0 = angle (b,a,0) ) ) assume that A1: Im a = 0 and A2: Re a > 0 and A3: Arg b = PI ; ::_thesis: ( ((angle (a,0,b)) + (angle (0,b,a))) + (angle (b,a,0)) = PI & 0 = angle (0,b,a) & 0 = angle (b,a,0) ) A4: Im (a - b) = (Im a) - (Im b) by COMPLEX1:19 .= - (Im b) by A1 ; A5: (Re b) + 0 < Re a by A2, A3, Th22; then (Re a) - (Re b) > 0 by XREAL_1:20; then A6: Re (a - b) > 0 by COMPLEX1:19; a = (Re a) + (0 * ) by A1, COMPLEX1:13; then A7: Arg a = 0 by A2, COMPTRIG:35; then A8: (Arg (b - 0c)) - (Arg (a - 0c)) > 0 by A3, COMPTRIG:5; - (- ((Re a) - (Re b))) > 0 by A5, XREAL_1:20; then (Re b) - (Re a) < 0 ; then A9: Re (b - a) < 0 by COMPLEX1:19; A10: Im (b - a) = (Im b) - (Im a) by COMPLEX1:19 .= 0 by A1, A3, Th22 ; then A11: - (Arg (b - a)) = - PI by A9, Th22; A12: Arg (b - a) = PI by A9, A10, Th22; A13: Arg (- b) = (Arg b) - PI by A3, Lm1, Th13, COMPTRIG:5; A14: Im b = 0 by A3, Th22; then A15: Arg (a - b) = 0 by A4, A6, Th21; Arg (- a) = (Arg a) + PI by A2, A7, Th13, COMPLEX1:4, COMPTRIG:5 .= PI by A7 ; then A16: angle (b,a,0c) = (Arg (0c - a)) - (Arg (b - a)) by A11, Def4; A17: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI) by A2, A7, Th13, COMPLEX1:4, COMPTRIG:5 .= - PI ; A18: Arg (- b) = (Arg b) - PI by A3, Lm1, Th13, COMPTRIG:5; then A19: (Arg (a - b)) - (Arg (0c - b)) = 0 by A3, A14, A4, A6, Th21; then angle (0c,b,a) = (Arg (a - b)) - (Arg (- b)) by Def4; hence A20: ((angle (a,0,b)) + (angle (0,b,a))) + (angle (b,a,0)) = (((Arg b) - (Arg a)) + ((Arg (a - b)) - (Arg (- b)))) + ((Arg (0 - a)) - (Arg (b - a))) by A8, A16, Def4 .= ((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a))) .= PI by A15, A12, A13, A17 ; ::_thesis: ( 0 = angle (0,b,a) & 0 = angle (b,a,0) ) ((Arg (a - b)) + PI) - (Arg b) = 0 by A3, A14, A4, A6, Th21; then A21: angle (0c,b,a) = (Arg (a - b)) - (Arg (0c - b)) by A18, Def4; thus 0 = angle (0,b,a) by A19, Def4; ::_thesis: 0 = angle (b,a,0) angle (a,0c,b) = (Arg b) - (Arg a) by A8, Def4; hence 0 = angle (b,a,0) by A3, A7, A19, A21, A20, XCMPLX_1:3; ::_thesis: verum end; theorem Th86: :: COMPLEX2:86 for a, b, c being Element of COMPLEX st a <> b & b <> c & angle (a,b,c) = PI holds ( angle (b,c,a) = 0 & angle (c,a,b) = 0 ) proof let a, b, c be Element of COMPLEX ; ::_thesis: ( a <> b & b <> c & angle (a,b,c) = PI implies ( angle (b,c,a) = 0 & angle (c,a,b) = 0 ) ) assume that A1: a <> b and A2: b <> c and A3: angle (a,b,c) = PI ; ::_thesis: ( angle (b,c,a) = 0 & angle (c,a,b) = 0 ) A4: c - b <> 0 by A2; set r = - (Arg (a + (- b))); set A = Rotate ((a + (- b)),(- (Arg (a + (- b))))); set B = Rotate ((c + (- b)),(- (Arg (a + (- b))))); A5: Rotate (0c,(- (Arg (a + (- b))))) = 0c by Th52; A6: angle ((a + (- b)),0c,(c + (- b))) = angle ((a + (- b)),(b + (- b)),(c + (- b))) .= angle (a,b,c) by Th72 ; A7: c + (- b) <> a + (- b) by A3, Th79, COMPTRIG:5; A8: a - b <> 0 by A1; then A9: angle ((a + (- b)),0c,(c + (- b))) = angle ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c,(Rotate ((c + (- b)),(- (Arg (a + (- b))))))) by A5, A4, Th78; a + (- b) <> 0c by A1; then |.(a + (- b)).| > 0 by COMPLEX1:47; then A10: ( Im (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0 & Re (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) > 0 ) by COMPLEX1:12, SIN_COS:31; then A11: Arg (Rotate ((a + (- b)),(- (Arg (a + (- b)))))) = 0c by Th21; then (Arg ((Rotate ((c + (- b)),(- (Arg (a + (- b)))))) - 0c)) - (Arg ((Rotate ((a + (- b)),(- (Arg (a + (- b)))))) - 0c)) >= 0 by COMPTRIG:34; then A12: angle (a,b,c) = Arg (Rotate ((c + (- b)),(- (Arg (a + (- b)))))) by A6, A9, A11, Def4; angle (b,c,a) = angle ((b + (- b)),(c + (- b)),(a + (- b))) by Th72 .= angle (0c,(Rotate ((c + (- b)),(- (Arg (a + (- b)))))),(Rotate ((a + (- b)),(- (Arg (a + (- b))))))) by A5, A7, A4, Th78 ; hence angle (b,c,a) = 0 by A3, A10, A12, Lm6; ::_thesis: angle (c,a,b) = 0 angle (c,a,b) = angle ((c + (- b)),(a + (- b)),(b + (- b))) by Th72 .= angle ((Rotate ((c + (- b)),(- (Arg (a + (- b)))))),(Rotate ((a + (- b)),(- (Arg (a + (- b)))))),0c) by A5, A8, A7, Th78 ; hence angle (c,a,b) = 0 by A3, A10, A12, Lm6; ::_thesis: verum end; theorem Th87: :: COMPLEX2:87 for a, b, c being Element of 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 ) proof let a, b, c be Element of COMPLEX ; ::_thesis: ( a <> b & a <> c & b <> c & angle (a,b,c) = 0 & not ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) implies ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) assume that A1: a <> b and A2: a <> c and A3: b <> c and A4: angle (a,b,c) = 0 ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) percases ( angle (b,c,a) <> 0 or angle (c,a,b) <> 0 ) by A1, A2, A3, A4, Th83; supposeA5: angle (b,c,a) <> 0 ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) A6: 0 <= angle (b,c,a) by Th70; thus ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) ::_thesis: verum proof percases ( angle (b,c,a) < PI or angle (b,c,a) = PI or angle (b,c,a) > PI ) by XXREAL_0:1; suppose angle (b,c,a) < PI ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A2, A3, A4, A5, A6, Th84; ::_thesis: verum end; suppose angle (b,c,a) = PI ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A2, A3, Th86; ::_thesis: verum end; suppose angle (b,c,a) > PI ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A2, A3, A4, Th85, COMPTRIG:5; ::_thesis: verum end; end; end; end; supposeA7: angle (c,a,b) <> 0 ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) A8: 0 <= angle (c,a,b) by Th70; thus ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) ::_thesis: verum proof percases ( angle (c,a,b) < PI or angle (c,a,b) = PI or angle (c,a,b) > PI ) by XXREAL_0:1; suppose angle (c,a,b) < PI ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A1, A2, A4, A7, A8, Th84; ::_thesis: verum end; suppose angle (c,a,b) = PI ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A1, A2, Th86; ::_thesis: verum end; suppose angle (c,a,b) > PI ; ::_thesis: ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) hence ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A1, A2, A4, Th85, COMPTRIG:5; ::_thesis: verum end; end; end; end; end; end; theorem :: COMPLEX2:88 for a, b, c being Element of 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 ) ) proof let a, b, c be Element of COMPLEX ; ::_thesis: ( ( ((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 ) ) hereby ::_thesis: ( a <> b & a <> c & b <> c & not ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI implies ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ) assume A1: ( ((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 ) ; ::_thesis: ( a <> b & a <> c & b <> c ) percases ( ((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 ) by A1; supposeA2: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = PI ; ::_thesis: ( a <> b & a <> c & b <> c ) thus ( a <> b & a <> c & b <> c ) ::_thesis: verum proof assume A3: ( not a <> b or not a <> c or not b <> c ) ; ::_thesis: contradiction percases ( a = b or a = c or b = c ) by A3; supposeA4: a = b ; ::_thesis: contradiction A5: angle (a,c,a) = 0 by Th79; ( not angle (a,a,c) = 0 or not angle (c,a,a) = 0 ) by A2, A4, Th79, COMPTRIG:5; hence contradiction by A2, A4, A5, Th80, COMPTRIG:5; ::_thesis: verum end; supposeA6: a = c ; ::_thesis: contradiction A7: angle (a,b,a) = 0 by Th79; ( not angle (a,a,b) = 0 or not angle (b,a,a) = 0 ) by A2, A6, Th79, COMPTRIG:5; hence contradiction by A2, A6, A7, Th80, COMPTRIG:5; ::_thesis: verum end; supposeA8: b = c ; ::_thesis: contradiction A9: angle (b,a,b) = 0 by Th79; ( not angle (a,b,b) = 0 or not angle (b,b,a) = 0 ) by A2, A8, Th79, COMPTRIG:5; hence contradiction by A2, A8, A9, Th80, COMPTRIG:5; ::_thesis: verum end; end; end; end; supposeA10: ((angle (a,b,c)) + (angle (b,c,a))) + (angle (c,a,b)) = 5 * PI ; ::_thesis: ( a <> b & a <> c & b <> c ) A11: (2 + 2) * PI < 5 * PI by COMPTRIG:5, XREAL_1:68; then A12: (2 * PI) + (2 * PI) < 5 * PI ; thus ( a <> b & a <> c & b <> c ) ::_thesis: verum proof assume A13: ( not a <> b or not a <> c or not b <> c ) ; ::_thesis: contradiction percases ( a = b or b = c or a = c ) by A13; suppose a = b ; ::_thesis: contradiction then angle (b,c,a) = 0 by Th79; then A14: (angle (a,b,c)) + (angle (b,c,a)) < 2 * PI by Th70; angle (c,a,b) < 2 * PI by Th70; hence contradiction by A10, A12, A14, XREAL_1:8; ::_thesis: verum end; supposeA15: b = c ; ::_thesis: contradiction ( angle (a,b,c) < 2 * PI & angle (b,c,a) < 2 * PI ) by Th70; then A16: (angle (a,b,c)) + (angle (b,c,a)) < (2 * PI) + (2 * PI) by XREAL_1:8; angle (c,a,b) = 0 by A15, Th79; hence contradiction by A10, A11, A16; ::_thesis: verum end; suppose a = c ; ::_thesis: contradiction then angle (a,b,c) = 0 by Th79; then A17: (angle (a,b,c)) + (angle (b,c,a)) < 2 * PI by Th70; angle (c,a,b) < 2 * PI by Th70; hence contradiction by A10, A12, A17, XREAL_1:8; ::_thesis: verum end; end; end; end; end; end; assume that A18: a <> b and A19: a <> c and A20: b <> c ; ::_thesis: ( ((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 ) percases ( angle (a,b,c) = 0 or ( 0 <> angle (a,b,c) & angle (a,b,c) < PI ) or ( 0 <> angle (a,b,c) & angle (a,b,c) = PI ) or ( 0 <> angle (a,b,c) & angle (a,b,c) > PI ) ) by XXREAL_0:1; supposeA21: angle (a,b,c) = 0 ; ::_thesis: ( ((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 ) (angle (b,c,a)) + (angle (c,a,b)) = PI proof percases ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ) by A18, A19, A20, A21, Th87; suppose ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) ; ::_thesis: (angle (b,c,a)) + (angle (c,a,b)) = PI hence (angle (b,c,a)) + (angle (c,a,b)) = PI ; ::_thesis: verum end; suppose ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) ; ::_thesis: (angle (b,c,a)) + (angle (c,a,b)) = PI hence (angle (b,c,a)) + (angle (c,a,b)) = PI ; ::_thesis: verum end; end; end; hence ( ((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 ) by A21; ::_thesis: verum end; supposeA22: ( 0 <> angle (a,b,c) & angle (a,b,c) < PI ) ; ::_thesis: ( ((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 ) 0 <= angle (a,b,c) by Th70; hence ( ((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 ) by A18, A20, A22, Th84; ::_thesis: verum end; supposeA23: ( 0 <> angle (a,b,c) & angle (a,b,c) = PI ) ; ::_thesis: ( ((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 ) then angle (b,c,a) = 0 by A18, A20, Th86; hence ( ((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 ) by A18, A20, A23, Th86; ::_thesis: verum end; suppose ( 0 <> angle (a,b,c) & angle (a,b,c) > PI ) ; ::_thesis: ( ((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 ) hence ( ((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 ) by A18, A20, Th85; ::_thesis: verum end; end; end;