let a, b be Complex; ( a <> 0 & b <> 0 implies ( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) ) )
assume that
A1:
a <> 0
and
A2:
b <> 0
; ( cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) )
A3:
( |.a.| <> 0 & |.b.| <> 0 )
by A1, A2, COMPLEX1:45;
set ra = Rotate (a,(- (Arg a)));
set rb = Rotate (b,(- (Arg a)));
set r = - (Arg a);
set mabi = (|.a.| * |.b.|) " ;
A4:
( |.a.| >= 0 & |.b.| >= 0 )
by COMPLEX1:46;
angle (a,b) = angle ((Rotate (a,(- (Arg a)))),(Rotate (b,(- (Arg a)))))
by A1, A2, Th63;
then A5: angle (a,b) =
angle ((|.a.| * ((|.a.| * |.b.|) ")),((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")))
by A3, A4, Th61, SIN_COS:31
.=
Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "))
by A4, Th59
;
A6:
a = (|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>)
by COMPTRIG:62;
then
Re a = |.a.| * (cos (Arg a))
by COMPLEX1:12;
then A7:
cos (Arg a) = (Re a) / |.a.|
by A1, COMPLEX1:45, XCMPLX_1:89;
Im a = |.a.| * (sin (Arg a))
by A6, COMPLEX1:12;
then A8:
sin (Arg a) = (Im a) / |.a.|
by A1, COMPLEX1:45, XCMPLX_1:89;
A9:
a .|. b = (((Re a) * (Re b)) + ((Im a) * (Im b))) + (((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i>)
by Th27;
then A10:
Re (a .|. b) = ((Re a) * (Re b)) + ((Im a) * (Im b))
by COMPLEX1:12;
Re (Rotate (b,(- (Arg a)))) = ((Re b) * (cos (- (Arg a)))) - ((Im b) * (sin (- (Arg a))))
by Th54;
then A11: Re (Rotate (b,(- (Arg a)))) =
((Re b) * (cos (- (Arg a)))) - ((Im b) * (- (sin (Arg a))))
by SIN_COS:31
.=
((Re b) * ((Re a) / |.a.|)) + ((Im b) * ((Im a) / |.a.|))
by A7, A8, SIN_COS:31
.=
(Re (a .|. b)) / |.a.|
by A10
;
A12:
(Im (Rotate (b,(- (Arg a))))) ^2 >= 0
by XREAL_1:63;
Im (Rotate (b,(- (Arg a)))) = ((Re b) * (sin (- (Arg a)))) + ((Im b) * (cos (- (Arg a))))
by Th54;
then A13: Im (Rotate (b,(- (Arg a)))) =
((Re b) * (- (sin (Arg a)))) + ((Im b) * (cos (- (Arg a))))
by SIN_COS:31
.=
((- (Re b)) * ((Im a) / |.a.|)) + ((Im b) * ((Re a) / |.a.|))
by A7, A8, SIN_COS:31
.=
- ((- (((- (Re b)) * (Im a)) + ((Im b) * (Re a)))) / |.a.|)
.=
- ((Im (a .|. b)) / |.a.|)
by A9, COMPLEX1:12
;
set IT = (Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ");
set mab = |.a.| * |.b.|;
A14:
( ((|.a.| * |.b.|) ") ^2 >= 0 & (Re (Rotate (b,(- (Arg a))))) ^2 >= 0 )
by XREAL_1:63;
(|.a.| * |.b.|) " = ((|.a.| * |.b.|) ") + (0 * <i>)
;
then A15:
( Re ((|.a.| * |.b.|) ") = (|.a.| * |.b.|) " & Im ((|.a.| * |.b.|) ") = 0 )
by COMPLEX1:12;
then A16: Re ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) =
((Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) - ((Im (Rotate (b,(- (Arg a))))) * 0)
by COMPLEX1:9
.=
(Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")
;
A17: Im ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) =
((Re (Rotate (b,(- (Arg a))))) * 0) + ((Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) "))
by A15, COMPLEX1:9
.=
(Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")
;
then A18: |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| =
sqrt ((((Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) ^2) + (((Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) ^2))
by A16, COMPLEX1:def 12
.=
sqrt ((((|.a.| * |.b.|) ") ^2) * (((Re (Rotate (b,(- (Arg a))))) ^2) + ((Im (Rotate (b,(- (Arg a))))) ^2)))
.=
(sqrt (((|.a.| * |.b.|) ") ^2)) * (sqrt (((Re (Rotate (b,(- (Arg a))))) ^2) + ((Im (Rotate (b,(- (Arg a))))) ^2)))
by A14, A12, SQUARE_1:29
.=
((|.a.| * |.b.|) ") * (sqrt (((Re (Rotate (b,(- (Arg a))))) ^2) + ((Im (Rotate (b,(- (Arg a))))) ^2)))
by A4, SQUARE_1:22
.=
((|.a.| * |.b.|) ") * |.(Rotate (b,(- (Arg a)))).|
by COMPLEX1:def 12
.=
((|.a.| * |.b.|) ") * |.b.|
by Th51
;
A19:
(Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ") = (|.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (cos (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "))))) + ((|.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) "))))) * <i>)
by COMPTRIG:62;
then
|.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (cos (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")))) = (Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")
by A16, COMPLEX1:12;
hence cos (angle (a,b)) =
((Re (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).|
by A3, A5, A18, XCMPLX_1:89
.=
(Re (Rotate (b,(- (Arg a))))) * (((|.a.| * |.b.|) ") / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).|)
.=
((Re (a .|. b)) / |.a.|) * ((((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.|)
by A11, A18, XCMPLX_1:78
.=
((Re (a .|. b)) / |.a.|) * (1 / |.b.|)
by A3, XCMPLX_1:60
.=
((Re (a .|. b)) * 1) / (|.a.| * |.b.|)
by XCMPLX_1:76
.=
(Re (a .|. b)) / (|.a.| * |.b.|)
;
sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|))
|.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")))) = (Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")
by A19, A17, COMPLEX1:12;
hence sin (angle (a,b)) =
((Im (Rotate (b,(- (Arg a))))) * ((|.a.| * |.b.|) ")) / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).|
by A3, A5, A18, XCMPLX_1:89
.=
(Im (Rotate (b,(- (Arg a))))) * (((|.a.| * |.b.|) ") / |.((Rotate (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")).|)
.=
(- ((Im (a .|. b)) / |.a.|)) * ((((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.|)
by A13, A18, XCMPLX_1:78
.=
((- (Im (a .|. b))) / |.a.|) * (1 / |.b.|)
by A3, XCMPLX_1:60
.=
((- (Im (a .|. b))) * 1) / (|.a.| * |.b.|)
by XCMPLX_1:76
.=
- ((Im (a .|. b)) / (|.a.| * |.b.|))
;
verum