Theorem chordthm

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 BQ² - PQ². This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. This is Metamath 100 proof #55. (Contributed by David Moews, 28-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		chordthm.angdef	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		chordthm.A	|- ( ph -> A e. CC )
3		chordthm.B	|- ( ph -> B e. CC )
4		chordthm.C	|- ( ph -> C e. CC )
5		chordthm.D	|- ( ph -> D e. CC )
6		chordthm.P	|- ( ph -> P e. CC )
7		chordthm.AneP	|- ( ph -> A =/= P )
8		chordthm.BneP	|- ( ph -> B =/= P )
9		chordthm.CneP	|- ( ph -> C =/= P )
10		chordthm.DneP	|- ( ph -> D =/= P )
11		chordthm.APB	|- ( ph -> ( ( A - P ) F ( B - P ) ) = _pi )
12		chordthm.CPD	|- ( ph -> ( ( C - P ) F ( D - P ) ) = _pi )
13		chordthm.Q	|- ( ph -> Q e. CC )
14		chordthm.ABcirc	|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
15		chordthm.ACcirc	|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( C - Q ) ) )
16		chordthm.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	8	necomd	|- ( ph -> P =/= B )
21	1 2 6 3 7 20	angpieqvd	|- ( ph -> ( ( ( A - P ) F ( B - P ) ) = _pi <-> E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) ) )
22	11 21	mpbid	|- ( ph -> E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) )
23	22	adantr	|- ( ( ph /\ ( v e. ( 0 (,) 1 ) /\ P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) ) ) -> E. w e. ( 0 (,) 1 ) P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) )
24	14	ad2antrr	|- ( ( ( 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 ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
25	16	ad2antrr	|- ( ( ( 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 ` ( A - Q ) ) = ( abs ` ( D - Q ) ) )
26	24 25	eqtr3d	|- ( ( ( 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 ) ) = ( abs ` ( D - Q ) ) )
27	26	oveq1d	|- ( ( ( 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 ` ( D - Q ) ) ^ 2 ) )
28	27	oveq1d	|- ( ( ( 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 ) ) )
29	2	ad2antrr	|- ( ( ( 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 ) ) ) ) -> A e. CC )
30	3	ad2antrr	|- ( ( ( 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 ) ) ) ) -> B e. CC )
31	13	ad2antrr	|- ( ( ( 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 ) ) ) ) -> Q e. CC )
32		ioossicc	|- ( 0 (,) 1 ) C_ ( 0 [,] 1 )
33		simprl	|- ( ( ( 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 ) ) ) ) -> w e. ( 0 (,) 1 ) )
34	32 33	sseldi	|- ( ( ( 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 ) ) ) ) -> w e. ( 0 [,] 1 ) )
35		simprr	|- ( ( ( 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 ) ) ) ) -> P = ( ( w x. A ) + ( ( 1 - w ) x. B ) ) )
36	29 30 31 34 35 24	chordthmlem5	|- ( ( ( 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 ) ) )
37	4	ad2antrr	|- ( ( ( 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 ) ) ) ) -> C e. CC )
38	5	ad2antrr	|- ( ( ( 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 ) ) ) ) -> D e. CC )
39		simplrl	|- ( ( ( 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 ) ) ) ) -> v e. ( 0 (,) 1 ) )
40	32 39	sseldi	|- ( ( ( 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 ) ) ) ) -> v e. ( 0 [,] 1 ) )
41		simplrr	|- ( ( ( 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 ) ) ) ) -> P = ( ( v x. C ) + ( ( 1 - v ) x. D ) ) )
42	15	ad2antrr	|- ( ( ( 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 ` ( A - Q ) ) = ( abs ` ( C - Q ) ) )
43	42 25	eqtr3d	|- ( ( ( 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 ` ( C - Q ) ) = ( abs ` ( D - Q ) ) )
44	37 38 31 40 41 43	chordthmlem5	|- ( ( ( 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 ) ) )
45	28 36 44	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 ) ) ) )
46	23 45	rexlimddv	|- ( ( 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 ) ) ) )
47	19 46	rexlimddv	|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) )