let a, b, c, d be Real; :: thesis: ( (a ^2) + (b ^2) = 1 & (c ^2) + (d ^2) = 1 & (c * a) + (d * b) = 1 implies b * c = a * d )
assume that
A1: (a ^2) + (b ^2) = 1 and
A2: (c ^2) + (d ^2) = 1 and
A3: (c * a) + (d * b) = 1 ; :: thesis: b * c = a * d
(c ^2) + (d ^2) = ((c * a) + (d * b)) ^2 by A3, A2
.= (((c ^2) * (a ^2)) + ((2 * (c * a)) * (d * b))) + ((d ^2) * (b ^2)) ;
then (((1 - (a ^2)) * (c ^2)) + ((1 - (b ^2)) * (d ^2))) - ((2 * (c * a)) * (d * b)) = 0 ;
then (((b * c) ^2) + ((a ^2) * (d ^2))) - ((2 * (c * a)) * (d * b)) = 0 by A1, SQUARE_1:9;
then ((b * c) - (a * d)) ^2 = 0 ;
then (b * c) - (a * d) = 0 ;
hence b * c = a * d ; :: thesis: verum