:: Heron's Formula and Ptolemy's Theorem
:: by Marco Riccardi
::
:: Received January 10, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
for p1, p2 being Point of (TOP-REAL 2) holds
( |.(p1 - p2).| = 0 iff p1 = p2 )
Lm2:
for p1, p2 being Point of (TOP-REAL 2) holds |.(p1 - p2).| = |.(p2 - p1).|
theorem Th1: :: EUCLID_6:1
for
p1,
p2,
p3,
p4,
p5,
p6 being
Point of
(TOP-REAL 2) st
sin (angle p1,p2,p3) = sin (angle p4,p5,p6) &
cos (angle p1,p2,p3) = cos (angle p4,p5,p6) holds
angle p1,
p2,
p3 = angle p4,
p5,
p6
theorem Th2: :: EUCLID_6:2
theorem Th3: :: EUCLID_6:3
Lm3:
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) + (2 * PI )
Lm4:
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) + (4 * PI )
Lm5:
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) - (4 * PI )
Lm6:
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 2) holds not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) - (6 * PI )
Lm7:
for p1, p2, p3 being Point of (TOP-REAL 2)
for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
angle p1,p2,p3 = angle c1,c2
Lm8:
for c1, c2 being Element of COMPLEX st c2 = 0 holds
Arg (Rotate c2,(- (Arg c1))) = 0
Lm9:
for c1, c2 being Element of COMPLEX st c2 = 0 & Arg c1 = 0 holds
angle c1,c2 = 0
Lm10:
for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) >= 0 holds
Arg (Rotate c2,(- (Arg c1))) = (Arg c2) - (Arg c1)
Lm11:
for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) >= 0 holds
angle c1,c2 = (Arg c2) - (Arg c1)
Lm12:
for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) < 0 holds
Arg (Rotate c2,(- (Arg c1))) = ((2 * PI ) - (Arg c1)) + (Arg c2)
Lm13:
for c1, c2 being Element of COMPLEX st c2 <> 0 & (Arg c2) - (Arg c1) < 0 holds
angle c1,c2 = ((2 * PI ) - (Arg c1)) + (Arg c2)
Lm14:
for c1, c2, c3 being Element of COMPLEX holds
( (angle c1,c2) + (angle c2,c3) = angle c1,c3 or (angle c1,c2) + (angle c2,c3) = (angle c1,c3) + (2 * PI ) )
theorem Th4: :: EUCLID_6:4
for
p1,
p4,
p2,
p3 being
Point of
(TOP-REAL 2) holds
(
(angle p1,p4,p2) + (angle p2,p4,p3) = angle p1,
p4,
p3 or
(angle p1,p4,p2) + (angle p2,p4,p3) = (angle p1,p4,p3) + (2 * PI ) )
Lm15:
for p1, p2 being Point of (TOP-REAL 2) holds
( (p1 - p2) `1 = (p1 `1 ) - (p2 `1 ) & (p1 - p2) `2 = (p1 `2 ) - (p2 `2 ) )
Lm16:
for p1, p2, p3 being Point of (TOP-REAL 2)
for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
( Re (c1 .|. c2) = (((p1 `1 ) - (p2 `1 )) * ((p3 `1 ) - (p2 `1 ))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `2 ) - (p2 `2 ))) & Im (c1 .|. c2) = (- (((p1 `1 ) - (p2 `1 )) * ((p3 `2 ) - (p2 `2 )))) + (((p1 `2 ) - (p2 `2 )) * ((p3 `1 ) - (p2 `1 ))) & |.c1.| = sqrt ((((p1 `1 ) - (p2 `1 )) ^2 ) + (((p1 `2 ) - (p2 `2 )) ^2 )) & |.(p1 - p2).| = |.c1.| )
:: deftheorem defines the_area_of_polygon3 EUCLID_6:def 1 :
:: deftheorem defines the_perimeter_of_polygon3 EUCLID_6:def 2 :
theorem Th5: :: EUCLID_6:5
theorem Th6: :: EUCLID_6:6
theorem Th7: :: EUCLID_6:7
theorem Th8: :: EUCLID_6:8
theorem Th9: :: EUCLID_6:9
theorem Th10: :: EUCLID_6:10
Lm17:
for p1, p2 being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in inside_of_circle a,b,r & p2 in outside_of_circle a,b,r holds
ex p being Point of (TOP-REAL 2) st p in (LSeg p1,p2) /\ (circle a,b,r)
theorem Th11: :: EUCLID_6:11
theorem Th12: :: EUCLID_6:12
theorem Th13: :: EUCLID_6:13
for
p,
p1,
p3,
p2 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p3 &
p <> p1 &
p <> p3 & not
(angle p1,p,p2) + (angle p2,p,p3) = PI holds
(angle p1,p,p2) + (angle p2,p,p3) = 3
* PI
theorem Th14: :: EUCLID_6:14
for
p,
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p2 &
p <> p1 &
p <> p2 & (
angle p3,
p,
p1 = PI / 2 or
angle p3,
p,
p1 = (3 / 2) * PI ) holds
angle p1,
p,
p3 = angle p3,
p,
p2
theorem Th15: :: EUCLID_6:15
for
p,
p1,
p3,
p2,
p4 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p3 &
p in LSeg p2,
p4 &
p <> p1 &
p <> p2 &
p <> p3 &
p <> p4 holds
angle p1,
p,
p2 = angle p3,
p,
p4
theorem Th16: :: EUCLID_6:16
theorem Th17: :: EUCLID_6:17
theorem Th18: :: EUCLID_6:18
for
p1,
p3,
p2,
p being
Point of
(TOP-REAL 2) st
|.(p1 - p3).| = |.(p2 - p3).| &
p in LSeg p1,
p2 &
p <> p3 &
p <> p1 & (
angle p3,
p,
p1 = PI / 2 or
angle p3,
p,
p1 = (3 / 2) * PI ) holds
angle p1,
p3,
p = angle p,
p3,
p2
theorem :: EUCLID_6:19
for
p1,
p2,
p3,
p being
Point of
(TOP-REAL 2) st
|.(p1 - p3).| = |.(p2 - p3).| &
p in LSeg p1,
p2 &
p <> p3 holds
( (
angle p1,
p3,
p = angle p,
p3,
p2 implies
|.(p1 - p).| = |.(p - p2).| ) & (
|.(p1 - p).| = |.(p - p2).| implies
|((p3 - p),(p2 - p1))| = 0 ) & (
|((p3 - p),(p2 - p1))| = 0 implies
angle p1,
p3,
p = angle p,
p3,
p2 ) )
:: deftheorem Def3 defines is_collinear EUCLID_6:def 3 :
theorem Th20: :: EUCLID_6:20
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) holds
(
p1,
p2,
p3 is_a_triangle iff (
p1,
p2,
p3 are_mutually_different &
angle p1,
p2,
p3 <> PI &
angle p2,
p3,
p1 <> PI &
angle p3,
p1,
p2 <> PI ) )
Lm18:
for p3, p2, p1, p5, p6, p4 being Point of (TOP-REAL 2) st p3 <> p2 & p3 <> p1 & p2 <> p1 & p5 <> p6 & p5 <> p4 & p6 <> p4 & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI & angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p6,p4,p5 holds
|.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
theorem Th21: :: EUCLID_6:21
for
p1,
p2,
p3,
p4,
p5,
p6 being
Point of
(TOP-REAL 2) st
p1,
p2,
p3 is_a_triangle &
p4,
p5,
p6 is_a_triangle &
angle p1,
p2,
p3 = angle p4,
p5,
p6 &
angle p3,
p1,
p2 = angle p6,
p4,
p5 holds
(
|.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| &
|.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| &
|.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| )
Lm19:
for p3, p2, p1, p4, p5, p6 being Point of (TOP-REAL 2) st p3 <> p2 & p3 <> p1 & p2 <> p1 & p4 <> p5 & p4 <> p6 & p5 <> p6 & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI & angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p5,p6,p4 holds
|.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).|
theorem Th22: :: EUCLID_6:22
for
p1,
p2,
p3,
p4,
p5,
p6 being
Point of
(TOP-REAL 2) st
p1,
p2,
p3 is_a_triangle &
p4,
p5,
p6 is_a_triangle &
angle p1,
p2,
p3 = angle p4,
p5,
p6 &
angle p3,
p1,
p2 = angle p5,
p6,
p4 holds
(
|.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| &
|.(p2 - p3).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p5 - p4).| &
|.(p3 - p1).| * |.(p6 - p5).| = |.(p1 - p2).| * |.(p4 - p6).| )
theorem Th23: :: EUCLID_6:23
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p1,
p2,
p3 are_mutually_different &
angle p1,
p2,
p3 <= PI holds
(
angle p2,
p3,
p1 <= PI &
angle p3,
p1,
p2 <= PI )
theorem Th24: :: EUCLID_6:24
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p1,
p2,
p3 are_mutually_different &
angle p1,
p2,
p3 > PI holds
(
angle p2,
p3,
p1 > PI &
angle p3,
p1,
p2 > PI )
Lm20:
for n being Element of NAT
for q1 being Point of (TOP-REAL n)
for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) holds
f is continuous
Lm21:
for n being Element of NAT
for q1 being Point of (TOP-REAL n) ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous )
theorem Th25: :: EUCLID_6:25
for
p,
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p2 &
p1,
p2,
p3 is_a_triangle &
angle p1,
p3,
p2 = angle p,
p3,
p2 holds
p = p1
theorem Th26: :: EUCLID_6:26
for
p,
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p2 & not
p3 in LSeg p1,
p2 &
angle p1,
p3,
p2 <= PI holds
angle p,
p3,
p2 <= angle p1,
p3,
p2
theorem Th27: :: EUCLID_6:27
for
p,
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p2 & not
p3 in LSeg p1,
p2 &
angle p1,
p3,
p2 > PI &
p <> p2 holds
angle p,
p3,
p2 >= angle p1,
p3,
p2
theorem Th28: :: EUCLID_6:28
for
p,
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p in LSeg p1,
p2 & not
p3 in LSeg p1,
p2 holds
ex
p4 being
Point of
(TOP-REAL 2) st
(
p4 in LSeg p1,
p2 &
angle p1,
p3,
p4 = angle p,
p3,
p2 )
theorem :: EUCLID_6:29
for
p1,
p2 being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in inside_of_circle a,
b,
r &
p2 in outside_of_circle a,
b,
r holds
ex
p being
Point of
(TOP-REAL 2) st
p in (LSeg p1,p2) /\ (circle a,b,r) by Lm17;
theorem Th30: :: EUCLID_6:30
for
p1,
p3,
p4,
p being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p3 in circle a,
b,
r &
p4 in circle a,
b,
r &
p in LSeg p1,
p3 &
p in LSeg p1,
p4 &
p3 <> p4 holds
p = p1
theorem Th31: :: EUCLID_6:31
for
p1,
p2,
p,
pc being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p in circle a,
b,
r &
pc = |[a,b]| &
pc in LSeg p,
p2 &
p1 <> p & not 2
* (angle p1,p,p2) = angle p1,
pc,
p2 holds
2
* ((angle p1,p,p2) - PI ) = angle p1,
pc,
p2
theorem Th32: :: EUCLID_6:32
theorem Th33: :: EUCLID_6:33
for
p1,
p2,
p,
pc being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p in circle a,
b,
r &
pc = |[a,b]| &
p1 <> p &
p2 <> p & not 2
* (angle p1,p,p2) = angle p1,
pc,
p2 holds
2
* ((angle p1,p,p2) - PI ) = angle p1,
pc,
p2
theorem Th34: :: EUCLID_6:34
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p3 in circle a,
b,
r &
p4 in circle a,
b,
r &
p1 <> p3 &
p1 <> p4 &
p2 <> p3 &
p2 <> p4 & not
angle p1,
p3,
p2 = angle p1,
p4,
p2 & not
angle p1,
p3,
p2 = (angle p1,p4,p2) - PI holds
angle p1,
p3,
p2 = (angle p1,p4,p2) + PI
theorem Th35: :: EUCLID_6:35
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p3 in circle a,
b,
r &
p1 <> p2 &
p2 <> p3 holds
angle p1,
p2,
p3 <> PI
Lm22:
for p1, p3, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p3 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p3 & p in LSeg p1,p4 holds
|.(p1 - p).| * |.(p - p3).| = |.(p1 - p).| * |.(p - p4).|
Lm23:
for p1, p2, p4, p being Point of (TOP-REAL 2)
for a, b, r being real number st p1 in circle a,b,r & p2 in circle a,b,r & p4 in circle a,b,r & p in LSeg p1,p1 & p in LSeg p2,p4 holds
|.(p1 - p).| * |.(p - p1).| = |.(p2 - p).| * |.(p - p4).|
theorem Th36: :: EUCLID_6:36
for
p1,
p2,
p3,
p4,
p being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p3 in circle a,
b,
r &
p4 in circle a,
b,
r &
p in LSeg p1,
p3 &
p in LSeg p2,
p4 &
p1,
p2,
p3,
p4 are_mutually_different holds
angle p1,
p4,
p2 = angle p1,
p3,
p2
theorem Th37: :: EUCLID_6:37
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p3 in circle a,
b,
r &
angle p1,
p2,
p3 = 0 &
p1 <> p2 &
p2 <> p3 holds
p1 = p3
theorem :: EUCLID_6:38
for
p1,
p2,
p3,
p4,
p being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p3 in circle a,
b,
r &
p4 in circle a,
b,
r &
p in LSeg p1,
p3 &
p in LSeg p2,
p4 holds
|.(p1 - p).| * |.(p - p3).| = |.(p2 - p).| * |.(p - p4).|
theorem :: EUCLID_6:39
theorem :: EUCLID_6:40
for
p1,
p2,
p3,
p4,
p being
Point of
(TOP-REAL 2) for
a,
b,
r being
real number st
p1 in circle a,
b,
r &
p2 in circle a,
b,
r &
p3 in circle a,
b,
r &
p4 in circle a,
b,
r &
p in LSeg p1,
p3 &
p in LSeg p2,
p4 holds
|.(p3 - p1).| * |.(p4 - p2).| = (|.(p2 - p1).| * |.(p4 - p3).|) + (|.(p3 - p2).| * |.(p4 - p1).|)
theorem :: EUCLID_6:41
theorem :: EUCLID_6:42
theorem :: EUCLID_6:43
theorem :: EUCLID_6:44
theorem :: EUCLID_6:45
theorem :: EUCLID_6:46
theorem :: EUCLID_6:47
theorem :: EUCLID_6:48
theorem :: EUCLID_6:49
theorem :: EUCLID_6:50
theorem :: EUCLID_6:51
theorem :: EUCLID_6:52