:: COMPLEX2 semantic presentation

begin

theorem :: COMPLEX2:1
for a, b being ( ( real ) ( complex real ext-real ) number ) st b : ( ( real ) ( complex real ext-real ) number ) > 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex r being ( ( real ) ( complex real ext-real ) number ) st
( r : ( ( real ) ( complex real ext-real ) number ) = (b : ( ( real ) ( complex real ext-real ) number ) * (- [\(a : ( ( real ) ( complex real ext-real ) number ) / b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) /] : ( ( integer ) ( complex real ext-real integer ) set ) ) : ( ( complex ) ( complex real ext-real integer ) set ) ) : ( ( ) ( complex real ext-real ) set ) + a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) <= r : ( ( real ) ( complex real ext-real ) number ) & r : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) ) ;

theorem :: COMPLEX2:2
for a, b, c being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) > 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex real ext-real ) number ) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( complex real ext-real ) number ) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( complex real ext-real ) number ) < a : ( ( real ) ( complex real ext-real ) number ) & c : ( ( real ) ( complex real ext-real ) number ) < a : ( ( real ) ( complex real ext-real ) number ) holds
for i being ( ( integer ) ( complex real ext-real integer ) Integer) st b : ( ( real ) ( complex real ext-real ) number ) = c : ( ( real ) ( complex real ext-real ) number ) + (a : ( ( real ) ( complex real ext-real ) number ) * i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) holds
b : ( ( real ) ( complex real ext-real ) number ) = c : ( ( real ) ( complex real ext-real ) number ) ;

