thus ( z <> 0 implies ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI ) ) :: thesis: ( not z <> 0 implies ex b1 being Real st b1 = 0 )
proof
assume A1: z <> 0 ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
then A2: |.z.| <> 0 by COMPLEX1:131;
A3: |.z.| >= 0 by COMPLEX1:132;
A4: (Re z) / |.z.| <= 1 by A3, COMPLEX1:140, XREAL_1:187;
reconsider z1 = z as complex number ;
now
per cases ( Im z >= 0 or Im z < 0 ) ;
suppose A5: Im z >= 0 ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
set 0PI = [.0 ,PI .];
reconsider cos1 = cos | [.0 ,PI .] as PartFunc of [.0 ,PI .],REAL by PARTFUN1:43;
reconsider cos1 = cos1 as one-to-one PartFunc of [.0 ,PI .],REAL by Th41, RFUNCT_2:82;
reconsider r = (cos1 " ) . ((Re z) / |.z.|) as Real ;
take r = r; :: thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
Re z >= - |.z.| by Th3;
then - 1 <= (Re z) / |.z.| by COMPLEX1:132, XREAL_1:195;
then A6: (Re z) / |.z.| in rng cos1 by A4, Th50, XXREAL_1:1;
then (Re z) / |.z.| in dom (cos1 " ) by FUNCT_1:55;
then r in rng (cos1 " ) by FUNCT_1:def 5;
then r in dom cos1 by FUNCT_1:55;
then A7: r in [.0 ,PI .] by RELAT_1:86;
A8: cos r = cos . r by SIN_COS:def 23
.= cos1 . r by A7, FUNCT_1:72
.= (Re z) / |.z.| by A6, FUNCT_1:57 ;
then A9: Re z = |.z.| * (cos r) by A1, COMPLEX1:131, XCMPLX_1:88;
A10: |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 ) by Th7;
( 0 <= r & r <= PI ) by A7, XXREAL_1:1;
then ( ( 0 = r or 0 < r ) & ( r = PI or r < PI ) ) by XXREAL_0:1;
then ( r = 0 or r = PI or r in ].0 ,PI .[ ) by XXREAL_1:4;
then A11: sin . r >= 0 by Th23, SIN_COS:33, SIN_COS:81;
((cos . r) ^2 ) + ((sin . r) ^2 ) = 1 by SIN_COS:31;
then (sin . r) ^2 = 1 - ((cos . r) ^2 )
.= 1 - (((Re z) / |.z.|) ^2 ) by A8, SIN_COS:def 23
.= 1 - (((Re z) ^2 ) / (|.z.| ^2 )) by XCMPLX_1:77
.= ((|.z.| ^2 ) / (|.z.| ^2 )) - (((Re z) ^2 ) / (|.z.| ^2 )) by A2, XCMPLX_1:60
.= ((|.z.| ^2 ) - ((Re z) ^2 )) / (|.z.| ^2 )
.= ((Im z) / |.z.|) ^2 by A10, XCMPLX_1:77 ;
then sin . r = sqrt (((Im z) / |.z.|) ^2 ) by A11, SQUARE_1:89
.= abs ((Im z) / |.z.|) by COMPLEX1:158
.= (abs (Im z)) / (abs |.z.|) by COMPLEX1:153
.= (abs (Im z)) / |.z.| ;
then abs (Im z) = |.z.| * (sin . r) by A1, COMPLEX1:131, XCMPLX_1:88;
then Im z = |.z.| * (sin . r) by A5, ABSVALUE:def 1
.= |.z.| * (sin r) by SIN_COS:def 21 ;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) by A9, COMPLEX1:29; :: thesis: ( 0 <= r & r < 2 * PI )
thus 0 <= r by A7, XXREAL_1:1; :: thesis: r < 2 * PI
r <= PI by A7, XXREAL_1:1;
hence r < 2 * PI by Lx3, XXREAL_0:2; :: thesis: verum
end;
suppose A12: Im z < 0 ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
now
per cases ( Re z <> |.z.| or Re z = |.z.| ) ;
suppose Re z <> |.z.| ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
then A13: (Re z) / |.z.| <> 1 by XCMPLX_1:58;
set 0PI = [.PI ,(2 * PI ).];
reconsider cos1 = cos | [.PI ,(2 * PI ).] as PartFunc of [.PI ,(2 * PI ).],REAL by PARTFUN1:43;
reconsider cos1 = cos1 as one-to-one PartFunc of [.PI ,(2 * PI ).],REAL by Th42, RFUNCT_2:82;
reconsider r = (cos1 " ) . ((Re z) / |.z.|) as Real ;
take r = r; :: thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
Re z >= - |.z.| by Th3;
then - 1 <= (Re z) / |.z.| by COMPLEX1:132, XREAL_1:195;
then A14: (Re z) / |.z.| in rng cos1 by A4, Th51, XXREAL_1:1;
then A15: (Re z) / |.z.| in dom (cos1 " ) by FUNCT_1:55;
then r in rng (cos1 " ) by FUNCT_1:def 5;
then r in dom cos1 by FUNCT_1:55;
then A16: r in [.PI ,(2 * PI ).] by RELAT_1:86;
A17: cos r = cos . r by SIN_COS:def 23
.= cos1 . r by A16, FUNCT_1:72
.= (Re z) / |.z.| by A14, FUNCT_1:57 ;
then A18: Re z = |.z.| * (cos r) by A1, COMPLEX1:131, XCMPLX_1:88;
A19: |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 ) by Th7;
( PI <= r & r <= 2 * PI ) by A16, XXREAL_1:1;
then ( ( PI = r or PI < r ) & ( r = 2 * PI or r < 2 * PI ) ) by XXREAL_0:1;
then ( r = PI or r = 2 * PI or r in ].PI ,(2 * PI ).[ ) by XXREAL_1:4;
then A20: sin . r <= 0 by Th25, SIN_COS:81;
((cos . r) ^2 ) + ((sin . r) ^2 ) = 1 by SIN_COS:31;
then (sin . r) ^2 = 1 - ((cos . r) ^2 )
.= 1 - (((Re z) / |.z.|) ^2 ) by A17, SIN_COS:def 23
.= 1 - (((Re z) ^2 ) / (|.z.| ^2 )) by XCMPLX_1:77
.= ((|.z.| ^2 ) / (|.z.| ^2 )) - (((Re z) ^2 ) / (|.z.| ^2 )) by A2, XCMPLX_1:60
.= ((|.z.| ^2 ) - ((Re z) ^2 )) / (|.z.| ^2 )
.= ((Im z) / |.z.|) ^2 by A19, XCMPLX_1:77 ;
then - (sin . r) = sqrt (((Im z) / |.z.|) ^2 ) by A20, SQUARE_1:90
.= abs ((Im z) / |.z.|) by COMPLEX1:158
.= (abs (Im z)) / (abs |.z.|) by COMPLEX1:153
.= (abs (Im z)) / |.z.| ;
then sin . r = (- (abs (Im z))) / |.z.| ;
then - (abs (Im z)) = |.z.| * (sin . r) by A1, COMPLEX1:131, XCMPLX_1:88;
then - (- (Im z)) = |.z.| * (sin . r) by A12, ABSVALUE:def 1
.= |.z.| * (sin r) by SIN_COS:def 21 ;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) by A18, COMPLEX1:29; :: thesis: ( 0 <= r & r < 2 * PI )
thus 0 <= r by A16, XXREAL_1:1; :: thesis: r < 2 * PI
A22: r <> 2 * PI r <= 2 * PI by A16, XXREAL_1:1;
hence r < 2 * PI by A22, XXREAL_0:1; :: thesis: verum
end;
suppose A29: Re z = |.z.| ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
then (Re z) ^2 = ((Re z) ^2 ) + ((Im z) ^2 ) by Th7;
then A30: Im z = 0 ;
reconsider r = 0 as Real ;
take r = r; :: thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
thus z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) by A29, A30, COMPLEX1:29, SIN_COS:34; :: thesis: ( 0 <= r & r < 2 * PI )
thus 0 <= r ; :: thesis: r < 2 * PI
thus r < 2 * PI by Lm0; :: thesis: verum
end;
end;
end;
hence ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI ) ; :: thesis: verum
end;
end;
end;
hence ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI ) ; :: thesis: verum
end;
thus ( not z <> 0 implies ex b1 being Real st b1 = 0 ) ; :: thesis: verum