let x, y, z be Real; ( (x + y) + z = PI implies (((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2 )
assume A1:
(x + y) + z = PI
; (((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2
sin ((x + y) - PI) = - (sin (x + y))
by COMPLEX2:5;
then
- (sin ((x + y) - PI)) = sin (x + y)
;
then A2:
(sin (- ((x + y) - PI))) ^2 = (sin (x + y)) ^2
by SIN_COS:31;
A3:
((cos y) ^2) + ((sin y) ^2) = 1
by SIN_COS:29;
A4:
((cos x) ^2) + ((sin x) ^2) = 1
by SIN_COS:29;
A5: (sin (x + y)) ^2 =
(((sin x) * (cos y)) + ((cos x) * (sin y))) ^2
by SIN_COS:75
.=
((((sin x) * (cos y)) ^2) + ((2 * ((sin x) * (cos y))) * ((cos x) * (sin y)))) + (((cos x) * (sin y)) ^2)
by SQUARE_1:4
.=
((((sin x) * (cos y)) * ((sin x) * (cos y))) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + (((cos x) * (sin y)) ^2)
by SQUARE_1:def 1
.=
((((sin x) * (cos y)) * ((sin x) * (cos y))) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + (((cos x) * (sin y)) * ((cos x) * (sin y)))
by SQUARE_1:def 1
.=
((((sin x) * (sin x)) * ((cos y) * (cos y))) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + ((((cos x) * (cos x)) * (sin y)) * (sin y))
.=
((((sin x) ^2) * ((cos y) * (cos y))) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + ((((cos x) * (cos x)) * (sin y)) * (sin y))
by SQUARE_1:def 1
.=
((((sin x) ^2) * ((cos y) ^2)) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + ((((cos x) * (cos x)) * (sin y)) * (sin y))
by SQUARE_1:def 1
.=
((((sin x) ^2) * ((cos y) ^2)) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + ((((cos x) ^2) * (sin y)) * (sin y))
by SQUARE_1:def 1
.=
((((sin x) ^2) * ((cos y) ^2)) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + (((cos x) ^2) * ((sin y) * (sin y)))
.=
((((sin x) ^2) * ((cos y) ^2)) + ((((2 * (sin x)) * (cos y)) * (cos x)) * (sin y))) + (((cos x) ^2) * ((sin y) ^2))
by SQUARE_1:def 1
;
(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) =
(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos (- ((x + y) - PI))))
by A1
.=
(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos ((x + y) - PI)))
by SIN_COS:31
.=
(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (- (cos (x + y))))
by COMPLEX2:5
.=
(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos (x + y)))
.=
(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (((cos x) * (cos y)) - ((sin x) * (sin y))))
by SIN_COS:75
.=
((((sin x) ^2) + ((sin y) ^2)) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))) - (((2 * ((sin x) * (sin x))) * (sin y)) * (sin y))
.=
((((sin x) ^2) + ((sin y) ^2)) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))) - (((2 * ((sin x) ^2)) * (sin y)) * (sin y))
by SQUARE_1:def 1
.=
((((sin x) ^2) + ((sin y) ^2)) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))) - ((2 * ((sin x) ^2)) * ((sin y) * (sin y)))
.=
((((sin x) ^2) + ((sin y) ^2)) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))) - ((2 * ((sin x) ^2)) * ((sin y) ^2))
by SQUARE_1:def 1
.=
(((((sin x) ^2) * (1 - ((sin y) ^2))) + ((sin y) ^2)) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))) - (((sin x) ^2) * ((sin y) ^2))
.=
((((sin x) ^2) * ((cos y) ^2)) + (((sin y) ^2) * (1 - ((sin x) ^2)))) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))
by A3
.=
((((sin x) ^2) * ((cos y) ^2)) + (((sin y) ^2) * ((cos x) ^2))) + ((((2 * (sin x)) * (sin y)) * (cos x)) * (cos y))
by A4
;
hence
(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2
by A1, A2, A5; verum