:: Altitude, Orthocenter of a Triangle and Triangulation
:: by Roland Coghetto
::
:: Received December 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


theorem Th1: :: EUCLID13:1
for i being Integer
for r being Real st 0 < i * r & i * r < r holds
i = 1
proof end;

theorem Th2: :: EUCLID13:2
for i being Integer st (- 3) / 2 < i & i < 1 / 2 & not i = 0 holds
i = - 1
proof end;

theorem Th3: :: EUCLID13:3
for r, s, t being Real st not r is zero & not s is zero & not t is zero holds
(((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = 1
proof end;

theorem Th4: :: EUCLID13:4
for r being Real st 0 < r & r < 2 * PI holds
sin (r / 2) <> 0
proof end;

theorem Th5: :: EUCLID13:5
for r being Real st - (2 * PI) < r & r < 0 holds
sin (r / 2) <> 0
proof end;

theorem Th6: :: EUCLID13:6
for r being Real holds tan ((2 * PI) - r) = - (tan r)
proof end;

theorem Th7: :: EUCLID13:7
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) st An in Line (Bn,Cn) & An <> Cn holds
Line (Bn,Cn) = Line (An,Cn)
proof end;

theorem Th8: :: EUCLID13:8
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) st An <> Cn & An in Line (Bn,Cn) holds
Bn in Line (An,Cn)
proof end;

theorem Th9: :: EUCLID13:9
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n)
for L1, L2 being Element of line_of_REAL n st An <> Bn & An <> Cn & |((An - Bn),(An - Cn))| = 0 & L1 = Line (An,Bn) & L2 = Line (An,Cn) holds
L1 _|_ L2
proof end;

theorem :: EUCLID13:10
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & |((Bn - An),(Bn - Cn))| = 0 holds
An <> Cn
proof end;

theorem Th10: :: EUCLID13:11
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds |((An - Bn),(An - Cn))| = |((Bn - An),(Cn - An))|
proof end;

theorem Th11: :: EUCLID13:12
for n being Nat
for r being Real
for An, Bn, Cn, Dn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & Dn = (r * Bn) + ((1 - r) * Cn) holds
|((Dn - An),(Dn - Cn))| = 0
proof end;

theorem Th12: :: EUCLID13:13
for n being Nat
for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st An <> Bn & Cn = (r * An) + ((1 - r) * Bn) & Cn = Bn holds
r = 0
proof end;

theorem Th13: :: EUCLID13:14
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds
( ((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)| = |((Cn - An),(Bn - Cn))| & |((Bn - Cn),(Bn - Cn))| + |((Cn - An),(Bn - Cn))| = |((Bn - Cn),(Bn - An))| )
proof end;

theorem Th14: :: EUCLID13:15
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds |((An - Bn),(An - Cn))| = - |((An - Bn),(Cn - An))|
proof end;

theorem Th15: :: EUCLID13:16
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds |((Bn - An),(Cn - An))| = |((An - Bn),(An - Cn))|
proof end;

theorem Th16: :: EUCLID13:17
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) holds |((Bn - An),(Cn - An))| = - |((Bn - An),(An - Cn))|
proof end;

