:: Altitude, Orthocenter of a Triangle and Triangulation :: by Roland Coghetto :: :: Received December 30, 2015 :: Copyright (c) 2015-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies INT_1, NUMBERS, NAT_1, SUBSET_1, COMPLEX1, REAL_1, RELAT_1, TARSKI, CARD_1, ARYTM_1, ARYTM_3, RVSUM_1, XXREAL_0, ZFMISC_1, XBOOLE_0, RLTOPSP1, PRE_TOPC, EUCLID, INCSP_1, PROJRED2, AFF_1, ANALOAF, SYMSP_1, EUCLIDLP, SIN_COS, COMPLEX2, XXREAL_1, PROJPL_1, EUCLID12, RUSUB_5, EUCLID_6, SIN_COS9, XCMPLX_0, SQUARE_1, EUCLID13; notations INT_1, EUCLIDLP, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, FINSEQ_2, RVSUM_1, PRE_TOPC, XXREAL_0, RLVECT_1, RLTOPSP1, EUCLID, EUCLID_4, SIN_COS, EUCLID_3, EUCLID_6, RCOMP_1, MENELAUS, ORDINAL1, SIN_COS4, SIN_COS9, EUCLID12, SQUARE_1, COMPLEX1; constructors EUCLID_4, MONOID_0, SIN_COS, EUCLID_3, MENELAUS, EUCLID_6, SIN_COS9, RCOMP_1, SIN_COS4, EUCLID12, SQUARE_1, COMPLEX1; registrations INT_1, MONOID_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, EUCLID, VALUED_0, ORDINAL1, EUCLIDLP, SIN_COS, SIN_COS9, XCMPLX_0, NAT_1, XBOOLE_0, SQUARE_1; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminaries reserve n for Nat; reserve i for Integer; reserve r,s,t for Real; reserve An,Bn,Cn,Dn for Point of TOP-REAL n; reserve L1,L2 for Element of line_of_REAL n; reserve A,B,C for Point of TOP-REAL 2; theorem :: EUCLID13:1 0 < i * r < r implies i = 1; theorem :: EUCLID13:2 for i being Integer st (-3)/2 < i < 1/2 holds i = 0 or i = -1; theorem :: EUCLID13:3 r is non zero & s is non zero & t is non zero implies ((-r) / (-s)) * ((-t)/(-r)) * ((-s)/(-t)) = 1; theorem :: EUCLID13:4 0 < r < 2 * PI implies sin (r/2) <> 0; theorem :: EUCLID13:5 -2 * PI < r < 0 implies sin (r/2) <> 0; theorem :: EUCLID13:6 tan (2*PI - r) = - tan r; theorem :: EUCLID13:7 An in Line(Bn,Cn) & An <> Cn implies Line(Bn,Cn) = Line(An,Cn); theorem :: EUCLID13:8 An <> Cn & An in Line(Bn,Cn) implies Bn in Line(An,Cn); theorem :: EUCLID13:9 An <> Bn & An <> Cn & |(An-Bn,An-Cn)| = 0 & L1 = Line(An,Bn) & L2 = Line(An,Cn) implies L1 _|_ L2; theorem :: EUCLID13:10 Bn <> Cn & |(Bn-An,Bn-Cn)| = 0 implies An <> Cn; theorem :: EUCLID13:11 |(An-Bn,An-Cn)| = |(Bn-An,Cn-An)|; theorem :: EUCLID13:12 Bn <> Cn & r = -(|(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)|)/|(Bn-Cn,Bn-Cn)|& Dn = r * Bn + (1 - r) * Cn implies |(Dn-An,Dn-Cn)| = 0; theorem :: EUCLID13:13 An <> Bn & Cn = r * An + (1-r) * Bn & Cn = Bn implies r = 0; theorem :: EUCLID13:14 |(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)| = |(Cn-An,Bn-Cn)| & |(Bn-Cn,Bn-Cn)|+|(Cn-An,Bn-Cn)| = |(Bn-Cn,Bn-An)|; theorem :: EUCLID13:15 |(An-Bn,An-Cn)| = - |(An-Bn,Cn-An)|; theorem :: EUCLID13:16 |(Bn-An,Cn-An)| = |(An-Bn,An-Cn)|; theorem :: EUCLID13:17 |(Bn-An,Cn-An)| = - |(Bn-An,An-Cn)|; theorem :: EUCLID13:18 Bn <> Cn & Cn <> An & An <> Bn & |(Cn-An,Bn-Cn)| is non zero & |(Bn-Cn,An-Bn)| is non zero & |(Cn-An,An-Bn)| is non 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)| implies r / (1-r) * s / (1-s) * t / (1-t) = 1; theorem :: EUCLID13:19 Cn = r * An + (1-r) * Bn & r = 1 implies Cn = An; theorem :: EUCLID13:20 Cn = r * An + (1-r) * Bn & r = 0 implies Cn = Bn; theorem :: EUCLID13:21 |(Bn-Cn,Bn-Cn)| = - |(Cn-An,Bn-Cn)| implies |(Bn-Cn,An-Bn)| = 0; theorem :: EUCLID13:22 Bn <> Cn & r = -(|(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)|)/|(Bn-Cn,Bn-Cn)| & r = 1 implies |(Bn-Cn,An-Bn)| = 0; theorem :: EUCLID13:23 A <> B & A <> C implies |.A - B.| + |.A - C.| <> 0; theorem :: EUCLID13:24 A,B,C is_a_triangle implies not A in Line(B,C); theorem :: EUCLID13:25 A <> B & B <> C & |(B-A,B-C)| = 0 implies angle(A,B,C)=PI/2 or angle(A,B,C)=3/2*PI; theorem :: EUCLID13:26 A,B,C is_a_triangle implies sin (angle(A,B,C)/2) > 0; theorem :: EUCLID13:27 angle(B,A,C) <> angle(C,B,A) implies sin ((angle(B,A,C) - angle(C,B,A))/2) <> 0; theorem :: EUCLID13:28 A,B,C is_a_triangle implies sin angle(A,B,C) <> 0; theorem :: EUCLID13:29 A,C,B is_a_triangle & angle(A,C,B) < PI implies angle(A,C,B) = PI - (angle(C,B,A) + angle(B,A,C)); theorem :: EUCLID13:30 A,C,B is_a_triangle & angle(A,C,B) < PI implies angle(B,A,C) + angle(C,B,A) = PI - angle(A,C,B); theorem :: EUCLID13:31 A,B,C is_a_triangle implies angle(B,A,C) - angle(C,B,A) <> PI; theorem :: EUCLID13:32 A,B,C is_a_triangle implies angle(B,A,C) - angle(C,B,A) <> -PI; theorem :: EUCLID13:33 A,B,C is_a_triangle implies (-2) * PI < angle(B,A,C) - angle(C,B,A) < 2 * PI; theorem :: EUCLID13:34 A,B,C is_a_triangle implies -PI < (angle(B,A,C) - angle(C,B,A))/2 < PI; theorem :: EUCLID13:35 A,B,C is_a_triangle & angle(B,A,C) < PI implies -PI < angle(B,A,C) - angle(C,B,A) < PI; theorem :: EUCLID13:36 A,B,C is_a_triangle & angle(B,A,C) < PI implies -PI/2 < (angle(B,A,C) - angle(C,B,A))/2 < PI/2; begin :: Orthocenter reserve D for Point of TOP-REAL 2; reserve a,b,c,d for Real; definition let A,B,C being Point of TOP-REAL 2; assume B <> C; func the_altitude(A,B,C) -> Element of line_of_REAL 2 means :: 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; end; theorem :: EUCLID13:37 B <> C implies A in the_altitude(A,B,C); theorem :: EUCLID13:38 B <> C implies the_altitude(A,B,C) is being_line; theorem :: EUCLID13:39 B <> C implies the_altitude(A,B,C) = the_altitude(A,C,B); theorem :: EUCLID13:40 B <> C & D in the_altitude(A,B,C) implies the_altitude(D,B,C) = the_altitude(A,B,C); theorem :: EUCLID13:41 B <> C & D in Line(B,C) & D <> C implies the_altitude(A,B,C) = the_altitude(A,D,C); definition let A,B,C being Point of TOP-REAL 2; assume B <> C; func the_foot_of_the_altitude(A,B,C) -> Point of TOP-REAL 2 means :: EUCLID13:def 2 ex P being Point of TOP-REAL 2 st it = P & the_altitude(A,B,C) /\ Line(B,C) = {P}; end; theorem :: EUCLID13:42 B <> C implies the_foot_of_the_altitude(A,B,C) = the_foot_of_the_altitude(A,C,B); theorem :: EUCLID13:43 B <> C implies 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); theorem :: EUCLID13:44 B <> C & not A in Line(B,C) implies the_altitude(A,B,C) = Line(A,the_foot_of_the_altitude(A,B,C)); theorem :: EUCLID13:45 B <> C & A in Line(B,C) implies the_foot_of_the_altitude(A,B,C) = A; theorem :: EUCLID13:46 B <> C & the_foot_of_the_altitude(A,B,C) = A implies A in Line(B,C); theorem :: EUCLID13:47 B <> C implies |(A - the_foot_of_the_altitude(A,B,C), B - C)| = 0; theorem :: EUCLID13:48 B <> C implies |(A - the_foot_of_the_altitude(A,B,C), B - the_foot_of_the_altitude(A,B,C))| = 0; theorem :: EUCLID13:49 B <> C implies |(A - the_foot_of_the_altitude(A,B,C), C - the_foot_of_the_altitude(A,B,C))| = 0; theorem :: EUCLID13:50 B <> C & B = the_foot_of_the_altitude(A,B,C) implies |(B-A,B-C)| = 0; theorem :: EUCLID13:51 B <> C & D in Line(B,C) & D <> C implies the_foot_of_the_altitude(A,B,C) = the_foot_of_the_altitude(A,D,C); theorem :: EUCLID13:52 B <> C & |(B-A,B-C)| = 0 implies B = the_foot_of_the_altitude(A,B,C); theorem :: EUCLID13:53 B <> C & B <> A & angle(A,B,C) = PI/2 implies the_foot_of_the_altitude(A,B,C) = B; theorem :: EUCLID13:54 A,B,C is_a_triangle implies A <> the_foot_of_the_altitude(A,B,C); theorem :: EUCLID13:55 A,B,C is_a_triangle & |(B-A,B-C)| <> 0 implies the_foot_of_the_altitude(A,B,C),B,A is_a_triangle; definition let A,B,C being Point of TOP-REAL 2; assume B <> C; func the_length_of_the_altitude(A,B,C) -> Real equals :: EUCLID13:def 3 |.A-the_foot_of_the_altitude(A,B,C).|; end; theorem :: EUCLID13:56 B <> C implies 0 <= the_length_of_the_altitude(A,B,C); theorem :: EUCLID13:57 B <> C implies the_length_of_the_altitude(A,B,C) = the_length_of_the_altitude(A,C,B); theorem :: EUCLID13:58 B <> C & |(B-A,B-C)| = 0 implies |.the_foot_of_the_altitude(A,B,C)-A.| = |.A-B.|; theorem :: EUCLID13:59 B <> C & r = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/|(B-C,B-C)|& D = r * B + (1 - r) * C & D <> C implies D = the_foot_of_the_altitude(A,B,C); theorem :: EUCLID13:60 B <> C & r = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/|(B-C,B-C)|& D = r * B + (1 - r) * C & D = C implies C = the_foot_of_the_altitude(A,B,C); theorem :: EUCLID13:61 A,B,C is_a_triangle & |(C-A,B-C)| is non zero & |(B-C,A-B)| is non zero & |(C-A,A-B)| is non 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; theorem :: EUCLID13:62 A,B,C is_a_triangle & |(C-A,B-C)| is zero implies the_foot_of_the_altitude(A,B,C) = C & the_foot_of_the_altitude(B,C,A) = C; theorem :: EUCLID13:63 A,B,C is_a_triangle & C in the_altitude(A,B,C) & C in the_altitude(B,C,A) implies the_altitude(A,B,C) /\ the_altitude(B,C,A) is being_point; theorem :: EUCLID13:64 B,C,A is_a_triangle & C in the_altitude(B,C,A) & C in the_altitude(C,A,B) implies the_altitude(B,C,A) /\ the_altitude(C,A,B) is being_point; theorem :: EUCLID13:65 C,A,B is_a_triangle & C in the_altitude(C,A,B) & C in the_altitude(A,B,C) implies the_altitude(C,A,B) /\ the_altitude(A,B,C) is being_point; theorem :: EUCLID13:66 A,B,C is_a_triangle & |(C-A,B-C)| = 0 implies 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}; theorem :: EUCLID13:67 A,B,C is_a_triangle implies 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}; definition let A,B,C being Point of TOP-REAL 2; assume 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}; end; begin :: Triangulation theorem :: EUCLID13:68 B <> A implies (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.|); theorem :: EUCLID13:69 B <> A implies 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.|); theorem :: EUCLID13:70 A,B,C is_a_triangle & angle(B,A,C) - angle(C,B,A) <> PI & angle(B,A,C) - angle(C,B,A) <> -PI implies cos ((angle(B,A,C) - angle(C,B,A))/2) <> 0; theorem :: EUCLID13:71 A,C,B is_a_triangle & angle(A,C,B) < PI implies tan ((angle(B,A,C) - angle(C,B,A))/2) = cot (angle(A,C,B) / 2) * ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|)); theorem :: EUCLID13:72 A,C,B is_a_triangle & angle(A,C,B) < PI implies (angle(B,A,C) - angle(C,B,A)) / 2 = arctan (cot (angle(A,C,B) / 2) * ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|))) ; theorem :: EUCLID13:73 A,C,B is_a_triangle & angle(A,C,B) < PI implies angle(B,A,C) - angle(C,B,A) = 2 * (arctan (cot (angle(A,C,B) / 2) * ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|)))); theorem :: EUCLID13:74 A,C,B is_a_triangle & angle(A,C,B) < PI implies 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.|))); theorem :: EUCLID13:75 A,C,B is_a_triangle & angle(A,C,B) < PI implies |.B-C.| = |.A-B.| * sin angle(B,A,C) / sin (angle(B,A,C) + angle(C,B,A)); theorem :: EUCLID13:76 A,C,B is_a_triangle & angle(A,C,B) < PI implies |.A-C.| = |.A-B.| * sin angle(C,B,A) / sin (angle(B,A,C) + angle(C,B,A)); theorem :: EUCLID13:77 A,C,B is_a_triangle & angle(C,A,B) = PI/2 implies the_length_of_the_altitude(C,A,B) = |.A-B.| * tan angle(A,B,C); theorem :: EUCLID13:78 A,B,C is_a_triangle & angle(C,A,B) = 3/2*PI implies the_length_of_the_altitude(C,A,B) = |.A-B.| * tan angle(C,B,A); theorem :: EUCLID13:79 A,C,B is_a_triangle & |(A-C,A-B)| = 0 implies the_length_of_the_altitude(C,A,B) = |.A-B.| * |. tan angle(A,B,C) .|; theorem :: EUCLID13:80 B <> C & the_foot_of_the_altitude(A,B,C),B,A is_a_triangle implies |.A-B.| * sin angle(A,B,the_foot_of_the_altitude(A,B,C)) = |.the_foot_of_the_altitude(A,B,C)-A.| or |.A-B.| * (- sin angle(A,B,the_foot_of_the_altitude(A,B,C))) = |.the_foot_of_the_altitude(A,B,C)-A.|; theorem :: EUCLID13:81 A,B,C is_a_triangle & |(B-A,B-C)| <> 0 implies |.A-B.| * sin angle(A,B,the_foot_of_the_altitude(A,B,C)) = |.the_foot_of_the_altitude(A,B,C)-A.| or |.A-B.| * (- sin angle(A,B,the_foot_of_the_altitude(A,B,C))) = |.the_foot_of_the_altitude(A,B,C)-A.|; :: C :: :: A f B :: C :: :: f A B :: C :: :: A B f theorem :: EUCLID13:82 A,C,B is_a_triangle & angle(A,C,B) < PI & |(A-C,A-B)| <> 0 implies 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))).|; theorem :: EUCLID13:83 0 < angle(B,A,D) < PI & 0 < angle(D,A,C) < PI & D,A,C are_mutually_distinct & B,A,D are_mutually_distinct implies angle(A,C,D) + angle(D,B,A) = 2 * PI - (angle(B,A,C) + angle(A,D,B) + angle(C,D,A)); :: B :: :: A :: :: D :: :: C theorem :: EUCLID13:84 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) implies |.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); theorem :: EUCLID13:85 sin(2*s) * cos d = cos (2*t) implies (r * cos s)^2 + (r * sin s)^2 - 2 * ( r * cos s) * ( r * sin s) * cos d = 2 * r^2 * (sin t)^2; theorem :: EUCLID13:86 for 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 < PI & sin (2*s) * cos d = cos(2*theta) holds |.D-C.| = |.A-B.| * sqrt 2 * R * sin theta; :: C :: :: B :: :: D A theorem :: EUCLID13:87 A,C,B is_a_triangle & angle(A,C,B) < PI & D,A,C is_a_triangle & angle(A,D,C)=PI/2 implies |.D-C.| = |.A-B.| * sin angle(C,B,A) / sin (angle(B,A,C) + angle(C,B,A)) * sin angle(C,A,D); :: C :: :: B :: :: A D theorem :: EUCLID13:88 B,C,A is_a_triangle & angle(B,C,A) < PI & D,C,A is_a_triangle & angle(C,D,A)=PI/2 implies |.D-C.| = |.A-B.| * sin angle(A,B,C) / sin (angle(A,B,C) + angle(C,A,B)) * sin angle(D,A,C); :: C :: :: D A B theorem :: EUCLID13:89 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 implies |.D-C.| = |.A-B.| * sin angle(C,B,A) / sin (angle(C,A,D) - angle(C,B,A)) * sin angle(C,A,D); :: C :: :: B A D theorem :: EUCLID13:90 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 implies |.D-C.| = |.A-B.| * sin angle(A,B,C) / sin (angle(D,A,C) - angle(A,B,C)) * sin angle(D,A,C);