:: 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 b₁, L1, L2 being Element of line_of_REAL 2 st
( b₁ = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 )

proof end;

uniqueness
for b₁, b₂ being Element of line_of_REAL 2 st ex L1, L2 being Element of line_of_REAL 2 st
( b₁ = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) & ex L1, L2 being Element of line_of_REAL 2 st
( b₂ = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) holds
b₁ = b₂

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 b₄ being Element of line_of_REAL 2 holds
( b₄ = the_altitude (A,B,C) iff ex L1, L2 being Element of line_of_REAL 2 st
( b₄ = 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 b₁, P being Point of (TOP-REAL 2) st
( b₁ = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} )

proof end;

uniqueness
for b₁, b₂ being Point of (TOP-REAL 2) st ex P being Point of (TOP-REAL 2) st
( b₁ = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) & ex P being Point of (TOP-REAL 2) st
( b₂ = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) holds
b₁ = b₂ 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 b₄ being Point of (TOP-REAL 2) holds
( b₄ = the_foot_of_the_altitude (A,B,C) iff ex P being Point of (TOP-REAL 2) st
( b₄ = 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 b₁ being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b₁} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b₁} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b₁} ) by A1, Th56;
uniqueness
for b₁, b₂ being Point of (TOP-REAL 2) st (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b₁} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b₁} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b₁} & (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b₂} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b₂} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b₂} holds
b₁ = b₂ 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 b₄ being Point of (TOP-REAL 2) holds
( b₄ = the_orthocenter (A,B,C) iff ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b₄} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b₄} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b₄} ) );

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;