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 b₁ being Real st b₁ = 0 )

proof

reconsider z1 = z as complex number ;
|.z.| >= 0 by COMPLEX1:132;
then A1: (Re z) / |.z.| <= 1 by COMPLEX1:140, XREAL_1:187;
assume A2: z <> 0 ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
then A3: |.z.| <> 0 by COMPLEX1:131;

now

per cases ( Im z >= 0 or Im z < 0 ) ;

suppose A4: 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 ;
A5: |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 ) by Th7;
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 A1, 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;
then r <= PI by XXREAL_1:1;
then A8: ( r = PI or r < PI ) by XXREAL_0:1;
A9: cos r = cos . r by SIN_COS:def 23
.= cos1 . r by A7, FUNCT_1:72
.= (Re z) / |.z.| by A6, FUNCT_1:57 ;
( 0 = r or 0 < r ) by A7, XXREAL_1:1;
then ( r = 0 or r = PI or r in ].0 ,PI .[ ) by A8, XXREAL_1:4;
then A10: 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 A9, SIN_COS:def 23
.= 1 - (((Re z) ^2 ) / (|.z.| ^2 )) by XCMPLX_1:77
.= ((|.z.| ^2 ) / (|.z.| ^2 )) - (((Re z) ^2 ) / (|.z.| ^2 )) by A3, XCMPLX_1:60
.= ((|.z.| ^2 ) - ((Re z) ^2 )) / (|.z.| ^2 )
.= ((Im z) / |.z.|) ^2 by A5, XCMPLX_1:77 ;
then sin . r = sqrt (((Im z) / |.z.|) ^2 ) by A10, 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 A2, COMPLEX1:131, XCMPLX_1:88;
then A11: Im z = |.z.| * (sin . r) by A4, ABSVALUE:def 1
.= |.z.| * (sin r) by SIN_COS:def 21 ;
Re z = |.z.| * (cos r) by A2, A9, COMPLEX1:131, XCMPLX_1:88;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) by A11, 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 Lm3, 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 A13: Re z <> |.z.| ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )

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 ;
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 A1, 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;
then r <= 2 * PI by XXREAL_1:1;
then A17: ( r = 2 * PI or r < 2 * PI ) by XXREAL_0:1;
A18: (Re z) / |.z.| <> 1 by A13, XCMPLX_1:58;
A19: r <> 2 * PI

proof

2 * PI in [.PI ,(2 * PI ).] by Lm3, XXREAL_1:1;
then ( 2 * PI in dom cos1 & cos1 . (2 * PI ) = 1 ) by FUNCT_1:72, RELAT_1:86, SIN_COS:27, SIN_COS:81;
then A20: (cos1 " ) . 1 = 2 * PI by FUNCT_1:54;
1 in rng cos1 by Th51, XXREAL_1:1;
then A21: 1 in dom (cos1 " ) by FUNCT_1:55;
assume r = 2 * PI ; :: thesis: contradiction
hence contradiction by A18, A15, A21, A20, FUNCT_1:def 8; :: thesis: verum

end;

A22: cos r = cos . r by SIN_COS:def 23
.= cos1 . r by A16, FUNCT_1:72
.= (Re z) / |.z.| by A14, FUNCT_1:57 ;
PI <= r by A16, XXREAL_1:1;
then ( PI = r or PI < r ) by XXREAL_0:1;
then ( r = PI or r = 2 * PI or r in ].PI ,(2 * PI ).[ ) by A17, XXREAL_1:4;
then A23: sin . r <= 0 by Th25, SIN_COS:81;
take r = r; :: thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
A24: |.z.| ^2 = ((Re z) ^2 ) + ((Im z) ^2 ) by Th7;
((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 A22, SIN_COS:def 23
.= 1 - (((Re z) ^2 ) / (|.z.| ^2 )) by XCMPLX_1:77
.= ((|.z.| ^2 ) / (|.z.| ^2 )) - (((Re z) ^2 ) / (|.z.| ^2 )) by A3, XCMPLX_1:60
.= ((|.z.| ^2 ) - ((Re z) ^2 )) / (|.z.| ^2 )
.= ((Im z) / |.z.|) ^2 by A24, XCMPLX_1:77 ;
then - (sin . r) = sqrt (((Im z) / |.z.|) ^2 ) by A23, 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 A2, COMPLEX1:131, XCMPLX_1:88;
then A25: - (- (Im z)) = |.z.| * (sin . r) by A12, ABSVALUE:def 1
.= |.z.| * (sin r) by SIN_COS:def 21 ;
Re z = |.z.| * (cos r) by A2, A22, COMPLEX1:131, XCMPLX_1:88;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) by A25, COMPLEX1:29; :: thesis: ( 0 <= r & r < 2 * PI )
thus 0 <= r by A16, XXREAL_1:1; :: thesis: r < 2 * PI
r <= 2 * PI by A16, XXREAL_1:1;
hence r < 2 * PI by A19, XXREAL_0:1; :: thesis: verum

end;

suppose A26: Re z = |.z.| ; :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )

reconsider r = 0 as Real ;
take r = r; :: thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) & 0 <= r & r < 2 * PI )
(Re z) ^2 = ((Re z) ^2 ) + ((Im z) ^2 ) by A26, Th7;
then Im z = 0 ;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i> ) by A26, COMPLEX1:29, SIN_COS:34; :: thesis: ( 0 <= r & r < 2 * PI )
thus 0 <= r ; :: thesis: r < 2 * PI
thus r < 2 * PI by Lm1; :: 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 b₁ being Real st b₁ = 0 ) ; :: thesis: verum