chordthm

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 \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	chordthm.A	$⊢ φ \to A \in ℂ$
	chordthm.B	$⊢ φ \to B \in ℂ$
	chordthm.C	$⊢ φ \to C \in ℂ$
	chordthm.D	$⊢ φ \to D \in ℂ$
	chordthm.P	$⊢ φ \to P \in ℂ$
	chordthm.AneP	$⊢ φ \to A \neq P$
	chordthm.BneP	$⊢ φ \to B \neq P$
	chordthm.CneP	$⊢ φ \to C \neq P$
	chordthm.DneP	$⊢ φ \to D \neq P$
	chordthm.APB	$⊢ φ \to (A - P) F (B - P) = π$
	chordthm.CPD	$⊢ φ \to (C - P) F (D - P) = π$
	chordthm.Q	$⊢ φ \to Q \in ℂ$
	chordthm.ABcirc	$⊢ φ \to \|A - Q\| = \|B - Q\|$
	chordthm.ACcirc	$⊢ φ \to \|A - Q\| = \|C - Q\|$
	chordthm.ADcirc	$⊢ φ \to \|A - Q\| = \|D - Q\|$
Assertion	chordthm	$⊢ φ \to \|P - A\| \|P - B\| = \|P - C\| \|P - D\|$

Proof

Step	Hyp	Ref	Expression
1		chordthm.angdef	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		chordthm.A	$⊢ φ \to A \in ℂ$
3		chordthm.B	$⊢ φ \to B \in ℂ$
4		chordthm.C	$⊢ φ \to C \in ℂ$
5		chordthm.D	$⊢ φ \to D \in ℂ$
6		chordthm.P	$⊢ φ \to P \in ℂ$
7		chordthm.AneP	$⊢ φ \to A \neq P$
8		chordthm.BneP	$⊢ φ \to B \neq P$
9		chordthm.CneP	$⊢ φ \to C \neq P$
10		chordthm.DneP	$⊢ φ \to D \neq P$
11		chordthm.APB	$⊢ φ \to (A - P) F (B - P) = π$
12		chordthm.CPD	$⊢ φ \to (C - P) F (D - P) = π$
13		chordthm.Q	$⊢ φ \to Q \in ℂ$
14		chordthm.ABcirc	$⊢ φ \to \|A - Q\| = \|B - Q\|$
15		chordthm.ACcirc	$⊢ φ \to \|A - Q\| = \|C - Q\|$
16		chordthm.ADcirc	$⊢ φ \to \|A - Q\| = \|D - Q\|$
17	10	necomd	$⊢ φ \to P \neq D$
18	1 4 6 5 9 17	angpieqvd	$⊢ φ \to ((C - P) F (D - P) = π \leftrightarrow \exists v \in (0, 1) P = v C + (1 - v) D)$
19	12 18	mpbid	$⊢ φ \to \exists v \in (0, 1) P = v C + (1 - v) D$
20	8	necomd	$⊢ φ \to P \neq B$
21	1 2 6 3 7 20	angpieqvd	$⊢ φ \to ((A - P) F (B - P) = π \leftrightarrow \exists w \in (0, 1) P = w A + (1 - w) B)$
22	11 21	mpbid	$⊢ φ \to \exists w \in (0, 1) P = w A + (1 - w) B$
23	22	adantr	$⊢ (φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \to \exists w \in (0, 1) P = w A + (1 - w) B$
24	14	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|A - Q\| = \|B - Q\|$
25	16	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|A - Q\| = \|D - Q\|$
26	24 25	eqtr3d	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|B - Q\| = \|D - Q\|$
27	26	oveq1d	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to {\|B - Q\|}^{2} = {\|D - Q\|}^{2}$
28	27	oveq1d	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to {\|B - Q\|}^{2} - {\|P - Q\|}^{2} = {\|D - Q\|}^{2} - {\|P - Q\|}^{2}$
29	2	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to A \in ℂ$
30	3	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to B \in ℂ$
31	13	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to Q \in ℂ$
32		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
33		simprl	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to w \in (0, 1)$
34	32 33	sselid	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to w \in [0, 1]$
35		simprr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to P = w A + (1 - w) B$
36	29 30 31 34 35 24	chordthmlem5	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|P - A\| \|P - B\| = {\|B - Q\|}^{2} - {\|P - Q\|}^{2}$
37	4	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to C \in ℂ$
38	5	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to D \in ℂ$
39		simplrl	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to v \in (0, 1)$
40	32 39	sselid	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to v \in [0, 1]$
41		simplrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to P = v C + (1 - v) D$
42	15	ad2antrr	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|A - Q\| = \|C - Q\|$
43	42 25	eqtr3d	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|C - Q\| = \|D - Q\|$
44	37 38 31 40 41 43	chordthmlem5	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|P - C\| \|P - D\| = {\|D - Q\|}^{2} - {\|P - Q\|}^{2}$
45	28 36 44	3eqtr4d	$⊢ ((φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \land (w \in (0, 1) \land P = w A + (1 - w) B)) \to \|P - A\| \|P - B\| = \|P - C\| \|P - D\|$
46	23 45	rexlimddv	$⊢ (φ \land (v \in (0, 1) \land P = v C + (1 - v) D)) \to \|P - A\| \|P - B\| = \|P - C\| \|P - D\|$
47	19 46	rexlimddv	$⊢ φ \to \|P - A\| \|P - B\| = \|P - C\| \|P - D\|$

Metamath Proof Explorer

Theorem chordthm

Proof