:: Altitude, Orthocenter of a Triangle and Triangulation
:: by Roland Coghetto
::
:: Received December 30, 2015
:: Copyright (c) 2015-2026 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;
equalities EUCLID, EUCLID_4, VALUED_1, XCMPLX_0, SIN_COS4;
expansions TARSKI, EUCLID_4, XBOOLE_0, ZFMISC_1;
theorems ABSVALUE, EUCLID11, XBOOLE_0, XCMPLX_1, RVSUM_1, EUCLID_4, XREAL_1,
EUCLIDLP, TARSKI, EUCLID, EUCLID_3, EUCLID_6, MENELAUS, SIN_COS,
XXREAL_1, EUCLID10, ZFMISC_1, SIN_COS6, SIN_COS4, INT_1, BORSUK_7,
XXREAL_0, SIN_COS9, EUCLID_2, COMPTRIG, EUCLID12, SQUARE_1, SIN_COS5,
COMPLEX2;
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 Th1:
0 < i * r < r implies i = 1
proof
assume
A1: 0 < i * r < r;
assume not i = 1;
then 0 < 1 - i or 0 < i - 1 by XREAL_1:55;
then 0 + i < 1 - i + i or 0 + 1 < i - 1 + 1 by XREAL_1:8;
then per cases;
suppose i < 1;
then i <= 1 - 1 by INT_1:52;
hence contradiction by A1;
end;
suppose i > 1;
hence contradiction by A1,XREAL_1:155;
end;
end;
theorem Th2:
for i being Integer st (-3)/2 < i < 1/2 holds i = 0 or i = -1
proof
let i be Integer;
assume
A1: (-3)/2 < i < 1/2;
assume
A2: not (i=0 or i= -1);
(-2) < i < 1 by A1,XXREAL_0:2;
then
A3: (-2) + 1 <= i & i + 1 <= 1 & 0 <= 1 by INT_1:7;
then
A4: (-1) <= i & i + 1 - 1 <= 1 - 1 by XREAL_1:9;
consider k be Nat such that
A5: i = k or i = - k by INT_1:2;
per cases by A5;
suppose i = k;
hence contradiction by A2,A4;
end;
suppose
A6: i = - k;
then (-k) * (-1) <= (-1) * (-1) by A3,XREAL_1:65;
then k = 0 or ... or k = 1;
hence contradiction by A6,A2;
end;
end;
theorem Th3:
r is non zero & s is non zero & t is non zero implies
((-r) / (-s)) * ((-t)/(-r)) * ((-s)/(-t)) = 1
proof
assume that
A1: r is non zero and
A2: s is non zero and
A3: t is non zero;
((-r) / (-s)) * ((-t)/(-r)) * ((-s)/(-t))
= (r/s) * ((-t)/(-r)) * ((-s)/(-t)) by XCMPLX_1:191
.= (r/s) * (t/r) * ((-s)/(-t)) by XCMPLX_1:191
.= (r/s) * (t/r) * (s/t) by XCMPLX_1:191
.= r/r * s/s * t/t
.= 1* s/s * t/t by A1,XCMPLX_1:60
.= 1 * 1 * t/t by A2,XCMPLX_1:60
.= 1 * 1 * 1 by A3,XCMPLX_1:60;
hence thesis;
end;
theorem Th4:
0 < r < 2 * PI implies sin (r/2) <> 0
proof
assume
A1: 0 < r < 2 * PI;
assume
A2: sin(r/2) = 0;
consider i0 be Integer such that
A3: r / 2 = PI * i0 by A2,BORSUK_7:7;
A4: r = 2 * i0 * PI by A3;
reconsider p = 2*PI as Real;
0 < i0 * p < p by A1,A4;
then i0 = 1 by Th1;
hence thesis by A1,A3;
end;
theorem Th5:
-2 * PI < r < 0 implies sin (r/2) <> 0
proof
assume
A1: -2 * PI < r < 0;
assume
A2: sin(r/2) = 0;
0 * (-1) < r * (-1) & r * (-1) < (-2 * PI) * (-1) by A1,XREAL_1:69;
then
A3: sin ((-r)/2) <> 0 by Th4;
reconsider r0 = r/2 as Real;
sin (-r0) = - sin (r0) by SIN_COS:31;
hence contradiction by A2,A3;
end;
theorem Th6:
tan (2*PI - r) = - tan r
proof
tan (2*PI - r) = (- sin(r)) / cos(2*PI-r) by EUCLID10:3
.= - sin(r) / cos(2*PI-r)
.= - tan (r) by EUCLID10:4;
hence thesis;
end;
theorem Th7:
An in Line(Bn,Cn) & An <> Cn implies Line(Bn,Cn) = Line(An,Cn)
proof
assume that
A1: An in Line(Bn,Cn) and
A2: An <> Cn;
Cn in Line(Bn,Cn) & An in Line(Bn,Cn) by A1,EUCLID_4:41;
hence thesis by A2,EUCLID_4:43,EUCLID_4:42;
end;
theorem Th8:
An <> Cn & An in Line(Bn,Cn) implies Bn in Line(An,Cn)
proof
assume that
A1: An <> Cn and
A2: An in Line(Bn,Cn);
Cn in Line(Bn,Cn) by EUCLID_4:41;
then Line(Bn,Cn) c= Line(An,Cn) by A1,A2,EUCLID_4:43;
hence thesis by EUCLID_4:41;
end;
theorem Th9:
An <> Bn & An <> Cn & |(An-Bn,An-Cn)| = 0 & L1 = Line(An,Bn) &
L2 = Line(An,Cn) implies L1 _|_ L2
proof
assume that
A1: An <> Bn and
A2: An <> Cn and
A3: |(An-Bn,An-Cn)| = 0 and
A4: L1 = Line(An,Bn) and
A5: L2 = Line(An,Cn);
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
A6: L1 = Line(rA,rB) by A4,EUCLID12:4;
A7: L2 = Line(rA,rC) by A5,EUCLID12:4;
A8: (rA-rB)<>0*n by A1,EUCLIDLP:9;
A9: (rA-rC)<>0*n by A2,EUCLIDLP:9;
(rA-rB) _|_ (rA-rC) by A8,A9,EUCLIDLP:def 3,A3,RVSUM_1:def 17;
hence thesis by A6,A7,EUCLIDLP:def 8;
end;
theorem
Bn <> Cn & |(Bn-An,Bn-Cn)| = 0 implies An <> Cn
proof
assume that
A1: Bn <> Cn and
A2: |(Bn-An,Bn-Cn)| = 0;
assume
A3: An = Cn;
reconsider rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
(rB-rC) = 0*n by A2,A3,EUCLID_4:17;
hence contradiction by A1,EUCLIDLP:9;
end;
theorem Th10:
|(An-Bn,An-Cn)| = |(Bn-An,Cn-An)|
proof
A1: |(An - Bn, An-Cn)| = |(-(An - Bn),-(An - Cn))| by EUCLID_2:23;
-(An-Bn)=Bn-An & -(Cn-An)=An-Cn by RVSUM_1:35;
hence thesis by A1;
end;
theorem Th11:
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
proof
assume that
A1: Bn <> Cn and
A2: r = -(|(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)|)/|(Bn-Cn,Bn-Cn)| and
A3: Dn = r * Bn + (1 - r) * Cn;
reconsider rA=An,rB=Bn,rC=Cn,rD=Dn as Element of REAL n by EUCLID:22;
reconsider rrB=r * rB,rrC=(1-r)*rC as Element of REAL n;
A4: |(rrB,rrB)| = r * |(rB,rrB)| by EUCLID_4:21
.= r * (r * |(rB,rB)|) by EUCLID_4:22
.= r * r * |(rB,rB)|;
A5: |(rrB,rrC)| = r * |(rB,rrC)| by EUCLID_4:21
.= r * ((1-r) * |(rB,rC)|) by EUCLID_4:22
.= r * (1-r) * |(rB,rC)|;
A6: |(rrC,rrC)| = (1 - r) * |(rC,rrC)| by EUCLID_4:21
.= (1 - r) * ((1-r) * |(rC,rC)|) by EUCLID_4:22
.= (1 - r) * (1-r) * |(rC,rC)|;
A7: |(rD,rD)| = |( rrB,rrB )| + 2 * |( rrB,rrC )|+ |( rrC,rrC )|
by A3,RVSUM_1:138
.= r * r * |(rB,rB)| + 2 * r * (1-r) * |(rB,rC)| + (1 - r) * (1-r)
* |(rC,rC)| by A4,A5,A6;
A8: |(rD,rC)| = |(rrB, rC)| + |(rrC,rC)| by A3,EUCLID_4:20
.= r * |(rB,rC)| + |(rrC,rC)| by EUCLID_4:21
.= r * |(rB,rC)| + (1-r) * |(rC,rC)| by EUCLID_4:21;
A9: |(rA,rD)| = |(rA,rrB)| + |(rA,rrC)| by A3,EUCLID_4:28
.= r * |(rA,rB)| + |(rA,rrC)| by EUCLID_4:22
.= r * |(rA,rB)| + (1-r) * |(rA,rC)| by EUCLID_4:22;
A10: |(rB,rB)| -2*|(rB,rC)| + |(rC,rC)| = |(rB-rC,rB-rC)| by RVSUM_1:139;
A11: rB - rC <> 0*n by A1,EUCLIDLP:9;
A12: r * |(rB-rC,rB-rC)| + |(rB,rC)| -|(rC,rC)| -|(rA,rB)|+|(rA,rC)|
= -(|(rB,rC)| -|(rC,rC)| -|(rA,rB)|+|(rA,rC)|)/|(rB-rC,rB-rC)|
* |(rB-rC,rB-rC)| + |(rB,rC)| -|(rC,rC)| -|(rA,rB)|+|(rA,rC)| by A2
.= -(|(rB,rC)| -|(rC,rC)| -|(rA,rB)|+|(rA,rC)|) + |(rB,rC)|
- |(rC,rC)| -|(rA,rB)|+|(rA,rC)| by A11,EUCLID_4:17,XCMPLX_1:87
.= 0;
|(rD - rA, rD - rC)| = r * r * |(rB,rB)| + 2 * r * |(rB,rC)|
- 2 * r * r * |(rB,rC)| + (|(rC,rC)|
- 2 * r * |(rC,rC)| + r * r * |(rC,rC)|)
- (r * |(rB,rC)| + (1-r) * |(rC,rC)|)
- (r * |(rA,rB)| + (1-r) * |(rA,rC)|)
+ |(rA,rC)| by A9,A7,A8,RVSUM_1:137
.= r * (r * |(rB,rB)| + |(rB,rC)| - 2 * r * |(rB,rC)|
+ r*|(rC,rC)| - |(rC,rC)| -|(rA,rB)|+|(rA,rC)|)
.= 0 by A10,A12;
hence thesis;
end;
theorem Th12:
An <> Bn & Cn = r * An + (1-r) * Bn & Cn = Bn implies r = 0
proof
assume that
A1: An <> Bn and
A2: Cn = r * An + (1-r) * Bn and
A3: Cn = Bn;
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
rC = r * rA + (1 * rB - r * rB) by A2,EUCLIDLP:11
.= r * rA + (-r * rB) + 1 * rB by RVSUM_1:15
.= r * rA - r * rB + 1 * rB;
then 0*n + rB = r * rA - r * rB + 1 * rB by A3,EUCLID_4:1
.= (r * rA - r * rB) + rB by EUCLID_4:3;
then 0*n = r * rA - r * rB by RVSUM_1:25;
then r * (rA-rB) = 0*n by EUCLIDLP:12;
then r = 0 or rA-rB=0*n by EUCLID_4:5;
hence thesis by A1,EUCLIDLP:9;
end;
theorem Th13:
|(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
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
(rB-rC) + (rC-rA) = (rB-rC+rC)-rA by RVSUM_1:40
.= rB-rA by RVSUM_1:43;
hence thesis by EUCLID_4:28,EUCLID_4:31;
end;
theorem Th14:
|(An-Bn,An-Cn)| = - |(An-Bn,Cn-An)|
proof
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
|(rA-rB,rA-rC)| = |(rA-rB,-(rC-rA))| by RVSUM_1:35
.= - |(rA-rB,rC-rA)| by EUCLID_4:24;
hence thesis;
end;
theorem Th15:
|(Bn-An,Cn-An)| = |(An-Bn,An-Cn)|
proof
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
|(rB-rA,rC-rA)| = |(-(rA-rB),rC-rA)| by RVSUM_1:35
.= |(-(rA-rB),-(rA-rC))| by RVSUM_1:35
.= |(rA-rB,rA-rC)| by EUCLID_4:25;
hence thesis;
end;
theorem Th16:
|(Bn-An,Cn-An)| = - |(Bn-An,An-Cn)|
proof
|(Bn-An,Cn-An)| = |(An-Bn,An-Cn)| by Th15;
hence thesis by Th14;
end;
theorem Th17:
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
proof
assume that
A1: Bn <> Cn and
A2: Cn <> An and
A3: An <> Bn and
A4: |(Cn-An,Bn-Cn)| is non zero & |(Bn-Cn,An-Bn)| is non zero &
|(Cn-An,An-Bn)| is non zero and
A5: r = -(|(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)|)/|(Bn-Cn,Bn-Cn)| and
A6: s = -(|(Cn,An)| -|(An,An)| -|(Bn,Cn)|+|(Bn,An)|)/|(Cn-An,Cn-An)| and
A7: t = -(|(An,Bn)| -|(Bn,Bn)| -|(Cn,An)|+|(Cn,Bn)|)/|(An-Bn,An-Bn)|;
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
A8: rB - rC <> 0*n by A1,EUCLIDLP:9;
A9: rC - rA <> 0*n by A2,EUCLIDLP:9;
A10: rA - rB <> 0*n by A3,EUCLIDLP:9;
set rBC = |(Bn-Cn,Bn-Cn)|, rCA = |(Cn-An,Cn-An)|,rAB=|(An-Bn,An-Bn)|,
A = An, B = Bn, C = Cn;
A11: r * rBC = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/rBC*rBC by A5
.= -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)
by A8,EUCLID_4:17,XCMPLX_1:87;
(r / (1-r)) = (r /(1-r)) * rBC / rBC by A8,EUCLID_4:17,XCMPLX_1:89
.= r * rBC / (1-r) /rBC
.= r * rBC / ((1-r)*rBC) by XCMPLX_1:78
.= (-(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)) /
(|(B-C,B-C)|+ |(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|) by A11;
then
A12: r/(1-r) = (-|(C-A,B-C)|)/(|(B-C,B-C)|
+ (|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)) by Th13
.= (-|(C-A,B-C)|)/(|(B-C,B-C)|+ |(C-A,B-C)|) by Th13
.= (-|(C-A,B-C)|)/(|(B-C,B-A)|) by Th13;
A13: s * rCA = -(|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)/rCA*rCA by A6
.= -(|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)
by A9,EUCLID_4:17,XCMPLX_1:87;
(s / (1-s)) = (s /(1-s)) * rCA / rCA by A9,EUCLID_4:17,XCMPLX_1:89
.= s * rCA / (1-s) /rCA
.= s * rCA / ((1-s)*rCA) by XCMPLX_1:78
.= (-(|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)) /
(|(C-A,C-A)|+ (|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)) by A13;
then
A14: s/(1-s) = (-|(C-A,A-B)|)/(|(C-A,C-A)|
+ (|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)) by Th13
.= (-|(C-A,A-B)|)/(|(C-A,C-A)|+ |(C-A,A-B)|) by Th13
.= (-|(C-A,A-B)|)/(|(C-A,C-B)|) by Th13;
A15: t * rAB = -(|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|)/rAB*rAB by A7
.= -(|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|)
by A10,EUCLID_4:17,XCMPLX_1:87;
(t / (1-t)) = (t /(1-t)) * rAB / rAB by A10,EUCLID_4:17,XCMPLX_1:89
.= t * rAB / (1-t) /rAB
.= t * rAB / ((1-t)*rAB) by XCMPLX_1:78
.= (-(|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|))
/ (|(A-B,A-B)|+ (|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|)) by A15;
then
A16: t/(1-t) = (-|(A-B,B-C)|)/(|(A-B,A-B)|
+ (|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|)) by Th13
.= (-|(A-B,B-C)|)/(|(A-B,A-B)|+ |(A-B,B-C)|) by Th13
.= (-|(A-B,B-C)|)/(|(A-B,A-C)|) by Th13;
r/(1-r)*s/(1-s)*t/(1-t) = ((-|(C-A,B-C)|)/(|(B-C,B-A)|))
* ((-|(C-A,A-B)|)/(|(C-A,C-B)|))
* ((-|(A-B,B-C)|)/(|(A-B,A-C)|)) by A12,A14,A16
.= ((-|(C-A,B-C)|)/(-(|(B-C,A-B)|)))
* ((-|(C-A,A-B)|)/(|(C-A,C-B)|))
* ((-|(A-B,B-C)|)/(|(A-B,A-C)|)) by Th14
.= ((-|(C-A,B-C)|)/(-(|(B-C,A-B)|)))
* ((-|(C-A,A-B)|)/(-(|(C-A,B-C)|)))
* ((-|(A-B,B-C)|)/(|(A-B,A-C)|)) by Th14
.= ((-|(C-A,B-C)|)/(-(|(B-C,A-B)|)))
* ((-|(C-A,A-B)|)/(-(|(C-A,B-C)|)))
* ((-|(B-C,A-B)|)/(-(|(C-A,A-B)|))) by Th14
.= 1 by A4,Th3;
hence thesis;
end;
theorem
Cn = r * An + (1-r) * Bn & r = 1 implies Cn = An
proof
assume that
A1: Cn = r * An + (1-r) * Bn and
A2: r = 1;
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
rC = rA + 0 * rB by A1,A2,EUCLID_4:3;
then rC = rA + 0*n by EUCLID_4:3;
hence thesis by EUCLID_4:1;
end;
theorem
Cn = r * An + (1-r) * Bn & r = 0 implies Cn = Bn
proof
assume that
A1: Cn = r * An + (1-r) * Bn and
A2: r = 0;
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
rC = 0 * rA + (1-0) * rB by A1,A2;
then rC = 0*n + 1 * rB by EUCLID_4:3;
then rC = 1 * rB by EUCLID_4:1;
hence thesis by EUCLID_4:3;
end;
theorem Th18:
|(Bn-Cn,Bn-Cn)| = - |(Cn-An,Bn-Cn)| implies |(Bn-Cn,An-Bn)| = 0
proof
assume
A1: |(Bn-Cn,Bn-Cn)| = - |(Cn-An,Bn-Cn)|;
reconsider rA=An,rB=Bn,rC=Cn as Element of REAL n by EUCLID:22;
|(rB-rC,rB-rC)| + |(rB-rC,rC-rA)| =0 by A1;
then |(rB-rC,(rB-rC)+(rC-rA))| = 0 by EUCLID_4:28;
then |(rB-rC,(rB-rC)+rC-rA)| = 0 by RVSUM_1:40;
then |(Bn-Cn,Bn-An)| = 0 by RVSUM_1:43;
then - |(Bn-Cn,An-Bn)| = 0 by Th14;
hence thesis;
end;
theorem Th19:
Bn <> Cn & r = -(|(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)|)/|(Bn-Cn,Bn-Cn)| &
r = 1 implies |(Bn-Cn,An-Bn)| = 0
proof
assume that
A1: Bn <> Cn and
A2: r = -(|(Bn,Cn)| -|(Cn,Cn)| -|(An,Bn)|+|(An,Cn)|)/|(Bn-Cn,Bn-Cn)| and
A3: r = 1;
set A = An, B = Bn, C = Cn;
reconsider rB=B,rC=C as Element of REAL n by EUCLID:22;
A4: rB - rC <> 0*n by A1,EUCLIDLP:9;
1 * |(B-C,B-C)| = (-(|(C-A,B-C)|)/|(B-C,B-C)|)*|(B-C,B-C)| by A3,A2,Th13;
then |(B-C,B-C)| = -(|(C-A,B-C)|)/|(B-C,B-C)|*|(B-C,B-C)|;
then |(B-C,B-C)| = -(|(C-A,B-C)|) by A4,EUCLID_4:17,XCMPLX_1:87;
hence thesis by Th18;
end;
theorem
A <> B & A <> C implies |.A - B.| + |.A - C.| <> 0
proof
assume A <> B & A <> C;
then |.A - B.| <> 0 & |.A - C.| <> 0 by EUCLID_6:42;
hence thesis;
end;
theorem Th20:
A,B,C is_a_triangle implies not A in Line(B,C)
proof
assume
A1: A,B,C is_a_triangle;
then
A2: A,B,C are_mutually_distinct by EUCLID_6:20;
assume A in Line(B,C);
hence thesis by A1,A2,MENELAUS:13;
end;
theorem
A <> B & B <> C & |(B-A,B-C)| = 0 implies angle(A,B,C)=PI/2 or
angle(A,B,C)=3/2*PI
proof
assume that
A1: A <> B and
A2: B <> C and
A3: |(B-A,B-C)| = 0;
|(A-B,C-B)| = |( -(A-B), -(C-B) )| by EUCLID_2:23
.= |( B-A, -(C-B) )| by RVSUM_1:35
.= 0 by A3,RVSUM_1:35;
hence thesis by A1,A2,EUCLID_3:45;
end;
theorem Th21:
A,B,C is_a_triangle implies sin (angle(A,B,C)/2) > 0
proof
assume
A1: A,B,C is_a_triangle;
0 <= angle(A,B,C) < 2 * PI by EUCLID11:2;
then 0 < angle(A,B,C) < 2 * PI by A1,EUCLID10:30;
then 0 / 2 < angle(A,B,C) / 2 < 2 * PI / 2 by XREAL_1:74;
then 2*PI*0 < angle(A,B,C)/2 < PI + 2*PI*0;
hence thesis by SIN_COS6:11;
end;
theorem
angle(B,A,C) <> angle(C,B,A) implies
sin ((angle(B,A,C) - angle(C,B,A))/2) <> 0
proof
assume
A1: angle(B,A,C) <> angle(C,B,A);
assume
A2: sin ((angle(B,A,C) - angle(C,B,A))/2) = 0;
then
consider i0 be Integer such that
A3: (angle(B,A,C) - angle(C,B,A))/2 = PI * i0 by BORSUK_7:7;
set a = angle(B,A,C) - angle(C,B,A);
A4: 0 <= angle(B,A,C) < 2 * PI & 0 <= angle(C,B,A) < 2 * PI by EUCLID11:2;
A5: 0 - (2*PI) < 0 - angle(C,B,A) by EUCLID11:2,XREAL_1:10;
per cases;
suppose i0 = 0;
hence contradiction by A3,A1;
end;
suppose
A6: i0 < 0;
PI in ]. 0, 4 .[ by SIN_COS:def 28;
then 0 < PI by XXREAL_1:4;
then
A7: a < 0 by A3,A6;
- 2 * PI < a by A5,EUCLID11:2,XREAL_1:8;
hence contradiction by A2,A7,Th5;
end;
suppose
A8: i0 > 0;
0 < a < 2 * PI
proof
thus 0 < a by A3,A8,COMPTRIG:5;
angle(B,A,C) - angle(C,B,A) < 2 * PI - 0 by A4,XREAL_1:14;
hence a < 2 * PI;
end;
hence contradiction by A2,Th4;
end;
end;
theorem Th22:
A,B,C is_a_triangle implies sin angle(A,B,C) <> 0
proof
assume
A1: A,B,C is_a_triangle;
assume
A2: sin angle(A,B,C) = 0;
the_area_of_polygon3(C,B,A)
= |.C-B.| * |.A-B.| * sin angle (A,B,C) /2 by EUCLID_6:5
.= 0 by A2;
then not C,B,A is_a_triangle by MENELAUS:9;
hence thesis by A1,MENELAUS:15;
end;
theorem Th23:
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))
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI;
A,C,B are_mutually_distinct by A1,EUCLID_6:20;
then angle(A,C,B) + angle (C,B,A) + angle (B,A,C) = PI by A2,EUCLID_3:47;
hence thesis;
end;
theorem Th24:
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)
proof
assume A,C,B is_a_triangle & angle(A,C,B) < PI;
then angle(A,C,B) = PI - (angle(C,B,A) + angle(B,A,C)) by Th23;
hence thesis;
end;
theorem Th25:
A,B,C is_a_triangle implies angle(B,A,C) - angle(C,B,A) <> PI
proof
assume
A1: A,B,C is_a_triangle;
then B,A,C is_a_triangle by MENELAUS:15;
then A1A: B,A,C are_mutually_distinct by EUCLID_6:20;
assume
A2: angle(B,A,C) - angle(C,B,A) = PI;
per cases by EUCLID11:3;
suppose
A3: 0 <= angle(B,A,C) < PI;
angle(B,A,C) - PI = angle(C,B,A) by A2;
hence contradiction by A3,XREAL_1:49,EUCLID11:2;
end;
suppose angle(B,A,C) = PI;
then angle(C,B,A) = 0 by A2;
hence contradiction by A1,EUCLID10:30;
end;
suppose
A4: PI < angle(B,A,C) < 2 * PI;
then angle(B,A,C) - PI < 2 * PI - PI by XREAL_1:14;
hence contradiction by A1A,A2,A4,EUCLID11:8;
end;
end;
theorem Th26:
A,B,C is_a_triangle implies angle(B,A,C) - angle(C,B,A) <> -PI
proof
assume
A1: A,B,C is_a_triangle;
then B,A,C is_a_triangle by MENELAUS:15;
then
A2: B,A,C are_mutually_distinct by EUCLID_6:20;
assume
A3: angle(B,A,C) - angle(C,B,A) = -PI;
per cases by EUCLID11:3;
suppose 0 <= angle(B,A,C) < PI;
then
A4: 0 < angle(B,A,C) < PI by A1,EUCLID10:30;
then 0 + PI < angle(B,A,C) + PI by XREAL_1:8;
hence contradiction by A3,A4,A2,EUCLID11:5;
end;
suppose angle(B,A,C) = PI;
hence contradiction by A3,EUCLID11:2;
end;
suppose PI < angle(B,A,C) < 2 * PI;
then PI + PI < angle(B,A,C) + PI by XREAL_1:8;
hence contradiction by A3,EUCLID11:2;
end;
end;
theorem Th27:
A,B,C is_a_triangle implies (-2) * PI < angle(B,A,C) - angle(C,B,A) < 2 * PI
proof
assume
A1: A,B,C is_a_triangle;
A2: 0 <= angle(B,A,C) < 2 * PI & 0 <= angle(C,B,A) < 2 * PI
by EUCLID11:2;
then
A3: 0 < angle(B,A,C) < 2 * PI & 0 < angle(C,B,A) < 2 * PI
by A1,EUCLID10:30;
0 - 2*PI < angle(B,A,C)-angle(C,B,A) by A3,XREAL_1:14;
hence (-2) * PI < angle(B,A,C)-angle(C,B,A);
angle(B,A,C) - angle(C,B,A) < 2 * PI - 0 by A2,XREAL_1:14;
hence thesis;
end;
theorem
A,B,C is_a_triangle implies -PI < (angle(B,A,C) - angle(C,B,A))/2 < PI
proof
assume A,B,C is_a_triangle;
then (-2) * PI < angle(B,A,C) - angle(C,B,A) < 2 * PI by Th27;
then (-2) * PI / 2 < (angle(B,A,C) - angle(C,B,A))/2 < (2 * PI) / 2
by XREAL_1:74;
hence thesis;
end;
theorem Th28:
A,B,C is_a_triangle & angle(B,A,C) < PI implies
-PI < angle(B,A,C) - angle(C,B,A) < PI
proof
assume that
A1: A,B,C is_a_triangle and
A2: angle(B,A,C) < PI;
B,A,C is_a_triangle by A1,MENELAUS:15;
then
A3: B,A,C are_mutually_distinct by EUCLID_6:20;
A4: 0 <= angle(B,A,C) & angle(B,A,C) is non zero by A1,EUCLID10:30,EUCLID11:2;
A5: 0 <= angle(B,A,C) < PI & 0 <= angle(C,B,A) < PI by A2,A4,A3,EUCLID11:5;
A6: 0 < angle(B,A,C) < PI & 0 < angle(C,B,A) < PI by A2,A4,A3,EUCLID11:5;
0 - PI < angle(B,A,C)-angle(C,B,A) by A6,XREAL_1:14;
hence -PI < angle(B,A,C)-angle(C,B,A);
angle(B,A,C) - angle(C,B,A) < PI - 0 by A5,XREAL_1:14;
hence thesis;
end;
theorem Th29:
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
proof
assume A,B,C is_a_triangle & angle(B,A,C) < PI;
then -PI < angle(B,A,C) - angle(C,B,A) < PI by Th28;
then (-PI) / 2 < (angle(B,A,C) - angle(C,B,A))/2 < PI / 2 by XREAL_1:74;
hence thesis;
end;
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
A1: B <> C;
func the_altitude(A,B,C) -> Element of line_of_REAL 2 means
:Def1:
ex L1,L2 being Element of line_of_REAL 2 st
it = L1 & L2 = Line(B,C) & A in L1 & L1 _|_ L2;
existence
proof
reconsider rA = A, rB = B, rC = C as Element of REAL 2 by EUCLID:22;
reconsider L2 = Line(rB,rC) as Element of line_of_REAL 2 by EUCLIDLP:47;
L2 is being_line by A1;
then consider L1 be Element of line_of_REAL 2 such that
A2: rA in L1 and
A3: L2 _|_ L1 by EUCLID12:47;
L2 = Line(B,C) by EUCLID12:4;
hence thesis by A2,A3;
end;
uniqueness
proof
let L1,L2 be Element of line_of_REAL 2 such that
A4: ex L11,L12 being Element of line_of_REAL 2 st L1 = L11 &
L12 = Line(B,C) & A in L11 & L11 _|_ L12 and
A5: ex L21,L22 being Element of line_of_REAL 2 st L2 = L21 &
L22 = Line(B,C) & A in L21 & L21 _|_ L22;
consider L11,L12 being Element of line_of_REAL 2 such that
A6: L1 = L11 and
A7: L12 = Line(B,C) and
A8: A in L11 and
A9: L11 _|_ L12 by A4;
consider L21,L22 being Element of line_of_REAL 2 such that
A10: L2 = L21 and
A11: L22 = Line(B,C) and
A12: A in L21 and
A13: L21 _|_ L22 by A5;
not L11 misses L21 by A8,A12,XBOOLE_0:def 4;
hence thesis by A6,A10,EUCLIDLP:71,A7,A11,EUCLID12:16,A9,A13,EUCLIDLP:111;
end;
end;
theorem Th30:
B <> C implies A in the_altitude(A,B,C)
proof
assume B <> C;
then consider L1,L2 be Element of line_of_REAL 2 such that
A1: the_altitude(A,B,C) = L1 and
L2 = Line(B,C) and
A2: A in L1 and
L1 _|_ L2 by Def1;
thus thesis by A1,A2;
end;
theorem Th31:
B <> C implies the_altitude(A,B,C) is being_line
proof
assume B <> C;
then consider L1,L2 be Element of line_of_REAL 2 such that
A1: the_altitude(A,B,C) = L1 and
L2 = Line(B,C) and
A in L1 and
A2: L1 _|_ L2 by Def1;
thus thesis by A1,A2,EUCLIDLP:67;
end;
theorem Th32:
B <> C implies the_altitude(A,B,C) = the_altitude(A,C,B)
proof
assume
A1: B <> C;
then consider L11,L12 being Element of line_of_REAL 2 such that
A2: the_altitude(A,B,C) = L11 and
A3: L12 = Line(B,C) and
A4: A in L11 and
A5: L11 _|_ L12 by Def1;
consider L21,L22 being Element of line_of_REAL 2 such that
A6: the_altitude(A,C,B) = L21 and
A7: L22 = Line(C,B) and
A8: A in L21 and
A9: L21 _|_ L22 by A1,Def1;
L11 // L21 by A5,A9,A3,A7,EUCLID12:16,EUCLIDLP:111;
hence thesis by A2,A6,A4,A8,XBOOLE_0:3,EUCLIDLP:71;
end;
theorem
B <> C & D in the_altitude(A,B,C) implies
the_altitude(D,B,C) = the_altitude(A,B,C)
proof
assume that
A1: B <> C and
A2: D in the_altitude(A,B,C);
consider L1,L2 being Element of line_of_REAL 2 such that
A3: the_altitude(A,B,C) = L1 and
A4: L2 = Line(B,C) and
A in L1 and
A5: L1 _|_ L2 by A1,Def1;
consider L11,L12 being Element of line_of_REAL 2 such that
A6: the_altitude(D,B,C) = L11 and
A7: L12 = Line(B,C) and
A8: D in L11 and
A9: L11 _|_ L12 by A1,Def1;
L1 // L11 & D in L1 & D in L11
by A2,A3,A8,A4,A7,A5,A9,EUCLID12:16,EUCLIDLP:111;
hence thesis by A3,A6,EUCLIDLP:71,XBOOLE_0:3;
end;
theorem Th33:
B <> C & D in Line(B,C) & D <> C implies
the_altitude(A,B,C) = the_altitude(A,D,C)
proof
assume that
A1: B <> C and
A2: D in Line(B,C) and
A3: D <> C;
consider L1,L2 being Element of line_of_REAL 2 such that
A4: the_altitude(A,B,C) = L1 and
A5: L2 = Line(B,C) and
A6: A in L1 and
A7: L1 _|_ L2 by A1,Def1;
consider L3,L4 being Element of line_of_REAL 2 such that
A8: the_altitude(A,D,C) = L3 and
A9: L4 = Line(D,C) and
A10: A in L3 and
A11: L3 _|_ L4 by A3,Def1;
A12: L2 = L4 by A2,A3,A5,A9,Th7;
L1 meets L3 by A6,A10,XBOOLE_0:def 4;
hence thesis by A4,A8,A7,A11,A12,EUCLIDLP:111,EUCLID12:16,EUCLIDLP:71;
end;
definition
let A,B,C being 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:
ex P being Point of TOP-REAL 2 st it = P &
the_altitude(A,B,C) /\ Line(B,C) = {P};
existence
proof
consider L1,L2 be Element of line_of_REAL 2 such that
A2: the_altitude(A,B,C) = L1 and
A3: L2 = Line(B,C) and
A in L1 and
A4: L1 _|_ L2 by A1,Def1;
consider x be Element of REAL 2 such that
A5: L1 /\ L2 = {x} by A4,EUCLID12:43;
reconsider P = x as Point of TOP-REAL 2 by EUCLID:22;
take P;
thus thesis by A2,A3,A5;
end;
uniqueness by ZFMISC_1:3;
end;
theorem Th34:
B <> C implies
the_foot_of_the_altitude(A,B,C) = the_foot_of_the_altitude(A,C,B)
proof
assume
A1: B <> C;
consider D being Point of TOP-REAL 2 such that
A2: the_foot_of_the_altitude(A,B,C) = D and
A3: the_altitude(A,B,C) /\ Line(B,C) = {D} by A1,Def2;
consider E being Point of TOP-REAL 2 such that
A4: the_foot_of_the_altitude(A,C,B) = E and
A5: the_altitude(A,C,B) /\ Line(C,B) = {E} by A1,Def2;
{D} = {E} by A3,A5,A1,Th32;
hence thesis by A2,A4,ZFMISC_1:3;
end;
theorem Th35:
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)
proof
assume B <> C;
then consider P be Point of TOP-REAL 2 such that
A1: P = the_foot_of_the_altitude(A,B,C) and
A2: the_altitude(A,B,C) /\ Line(B,C) = {P} by Def2;
P in {P} by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 4;
end;
theorem Th36:
B <> C & not A in Line(B,C) implies
the_altitude(A,B,C) = Line(A,the_foot_of_the_altitude(A,B,C))
proof
assume that
A1: B <> C and
A2: not A in Line(B,C);
consider L1,L2 being Element of line_of_REAL 2 such that
A3: the_altitude(A,B,C) = L1 and
A4: L2 = Line(B,C) and
A5: A in L1 and
A6: L1 _|_ L2 by A1,Def1;
consider P being Point of TOP-REAL 2 such that
A7: the_foot_of_the_altitude(A,B,C) = P and
A8: the_altitude(A,B,C) /\ Line(B,C) = {P} by A1,Def2;
reconsider rA = A, rP = P as Element of REAL 2 by EUCLID:22;
reconsider L3 = Line(rA,rP) as Element of line_of_REAL 2 by EUCLIDLP:47;
per cases;
suppose A = P;
then A in the_altitude(A,B,C) /\ Line(B,C) by A8,TARSKI:def 1;
hence thesis by A2,XBOOLE_0:def 4;
end;
suppose
A9: A <> P;
A in L1 & P in L1 & L1 is being_line by A6,A3,A5,A1,A7,Th35,EUCLIDLP:67;
then Line(A,P) = L1 by A9,EUCLID12:49;
then A in L3 & L3 _|_ L2 by A6,EUCLID12:4,EUCLID_4:9;
then L3 = the_altitude(A,B,C) & L3 = Line(A,P) by A1,A4,Def1,EUCLID12:4;
hence thesis by A7;
end;
end;
theorem Th37:
B <> C & A in Line(B,C) implies the_foot_of_the_altitude(A,B,C) = A
proof
assume that
A1: B <> C and
A2: A in Line(B,C);
consider P being Point of TOP-REAL 2 such that
A3: the_foot_of_the_altitude(A,B,C) = P and
A4: the_altitude(A,B,C) /\ Line(B,C) = {P} by A1,Def2;
consider L1,L2 being Element of line_of_REAL 2 such that
A5: the_altitude(A,B,C) = L1 and
A6: L2 = Line(B,C) and
A7: A in L1 and
L1 _|_ L2 by A1,Def1;
A in L1 /\ L2 by A6,A7,A2,XBOOLE_0:def 4;
hence thesis by A3,A4,A5,A6,TARSKI:def 1;
end;
theorem
B <> C & the_foot_of_the_altitude(A,B,C) = A implies A in Line(B,C) by Th35;
theorem Th38ThJ8:
B <> C implies |(A - the_foot_of_the_altitude(A,B,C), B - C)| = 0
proof
assume
A1: B <> C;
consider L1,L2 be Element of line_of_REAL 2 such that
A2: the_altitude(A,B,C) = L1 and
A3: L2 = Line(B,C) & A in L1 & L1 _|_ L2 by A1,Def1;
per cases;
suppose not A in Line(B,C);
then L1 _|_ L2 & L1 = Line(A,the_foot_of_the_altitude(A,B,C)) &
L2 = Line(B,C) by A1,A2,A3,Th36;
hence thesis by EUCLID12:48;
end;
suppose A in Line(B,C);
then
A4: the_foot_of_the_altitude(A,B,C) = A by A1,Th37;
|(A - the_foot_of_the_altitude(A,B,C), B - C)|
= |(A,B - C)| - |(the_foot_of_the_altitude(A,B,C),B-C)|
by EUCLID_2:27
.= 0 by A4;
hence thesis;
end;
end;
theorem Th39:
B <> C implies |(A - the_foot_of_the_altitude(A,B,C),
B - the_foot_of_the_altitude(A,B,C))| = 0
proof
assume
A1: B <> C;
consider L1,L2 be Element of line_of_REAL 2 such that
A2: the_altitude(A,B,C) = L1 and
A3: L2 = Line(B,C) & A in L1 & L1 _|_ L2 by A1,Def1;
per cases;
suppose
A4: B = the_foot_of_the_altitude(A,B,C);
|(A - the_foot_of_the_altitude(A,B,C),
B - the_foot_of_the_altitude(A,B,C))|
= |( A - the_foot_of_the_altitude(A,B,C), B )|
- |(A - the_foot_of_the_altitude(A,B,C),
the_foot_of_the_altitude(A,B,C))|
by EUCLID_2:27;
hence thesis by A4;
end;
suppose
A5: B <> the_foot_of_the_altitude(A,B,C);
A6: L2 is being_line by A3,EUCLIDLP:67;
the_foot_of_the_altitude(A,B,C) in Line(B,C) & B in Line(B,C) &
C in Line(B,C) by EUCLID_4:41,A1,Th35;
then
A7: Line(B,C) = Line(B,the_foot_of_the_altitude(A,B,C))
by A6,A5,A3,EUCLID12:49;
per cases;
suppose not A in Line(B,C);
then L1 _|_ L2 & L1 = Line(A,the_foot_of_the_altitude(A,B,C)) &
L2 = Line(B,C) by A1,A2,A3,Th36;
hence thesis by A7,EUCLID12:48;
end;
suppose A in Line(B,C);
then
A8: A = the_foot_of_the_altitude(A,B,C) by A1,Th37;
|(A - the_foot_of_the_altitude(A,B,C),
B - the_foot_of_the_altitude(A,B,C))|
= |(A,B - the_foot_of_the_altitude(A,B,C))|
- |(the_foot_of_the_altitude(A,B,C),
B - the_foot_of_the_altitude(A,B,C))| by EUCLID_2:27
.= 0 by A8;
hence thesis;
end;
end;
end;
theorem Th40:
B <> C implies |(A - the_foot_of_the_altitude(A,B,C),
C - the_foot_of_the_altitude(A,B,C))| = 0
proof
assume
A1: B <> C;
then the_foot_of_the_altitude(A,C,B)
= the_foot_of_the_altitude(A,B,C) by Th34;
hence thesis by A1,Th39;
end;
theorem Th41:
B <> C & B = the_foot_of_the_altitude(A,B,C) implies |(B-A,B-C)| = 0
proof
assume that
A1: B <> C and
A2: B = the_foot_of_the_altitude(A,B,C);
set ph = the_foot_of_the_altitude(A,B,C);
per cases;
suppose A,B,C is_a_triangle;
|(A - ph, C - ph)| = 0 by A1,Th40;
hence thesis by A2,Th10;
end;
suppose
A4: not A,B,C is_a_triangle;
consider P being Point of TOP-REAL 2 such that
A5: the_foot_of_the_altitude(A,B,C) = P and
A6: the_altitude(A,B,C) /\ Line(B,C) = {P} by A1,Def2;
consider L1,L2 being Element of line_of_REAL 2 such that
A7: the_altitude(A,B,C) = L1 and
L2 = Line(B,C) and
A8: A in L1 and
L1 _|_ L2 by A1,Def1;
A in Line(B,C) & B in Line(B,C) & A in the_altitude(A,B,C) &
B in the_altitude(A,B,C) by A1,A4,MENELAUS:13,A7,A8,Th35,A2;
then A in {the_foot_of_the_altitude(A,B,C)} by A5,A6,XBOOLE_0:def 4;
then A11: A = B by A2,TARSKI:def 1;
|(B-A,B-C)| = |(B,B-C)| - |(A,B-C)| by EUCLID_2:24
.= 0 by A11;
hence thesis;
end;
end;
theorem Th42:
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)
proof
assume that
A1: B <> C and
A2: D in Line(B,C) and
A3: D <> C;
consider P1 being Point of TOP-REAL 2 such that
A4: the_foot_of_the_altitude(A,B,C) = P1 and
A5: the_altitude(A,B,C) /\ Line(B,C) = {P1} by A1,Def2;
consider P2 being Point of TOP-REAL 2 such that
A6: the_foot_of_the_altitude(A,D,C) = P2 and
A7: the_altitude(A,D,C) /\ Line(D,C) = {P2} by A3,Def2;
Line(D,C) = Line(B,C) by A2,A3,Th7;
then {P1} = {P2} by A7,A5,A1,A2,A3,Th33;
hence thesis by A4,A6,ZFMISC_1:3;
end;
theorem Th43:
B <> C & |(B-A,B-C)| = 0 implies B = the_foot_of_the_altitude(A,B,C)
proof
assume that
A1: B <> C and
A2: |(B-A,B-C)| = 0;
set p = the_foot_of_the_altitude(A,B,C);
consider P being Point of TOP-REAL 2 such that
A3: p = P and
A4: the_altitude(A,B,C) /\ Line(B,C) = {P} by A1,Def2;
consider L1,L2 being Element of line_of_REAL 2 such that
A5: the_altitude(A,B,C) = L1 and
A6: L2 = Line(B,C) and
A7: A in L1 and
A8: L1 _|_ L2 by A1,Def1;
per cases;
suppose
A9: A = p;
A = B
proof
assume
A10: A <> B;
reconsider rA=A,rB=B,rC=C as Element of REAL 2 by EUCLID:22;
reconsider LBA=Line(rB,rA),LBC=Line(rB,rC) as
Element of line_of_REAL 2 by EUCLIDLP:47;
A11: Line(B,A)=Line(rB,rA) by EUCLID12:4;
then A in LBA & B in LBA by EUCLID_4:41;
then
A12: L1 meets LBA by A7,XBOOLE_0:def 4;
A <> B & B <> C & |(B-A,B-C)| = 0 & LBA = Line(B,A) &
LBC = Line(B,C) by A1,A2,A10,EUCLID12:4;
then LBA _|_ LBC & L1 _|_ LBC & LBA c= REAL 2 & L1 c= REAL 2 &
LBC c= REAL 2 by A6,A8,Th9;
then LBA = L1 by EUCLIDLP:111,EUCLID12:16,A12,EUCLIDLP:71;
then B in L1 & B in L2 by A6,A11,EUCLID_4:41;
then B in {P} by A4,A5,A6,XBOOLE_0:def 4;
hence contradiction by A10,A9,A3,TARSKI:def 1;
end;
hence thesis by A9;
end;
suppose
A13: A <> p;
A14: A <> B
proof
assume A = B;
then A in Line(B,C) by EUCLID_4:41;
hence contradiction by A13,A1,Th37;
end;
reconsider rA=A,rB=B,rC=C as Element of REAL 2 by EUCLID:22;
reconsider LBA=Line(rB,rA),LBC=Line(rB,rC) as
Element of line_of_REAL 2 by EUCLIDLP:47;
A15: Line(B,A)=Line(rB,rA) by EUCLID12:4;
then A in LBA & B in LBA by EUCLID_4:41;
then
A16: L1 meets LBA by A7,XBOOLE_0:def 4;
A <> B & B <> C & |(B-A,B-C)| = 0 & LBA = Line(B,A) &
LBC = Line(B,C) by A1,A2,A14,EUCLID12:4;
then LBA _|_ LBC & L1 _|_ LBC & LBA c= REAL 2 & L1 c= REAL 2 &
LBC c= REAL 2 by A6,A8,Th9;
then LBA = L1 by EUCLIDLP:111,EUCLID12:16,A16,EUCLIDLP:71;
then B in L1 & B in L2 by A6,A15,EUCLID_4:41;
then B in {P} by A4,A5,A6,XBOOLE_0:def 4;
hence thesis by A3,TARSKI:def 1;
end;
end;
theorem
B <> C & B <> A & angle(A,B,C) = PI/2 implies
the_foot_of_the_altitude(A,B,C) = B
proof
assume that
A1: B <> C and
A2: B <> A and
A3: angle(A,B,C) = PI/2;
|(A-B,C-B)| = 0 by A1,A2,A3,EUCLID_3:45;
then |(B-A,B-C)| = 0 by Th10;
hence thesis by A1,Th43;
end;
theorem Th44:
A,B,C is_a_triangle implies A <> the_foot_of_the_altitude(A,B,C)
proof
assume
A1: A,B,C is_a_triangle;
assume
A2: A = the_foot_of_the_altitude(A,B,C);
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
then A in Line(B,C) by A2,Th35;
hence contradiction by A1,A3,MENELAUS:13;
end;
theorem Th45:
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
proof
assume that
A1: A,B,C is_a_triangle and
A2: |(B-A,B-C)| <> 0;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
set p = the_foot_of_the_altitude(A,B,C);
consider P being Point of TOP-REAL 2 such that
A4: the_foot_of_the_altitude(A,B,C) = P and
A5: the_altitude(A,B,C) /\ Line(B,C) = {P} by A3,Def2;
consider L1,L2 being Element of line_of_REAL 2 such that
A6: the_altitude(A,B,C) = L1 and
A7: L2 = Line(B,C) and
A8: A in L1 and L1 _|_ L2 by A3,Def1;
A9: P <> B by A4,A3,A2,Th41;
A10: p <> A by A1,Th44;
A11: p,B,A are_mutually_distinct by A3,A2,Th41,A1,Th44;
P in Line(B,C) by A4,A3,Th35;
then B in Line(B,P) & C in Line(B,P) by A9,Th8,EUCLID_4:41;
then
A12: Line(B,P) c= Line(B,C) by A3,EUCLID_4:43;
A13: angle(p,B,A) <> PI
proof
assume angle(p,B,A) = PI;
then B in LSeg(p,A) by EUCLID_6:11;
then B in Line(P,A) by A4,MENELAUS:12;
then A in Line(B,P) by A3,A2,Th41,A4,Th8;
then A in L1 /\ L2 by A12,A8,A7,XBOOLE_0:def 4;
hence contradiction by A5,A6,A7,A4,A10,TARSKI:def 1;
end;
A14: angle(B,A,p) <> PI
proof
assume angle(B,A,p) = PI;
then A in LSeg(B,p) by EUCLID_6:11;
then A in L1 & A in L2 by A12,A8,A7,A4,MENELAUS:12;
then A in L1 /\ L2 by XBOOLE_0:def 4;
hence contradiction by A4,A10,A5,A6,A7,TARSKI:def 1;
end;
angle(A,p,B) <> PI
proof
assume angle(A,p,B) = PI;
then p in LSeg(A,B) by EUCLID_6:11;
then P in Line(A,B) by A4,MENELAUS:12;
then A in Line(B,P) by A9,Th8;
then A in L1 /\ L2 by A12,A8,A7,XBOOLE_0:def 4;
then A = P by A5,A6,A7,TARSKI:def 1;
hence contradiction by A4,A1,Th44;
end;
hence thesis by A11,A13,A14,EUCLID_6:20;
end;
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
:Def3:
|.A-the_foot_of_the_altitude(A,B,C).|;
correctness;
end;
theorem Th46:
B <> C implies 0 <= the_length_of_the_altitude(A,B,C)
proof
assume B <> C;
then the_length_of_the_altitude(A,B,C)
= |.A-the_foot_of_the_altitude(A,B,C).| by Def3;
hence thesis;
end;
theorem
B <> C implies
the_length_of_the_altitude(A,B,C) = the_length_of_the_altitude(A,C,B)
proof
assume
A1: B <> C;
then the_length_of_the_altitude(A,B,C)
= |.A - the_foot_of_the_altitude(A,B,C).| by Def3
.= |.A - the_foot_of_the_altitude(A,C,B).| by A1,Th34
.= the_length_of_the_altitude(A,C,B) by A1,Def3;
hence thesis;
end;
theorem Th47:
B <> C & |(B-A,B-C)| = 0 implies
|.the_foot_of_the_altitude(A,B,C)-A.| = |.A-B.|
proof
assume that
A1: B <> C and
A2: |(B-A,B-C)| = 0;
|.the_foot_of_the_altitude(A,B,C)-A.| = |.B-A.| by A1,A2,Th43;
hence thesis by EUCLID_6:43;
end;
theorem Th48:
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)
proof
assume that
A1: B <> C and
A2: r = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/|(B-C,B-C)| and
A3: D = r * B + (1 - r) * C and
A4: D <> C;
|(D-A,D-C)| = 0 by A1,A2,A3,Th11;
then
A5: D = the_foot_of_the_altitude(A,D,C) by A4,Th43;
reconsider rB = B, rC = C as Element of REAL 2 by EUCLID:22;
D in Line(B,C)
proof
D in Line(rC,rB) by A3;
hence thesis by EUCLID12:4;
end;
hence thesis by A1,A4,A5,Th42;
end;
theorem Th49:
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)
proof
assume that
A1: B <> C and
A2: r = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/|(B-C,B-C)| and
A3: D = r * B + (1 - r) * C and
A4: D = C;
reconsider rB=B,rC=C as Element of REAL 2 by EUCLID:22;
reconsider n = 2 as Nat;
A5: rB - rC <> 0*n by A1,EUCLIDLP:9;
0 = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/|(B-C,B-C)|
by A2,A1,A3,A4,Th12;
then 0 * |(B-C,B-C)| = -(|(C-A,B-C)|)/|(B-C,B-C)|*|(B-C,B-C)| by Th13;
then 0 = - |(C-A,B-C)| by A5,EUCLID_4:17,XCMPLX_1:87;
then |(C-A,C-B)| = 0 by Th14;
then C = the_foot_of_the_altitude(A,C,B) by A1,Th43;
hence thesis by A1,Th34;
end;
theorem Th50:
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
proof
assume that
A1: A,B,C is_a_triangle and
A2: |(C-A,B-C)| is non zero & |(B-C,A-B)| is non zero &
|(C-A,A-B)| is non zero;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
set r = -(|(B,C)| -|(C,C)| -|(A,B)|+|(A,C)|)/|(B-C,B-C)|,
s = -(|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)/|(C-A,C-A)|,
t = -(|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|)/|(A-B,A-B)|,
D = r * B + (1 - r) * C, E = s * C + (1 - s) * A,
F = t * A + (1 - t) * B;
D <> C & E <> A & F <> B
proof
assume not (D <> C & E <> A & F <> B);
then
A4: C = the_foot_of_the_altitude(A,B,C) or
A = the_foot_of_the_altitude(B,C,A) or
B = the_foot_of_the_altitude(C,A,B) by A3,Th49;
|(A-C,B-C)| = - |(C-A,B-C)| & |(B-A,C-A)| = - |(C-A,A-B)| &
|(C-B,A-B)| = - |(B-C,A-B)| by Th16;
hence contradiction by A4,A2,A3,Th38ThJ8;
end;
then
A5: D = the_foot_of_the_altitude(A,B,C) & E = the_foot_of_the_altitude(B,C,A) &
F = the_foot_of_the_altitude(C,A,B) by A3,Th48;
r/(1-r)*s/(1-s)*t/(1-t) = 1 by A3,A2,Th17;
then
A6: (r/(1-r))*(t/(1-t))*(s/(1-s)) = 1;
A7: A,C,B is_a_triangle by A1,MENELAUS:15;
r <> 1 & s <> 1 & t <> 1
proof
assume not (r <> 1 & s <> 1 & t <> 1);
then (r=1 & B <> C & r = -(|(B,C)| -|(C,C)| -|(A,B)|
+|(A,C)|)/|(B-C,B-C)| &
D = r * B + (1 - r) * C) or
(s = 1 & C <> A & s = -(|(C,A)| -|(A,A)| -|(B,C)|+|(B,A)|)/|(C-A,C-A)| &
E = s * C + (1 - s) * A) or
(t = 1 & A <> B & t = -(|(A,B)| -|(B,B)| -|(C,A)|+|(C,B)|)/|(A-B,A-B)| &
F = t * A + (1 - t) * B);
hence contradiction by A2,Th19;
end;
hence thesis by A5,A6,A7,MENELAUS:22;
end;
theorem Th51:
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
proof
assume that
A1: A,B,C is_a_triangle and
A2: |(C-A,B-C)| is zero;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
A4: - |( C - A, B - C )| = |(C-B,C-A)| by Th14;
|(C-A,C-B)| = - |(C-A,B-C)| by Th14;
then the_foot_of_the_altitude(A,C,B) = C by A2,A3,Th43;
hence thesis by A2,A3,A4,Th43,Th34;
end;
theorem Th52:
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
proof
assume that
A1: A,B,C is_a_triangle and
A2: C in the_altitude(A,B,C) and
A3: C in the_altitude(B,C,A);
A4: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
consider L1,L2 being Element of line_of_REAL 2 such that
A5: the_altitude(A,B,C) = L1 and
A6: L2 = Line(B,C) and A in L1 and
A7: L1 _|_ L2 by A4,Def1;
consider L3,L4 being Element of line_of_REAL 2 such that
A8: the_altitude(B,C,A) = L3 and
A9: L4 = Line(C,A) and B in L3 and
A10: L3 _|_ L4 by A4,Def1;
A11: not L1 // L3
proof
assume
A12: L1 // L3;
L1 <> L3
proof
assume L1 = L3;
then L1 _|_ L2 & L1 _|_ L4 & C in L1 & C in L2 & C in L4
by A6,A9,A7,A10,A2,A5,EUCLID_4:41;
then L2 = L4 by EUCLID12:16,EUCLIDLP:108;
then A in Line(B,C) by A6,A9,EUCLID_4:41;
hence contradiction by A1,A4,MENELAUS:13;
end;
hence contradiction by XBOOLE_0:3,A12,EUCLIDLP:71,A5,A8,A2,A3;
end;
not L1 is being_point & not L3 is being_point
by A4,A5,A8,Th31,EUCLID12:9;
hence thesis by A5,A8,A11,EUCLID12:21;
end;
theorem Th53:
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
proof
assume that
A1: B,C,A is_a_triangle and
A2: C in the_altitude(B,C,A) and
A3: C in the_altitude(C,A,B);
A4: B,C,A are_mutually_distinct by A1,EUCLID_6:20;
consider L1,L2 being Element of line_of_REAL 2 such that
A5: the_altitude(B,C,A) = L1 and
A6: L2 = Line(C,A) and
B in L1 and
A7: L1 _|_ L2 by A4,Def1;
consider L3,L4 being Element of line_of_REAL 2 such that
A8: the_altitude(C,A,B) = L3 and
A9: L4 = Line(A,B) and
C in L3 and
A10: L3 _|_ L4 by A4,Def1;
A11: not L1 // L3
proof
assume L1 // L3;
then L1 = L3 by EUCLIDLP:71,A2,A3,A5,A8,XBOOLE_0:3;
then
A12: L2 // L4 by A7,A10,EUCLIDLP:111,EUCLID12:16;
A in L2 & A in L4 by A6,A9,EUCLID_4:41;
then Line(C,A) = Line(A,B) by A6,A9,XBOOLE_0:3,A12,EUCLIDLP:71;
then B in Line(C,A) by EUCLID_4:41;
hence contradiction by A1,A4,MENELAUS:13;
end;
not L1 is being_point & not L3 is being_point
by A4,A5,A8,Th31,EUCLID12:9;
hence thesis by A5,A8,A11,EUCLID12:21;
end;
theorem Th54:
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
proof
assume that
A1: C,A,B is_a_triangle and
A2: C in the_altitude(C,A,B) and
A3: C in the_altitude(A,B,C);
A4: C,A,B are_mutually_distinct by A1,EUCLID_6:20;
consider L1,L2 being Element of line_of_REAL 2 such that
A5: the_altitude(C,A,B) = L1 and
A6: L2 = Line(A,B) and
C in L1 and
A7: L1 _|_ L2 by A4,Def1;
consider L3,L4 being Element of line_of_REAL 2 such that
A8: the_altitude(A,B,C) = L3 and
A9: L4 = Line(B,C) and
A in L3 and
A10: L3 _|_ L4 by A4,Def1;
A11: not L1 // L3
proof
assume L1 // L3;
then L1 = L3 by A2,A3,A5,A8,XBOOLE_0:3,EUCLIDLP:71;
then
A12: L2 // L4 by A7,A10,EUCLIDLP:111,EUCLID12:16;
B in L2 & B in L4 by A6,A9,EUCLID_4:41;
then Line(A,B) = Line(B,C) by A6,A9,XBOOLE_0:3,A12,EUCLIDLP:71;
then C in Line(A,B) by EUCLID_4:41;
hence contradiction by A4,MENELAUS:13,A1;
end;
not L1 is being_point & not L3 is being_point
by A4,A5,A8,Th31,EUCLID12:9;
hence thesis by A5,A8,A11,EUCLID12:21;
end;
theorem Th55:
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}
proof
assume that
A1: A,B,C is_a_triangle and
A2: |(C-A,B-C)| = 0;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
B,C,A is_a_triangle by A1,MENELAUS:15;
then
A4: not A in Line(B,C) & not B in Line(C,A) by A1,Th20;
the_foot_of_the_altitude(A,B,C) = C & the_foot_of_the_altitude(B,C,A) = C
by A1,A2,Th51;
then the_altitude(A,B,C) = Line(A,C) & the_altitude(B,C,A) = Line(B,C)
by A3,A4,Th36;
then
A5: C in the_altitude(A,B,C) & C in the_altitude(B,C,A) by EUCLID_4:41;
A6: C in the_altitude(C,A,B) by A3,Th30;
A7: the_altitude(A,B,C) /\ the_altitude(B,C,A) = {C}
proof
C in the_altitude(A,B,C) /\ the_altitude(B,C,A) by A5,XBOOLE_0:def 4;
hence thesis by EUCLID12:22,A1,A5,Th52;
end;
A8: the_altitude(B,C,A) /\ the_altitude(C,A,B) = {C}
proof
B,C,A is_a_triangle by A1,MENELAUS:15;
then
A9: the_altitude(B,C,A) /\ the_altitude(C,A,B) is being_point
by A5,A3,Th30,Th53;
C in the_altitude(B,C,A) /\ the_altitude(C,A,B) by A5,A6,XBOOLE_0:def 4;
hence thesis by A9,EUCLID12:22;
end;
the_altitude(C,A,B) /\ the_altitude(A,B,C) = {C}
proof
C,A,B is_a_triangle by A1,MENELAUS:15;
then
A10: the_altitude(C,A,B) /\ the_altitude(A,B,C) is being_point
by A5,A3,Th30,Th54;
C in the_altitude(C,A,B) /\ the_altitude(A,B,C) by A5,A6,XBOOLE_0:def 4;
hence thesis by A10,EUCLID12:22;
end;
hence thesis by A7,A8;
end;
theorem Th56:
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}
proof
assume
A1: A,B,C is_a_triangle;
per cases;
suppose
A2: |(C-A,B-C)| = 0;
take C;
thus thesis by A1,A2,Th55;
end;
suppose
A3: |(B-C,A-B)| = 0;
take B;
C,A,B is_a_triangle by A1,MENELAUS:15;
hence thesis by A3,Th55;
end;
suppose
A4: |(C-A,A-B)| = 0;
take A;
B,C,A is_a_triangle by A1,MENELAUS:15;
hence thesis by A4,Th55;
end;
suppose not |(C-A,B-C)| = 0 & not |(B-C,A-B)| = 0 & not |(C-A,A-B)| = 0;
then
A5: Line(A,the_foot_of_the_altitude(A,B,C)),
Line(C,the_foot_of_the_altitude(C,A,B)),
Line(B,the_foot_of_the_altitude(B,C,A)) are_concurrent by A1,Th50;
A6: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
A7: B,C,A is_a_triangle & C,A,B is_a_triangle by A1,MENELAUS:15;
then not A in Line(B,C) & not B in Line(C,A) & not C in Line(A,B)
by A1,Th20;
then
A8: the_altitude(A,B,C)=Line(A,the_foot_of_the_altitude(A,B,C)) &
the_altitude(C,A,B)=Line(C,the_foot_of_the_altitude(C,A,B)) &
the_altitude(B,C,A)=Line(B,the_foot_of_the_altitude(B,C,A)) by A6,Th36;
consider L1,L2 being Element of line_of_REAL 2 such that
A9: the_altitude(A,B,C) = L1 and
A10: L2 = Line(B,C) and
A in L1 and
A11: L1 _|_ L2 by A6,Def1;
consider L3,L4 being Element of line_of_REAL 2 such that
A12: the_altitude(C,A,B) = L3 and
A13: L4 = Line(A,B) and C in L3 and
A14: L3 _|_ L4 by A6,Def1;
consider L5,L6 being Element of line_of_REAL 2 such that
A15: the_altitude(B,C,A) = L5 and
A16: L6 = Line(C,A) and B in L5 and
A17: L5 _|_ L6 by A6,Def1;
A18: not (Line(A,the_foot_of_the_altitude(A,B,C)) is_parallel_to
Line(C,the_foot_of_the_altitude(C,A,B)))
proof
assume
A19: Line(A,the_foot_of_the_altitude(A,B,C)) is_parallel_to
Line(C,the_foot_of_the_altitude(C,A,B));
L1 is being_line & L3 is being_line & L1, L3 are_coplane
by A9,A12,A6,Th31,EUCLID12:39;
then L1 // L3 by A19,A8,A9,A12,EUCLIDLP:113;
then L1 _|_ L4 by A14,EUCLIDLP:61;
then
A20: L2 // L4 by A11,EUCLIDLP:111,EUCLID12:16;
B in L2 & B in L4 by A10,A13,EUCLID_4:41;
then Line(A,B) = Line(B,C) by A10,A13,A20,XBOOLE_0:3,EUCLIDLP:71;
then C in Line(A,B) by EUCLID_4:41;
hence contradiction by A7,A6,MENELAUS:13;
end;
consider D such that
A21: D in the_altitude(A,B,C) and
A22: D in the_altitude(C,A,B) and
A23: D in the_altitude(B,C,A) by A8,A18,A5,MENELAUS:def 1;
A24: D in L1 /\ L3 & D in L1/\L5 & D in L3/\L5
by A21,A22,A23,A9,A12,A15,XBOOLE_0:def 4;
A25: L1 meets L3 & L1 meets L5 & L3 meets L5
by A21,A22,A23,A9,A12,A15,XBOOLE_0:def 4;
L1 <> L3
proof
assume L1 = L3;
then
A26: L2 // L4 by A14,A11,EUCLIDLP:111,EUCLID12:16;
B in L2 & B in L4 by A10,A13,EUCLID_4:41;
then L2 = L4 by A26,XBOOLE_0:3,EUCLIDLP:71;
then C in Line(A,B) by A10,A13,EUCLID_4:41;
hence contradiction by A7,A6,MENELAUS:13;
end;
then
A27: not L1 // L3 by A25,EUCLIDLP:71;
not L1 is being_point & not L3 is being_point
by A9,A12,A6,Th31,EUCLID12:9;
then
A28: L1 /\ L3 = {D} by A24,EUCLID12:22,A27,EUCLID12:21;
L1 <> L5
proof
assume L1 = L5;
then
A29: L2 // L6 by A17,A11,EUCLIDLP:111,EUCLID12:16;
C in L2 & C in L6 by A16,A10,EUCLID_4:41;
then L2 = L6 by A29,XBOOLE_0:3,EUCLIDLP:71;
then A in Line(B,C) by A16,A10,EUCLID_4:41;
hence contradiction by A1,A6,MENELAUS:13;
end;
then
A30: not L1 // L5 by A25,EUCLIDLP:71;
not L1 is being_point & not L5 is being_point
by A15,A9,A6,Th31,EUCLID12:9;
then
A31: L1 /\ L5 = {D} by A24,EUCLID12:22,A30,EUCLID12:21;
L3 <> L5
proof
assume L3 = L5;
then
A32: L4 // L6 by A17,A14,EUCLIDLP:111,EUCLID12:16;
A in L4 & A in L6 by A16,A13,EUCLID_4:41;
then Line(A,B) = Line(C,A) by A16,A13,A32,XBOOLE_0:3,EUCLIDLP:71;
then C in Line(A,B) by EUCLID_4:41;
hence contradiction by A7,A6,MENELAUS:13;
end;
then
A33: not L3 // L5 by A25,EUCLIDLP:71;
not L3 is being_point & not L5 is being_point
by A15,A12,A6,Th31,EUCLID12:9;
then L3 /\ L5 = {D} by A24,EUCLID12:22,A33,EUCLID12:21;
hence thesis by A28,A31,A9,A12,A15;
end;
end;
definition
let A,B,C being 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
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 by A1,Th56;
uniqueness by ZFMISC_1:3;
end;
begin :: Triangulation
theorem Th57:
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.|)
proof
assume B<>A;
then |.C-B.| * sin angle(C,B,A) = |.C-A.| * sin angle(B,A,C) by EUCLID_6:6;
hence thesis;
end;
theorem Th58:
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.|)
proof
assume B<>A;
then
A1: (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.|) by Th57;
set BAC = angle(B,A,C), CBA = angle(C,B,A);
sin BAC + sin CBA = 2 * (cos((BAC-CBA)/2)*sin((BAC+CBA)/2)) by SIN_COS4:15;
then 2 * (cos ((BAC-CBA)/2) * sin((BAC+CBA)/2)) * (|.C-B.| - |.C-A.|)=
2 * (cos ((BAC+CBA)/2) * sin((BAC-CBA)/2))*(|.C-B.| + |.C-A.|)
by A1,SIN_COS4:16;
hence thesis;
end;
theorem Th59:
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
proof
assume that
A1: A,B,C is_a_triangle and
A2: angle(B,A,C) - angle(C,B,A) <> PI and
A3: angle(B,A,C) - angle(C,B,A) <> -PI;
assume
A4: cos((angle(B,A,C) - angle(C,B,A))/2) = 0;
consider i0 be Integer such that
A5: (angle(B,A,C) - angle(C,B,A))/2 = PI/2 + PI * i0 by A4,BORSUK_7:8;
set a = angle(B,A,C) - angle(C,B,A);
A6: 0 <= angle(B,A,C) < 2 * PI & 0 <= angle(C,B,A) < 2 * PI
by EUCLID11:2;
then
A7: 0 < angle(B,A,C) < 2 * PI & 0 < angle(C,B,A) < 2 * PI
by A1,EUCLID10:30;
A8: 0 - 2*PI < angle(B,A,C)-angle(C,B,A) by A7,XREAL_1:14;
angle(B,A,C) - angle(C,B,A) < 2 * PI - 0 by A6,XREAL_1:14;
then (-2)*PI/PI<(1+2*i0)*PI/PI<2*PI/PI & PI <> 0
by A8,A5,COMPTRIG:5,XREAL_1:74;
then (-2)*(PI/PI)<(1+2*i0)*(PI/PI)<2*(PI/PI) & PI/PI = 1 by XCMPLX_1:60;
then (-2) - 1 < 1 + 2 * i0 - 1< 2 - 1 by XREAL_1:14;
then (-3) / 2 < 2 * i0 / 2 < 1 / 2 by XREAL_1:74;
then i0 = 0 or i0 = -1 by Th2;
hence contradiction by A5,A2,A3;
end;
theorem Th60:
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.|))
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI;
A3: A,C,B are_mutually_distinct by A1,EUCLID_6:20;
A4: A,B,C is_a_triangle by A1,MENELAUS:15;
then
A5: (angle(B,A,C) - angle(C,B,A) <> PI & angle(B,A,C) - angle(C,B,A) <> -PI)
by Th25,Th26;
set alpha = (angle(B,A,C) - angle(C,B,A))/2,
beta = (angle(B,A,C) + angle(C,B,A))/2;
angle(A,C,B) = PI - (angle(C,B,A) + angle(B,A,C)) by A1,A2,Th23;
then
A8: beta = PI/2 - angle(A,C,B)/2;
set a2 = angle(A,C,B) / 2;
A9: sin beta = cos a2 & cos beta = sin a2 by A8,SIN_COS:79;
A10: sin a2 <> 0 by A1,Th21;
A11: |.C-B.| + |.C-A.| <> 0
proof
|.C-B.| <> 0 & |.C-A.| <> 0 by A3,EUCLID_6:42;
hence thesis;
end;
sin beta * cos alpha * (|.C-B.| - |.C-A.|) =
sin alpha * cos beta * (|.C-B.| + |.C-A.|) by A3,Th58;
then (|.C-B.| - |.C-A.|) * cos a2 * cos alpha / cos alpha
= (|.C-B.| + |.C-A.|) * sin a2 * sin alpha / cos alpha by A9;
then (|.C-B.| - |.C-A.|) * cos a2 * (cos alpha / cos alpha)
= (|.C-B.| + |.C-A.|) * sin a2 * (sin alpha / cos alpha);
then (|.C-B.| - |.C-A.|) * cos a2 * (1)
= (|.C-B.| + |.C-A.|) * sin a2 * (sin alpha / cos alpha)
by A5,A4,Th59,XCMPLX_1:60;
then (|.C-B.| - |.C-A.|) * cos a2 / sin a2
= (|.C-B.| + |.C-A.|) * tan alpha * sin a2 / sin a2;
then (|.C-B.| - |.C-A.|) * (cos a2 / sin a2)
= (|.C-B.| + |.C-A.|) * tan alpha * (sin a2 / sin a2)
.= (|.C-B.| + |.C-A.|) * tan alpha * (1) by A10,XCMPLX_1:60;
then tan alpha * (|.C-B.| + |.C-A.|) / (|.C-B.|+|.C-A.|)
= cot a2 * (|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|);
then tan alpha * ((|.C-B.| + |.C-A.|) / (|.C-B.|+|.C-A.|))
= cot a2 * ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|));
then tan alpha * (1) = cot a2 * ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|))
by A11,XCMPLX_1:60;
hence thesis;
end;
theorem Th61:
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.|)))
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI;
set r = ((angle(B,A,C) - angle(C,B,A))/2);
A3: tan r = cot (angle(A,C,B) / 2) * ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|))
by A1,A2,Th60;
0 <= angle(A,C,B) by EUCLID11:2;
then
A4: 0 < angle(A,C,B) < PI &
A,C,B are_mutually_distinct by A1,A2,EUCLID10:30,EUCLID_6:20;
0 < angle(B,A,C) < PI &
A,B,C is_a_triangle by A4,EUCLID11:5,A1,MENELAUS:15;
then -PI/2 < r < PI/2 by Th29;
hence thesis by A3,SIN_COS9:35;
end;
theorem Th62:
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.|))))
proof
assume A,C,B is_a_triangle & angle(A,C,B) < PI;
then (angle(B,A,C) - angle(C,B,A)) / 2
= arctan (cot (angle(A,C,B) / 2)
* ((|.C-B.|-|.C-A.|) / (|.C-B.| + |.C-A.|))) by Th61;
hence thesis;
end;
theorem
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.|)))
proof
assume A,C,B is_a_triangle & angle(A,C,B) < PI;
then 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) = (PI - angle(A,C,B)) by Th62,Th24;
hence thesis;
end;
theorem Th63:
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))
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI;
A3: A,C,B are_mutually_distinct by A1,EUCLID_6:20;
A4: |.B-C.| = |.A-B.| * sin angle(B,A,C) / sin angle(A,C,B)
proof
|.B-A.| * sin angle(B,A,C) = |.B-C.| * sin angle(A,C,B) by A3,EUCLID_6:6;
then |.A-B.| * sin angle(B,A,C) / sin angle(A,C,B)
= |.B-C.| * sin angle(A,C,B) / sin angle (A,C,B) by EUCLID_6:43
.= |.B-C.| * (sin angle(A,C,B) / sin angle (A,C,B))
.= |.B-C.| * 1 by A1,Th22,XCMPLX_1:60
.= |.B-C.|;
hence thesis;
end;
angle(A,C,B) = PI - (angle(C,B,A) + angle(B,A,C)) by A1,A2,Th23;
hence thesis by A4,EUCLID10:1;
end;
theorem Th64:
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))
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI;
A3: A,C,B are_mutually_distinct by A1,EUCLID_6:20;
A4: |.A-C.| = |.A-B.| * sin angle(C,B,A) / sin angle(A,C,B)
proof
|.A - B.| * sin angle(C,B,A) / sin angle(A,C,B)
= |.A - C.| * sin angle(A,C,B) / sin angle (A,C,B)
by A3,EUCLID_6:6
.= |.A - C.| * (sin angle(A,C,B) / sin angle (A,C,B))
.= |.A - C.| * 1 by A1,Th22,XCMPLX_1:60
.= |.A - C.|;
hence thesis;
end;
angle(A,C,B) = PI - (angle(C,B,A) + angle(B,A,C))
proof
A,C,B are_mutually_distinct by A1,EUCLID_6:20;
then angle(A,C,B) + angle (C,B,A) + angle (B,A,C) = PI by A2,EUCLID_3:47;
hence thesis;
end;
hence thesis by A4,EUCLID10:1;
end;
theorem Th65:
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)
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(C,A,B)=PI/2;
A3: A,C,B are_mutually_distinct by A1,EUCLID_6:20;
then |(B-A,C-A)| = 0 by A2,EUCLID_3:45;
then
A4: |(A-B,A-C)| = 0 by Th10;
tan angle(A,B,C) * |.A-B.| = |.A-C.|/|.A-B.| * |.A-B.|
by A1,A2,EUCLID10:35
.= |.A-C.| by A3,EUCLID_6:42,XCMPLX_1:87
.= |.C-A.| by EUCLID_6:43;
then tan angle(A,B,C)*|.A-B.|
= |.the_foot_of_the_altitude(C,A,B) - C.| by A4,A3,Th47
.= |.C - the_foot_of_the_altitude(C,A,B).| by EUCLID_6:43;
hence thesis by A3,Def3;
end;
theorem Th66:
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)
proof
assume that
A1: A,B,C is_a_triangle and
A2: angle(C,A,B) = 3/2*PI;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
then |(C-A,B-A)| = 0 by A2,EUCLID_3:45;
then
A4: |(A-B,A-C)| = 0 by Th10;
angle(B,A,C) = 2*PI - 3/2*PI by A1,A2,EUCLID10:31
.= PI/2;
then tan angle(C,B,A) * |.A-B.| = |.A-C.|/|.A-B.|*|.A-B.| by A1,EUCLID10:35
.= |.A-C.| by A3,EUCLID_6:42,XCMPLX_1:87
.= |.C-A.| by EUCLID_6:43;
then |.A-B.| * tan angle(C,B,A)
= |.the_foot_of_the_altitude(C,A,B) - C.| by A4,A3,Th47
.= |.C - the_foot_of_the_altitude(C,A,B).| by EUCLID_6:43;
hence thesis by A3,Def3;
end;
theorem
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) .|
proof
assume that
A1: A,C,B is_a_triangle and
A2: |(A-C,A-B)| = 0;
A3: A,C,B are_mutually_distinct & |(C-A,B-A)| = 0
by A2,Th10,A1,EUCLID_6:20;
A4: |.A-B.| <> 0 by A3,EUCLID_6:42;
per cases by A3,EUCLID_3:45;
suppose angle(C,A,B) = PI/2;
then
A5: the_length_of_the_altitude(C,A,B) = |.A-B.| * tan angle(A,B,C)
by A1,Th65;
then 0 <= tan angle(A,B,C) by A4,A3,Th46;
hence thesis by A5,ABSVALUE:def 1;
end;
suppose
A6: angle(C,A,B) = 3/2*PI;
A7: A,B,C is_a_triangle by A1,MENELAUS:15;
tan angle(C,B,A) = tan (2*PI-angle(A,B,C)) by A1,EUCLID10:31
.= - tan angle(A,B,C) by Th6;
then
A8: (- tan angle(A,B,C)) * |.A-B.| = the_length_of_the_altitude(C,A,B)
by A7,A6,Th66;
then tan angle(A,B,C) <= 0 by A4,A3,Th46;
hence thesis by A8,ABSVALUE:30;
end;
end;
theorem Th67:
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.|
proof
assume that
A1: B <> C and
A2: the_foot_of_the_altitude(A,B,C),B,A is_a_triangle;
|(B-the_foot_of_the_altitude(A,B,C),
A-the_foot_of_the_altitude(A,B,C))| = 0 by A1,Th39;
hence thesis by A2,EUCLID10:32;
end;
theorem
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.|
proof
assume that
A1: A,B,C is_a_triangle and
A2: |(B-A,B-C)| <> 0;
A,B,C are_mutually_distinct by A1,EUCLID_6:20;
hence thesis by A1,A2,Th67,Th45;
end;
:: C
::
:: A f B
:: C
::
:: f A B
:: C
::
:: A B f
theorem
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))).|
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI and
A3: |(A-C,A-B)| <> 0;
A4: |.A-C.| = |.A-B.| * sin angle(C,B,A) /
sin (angle(B,A,C) + angle(C,B,A)) by A1,A2,Th64;
A5: C,A,B is_a_triangle & A,C,B are_mutually_distinct
by A1,EUCLID_6:20,MENELAUS:15;
then |.the_foot_of_the_altitude(C,A,B)-C.| = |.C-A.|
* sin angle(C,A,the_foot_of_the_altitude(C,A,B)) or
|.the_foot_of_the_altitude(C,A,B)-C.| = |.C-A.|
* (- sin angle(C,A,the_foot_of_the_altitude(C,A,B)))
by A3,Th45,Th67;
then |.the_foot_of_the_altitude(C,A,B)-C.| = |.A-C.|
* sin angle(C,A,the_foot_of_the_altitude(C,A,B)) or
|.the_foot_of_the_altitude(C,A,B)-C.| = |.A-C.|
* (- sin angle(C,A,the_foot_of_the_altitude(C,A,B)))
by EUCLID_6:43;
then per cases by A4;
suppose
A7: |.the_foot_of_the_altitude(C,A,B)-C.| = |.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)));
|.A-B.| <> 0 by A5,EUCLID_6:42;
then
A8: 0 <= 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)) by A7;
the_length_of_the_altitude(C,A,B)
= |.C - the_foot_of_the_altitude(C,A,B).| by A5,Def3
.= |.the_foot_of_the_altitude(C,A,B)-C.| by EUCLID_6:43
.= |.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)).|
by A7,A8,ABSVALUE:def 1;
hence thesis;
end;
suppose
A10: |.the_foot_of_the_altitude(C,A,B)-C.| = |.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))));
|.A-B.| <> 0 by A5,EUCLID_6:42;
then
A11: (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)))) <= 0 by A10;
the_length_of_the_altitude(C,A,B)
= |.C - the_foot_of_the_altitude(C,A,B).| by A5,Def3
.= |.the_foot_of_the_altitude(C,A,B)-C.| by EUCLID_6:43
.= |.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)).|
by A10,A11,ABSVALUE:30;
hence thesis;
end;
end;
theorem
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))
proof
assume that
A1: 0 < angle(B,A,D) < PI and
A2: 0 < angle(D,A,C) < PI and
A3: D,A,C are_mutually_distinct and
A4: B,A,D are_mutually_distinct;
A5: angle(B,A,D) + angle(D,A,C) = angle(B,A,C)
proof
not angle(B,A,D) + angle(D,A,C) = angle(B,A,C) + 2 * PI
proof
assume
A6: angle(B,A,D) + angle(D,A,C) = angle(B,A,C) + 2 * PI;
0 <= angle(B,A,C) by EUCLID11:2;
then
A7: 0 + 2 * PI <= angle(B,A,C) + 2 * PI by XREAL_1:7;
angle(B,A,D) + angle(D,A,C) < PI + PI by A1,A2,XREAL_1:8;
hence contradiction by A7,A6;
end;
hence thesis by EUCLID_6:4;
end;
A8: angle(A,C,D) = PI - (angle(C,D,A) + angle(D,A,C))
proof
angle(D,A,C) + angle(A,C,D) + angle(C,D,A)= PI by A2,A3,EUCLID_3:47;
hence thesis;
end;
angle(D,B,A) = PI - (angle(A,D,B) + angle(B,A,D))
proof
angle(B,A,D) + angle(A,D,B) + angle(D,B,A) = PI by A1,A4,EUCLID_3:47;
hence thesis;
end;
hence thesis by A8,A5;
end;
:: B
::
:: A
::
:: D
::
:: C
theorem Th68:
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)
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI and
A3: A,D,B is_a_triangle and
A4: angle(A,D,B) < PI and
A5: a = angle(C,B,A) & b = angle(B,A,C) & c = angle(D,B,A) & d = angle(C,A,D);
set e = b + d;
A6: e = angle(B,A,D) or e = angle(B,A,D) + 2 * PI by A5,EUCLID_6:4;
A7: sin (e+c) = sin (angle(B,A,D)+angle(D,B,A))
proof
sin (angle(B,A,D) + c + 2*PI) = sin (angle(B,A,D) + c) by SIN_COS:79;
hence thesis by A5,A6;
end;
A8: |.C-A.| = |.A-C.| by EUCLID_6:43
.= |.A-B.| * sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)) by A1,A2,Th64;
then
A9: |.C-A.|^2 = (|.A-B.| * (sin angle(C,B,A) / sin (angle(B,A,C)
+ angle(C,B,A))))^2
.= (|.A-B.|)^2 * (sin angle(C,B,A) / sin (angle(B,A,C)
+ angle(C,B,A)))^2
by SQUARE_1:9;
A10: |.D-A.| = |.A-D.| by EUCLID_6:43
.= |.A-B.| * sin angle(D,B,A) / sin (angle(B,A,D) + angle(D,B,A))
by A3,A4,Th64;
then
A11: |.D-A.|^2 = ((|.A-B.|) * (sin angle(D,B,A)
/ sin (angle(B,A,D) + angle(D,B,A))))^2
.= (|.A-B.|)^2 * (sin angle(D,B,A)
/ sin (angle(B,A,D) + angle(D,B,A)))^2
by SQUARE_1:9;
|.D-C.|^2 = ((|.A-B.|)^2 * (sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)))^2) + ((|.A-B.|)^2
* (sin angle(D,B,A) / sin (angle(B,A,D) + angle(D,B,A)))^2)
- 2 * (|.A-B.| * sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)))
* (|.A-B.| * sin angle(D,B,A)
/ sin (angle(B,A,D) + angle(D,B,A)))
* cos angle(C,A,D) by A8,A9,A10,A11,EUCLID_6:7
.= ((|.A-B.|)^2 * (sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)))^2)
+ ((|.A-B.|)^2 * (sin angle(D,B,A) / sin (angle(B,A,D)
+ angle(D,B,A)))^2)
- 2 * ((|.A-B.|*|.A-B.|) * sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)))
* sin angle(D,B,A)
/ sin (angle(B,A,D) + angle(D,B,A))
* cos angle(C,A,D)
.= ((|.A-B.|)^2 * (sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)))^2)
+ ((|.A-B.|)^2 * (sin angle(D,B,A) / sin (angle(B,A,D)
+ angle(D,B,A)))^2)
- 2 * (|.A-B.|^2 * sin angle(C,B,A)
/ sin (angle(B,A,C) + angle(C,B,A)))
* sin angle(D,B,A) / sin (angle(B,A,D) + angle(D,B,A))
* cos angle(C,A,D) by SQUARE_1:def 1
.= (|.A-B.|)^2
* (((sin a / sin (a+b))^2) + ((sin c / sin (e + c))^2)
- 2 * (sin a / sin (b + a))
* (sin c / sin (e + c)) * cos d) by A5,A7;
hence thesis;
end;
theorem Th69:
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
proof
assume
A1: sin(2*s) * cos d = cos (2*t);
(r * cos s)^2 + (r * sin s)^2 - 2*(r*cos s)*(r*sin s)*cos d
=(r * cos s) * (r * cos s) +(r * sin s)^2 - 2*(r*cos s)*(r*sin s)*(cos d)
by SQUARE_1:def 1
.=(r * cos s) * (r * cos s) +(r * sin s)*(r* sin s)
- 2*(r*cos s)*(r*sin s)*cos d by SQUARE_1:def 1
.= r * r *(cos s * cos s +sin s * sin s)
- r * 2 * r * cos s * sin s * cos d
.= r* r * 1 - r * 2 * r * cos s * sin s * cos d by SIN_COS:29
.= r^2- (r * r) * 2 * cos s * sin s * cos d by SQUARE_1:def 1
.= r^2- r^2 * 2 * cos s * sin s * cos d by SQUARE_1:def 1
.= r^2- r^2 * (2 * sin s * cos s) * cos d
.= r^2 - r^2 * sin (2*s) * cos d by SIN_COS5:5
.= r^2-r^2*(cos (2*t)) by A1
.= r^2 - r^2 * ((cos t)^2-(sin t)^2) by SIN_COS5:7
.= r^2 * ( 1 - ((cos t)^2-(sin t)^2))
.= r^2* (((cos t)^2+(sin t)^2)-((cos t)^2-(sin t)^2)) by SIN_COS:29
.= 2 * r^2 * (sin t)^2;
hence thesis;
end;
theorem
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
proof
let R,theta be Real;
assume that
A1: D <> C and
A2: 0 <= R and
A3: 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) and
A4: R * cos s = sin a / sin (a+b) and
A5: R * sin s = sin c / sin (b + d + c) and
A6: 0 < theta < PI and
A7: sin (2*s) * cos d = cos (2*theta);
A8: |.D-C.|^2 = (|.A-B.|)^2 * (((R * cos s)^2) + ((R * sin s)^2)
- 2 * (R * cos s) * (R * sin s) * cos d) by A3,A4,A5,Th68
.= (|.A-B.|)^2 * (2 * R^2 * (sin theta)^2) by A7,Th69;
A9: 0 < 2 & sqrt (2*2) = 2 by SQUARE_1:20;
A10: (|.A-B.|)^2 * (2 * R^2 * (sin theta)^2)
= (|.A-B.| * |.A-B.|) * (2 * R^2 * (sin theta)^2) by SQUARE_1:def 1
.= (|.A-B.| * |.A-B.|) * ((sqrt 2 * sqrt 2) * R^2
* (sin theta)^2) by A9,SQUARE_1:29
.= (|.A-B.| * |.A-B.|) * ((sqrt 2 * sqrt 2) * (R*R)
* (sin theta)^2) by SQUARE_1:def 1
.= (|.A-B.| * |.A-B.|) * ((sqrt 2 * sqrt 2) * (R*R)
* (sin theta * sin theta)) by SQUARE_1:def 1
.= (|.A-B.| * sqrt 2 * R * sin theta) * (|.A-B.| * sqrt 2 * R * sin theta)
.= (|.A-B.| * sqrt 2 * R * sin theta)^2 by SQUARE_1:def 1;
2*PI*0 < theta < 2*PI*0+PI by A6;
then
A11: 0 < sin theta by SIN_COS6:11;
not |.D-C.| = - |.A-B.| * sqrt 2 * R * sin theta
proof
assume
A12: |.D-C.| = - |.A-B.| * sqrt 2 * R * sin theta;
0 < sqrt 2 by SQUARE_1:25;
then |.D-C.| = 0 by A12,A2,A11;
hence contradiction by A1,EUCLID_6:42;
end;
hence thesis by A10,A8,SQUARE_1:40;
end;
:: C
::
:: B
::
:: D A
theorem Th70:
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)
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI and
A3: D,A,C is_a_triangle and
A4: angle(A,D,C)=PI/2;
|.D-C.| = |.C-A.| * sin angle(C,A,D) by A3,A4,EUCLID10:34
.= |.A-C.| * sin angle(C,A,D) by EUCLID_6:43
.= |.A-B.| * sin angle(C,B,A) / sin (angle(B,A,C) + angle(C,B,A))
* sin angle(C,A,D) by A1,A2,Th64;
hence thesis;
end;
:: C
::
:: B
::
:: A D
theorem Th71:
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)
proof
assume that
A1: B,C,A is_a_triangle and
A2: angle(B,C,A) < PI and
A3: D,C,A is_a_triangle and
A4: angle(C,D,A)=PI/2;
|.D-C.| = |.A-C.| * sin angle(D,A,C) by A3,A4,EUCLID10:34
.= |.B-A.| * sin angle(A,B,C) / sin (angle(A,B,C) + angle(C,A,B))
* sin angle(D,A,C) by A1,A2,Th63;
hence thesis by EUCLID_6:43;
end;
:: C
::
:: D A B
theorem
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)
proof
assume that
A1: A,C,B is_a_triangle and
A2: angle(A,C,B) < PI and
A3: D,A,C is_a_triangle and
A4: angle(A,D,C)=PI/2 and
A5: A in LSeg(B,D) and
A6: A <> D;
A,C,B are_mutually_distinct by A1,EUCLID_6:20;
then angle(B,A,C) + angle(C,A,D) = PI or
angle(B,A,C) + angle(C,A,D) = 3*PI by A5,A6,EUCLID_6:13;
then sin (angle(B,A,C) + angle(C,B,A))
= sin (PI - (angle(C,A,D) - angle(C,B,A))) or
sin (angle(B,A,C) + angle(C,B,A))
= sin (2*PI*1 + (PI - (angle(C,A,D) - angle(C,B,A))));
then sin (angle(B,A,C) + angle(C,B,A))
= sin (PI - (angle(C,A,D) - angle(C,B,A))) or
sin (angle(B,A,C) + angle(C,B,A))
= sin (PI - (angle(C,A,D) - angle(C,B,A))) by COMPLEX2:8;
then sin (angle(B,A,C) + angle(C,B,A))
= sin (angle(C,A,D) - angle(C,B,A)) by EUCLID10:1;
hence thesis by A1,A2,A3,A4,Th70;
end;
:: C
::
:: B A D
theorem
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)
proof
assume that
A1: B,C,A is_a_triangle and
A2: angle(B,C,A) < PI and
A3: D,C,A is_a_triangle and
A4: angle(C,D,A)=PI/2 and
A5: A in LSeg(D,B) and
A6: A <> D;
B,C,A are_mutually_distinct by A1,EUCLID_6:20;
then
A7: angle(D,A,C) + angle(C,A,B) = PI or
angle(D,A,C) + angle(C,A,B) = 3*PI by A5,A6,EUCLID_6:13;
sin (angle(C,A,B) + angle(A,B,C)) = sin (angle(D,A,C)-angle(A,B,C))
proof
per cases by A7;
suppose angle(C,A,B) = PI - angle(D,A,C);
then sin (angle(C,A,B)+angle(A,B,C))
= sin (PI - (angle(D,A,C)-angle(A,B,C)))
.= sin (angle(D,A,C)-angle(A,B,C)) by EUCLID10:1;
hence thesis;
end;
suppose angle(C,A,B) = 3*PI - angle(D,A,C);
then sin (angle(C,A,B)+angle(A,B,C))
= sin (2*PI*1 + (PI - (angle(D,A,C)-angle(A,B,C))))
.= sin (PI- (angle(D,A,C)-angle(A,B,C))) by COMPLEX2:8
.= sin (angle(D,A,C)-angle(A,B,C)) by EUCLID10:1;
hence thesis;
end;
end;
hence thesis by A1,A2,A3,A4,Th71;
end;