thus
( z <> 0 implies ex r being Real st
( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * <i>) & 0 <= r & r < 2 * PI ) )
( 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
;
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 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
;
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;
( 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;
( 0 <= r & r < 2 * PI )thus
0 <= r
by A7, XXREAL_1:1;
r < 2 * PI
r <= PI
by A7, XXREAL_1:1;
hence
r < 2
* PI
by Lm3, XXREAL_0:2;
verum end; suppose A12:
Im z < 0
;
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.|
;
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
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:49, RELAT_1:57, SIN_COS:24, SIN_COS:76;
then A20:
(cos1 ") . 1
= 2
* PI
by FUNCT_1:32;
1
in rng cos1
by Th33, XXREAL_1:1;
then A21:
1
in dom (cos1 ")
by FUNCT_1:33;
assume
r = 2
* PI
;
contradiction
hence
contradiction
by A18, A15, A21, A20, FUNCT_1:def 4;
verum
end; 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;
( 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;
( 0 <= r & r < 2 * PI )thus
0 <= r
by A16, XXREAL_1:1;
r < 2 * PI
r <= 2
* PI
by A16, XXREAL_1:1;
hence
r < 2
* PI
by A19, XXREAL_0:1;
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 )
;
verum
end;
thus
( not z <> 0 implies ex b1 being Real st b1 = 0 )
; verum