let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle & not |((C - A),(B - C))| is zero & not |((B - C),(A - B))| is zero & not |((C - A),(A - B))| is zero implies Line (A,(the_foot_of_the_altitude (A,B,C))), Line (C,(the_foot_of_the_altitude (C,A,B))), Line (B,(the_foot_of_the_altitude (B,C,A))) are_concurrent )
assume that
A1:
A,B,C is_a_triangle
and
A2:
( not |((C - A),(B - C))| is zero & not |((B - C),(A - B))| is zero & not |((C - A),(A - B))| is zero )
; Line (A,(the_foot_of_the_altitude (A,B,C))), Line (C,(the_foot_of_the_altitude (C,A,B))), Line (B,(the_foot_of_the_altitude (B,C,A))) are_concurrent
A3:
A,B,C are_mutually_distinct
by A1, EUCLID_6:20;
set r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|);
set s = - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|);
set t = - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|);
set D = ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C);
set E = ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A);
set F = ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B);
( ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) <> C & ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) <> A & ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) <> B )
proof
assume
( not
((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) <> C or not
((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) <> A or not
((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) <> B )
;
contradiction
then A4:
(
C = the_foot_of_the_altitude (
A,
B,
C) or
A = the_foot_of_the_altitude (
B,
C,
A) or
B = the_foot_of_the_altitude (
C,
A,
B) )
by A3, Th49;
(
|((A - C),(B - C))| = - |((C - A),(B - C))| &
|((B - A),(C - A))| = - |((C - A),(A - B))| &
|((C - B),(A - B))| = - |((B - C),(A - B))| )
by Th16;
hence
contradiction
by A4, A2, A3, Th38ThJ8;
verum
end;
then A5:
( ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) = the_foot_of_the_altitude (A,B,C) & ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) = the_foot_of_the_altitude (B,C,A) & ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) = the_foot_of_the_altitude (C,A,B) )
by A3, Th48;
(((((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) / (1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)))) * (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) / (1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)))) * (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) / (1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) = 1
by A3, A2, Th17;
then A6:
(((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) / (1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)))) * ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) / (1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))))) * ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) / (1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)))) = 1
;
A7:
A,C,B is_a_triangle
by A1, MENELAUS:15;
( - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) <> 1 & - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) <> 1 & - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) <> 1 )
proof
assume
( not
- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) <> 1 or not
- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) <> 1 or not
- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) <> 1 )
;
contradiction
then
( (
- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) = 1 &
B <> C &
- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) &
((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) = ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) ) or (
- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) = 1 &
C <> A &
- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) = - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) &
((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) = ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) ) or (
- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) = 1 &
A <> B &
- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) = - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) &
((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) = ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) ) )
;
hence
contradiction
by A2, Th19;
verum
end;
hence
Line (A,(the_foot_of_the_altitude (A,B,C))), Line (C,(the_foot_of_the_altitude (C,A,B))), Line (B,(the_foot_of_the_altitude (B,C,A))) are_concurrent
by A5, A6, A7, MENELAUS:22; verum