theorem Th17: :: EUCLID13:18
for n being Nat
for r, s, t being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & Cn <> An & An <> Bn & not |((Cn - An),(Bn - Cn))| is zero & not |((Bn - Cn),(An - Bn))| is zero & not |((Cn - An),(An - Bn))| is zero & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & s = - ((((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|) / |((Cn - An),(Cn - An))|) & t = - ((((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|) / |((An - Bn),(An - Bn))|) holds
((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) = 1
proof end;

theorem :: EUCLID13:19
for n being Nat
for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Cn = (r * An) + ((1 - r) * Bn) & r = 1 holds
Cn = An
proof end;

theorem :: EUCLID13:20
for n being Nat
for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Cn = (r * An) + ((1 - r) * Bn) & r = 0 holds
Cn = Bn
proof end;

theorem Th18: :: EUCLID13:21
for n being Nat
for An, Bn, Cn being Point of (TOP-REAL n) st |((Bn - Cn),(Bn - Cn))| = - |((Cn - An),(Bn - Cn))| holds
|((Bn - Cn),(An - Bn))| = 0
proof end;

theorem Th19: :: EUCLID13:22
for n being Nat
for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & r = 1 holds
|((Bn - Cn),(An - Bn))| = 0
proof end;

theorem :: EUCLID13:23
for A, B, C being Point of (TOP-REAL 2) st A <> B & A <> C holds
|.(A - B).| + |.(A - C).| <> 0
proof end;

theorem Th20: :: EUCLID13:24
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
not A in Line (B,C)
proof end;

theorem :: EUCLID13:25
for A, B, C being Point of (TOP-REAL 2) st A <> B & B <> C & |((B - A),(B - C))| = 0 & not angle (A,B,C) = PI / 2 holds
angle (A,B,C) = (3 / 2) * PI
proof end;

theorem Th21: :: EUCLID13:26
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
sin ((angle (A,B,C)) / 2) > 0
proof end;

theorem :: EUCLID13:27
for A, B, C being Point of (TOP-REAL 2) st angle (B,A,C) <> angle (C,B,A) holds
sin (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0
proof end;

theorem Th22: :: EUCLID13:28
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
sin (angle (A,B,C)) <> 0
proof end;

theorem Th23: :: EUCLID13:29
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
angle (A,C,B) = PI - ((angle (C,B,A)) + (angle (B,A,C)))
proof end;

theorem Th24: :: EUCLID13:30
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
(angle (B,A,C)) + (angle (C,B,A)) = PI - (angle (A,C,B))
proof end;

theorem Th25: :: EUCLID13:31
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
(angle (B,A,C)) - (angle (C,B,A)) <> PI
proof end;

theorem Th26: :: EUCLID13:32
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
(angle (B,A,C)) - (angle (C,B,A)) <> - PI
proof end;

theorem Th27: :: EUCLID13:33
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( (- 2) * PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < 2 * PI )
proof end;

theorem :: EUCLID13:34
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( - PI < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI )
proof end;

theorem Th28: :: EUCLID13:35
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) < PI holds
( - PI < (angle (B,A,C)) - (angle (C,B,A)) & (angle (B,A,C)) - (angle (C,B,A)) < PI )
proof end;

theorem Th29: :: EUCLID13:36
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) < PI holds
( - (PI / 2) < ((angle (B,A,C)) - (angle (C,B,A))) / 2 & ((angle (B,A,C)) - (angle (C,B,A))) / 2 < PI / 2 )
proof end;

definition
let A, B, C be Point of (TOP-REAL 2);
assume A1: B <> C ;
func the_altitude (A,B,C) -> Element of line_of_REAL 2 means :Def1: :: EUCLID13:def 1
 ex L1, L2 being Element of line_of_REAL 2 st
( it = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 );
existence
ex b1, L1, L2 being Element of line_of_REAL 2 st
( b1 = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 )
proof end;
uniqueness
for b1, b2 being Element of line_of_REAL 2 st ex L1, L2 being Element of line_of_REAL 2 st
( b1 = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) & ex L1, L2 being Element of line_of_REAL 2 st
( b2 = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_altitude EUCLID13:def 1 :
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
for b4 being Element of line_of_REAL 2 holds
( b4 = the_altitude (A,B,C) iff ex L1, L2 being Element of line_of_REAL 2 st
( b4 = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) );

theorem Th30: :: EUCLID13:37
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
A in the_altitude (A,B,C)
proof end;

theorem Th31: :: EUCLID13:38
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
the_altitude (A,B,C) is being_line
proof end;

theorem Th32: :: EUCLID13:39
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
the_altitude (A,B,C) = the_altitude (A,C,B)
proof end;

theorem :: EUCLID13:40
for A, B, C, D being Point of (TOP-REAL 2) st B <> C & D in the_altitude (A,B,C) holds
the_altitude (D,B,C) = the_altitude (A,B,C)
proof end;

theorem Th33: :: EUCLID13:41
for A, B, C, D being Point of (TOP-REAL 2) st B <> C & D in Line (B,C) & D <> C holds
the_altitude (A,B,C) = the_altitude (A,D,C)
proof end;

definition
let A, B, C be Point of (TOP-REAL 2);
assume A1: B <> C ;
func the_foot_of_the_altitude (A,B,C) -> Point of (TOP-REAL 2) means :Def2: :: EUCLID13:def 2
 ex P being Point of (TOP-REAL 2) st
( it = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} );
existence
ex b1, P being Point of (TOP-REAL 2) st
( b1 = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} )
proof end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st ex P being Point of (TOP-REAL 2) st
( b1 = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) & ex P being Point of (TOP-REAL 2) st
( b2 = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) holds
b1 = b2 by ZFMISC_1:3;
end;

:: deftheorem Def2 defines the_foot_of_the_altitude EUCLID13:def 2 :
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
for b4 being Point of (TOP-REAL 2) holds
( b4 = the_foot_of_the_altitude (A,B,C) iff ex P being Point of (TOP-REAL 2) st
( b4 = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) );

theorem Th34: :: EUCLID13:42
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,C,B)
proof end;

theorem Th35: :: EUCLID13:43
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
( the_foot_of_the_altitude (A,B,C) in Line (B,C) & the_foot_of_the_altitude (A,B,C) in the_altitude (A,B,C) )
proof end;

theorem Th36: :: EUCLID13:44
for A, B, C being Point of (TOP-REAL 2) st B <> C & not A in Line (B,C) holds
the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))
proof end;

