:: by Roland Coghetto

::

:: Received December 30, 2015

:: Copyright (c) 2015-2021 Association of Mizar Users

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

(((- r) / (- s)) * ((- t) / (- r))) * ((- s) / (- t)) = 1

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)

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)

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

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

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))|

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

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

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))| )

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))|

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))|

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))|

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

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

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

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

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

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: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

angle (A,B,C) = (3 / 2) * PI

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

sin (((angle (B,A,C)) - (angle (C,B,A))) / 2) <> 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)))

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))

(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

(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

(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 )

( (- 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 )

( - 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 )

( - 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 )

( - (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 ;

ex b_{1}, L1, L2 being Element of line_of_REAL 2 st

( b_{1} = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 )

for b_{1}, b_{2} being Element of line_of_REAL 2 st ex L1, L2 being Element of line_of_REAL 2 st

( b_{1} = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) & ex L1, L2 being Element of line_of_REAL 2 st

( b_{2} = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) holds

b_{1} = b_{2}

end;
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 L1, L2 being Element of line_of_REAL 2 st

( it = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof 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_{4} being Element of line_of_REAL 2 holds

( b_{4} = the_altitude (A,B,C) iff ex L1, L2 being Element of line_of_REAL 2 st

( b_{4} = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) );

for A, B, C being Point of (TOP-REAL 2) st B <> C holds

for b

( b

( b

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)

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)

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 ;

ex b_{1}, P being Point of (TOP-REAL 2) st

( b_{1} = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} )

for b_{1}, b_{2} being Point of (TOP-REAL 2) st ex P being Point of (TOP-REAL 2) st

( b_{1} = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) & ex P being Point of (TOP-REAL 2) st

( b_{2} = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) holds

b_{1} = b_{2}
by ZFMISC_1:3;

end;
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 P being Point of (TOP-REAL 2) st

( it = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: 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_{4} being Point of (TOP-REAL 2) holds

( b_{4} = the_foot_of_the_altitude (A,B,C) iff ex P being Point of (TOP-REAL 2) st

( b_{4} = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) );

for A, B, C being Point of (TOP-REAL 2) st B <> C holds

for b

( b

( b

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)

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) )

( 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)))

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

the_foot_of_the_altitude (A,B,C) = A

proof end;

theorem :: EUCLID13:46

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

|((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

|((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

|((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

|((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)

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)

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

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)

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

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 ;

coherence

|.(A - (the_foot_of_the_altitude (A,B,C))).| is Real;

;

end;
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 |.(A - (the_foot_of_the_altitude (A,B,C))).|;

coherence

|.(A - (the_foot_of_the_altitude (A,B,C))).| is Real;

;

:: 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))).|;

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 :: 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)

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).|

|.((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)

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)

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

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 )

( 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

(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

(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

(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} )

( (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} )

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 ;

ex b_{1} being Point of (TOP-REAL 2) st

( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b_{1}} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b_{1}} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b_{1}} )
by A1, Th56;

uniqueness

for b_{1}, b_{2} being Point of (TOP-REAL 2) st (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b_{1}} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b_{1}} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b_{1}} & (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b_{2}} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b_{2}} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b_{2}} holds

b_{1} = b_{2}
by ZFMISC_1:3;

end;
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 ( (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} );

ex b

( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b

uniqueness

for b

b

:: 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_{4} being Point of (TOP-REAL 2) holds

( b_{4} = the_orthocenter (A,B,C) iff ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b_{4}} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b_{4}} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b_{4}} ) );

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b

( 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).|)

((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).|)

((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

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).|))

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).|)))

((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).|))))

(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).|)))) )

( 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))))

|.(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))))

|.(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)))

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)))

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))).|

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).|

|.(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).|

|.(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: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)))))).|

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)))

(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

::

:: 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)))

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)

(((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)

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

::

:: 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)))

|.(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

::

:: 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)))

|.(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

::

:: 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)))

|.(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

::

:: 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)))

|.(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;

::

:: A f B

:: C

::

:: f A B

:: C

::

:: A B f