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'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 | ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) | |
| chordthm.A | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | ||
| chordthm.B | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | ||
| chordthm.C | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) | ||
| chordthm.D | ⊢ ( 𝜑 → 𝐷 ∈ ℂ ) | ||
| chordthm.P | ⊢ ( 𝜑 → 𝑃 ∈ ℂ ) | ||
| chordthm.AneP | ⊢ ( 𝜑 → 𝐴 ≠ 𝑃 ) | ||
| chordthm.BneP | ⊢ ( 𝜑 → 𝐵 ≠ 𝑃 ) | ||
| chordthm.CneP | ⊢ ( 𝜑 → 𝐶 ≠ 𝑃 ) | ||
| chordthm.DneP | ⊢ ( 𝜑 → 𝐷 ≠ 𝑃 ) | ||
| chordthm.APB | ⊢ ( 𝜑 → ( ( 𝐴 − 𝑃 ) 𝐹 ( 𝐵 − 𝑃 ) ) = π ) | ||
| chordthm.CPD | ⊢ ( 𝜑 → ( ( 𝐶 − 𝑃 ) 𝐹 ( 𝐷 − 𝑃 ) ) = π ) | ||
| chordthm.Q | ⊢ ( 𝜑 → 𝑄 ∈ ℂ ) | ||
| chordthm.ABcirc | ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) ) | ||
| chordthm.ACcirc | ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐶 − 𝑄 ) ) ) | ||
| chordthm.ADcirc | ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) ) | ||
| Assertion | chordthm | ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | chordthm.angdef | ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) | |
| 2 | chordthm.A | ⊢ ( 𝜑 → 𝐴 ∈ ℂ ) | |
| 3 | chordthm.B | ⊢ ( 𝜑 → 𝐵 ∈ ℂ ) | |
| 4 | chordthm.C | ⊢ ( 𝜑 → 𝐶 ∈ ℂ ) | |
| 5 | chordthm.D | ⊢ ( 𝜑 → 𝐷 ∈ ℂ ) | |
| 6 | chordthm.P | ⊢ ( 𝜑 → 𝑃 ∈ ℂ ) | |
| 7 | chordthm.AneP | ⊢ ( 𝜑 → 𝐴 ≠ 𝑃 ) | |
| 8 | chordthm.BneP | ⊢ ( 𝜑 → 𝐵 ≠ 𝑃 ) | |
| 9 | chordthm.CneP | ⊢ ( 𝜑 → 𝐶 ≠ 𝑃 ) | |
| 10 | chordthm.DneP | ⊢ ( 𝜑 → 𝐷 ≠ 𝑃 ) | |
| 11 | chordthm.APB | ⊢ ( 𝜑 → ( ( 𝐴 − 𝑃 ) 𝐹 ( 𝐵 − 𝑃 ) ) = π ) | |
| 12 | chordthm.CPD | ⊢ ( 𝜑 → ( ( 𝐶 − 𝑃 ) 𝐹 ( 𝐷 − 𝑃 ) ) = π ) | |
| 13 | chordthm.Q | ⊢ ( 𝜑 → 𝑄 ∈ ℂ ) | |
| 14 | chordthm.ABcirc | ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) ) | |
| 15 | chordthm.ACcirc | ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐶 − 𝑄 ) ) ) | |
| 16 | chordthm.ADcirc | ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) ) | |
| 17 | 10 | necomd | ⊢ ( 𝜑 → 𝑃 ≠ 𝐷 ) |
| 18 | 1 4 6 5 9 17 | angpieqvd | ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑃 ) 𝐹 ( 𝐷 − 𝑃 ) ) = π ↔ ∃ 𝑣 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) |
| 19 | 12 18 | mpbid | ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) |
| 20 | 8 | necomd | ⊢ ( 𝜑 → 𝑃 ≠ 𝐵 ) |
| 21 | 1 2 6 3 7 20 | angpieqvd | ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑃 ) 𝐹 ( 𝐵 − 𝑃 ) ) = π ↔ ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) |
| 22 | 11 21 | mpbid | ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) |
| 23 | 22 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) |
| 24 | 14 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) ) |
| 25 | 16 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) ) |
| 26 | 24 25 | eqtr3d | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( abs ‘ ( 𝐵 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) ) |
| 27 | 26 | oveq1d | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) ) |
| 28 | 27 | oveq1d | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) ) |
| 29 | 2 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝐴 ∈ ℂ ) |
| 30 | 3 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝐵 ∈ ℂ ) |
| 31 | 13 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑄 ∈ ℂ ) |
| 32 | ioossicc | ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) | |
| 33 | simprl | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑤 ∈ ( 0 (,) 1 ) ) | |
| 34 | 32 33 | sseldi | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑤 ∈ ( 0 [,] 1 ) ) |
| 35 | simprr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) | |
| 36 | 29 30 31 34 35 24 | chordthmlem5 | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) ) |
| 37 | 4 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝐶 ∈ ℂ ) |
| 38 | 5 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝐷 ∈ ℂ ) |
| 39 | simplrl | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑣 ∈ ( 0 (,) 1 ) ) | |
| 40 | 32 39 | sseldi | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑣 ∈ ( 0 [,] 1 ) ) |
| 41 | simplrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) | |
| 42 | 15 | ad2antrr | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐶 − 𝑄 ) ) ) |
| 43 | 42 25 | eqtr3d | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( abs ‘ ( 𝐶 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) ) |
| 44 | 37 38 31 40 41 43 | chordthmlem5 | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) ) |
| 45 | 28 36 44 | 3eqtr4d | ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) |
| 46 | 23 45 | rexlimddv | ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) |
| 47 | 19 46 | rexlimddv | ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) |