let A, B, C be Point of (TOP-REAL 2); :: thesis: for a, b, r being Real st A,B,C is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & |[a,b]| in LSeg (A,C) holds
angle (C,B,A) = PI / 2
let a, b, r be Real; :: thesis: ( A,B,C is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & |[a,b]| in LSeg (A,C) implies angle (C,B,A) = PI / 2 )
assume that
A1: A,B,C is_a_triangle and
A2: angle (C,B,A) in ].0,PI.[ and
A3: angle (B,A,C) in ].0,PI.[ and
A4: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) and
A5: |[a,b]| in LSeg (A,C) ; :: thesis: angle (C,B,A) = PI / 2
A6: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
set O = |[a,b]|;
A7: ( angle (C,B,A) > 0 & angle (C,B,A) < PI ) by A2, XXREAL_1:4;
A8: ( angle (B,A,C) > 0 & angle (B,A,C) < PI ) by A3, XXREAL_1:4;
A9: circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by JGRAPH_6:def 5;
consider JA being Point of (TOP-REAL 2) such that
A10: A = JA and
A11: |.(JA - |[a,b]|).| = r by A4, A9;
consider JB being Point of (TOP-REAL 2) such that
A12: B = JB and
A13: |.(JB - |[a,b]|).| = r by A4, A9;
consider JC being Point of (TOP-REAL 2) such that
A14: C = JC and
A15: |.(JC - |[a,b]|).| = r by A4, A9;
r is positive by A1, A4, Thm24;
then A16: ( |[a,b]| <> A & |[a,b]| <> C ) by A4, Thm25;
A17: angle (C,B,A) < PI by A2, XXREAL_1:4;
A18: ( |.(B - |[a,b]|).| = |.(|[a,b]| - C).| & B <> C ) by A12, A13, A14, A15, A6, EUCLID_6:43;
A19: angle (C,B,|[a,b]|) < PI
proof
assume angle (C,B,|[a,b]|) >= PI ; :: thesis: contradiction
then angle (|[a,b]|,C,B) >= PI by A18, EUCLID_6:16;
then A20: angle (A,C,B) >= PI by A5, A16, EUCLID_6:9;
((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = PI by A17, A6, EUCLID_3:47;
then A21: (angle (C,B,A)) + (angle (B,A,C)) = PI - (angle (A,C,B)) ;
angle (B,A,C) <= 0
proof
assume A22: angle (B,A,C) > 0 ; :: thesis: contradiction
angle (C,B,A) > 0 by A2, XXREAL_1:4;
hence contradiction by A21, A20, A22, XREAL_1:47; :: thesis: verum
end;
hence contradiction by A3, XXREAL_1:4; :: thesis: verum
end;
A23: ( A,|[a,b]|,B is_a_triangle & C,|[a,b]|,B is_a_triangle )
proof
A23a: r is positive by A1, A4, Thm24;
then A24: ( |[a,b]| <> B & |[a,b]| <> A & |[a,b]| <> C ) by A4, Thm25;
not A in Line (|[a,b]|,B)
proof
assume A25: A in Line (|[a,b]|,B) ; :: thesis: contradiction
B in Line (|[a,b]|,B) by RLTOPSP1:72;
then Line (A,B) = Line (|[a,b]|,B) by A6, A25, RLTOPSP1:75;
then ( |[a,b]| in Line (A,B) & A in Line (A,B) ) by RLTOPSP1:72;
then A26: Line (|[a,b]|,A) = Line (A,B) by A4, A23a, Thm25, RLTOPSP1:75;
( |[a,b]| in Line (A,C) & A in Line (A,C) ) by A5, MENELAUS:12, RLTOPSP1:72;
then Line (|[a,b]|,A) = Line (A,C) by A4, A23a, Thm25, RLTOPSP1:75;
then ( A in Line (A,B) & B in Line (A,B) & C in Line (A,B) ) by A26, RLTOPSP1:72;
hence contradiction by A1, RLTOPSP1:def 16; :: thesis: verum
end;
hence A,|[a,b]|,B is_a_triangle by A24, MENELAUS:13; :: thesis: C,|[a,b]|,B is_a_triangle
not C,|[a,b]|,B are_collinear
proof
assume A28: C,|[a,b]|,B are_collinear ; :: thesis: contradiction
then ( C in Line (|[a,b]|,B) & B in Line (|[a,b]|,B) ) by A24, MENELAUS:13, RLTOPSP1:72;
then A29: Line (C,B) = Line (|[a,b]|,B) by A6, RLTOPSP1:75;
( C in Line (|[a,b]|,B) & |[a,b]| in Line (|[a,b]|,B) & |[a,b]| <> C ) by A28, A24, MENELAUS:13, RLTOPSP1:72;
then A30: Line (C,|[a,b]|) = Line (|[a,b]|,B) by RLTOPSP1:75;
A31: ( |[a,b]| in Line (A,C) & A in Line (A,C) & C in Line (C,A) ) by A5, MENELAUS:12, RLTOPSP1:72;
then Line (C,|[a,b]|) = Line (A,C) by A4, A23a, Thm25, RLTOPSP1:75;
hence contradiction by A30, A31, A29, A1, A6, MENELAUS:13; :: thesis: verum
end;
hence C,|[a,b]|,B is_a_triangle ; :: thesis: verum
end;
then A32: ( A,|[a,b]|,B are_mutually_distinct & C,|[a,b]|,B are_mutually_distinct ) by EUCLID_6:20;
then angle (B,A,|[a,b]|) < PI by A8, A5, EUCLID_6:10;
then A33: ((angle (B,A,|[a,b]|)) + (angle (A,|[a,b]|,B))) + (angle (|[a,b]|,B,A)) = PI by A32, EUCLID_3:47;
|.(|[a,b]| - A).| = |.(B - |[a,b]|).| by A10, A11, A12, A13, EUCLID_6:43;
then A34: angle (|[a,b]|,A,B) = angle (A,B,|[a,b]|) by A6, EUCLID_6:16;
|.(|[a,b]| - B).| = |.(C - |[a,b]|).| by A12, A13, A14, A15, EUCLID_6:43;
then A35: angle (|[a,b]|,B,C) = angle (B,C,|[a,b]|) by A6, EUCLID_6:16;
A36: ( (((angle (C,B,|[a,b]|)) + (angle (|[a,b]|,C,B))) + (angle (|[a,b]|,B,A))) + (angle (B,A,|[a,b]|)) = PI or (((angle (C,B,|[a,b]|)) + (angle (|[a,b]|,C,B))) + (angle (|[a,b]|,B,A))) + (angle (B,A,|[a,b]|)) = - PI )
proof
A37: ( (angle (A,|[a,b]|,B)) + (angle (B,|[a,b]|,C)) = PI or (angle (A,|[a,b]|,B)) + (angle (B,|[a,b]|,C)) = 3 * PI ) by A32, A5, EUCLID_6:13;
((angle (C,B,|[a,b]|)) + (angle (B,|[a,b]|,C))) + (angle (|[a,b]|,C,B)) = PI by A19, A32, EUCLID_3:47;
hence ( (((angle (C,B,|[a,b]|)) + (angle (|[a,b]|,C,B))) + (angle (|[a,b]|,B,A))) + (angle (B,A,|[a,b]|)) = PI or (((angle (C,B,|[a,b]|)) + (angle (|[a,b]|,C,B))) + (angle (|[a,b]|,B,A))) + (angle (B,A,|[a,b]|)) = - PI ) by A33, A37; :: thesis: verum
end;
( angle (|[a,b]|,C,B) = angle (C,B,|[a,b]|) & angle (B,A,|[a,b]|) = angle (|[a,b]|,B,A) )
proof
( (2 * PI) - (angle (C,B,|[a,b]|)) = angle (|[a,b]|,B,C) & (2 * PI) - (angle (|[a,b]|,C,B)) = angle (B,C,|[a,b]|) ) by A23, Thm20;
hence angle (|[a,b]|,C,B) = angle (C,B,|[a,b]|) by A35; :: thesis: angle (B,A,|[a,b]|) = angle (|[a,b]|,B,A)
( (2 * PI) - (angle (|[a,b]|,B,A)) = angle (A,B,|[a,b]|) & (2 * PI) - (angle (|[a,b]|,A,B)) = angle (B,A,|[a,b]|) ) by A23, Thm20;
hence angle (B,A,|[a,b]|) = angle (|[a,b]|,B,A) by A34; :: thesis: verum
end;
then ( (angle (C,B,|[a,b]|)) + (angle (|[a,b]|,B,A)) = PI / 2 or (angle (C,B,|[a,b]|)) + (angle (|[a,b]|,B,A)) = - (PI / 2) ) by A36;
then ( angle (C,B,A) = PI / 2 or (angle (C,B,A)) + (2 * PI) = PI / 2 or angle (C,B,A) = - (PI / 2) or (angle (C,B,A)) + (2 * PI) = - (PI / 2) ) by EUCLID_6:4;
then ( angle (C,B,A) = PI / 2 or angle (C,B,A) = - ((3 * PI) / 2) or angle (C,B,A) = - (PI / 2) or angle (C,B,A) = - ((5 * PI) / 2) ) ;
hence angle (C,B,A) = PI / 2 by A7; :: thesis: verum