let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( B,C,A is_a_triangle & angle (B,C,A) < PI & D,C,A is_a_triangle & angle (C,D,A) = PI / 2 & A in LSeg (D,B) & A <> D implies |.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (D,A,C)) - (angle (A,B,C))))) * (sin (angle (D,A,C))) )
assume that
A1: B,C,A is_a_triangle and
A2: angle (B,C,A) < PI and
A3: D,C,A is_a_triangle and
A4: angle (C,D,A) = PI / 2 and
A5: A in LSeg (D,B) and
A6: A <> D ; :: thesis: |.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (D,A,C)) - (angle (A,B,C))))) * (sin (angle (D,A,C)))
B,C,A are_mutually_distinct by A1, EUCLID_6:20;
then A7: ( (angle (D,A,C)) + (angle (C,A,B)) = PI or (angle (D,A,C)) + (angle (C,A,B)) = 3 * PI ) by A5, A6, EUCLID_6:13;
sin ((angle (C,A,B)) + (angle (A,B,C))) = sin ((angle (D,A,C)) - (angle (A,B,C)))
proof
per cases ( angle (C,A,B) = PI - (angle (D,A,C)) or angle (C,A,B) = (3 * PI) - (angle (D,A,C)) ) by A7;
suppose angle (C,A,B) = PI - (angle (D,A,C)) ; :: thesis: sin ((angle (C,A,B)) + (angle (A,B,C))) = sin ((angle (D,A,C)) - (angle (A,B,C)))
then sin ((angle (C,A,B)) + (angle (A,B,C))) = sin (PI - ((angle (D,A,C)) - (angle (A,B,C))))
.= sin ((angle (D,A,C)) - (angle (A,B,C))) by EUCLID10:1 ;
hence sin ((angle (C,A,B)) + (angle (A,B,C))) = sin ((angle (D,A,C)) - (angle (A,B,C))) ; :: thesis: verum
end;
suppose angle (C,A,B) = (3 * PI) - (angle (D,A,C)) ; :: thesis: sin ((angle (C,A,B)) + (angle (A,B,C))) = sin ((angle (D,A,C)) - (angle (A,B,C)))
then sin ((angle (C,A,B)) + (angle (A,B,C))) = sin (((2 * PI) * 1) + (PI - ((angle (D,A,C)) - (angle (A,B,C)))))
.= sin (PI - ((angle (D,A,C)) - (angle (A,B,C)))) by COMPLEX2:8
.= sin ((angle (D,A,C)) - (angle (A,B,C))) by EUCLID10:1 ;
hence sin ((angle (C,A,B)) + (angle (A,B,C))) = sin ((angle (D,A,C)) - (angle (A,B,C))) ; :: thesis: verum
end;
end;
end;
hence |.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (D,A,C)) - (angle (A,B,C))))) * (sin (angle (D,A,C))) by A1, A2, A3, A4, Th71; :: thesis: verum