theorem :: COMPLEX2:3
for a, b being ( ( real ) ( complex real ext-real ) number ) holds
( sin (a : ( ( real ) ( complex real ext-real ) number ) - b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = ((sin a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (cos b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) - ((cos a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (sin b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) & cos (a : ( ( real ) ( complex real ext-real ) number ) - b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) = ((cos a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (cos b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) + ((sin a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) * (sin b : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: COMPLEX2:4
for a being ( ( real ) ( complex real ext-real ) number ) holds
( sin : ( ( V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -defined REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -valued V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ,REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( real ) ( complex real ext-real ) number ) - PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -defined REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -valued V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ,REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & cos : ( ( V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -defined REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -valued V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ,REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . (a : ( ( real ) ( complex real ext-real ) number ) - PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -defined REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) -valued V6() V18( REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) , REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ,REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:5
for a being ( ( real ) ( complex real ext-real ) number ) holds
( sin (a : ( ( real ) ( complex real ext-real ) number ) - PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (sin a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) & cos (a : ( ( real ) ( complex real ext-real ) number ) - PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (cos a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) : ( ( complex ) ( complex real ext-real ) set ) ) ;

theorem :: COMPLEX2:6
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) in ].0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,(PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .[ : ( ( ) ( V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( real ) ( complex real ext-real ) number ) in ].0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,(PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .[ : ( ( ) ( V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) holds
( a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) iff sin a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) < sin b : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: COMPLEX2:7
for a, b being ( ( real ) ( complex real ext-real ) number ) st a : ( ( real ) ( complex real ext-real ) number ) in ].(PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) .[ : ( ( ) ( V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( real ) ( complex real ext-real ) number ) in ].(PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) .[ : ( ( ) ( V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) holds
( a : ( ( real ) ( complex real ext-real ) number ) < b : ( ( real ) ( complex real ext-real ) number ) iff sin a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) > sin b : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) ) ;

theorem :: COMPLEX2:8
for a being ( ( real ) ( complex real ext-real ) number )
for i being ( ( integer ) ( complex real ext-real integer ) Integer) holds sin a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = sin (((2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:9
for a being ( ( real ) ( complex real ext-real ) number )
for i being ( ( integer ) ( complex real ext-real integer ) Integer) holds cos a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = cos (((2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + a : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:10
for a being ( ( real ) ( complex real ext-real ) number ) st sin a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
cos a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:11
for a, b being ( ( real ) ( complex real ext-real ) number ) st 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( complex real ext-real ) number ) & a : ( ( real ) ( complex real ext-real ) number ) < 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) <= b : ( ( real ) ( complex real ext-real ) number ) & b : ( ( real ) ( complex real ext-real ) number ) < 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & sin a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = sin b : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) & cos a : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = cos b : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) holds
a : ( ( real ) ( complex real ext-real ) number ) = b : ( ( real ) ( complex real ext-real ) number ) ;

begin

theorem :: COMPLEX2:12
for z being ( ( complex ) ( complex ) number ) holds z : ( ( complex ) ( complex ) number ) = (|.z : ( ( complex ) ( complex ) number ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (cos (Arg z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((|.z : ( ( complex ) ( complex ) number ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (sin (Arg z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

theorem :: COMPLEX2:13
for z being ( ( complex ) ( complex ) number ) st z : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) implies Arg (- z : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = (Arg z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) & ( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) >= PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) implies Arg (- z : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = (Arg z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) - PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ) ;

theorem :: COMPLEX2:14
for r being ( ( ) ( complex real ext-real ) Real) st r : ( ( ) ( complex real ext-real ) Real) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Arg r : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:15
for z being ( ( complex ) ( complex ) number ) holds
( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff z : ( ( complex ) ( complex ) number ) = |.z : ( ( complex ) ( complex ) number ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:16
for z being ( ( complex ) ( complex ) number ) st z : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) iff Arg (- z : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) >= PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:17
for x, y being ( ( complex ) ( complex ) number ) st ( x : ( ( complex ) ( complex ) number ) <> y : ( ( complex ) ( complex ) number ) or x : ( ( complex ) ( complex ) number ) - y : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) set ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
( Arg (x : ( ( complex ) ( complex ) number ) - y : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) iff Arg (y : ( ( complex ) ( complex ) number ) - x : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) >= PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:18
for z being ( ( complex ) ( complex ) number ) holds
( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) in ].0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) .[ : ( ( ) ( V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) iff Im z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) > 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: COMPLEX2:19
for z being ( ( complex ) ( complex ) number ) st Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) iff sin (Arg z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) > 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: COMPLEX2:20
for x, y being ( ( complex ) ( complex ) number ) st Arg x : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & Arg y : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
Arg (x : ( ( complex ) ( complex ) number ) + y : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:21
for z being ( ( complex ) ( complex ) number ) holds
( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff ( Re z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & Im z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: COMPLEX2:22
for z being ( ( complex ) ( complex ) number ) holds
( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) iff ( Re z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) < 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & Im z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: COMPLEX2:23
for z being ( ( complex ) ( complex ) number ) holds
( Im z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff ( Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) or Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ) ;

theorem :: COMPLEX2:24
for z being ( ( complex ) ( complex ) number ) st Arg z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) <= PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
Im z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:25
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( cos (Arg (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (cos (Arg z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & sin (Arg (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (sin (Arg z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:26
for a being ( ( complex ) ( complex ) number ) st a : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( cos (Arg a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = (Re a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / |.a : ( ( complex ) ( complex ) number ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & sin (Arg a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = (Im a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / |.a : ( ( complex ) ( complex ) number ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) ;

theorem :: COMPLEX2:27
for a being ( ( complex ) ( complex ) number )
for r being ( ( ) ( complex real ext-real ) Real) st r : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Arg (a : ( ( complex ) ( complex ) number ) * r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:28
for a being ( ( complex ) ( complex ) number )
for r being ( ( ) ( complex real ext-real ) Real) st r : ( ( ) ( complex real ext-real ) Real) < 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Arg (a : ( ( complex ) ( complex ) number ) * r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg (- a : ( ( complex ) ( complex ) number ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

begin

definition
let x, y be ( ( complex ) ( complex ) number ) ;
func x .|. y -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) equals :: COMPLEX2:def 1
x : ( ( complex ) ( complex ) set ) * (y : ( ( complex ) ( complex ) set ) *') : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) set ) ;
end;

theorem :: COMPLEX2:29
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (((Re x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (Re y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((Im x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (Im y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + (((- ((Re x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (Im y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((Im x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (Re y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;

theorem :: COMPLEX2:30
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
( z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = ((Re z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (Re z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((Im z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (Im z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = ((Re z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((Im z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:31
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
( z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = |.z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & |.z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Re (z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:32
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds |.(x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = |.x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:33
for x being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:34
for y, x being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) *' : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:35
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:36
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:37
for a, x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:38
for x, a, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) *') : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:39
for a, x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) *') : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:40
for a, x, b, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:41
for x, a, y, b, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) *') : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + ((b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) *') : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:42
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (- x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (- y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:43
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (- x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = - (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:44
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds - (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (- y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:45
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (- x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (- y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:46
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:47
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:48
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (((x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:49
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (((x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:50
for x, y being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
( Re (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff ( Im (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = |.x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) or Im (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (|.x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ) ;

begin

definition
let a be ( ( complex ) ( complex ) number ) ;
let r be ( ( ) ( complex real ext-real ) Real) ;
func Rotate (a,r) -> ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) equals :: COMPLEX2:def 2
(|.a : ( ( complex ) ( complex ) set ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (cos (r : ( ( complex ) ( complex ) set ) + (Arg a : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((|.a : ( ( complex ) ( complex ) set ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (sin (r : ( ( complex ) ( complex ) set ) + (Arg a : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * <i> : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) set ) : ( ( ) ( complex ) set ) ;
end;

theorem :: COMPLEX2:51
for a being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:52
for r being ( ( ) ( complex real ext-real ) Real)
for a being ( ( complex ) ( complex ) number ) holds
( Rotate (a : ( ( complex ) ( complex ) number ) ,r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff a : ( ( complex ) ( complex ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: COMPLEX2:53
for r being ( ( ) ( complex real ext-real ) Real)
for a being ( ( complex ) ( complex ) number ) holds |.(Rotate (a : ( ( complex ) ( complex ) number ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = |.a : ( ( complex ) ( complex ) number ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:54
for r being ( ( ) ( complex real ext-real ) Real)
for a being ( ( complex ) ( complex ) number ) st a : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ex i being ( ( integer ) ( complex real ext-real integer ) Integer) st Arg (Rotate (a : ( ( complex ) ( complex ) number ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = ((2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * i : ( ( integer ) ( complex real ext-real integer ) Integer) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + (r : ( ( ) ( complex real ext-real ) Real) + (Arg a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:55
for a being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(- (Arg a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = |.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:56
for a being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) holds
( Re (Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = ((Re a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (cos r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) - ((Im a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (sin r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & Im (Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = ((Re a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (sin r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((Im a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * (cos r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:57
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) holds Rotate ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + (Rotate (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:58
for a being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) holds Rotate ((- a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = - (Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:59
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) holds Rotate ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = (Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - (Rotate (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

theorem :: COMPLEX2:60
for a being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) = - a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ;

begin

definition
let a, b be ( ( complex ) ( complex ) number ) ;
func angle (a,b) -> ( ( ) ( complex real ext-real ) Real) equals :: COMPLEX2:def 3
 Arg (Rotate (b : ( ( complex ) ( complex ) set ) ,(- (Arg a : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) if ( Arg a : ( ( complex ) ( complex ) set ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) or b : ( ( complex ) ( complex ) set ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) )
otherwise (2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) - (Arg a : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;
end;

theorem :: COMPLEX2:61
for r being ( ( ) ( complex real ext-real ) Real)
for a being ( ( complex ) ( complex ) number ) st r : ( ( ) ( complex real ext-real ) Real) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (r : ( ( ) ( complex real ext-real ) Real) ,a : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex real ext-real ) Real) = Arg a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:62
for r being ( ( ) ( complex real ext-real ) Real)
for a, b being ( ( complex ) ( complex ) number ) st Arg a : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg b : ( ( complex ) ( complex ) number ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & a : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
Arg (Rotate (a : ( ( complex ) ( complex ) number ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg (Rotate (b : ( ( complex ) ( complex ) number ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:63
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) st r : ( ( ) ( complex real ext-real ) Real) > 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = angle ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) set ) ,(b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Real) ;

theorem :: COMPLEX2:64
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & Arg a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
Arg (- a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg (- b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:65
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = angle ((Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(Rotate (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) ;

theorem :: COMPLEX2:66
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) st r : ( ( ) ( complex real ext-real ) Real) < 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = angle ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) set ) ,(b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * r : ( ( ) ( complex real ext-real ) Real) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Real) ;

theorem :: COMPLEX2:67
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = angle ((- a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(- b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) ;

theorem :: COMPLEX2:68
for b, a being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(- b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:69
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( cos (angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = (Re (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / (|.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & sin (angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( ) ( complex real ext-real ) Real) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - ((Im (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / (|.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) ;

definition
let x, y, z be ( ( complex ) ( complex ) number ) ;
func angle (x,y,z) -> ( ( real ) ( complex real ext-real ) number ) equals :: COMPLEX2:def 4
(Arg (z : ( ( ) ( ) set ) - y : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) - (Arg (x : ( ( complex ) ( complex ) set ) - y : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) if (Arg (z : ( ( ) ( ) set ) - y : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) - (Arg (x : ( ( complex ) ( complex ) set ) - y : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) >= 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) )
otherwise (2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + ((Arg (z : ( ( ) ( ) set ) - y : ( ( complex ) ( complex ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) - (Arg (x : ( ( complex ) ( complex ) set ) - y : ( ( complex ) ( complex ) set ) ) : ( ( ) ( complex ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;
end;

theorem :: COMPLEX2:70
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
( 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) <= angle (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) & angle (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) < 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:71
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds angle (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = angle ((x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,(z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) ;

theorem :: COMPLEX2:72
for a, b, c, d being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = angle ((a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + d : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + d : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) + d : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) ;

theorem :: COMPLEX2:73
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Real) = angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) ;

theorem :: COMPLEX2:74
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st angle (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( Arg (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = Arg (z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & angle (z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: COMPLEX2:75
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( Re (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff ( angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) or angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = (3 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ) ;

theorem :: COMPLEX2:76
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ( ( not Im (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = |.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & not Im (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (|.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) or angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) or angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = (3 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) & ( ( not angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & not angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = (3 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) or Im (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = |.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) or Im (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .|. b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = - (|.a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) * |.b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ) ;

theorem :: COMPLEX2:77
for x, y, z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & ( angle (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) or angle (x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = (3 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) holds
(|.(x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) + (|.(z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - y : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) = |.(x : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) - z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) .| : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ^2 : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:78
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) )
for r being ( ( ) ( complex real ext-real ) Real) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = angle ((Rotate (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(Rotate (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,(Rotate (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,r : ( ( ) ( complex real ext-real ) Real) )) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) ;

theorem :: COMPLEX2:79
for a, b being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:80
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
( angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) iff (angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) + (angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = 2 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:81
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:82
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ;

theorem :: COMPLEX2:83
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & not angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & not angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) holds
angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) <> 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: COMPLEX2:84
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) < angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) & angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) < PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
( ((angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) + (angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) < angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) & 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) < angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) ) ;

theorem :: COMPLEX2:85
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) > PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
( ((angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) + (angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = 5 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) > PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) > PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) ;

theorem :: COMPLEX2:86
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) holds
( angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: COMPLEX2:87
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) st a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & not ( angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) & angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) holds
( angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) & angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) : ( ( real ) ( complex real ext-real ) number ) = 0 : ( ( ) ( zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: COMPLEX2:88
for a, b, c being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) holds
( ( ((angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) + (angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) or ((angle (a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) + (angle (b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) ) : ( ( ) ( complex real ext-real ) set ) + (angle (c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ,b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) )) : ( ( real ) ( complex real ext-real ) number ) : ( ( ) ( complex real ext-real ) set ) = 5 : ( ( ) ( non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() ) Element of NAT : ( ( ) ( V61() V62() V63() V64() V65() V66() V67() ) Element of K19(REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V50() V61() V62() V63() V67() ) set ) ) ) iff ( a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & a : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) & b : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) <> c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V50() V61() V67() ) set ) ) ) ) ;