theorem Th37: :: EUCLID13:45
for A, B, C being Point of (TOP-REAL 2) st B <> C & A in Line (B,C) holds
the_foot_of_the_altitude (A,B,C) = A
proof end;

theorem :: EUCLID13:46
for A, B, C being Point of (TOP-REAL 2) st B <> C & the_foot_of_the_altitude (A,B,C) = A holds
A in Line (B,C) by Th35;

theorem Th38ThJ8: :: EUCLID13:47
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
|((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = 0
proof end;

theorem Th39: :: EUCLID13:48
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
|((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = 0
proof end;

theorem Th40: :: EUCLID13:49
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
|((A - (the_foot_of_the_altitude (A,B,C))),(C - (the_foot_of_the_altitude (A,B,C))))| = 0
proof end;

theorem Th41: :: EUCLID13:50
for A, B, C being Point of (TOP-REAL 2) st B <> C & B = the_foot_of_the_altitude (A,B,C) holds
|((B - A),(B - C))| = 0
proof end;

theorem Th42: :: EUCLID13:51
for A, B, C, D being Point of (TOP-REAL 2) st B <> C & D in Line (B,C) & D <> C holds
the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,D,C)
proof end;

theorem Th43: :: EUCLID13:52
for A, B, C being Point of (TOP-REAL 2) st B <> C & |((B - A),(B - C))| = 0 holds
B = the_foot_of_the_altitude (A,B,C)
proof end;

theorem :: EUCLID13:53
for A, B, C being Point of (TOP-REAL 2) st B <> C & B <> A & angle (A,B,C) = PI / 2 holds
the_foot_of_the_altitude (A,B,C) = B
proof end;

theorem Th44: :: EUCLID13:54
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
A <> the_foot_of_the_altitude (A,B,C)
proof end;

theorem Th45: :: EUCLID13:55
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((B - A),(B - C))| <> 0 holds
the_foot_of_the_altitude (A,B,C),B,A is_a_triangle
proof end;

definition
let A, B, C be Point of (TOP-REAL 2);
assume B <> C ;
func the_length_of_the_altitude (A,B,C) -> Real equals :Def3: :: EUCLID13:def 3
|.(A - (the_foot_of_the_altitude (A,B,C))).|;
correctness
coherence
|.(A - (the_foot_of_the_altitude (A,B,C))).| is Real;
;
end;

:: deftheorem Def3 defines the_length_of_the_altitude EUCLID13:def 3 :
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
the_length_of_the_altitude (A,B,C) = |.(A - (the_foot_of_the_altitude (A,B,C))).|;

theorem Th46: :: EUCLID13:56
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
0 <= the_length_of_the_altitude (A,B,C)
proof end;

theorem :: EUCLID13:57
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
the_length_of_the_altitude (A,B,C) = the_length_of_the_altitude (A,C,B)
proof end;

theorem Th47: :: EUCLID13:58
for A, B, C being Point of (TOP-REAL 2) st B <> C & |((B - A),(B - C))| = 0 holds
|.((the_foot_of_the_altitude (A,B,C)) - A).| = |.(A - B).|
proof end;

theorem Th48: :: EUCLID13:59
for r being Real
for A, B, C, D being Point of (TOP-REAL 2) st B <> C & r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) & D = (r * B) + ((1 - r) * C) & D <> C holds
D = the_foot_of_the_altitude (A,B,C)
proof end;

theorem Th49: :: EUCLID13:60
for r being Real
for A, B, C, D being Point of (TOP-REAL 2) st B <> C & r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) & D = (r * B) + ((1 - r) * C) & D = C holds
C = the_foot_of_the_altitude (A,B,C)
proof end;

theorem Th50: :: EUCLID13:61
for A, B, C being Point of (TOP-REAL 2) st 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 holds
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
proof end;

theorem Th51: :: EUCLID13:62
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((C - A),(B - C))| is zero holds
( the_foot_of_the_altitude (A,B,C) = C & the_foot_of_the_altitude (B,C,A) = C )
proof end;

theorem Th52: :: EUCLID13:63
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & C in the_altitude (A,B,C) & C in the_altitude (B,C,A) holds
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) is being_point
proof end;

