Metamath Proof Explorer

Theorem chordthmALT

Description: The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA x. PB and PC x. PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to _pi . The result is proven by using chordthmlem5 twice to show that PA x. PB and PC x. PD both equal BQ2 - PQ2. This is similar to the proof of the theorem given in Euclid'sElements, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm . https://us.metamath.org/other/completeusersproof/chordthmaltvd.html is a Virtual Deduction User's Proof transcription of chordthm . That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT Metamath proof. (Contributed by Alan Sare, 19-Sep-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses chordthmALT.angdef 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
chordthmALT.A 
|- ( ph -> A e. CC )
chordthmALT.B 
|- ( ph -> B e. CC )
chordthmALT.C 
|- ( ph -> C e. CC )
chordthmALT.D 
|- ( ph -> D e. CC )
chordthmALT.P 
|- ( ph -> P e. CC )
chordthmALT.AneP 
|- ( ph -> A =/= P )
chordthmALT.BneP 
|- ( ph -> B =/= P )
chordthmALT.CneP 
|- ( ph -> C =/= P )
chordthmALT.DneP 
|- ( ph -> D =/= P )
chordthmALT.APB 
|- ( ph -> ( ( A - P ) F ( B - P ) ) = _pi )
chordthmALT.CPD 
|- ( ph -> ( ( C - P ) F ( D - P ) ) = _pi )
chordthmALT.Q 
|- ( ph -> Q e. CC )
chordthmALT.ABcirc 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
chordthmALT.ACcirc 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( C - Q ) ) )
chordthmALT.ADcirc 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( D - Q ) ) )
Assertion chordthmALT 
|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) )

Proof

Step Hyp Ref Expression
1 chordthmALT.angdef 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 chordthmALT.A 
 |-  ( ph -> A e. CC )
3 chordthmALT.B 
 |-  ( ph -> B e. CC )
4 chordthmALT.C 
 |-  ( ph -> C e. CC )
5 chordthmALT.D 
 |-  ( ph -> D e. CC )
6 chordthmALT.P 
 |-  ( ph -> P e. CC )
7 chordthmALT.AneP 
 |-  ( ph -> A =/= P )
8 chordthmALT.BneP 
 |-  ( ph -> B =/= P )
9 chordthmALT.CneP 
 |-  ( ph -> C =/= P )
10 chordthmALT.DneP 
 |-  ( ph -> D =/= P )
11 chordthmALT.APB 
 |-  ( ph -> ( ( A - P ) F ( B - P ) ) = _pi )
12 chordthmALT.CPD 
 |-  ( ph -> ( ( C - P ) F ( D - P ) ) = _pi )
13 chordthmALT.Q 
 |-  ( ph -> Q e. CC )
14 chordthmALT.ABcirc 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
15 chordthmALT.ACcirc 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( C - Q ) ) )
16 chordthmALT.ADcirc 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( D - Q ) ) )
17 10 necomd 
 |-  ( ph -> P =/= D )
18 1 4 6 5 9 17 angpieqvd 
 |-  ( ph -> ( ( ( C - P ) F ( D - P ) ) = _pi <-> E. v e. ( 0 (,) 1 ) P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) )
19 12 18 mpbid 
 |-  ( ph -> E. v e. ( 0 (,) 1 ) P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) )
20 df-rex 
 |-  ( E. v e. ( 0 (,) 1 ) P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) <-> E. v ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) )
21 20 biimpi 
 |-  ( E. v e. ( 0 (,) 1 ) P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) -> E. v ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) )
22 19 21 syl 
 |-  ( ph -> E. v ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) )
23 8 necomd 
 |-  ( ph -> P =/= B )
24 1 2 6 3 7 23 angpieqvd 
 |-  ( ph -> ( ( ( A - P ) F ( B - P ) ) = _pi <-> E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) )
25 11 24 mpbid 
 |-  ( ph -> E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) )
26 df-rex 
 |-  ( E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) <-> E. w ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) )
27 26 biimpi 
 |-  ( E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) -> E. w ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) )
28 25 27 syl 
 |-  ( ph -> E. w ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) )
29 28 adantr 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) ) -> E. w ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) )
30 14 16 eqtr3d 
 |-  ( ph -> ( abs ` ( B - Q ) ) = ( abs ` ( D - Q ) ) )
31 30 oveq1d 
 |-  ( ph -> ( ( abs ` ( B - Q ) ) ^ 2 ) = ( ( abs ` ( D - Q ) ) ^ 2 ) )
32 31 oveq1d 
 |-  ( ph -> ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) = ( ( ( abs ` ( D - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
33 32 3ad2ant1 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) /\ ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) ) -> ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) = ( ( ( abs ` ( D - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
34 2 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> A e. CC )
35 3 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> B e. CC )
36 13 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> Q e. CC )
37 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
38 id 
 |-  ( w e. ( 0 (,) 1 ) -> w e. ( 0 (,) 1 ) )
39 37 38 sselid 
 |-  ( w e. ( 0 (,) 1 ) -> w e. ( 0 [,] 1 ) )
40 39 3ad2ant2 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> w e. ( 0 [,] 1 ) )
41 id 
 |-  ( P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) -> P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) )
42 41 3ad2ant3 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) )
43 14 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
44 34 35 36 40 42 43 chordthmlem5 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
45 44 3expb 
 |-  ( ( ph /\ ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
46 45 3adant2 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) /\ ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
47 4 3ad2ant1 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> C e. CC )
48 5 3ad2ant1 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> D e. CC )
49 13 3ad2ant1 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> Q e. CC )
50 id 
 |-  ( v e. ( 0 (,) 1 ) -> v e. ( 0 (,) 1 ) )
51 37 50 sselid 
 |-  ( v e. ( 0 (,) 1 ) -> v e. ( 0 [,] 1 ) )
52 51 3ad2ant2 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> v e. ( 0 [,] 1 ) )
53 id 
 |-  ( P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) -> P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) )
54 53 3ad2ant3 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) )
55 15 16 eqtr3d 
 |-  ( ph -> ( abs ` ( C - Q ) ) = ( abs ` ( D - Q ) ) )
56 55 3ad2ant1 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> ( abs ` ( C - Q ) ) = ( abs ` ( D - Q ) ) )
57 47 48 49 52 54 56 chordthmlem5 
 |-  ( ( ph /\ v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) = ( ( ( abs ` ( D - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
58 57 3expb 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) ) -> ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) = ( ( ( abs ` ( D - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
59 58 3adant3 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) /\ ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) ) -> ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) = ( ( ( abs ` ( D - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
60 33 46 59 3eqtr4d 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) /\ ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) )
61 60 3expia 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) ) -> ( ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) ) )
62 61 exlimdv 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) ) -> ( E. w ( w e. ( 0 (,) 1 ) /\ P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) ) )
63 29 62 mpd 
 |-  ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) )
64 63 ex 
 |-  ( ph -> ( ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) ) )
65 64 exlimdv 
 |-  ( ph -> ( E. v ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) ) )
66 22 65 mpd 
 |-  ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) )