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
|.z.| >= 0 by COMPLEX1:46;
then A1: (Re z) / |.z.| <= 1 by COMPLEX1:54, XREAL_1:185;
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:45;
now :: thesis: ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i>) & 0 <= r & r < 2 * PI )
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:10;
reconsider cos1 = cos1 as one-to-one PartFunc of [.0,PI.],REAL by Th25, RFUNCT_2:50;
reconsider r = (cos1 ") . ((Re z) / |.z.|) as Real ;
A5: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) by Th3;
take r = r; :: thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i>) & 0 <= r & r < 2 * PI )
Re z >= - |.z.| by Th1;
then - 1 <= (Re z) / |.z.| by COMPLEX1:46, XREAL_1:193;
then A6: (Re z) / |.z.| in rng cos1 by A1, Th32, XXREAL_1:1;
then (Re z) / |.z.| in dom (cos1 ") by FUNCT_1:33;
then r in rng (cos1 ") by FUNCT_1:def 3;
then r in dom cos1 by FUNCT_1:33;
then A7: r in [.0,PI.] by RELAT_1:57;
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 19
.= cos1 . r by A7, FUNCT_1:49
.= (Re z) / |.z.| by A6, FUNCT_1:35 ;
( 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 Th7, SIN_COS:30, SIN_COS:76;
((cos . r) ^2) + ((sin . r) ^2) = 1 by SIN_COS:28;
then (sin . r) ^2 = 1 - ((cos . r) ^2)
.= 1 - (((Re z) / |.z.|) ^2) by A9, SIN_COS:def 19
.= 1 - (((Re z) ^2) / (|.z.| ^2)) by XCMPLX_1:76
.= ((|.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:76 ;
then sin . r = sqrt (((Im z) / |.z.|) ^2) by A10, SQUARE_1:22
.= |.((Im z) / |.z.|).| by COMPLEX1:72
.= |.(Im z).| / |.|.z.|.| by COMPLEX1:67
.= |.(Im z).| / |.z.| ;
then |.(Im z).| = |.z.| * (sin . r) by A2, COMPLEX1:45, XCMPLX_1:87;
then A11: Im z = |.z.| * (sin . r) by A4, ABSVALUE:def 1
.= |.z.| * (sin r) by SIN_COS:def 17 ;
Re z = |.z.| * (cos r) by A2, A9, COMPLEX1:45, XCMPLX_1:87;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i>) by A11, COMPLEX1:13; :: 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 )
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:10;
reconsider cos1 = cos1 as one-to-one PartFunc of [.PI,(2 * PI).],REAL by Th26, RFUNCT_2:50;
reconsider r = (cos1 ") . ((Re z) / |.z.|) as Real ;
Re z >= - |.z.| by Th1;
then - 1 <= (Re z) / |.z.| by COMPLEX1:46, XREAL_1:193;
then A14: (Re z) / |.z.| in rng cos1 by A1, Th33, XXREAL_1:1;
then A15: (Re z) / |.z.| in dom (cos1 ") by FUNCT_1:33;
then r in rng (cos1 ") by FUNCT_1:def 3;
then r in dom cos1 by FUNCT_1:33;
then A16: r in [.PI,(2 * PI).] by RELAT_1:57;
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 A22: cos r = cos . r by SIN_COS:def 19
.= cos1 . r by A16, FUNCT_1:49
.= (Re z) / |.z.| by A14, FUNCT_1:35 ;
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 Th9, SIN_COS:76;
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 Th3;
((cos . r) ^2) + ((sin . r) ^2) = 1 by SIN_COS:28;
then (sin . r) ^2 = 1 - ((cos . r) ^2)
.= 1 - (((Re z) / |.z.|) ^2) by A22, SIN_COS:def 19
.= 1 - (((Re z) ^2) / (|.z.| ^2)) by XCMPLX_1:76
.= ((|.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:76 ;
then - (sin . r) = sqrt (((Im z) / |.z.|) ^2) by A23, SQUARE_1:23
.= |.((Im z) / |.z.|).| by COMPLEX1:72
.= |.(Im z).| / |.|.z.|.| by COMPLEX1:67
.= |.(Im z).| / |.z.| ;
then sin . r = (- |.(Im z).|) / |.z.| ;
then - |.(Im z).| = |.z.| * (sin . r) by A2, COMPLEX1:45, XCMPLX_1:87;
then A25: - (- (Im z)) = |.z.| * (sin . r) by A12, ABSVALUE:def 1
.= |.z.| * (sin r) by SIN_COS:def 17 ;
Re z = |.z.| * (cos r) by A2, A22, COMPLEX1:45, XCMPLX_1:87;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i>) by A25, COMPLEX1:13; :: 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, Th3;
then Im z = 0 ;
hence z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i>) by A26, COMPLEX1:13, SIN_COS:31; :: thesis: ( 0 <= r & r < 2 * PI )
thus 0 <= r ; :: thesis: r < 2 * PI
thus r < 2 * PI by Lm1; :: thesis: verum
end;
end;
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