theorem Th53: :: EUCLID13:64
for A, B, C being Point of (TOP-REAL 2) st B,C,A is_a_triangle & C in the_altitude (B,C,A) & C in the_altitude (C,A,B) holds
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) is being_point
proof end;

theorem Th54: :: EUCLID13:65
for A, B, C being Point of (TOP-REAL 2) st C,A,B is_a_triangle & C in the_altitude (C,A,B) & C in the_altitude (A,B,C) holds
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) is being_point
proof end;

theorem Th55: :: EUCLID13:66
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((C - A),(B - C))| = 0 holds
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} )
proof end;

theorem Th56: :: EUCLID13:67
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )
proof end;

definition
let A, B, C be Point of (TOP-REAL 2);
assume A1: A,B,C is_a_triangle ;
func the_orthocenter (A,B,C) -> Point of (TOP-REAL 2) means :: EUCLID13:def 4
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {it} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {it} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {it} );
existence
ex b1 being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b1} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b1} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b1} ) by A1, Th56;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b1} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b1} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b1} & (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b2} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b2} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b2} holds
b1 = b2 by ZFMISC_1:3;
end;

:: deftheorem defines the_orthocenter EUCLID13:def 4 :
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
for b4 being Point of (TOP-REAL 2) holds
( b4 = the_orthocenter (A,B,C) iff ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b4} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b4} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b4} ) );

theorem Th57: :: EUCLID13:68
for A, B, C being Point of (TOP-REAL 2) st B <> A holds
((sin (angle (B,A,C))) + (sin (angle (C,B,A)))) * (|.(C - B).| - |.(C - A).|) = ((sin (angle (B,A,C))) - (sin (angle (C,B,A)))) * (|.(C - B).| + |.(C - A).|)
proof end;

theorem Th58: :: EUCLID13:69
for A, B, C being Point of (TOP-REAL 2) st B <> A holds
((sin (((angle (B,A,C)) + (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * (|.(C - B).| - |.(C - A).|) = ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) + (angle (C,B,A))) / 2))) * (|.(C - B).| + |.(C - A).|)
proof end;

theorem Th59: :: EUCLID13:70
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & (angle (B,A,C)) - (angle (C,B,A)) <> PI & (angle (B,A,C)) - (angle (C,B,A)) <> - PI holds
cos (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 0
proof end;

theorem Th60: :: EUCLID13:71
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
tan (((angle (B,A,C)) - (angle (C,B,A))) / 2) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|))
proof end;

theorem Th61: :: EUCLID13:72
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
((angle (B,A,C)) - (angle (C,B,A))) / 2 = arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))
proof end;

theorem Th62: :: EUCLID13:73
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
(angle (B,A,C)) - (angle (C,B,A)) = 2 * (arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|))))
proof end;

theorem :: EUCLID13:74
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
( angle (B,A,C) = ((arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) + (PI / 2)) - ((angle (A,C,B)) / 2) & angle (C,B,A) = ((PI / 2) - ((angle (A,C,B)) / 2)) - (arctan ((cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)))) )
proof end;

theorem Th63: :: EUCLID13:75
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
|.(B - C).| = (|.(A - B).| * (sin (angle (B,A,C)))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))
proof end;

theorem Th64: :: EUCLID13:76
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI holds
|.(A - C).| = (|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))
proof end;

theorem Th65: :: EUCLID13:77
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (C,A,B) = PI / 2 holds
the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (A,B,C)))
proof end;

theorem Th66: :: EUCLID13:78
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,A,B) = (3 / 2) * PI holds
the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (C,B,A)))
proof end;

theorem :: EUCLID13:79
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & |((A - C),(A - B))| = 0 holds
the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).|
proof end;

theorem Th67: :: EUCLID13:80
for A, B, C being Point of (TOP-REAL 2) st B <> C & the_foot_of_the_altitude (A,B,C),B,A is_a_triangle & not |.(A - B).| * (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| holds
|.(A - B).| * (- (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C)))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).|
proof end;

theorem :: EUCLID13:81
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((B - A),(B - C))| <> 0 & not |.(A - B).| * (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| holds
|.(A - B).| * (- (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C)))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).|
proof end;

:: C
::
:: A f B
:: C
::
:: f A B
:: C
::
:: A B f
theorem :: EUCLID13:82
for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI & |((A - C),(A - B))| <> 0 holds
the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
proof end;

theorem :: EUCLID13:83
for A, B, C, D being Point of (TOP-REAL 2) st 0 < angle (B,A,D) & angle (B,A,D) < PI & 0 < angle (D,A,C) & angle (D,A,C) < PI & D,A,C are_mutually_distinct & B,A,D are_mutually_distinct holds
(angle (A,C,D)) + (angle (D,B,A)) = (2 * PI) - (((angle (B,A,C)) + (angle (A,D,B))) + (angle (C,D,A)))
proof end;

:: B
::
:: A
::
:: D
::
:: C
theorem Th68: :: EUCLID13:84
for A, B, C, D being Point of (TOP-REAL 2)
for a, b, c, d being Real st A,C,B is_a_triangle & angle (A,C,B) < PI & A,D,B is_a_triangle & angle (A,D,B) < PI & a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) holds
|.(D - C).| ^2 = (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d)))
proof end;

theorem Th69: :: EUCLID13:85
for r, s, t, d being Real st (sin (2 * s)) * (cos d) = cos (2 * t) holds
(((r * (cos s)) ^2) + ((r * (sin s)) ^2)) - (((2 * (r * (cos s))) * (r * (sin s))) * (cos d)) = (2 * (r ^2)) * ((sin t) ^2)
proof end;

theorem :: EUCLID13:86
for s being Real
for A, B, C, D being Point of (TOP-REAL 2)
for a, b, c, d, R, theta being Real st D <> C & 0 <= R & A,C,B is_a_triangle & angle (A,C,B) < PI & A,D,B is_a_triangle & angle (A,D,B) < PI & a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) & R * (cos s) = (sin a) / (sin (a + b)) & R * (sin s) = (sin c) / (sin ((b + d) + c)) & 0 < theta & theta < PI & (sin (2 * s)) * (cos d) = cos (2 * theta) holds
|.(D - C).| = ((|.(A - B).| * (sqrt 2)) * R) * (sin theta)
proof end;

:: C
::
:: B
::
:: D A
theorem Th70: :: EUCLID13:87
for A, B, C, D being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI & D,A,C is_a_triangle & angle (A,D,C) = PI / 2 holds
|.(D - C).| = ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,D)))
proof end;

:: C
::
:: B
::
:: A D
theorem Th71: :: EUCLID13:88
for A, B, C, D being Point of (TOP-REAL 2) st B,C,A is_a_triangle & angle (B,C,A) < PI & D,C,A is_a_triangle & angle (C,D,A) = PI / 2 holds
|.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (A,B,C)) + (angle (C,A,B))))) * (sin (angle (D,A,C)))
proof end;

:: C
::
:: D A B
theorem :: EUCLID13:89
for A, B, C, D being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (A,C,B) < PI & D,A,C is_a_triangle & angle (A,D,C) = PI / 2 & A in LSeg (B,D) & A <> D holds
|.(D - C).| = ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (C,A,D)) - (angle (C,B,A))))) * (sin (angle (C,A,D)))
proof end;

:: C
::
:: B A D
theorem :: EUCLID13:90
for A, B, C, D being Point of (TOP-REAL 2) st 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 holds
|.(D - C).| = ((|.(A - B).| * (sin (angle (A,B,C)))) / (sin ((angle (D,A,C)) - (angle (A,B,C))))) * (sin (angle (D,A,C)))
proof end;