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 · PB and
PC · 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 𝜋. The
result is proven by using chordthmlem5 twice to show that PA
· PB and PC · PD both equal BQ
2
−
PQ
2
. This is similar to the proof of the
theorem given in Euclid's Elements_, where it is Proposition III.35.
Proven by David Moews
on 28-Feb-2017 as chordthm.
chordthmALTVD is a Virtual
Deduction User's Proof transcription of chordthm. Using the command
line argument argv1 having the value "runCompleteusersproofsmv" and
excluding bnj1196, completeusersproof will automatically
complete
chordthmALTVD, transforming it
into the set.mm Metamath proof chordthmALT. The text file
VirtualDeductionProofs.txt included in the completeusersproof download
contains the chordthmALTVD 28765 proof
in .txt format. That proof may copied into its own .txt file. That file
may be input into completeusersproof and an RPN proof of chordthmALT
will be generated. The proof of
chordthmALTRO is a form of the
completed proof which preserves the Virtual Deduction proof's step
numbers and their ordering. The qed step and the step numbers of
chordthmALTVD which contain "h"
or only numerals correspond to step numbers of chordthm. The step
numbers containing "b" or "c" are of added steps.
(Contributed by Alan Sare, 18-Sep-2017.)
Hypotheses
| Ref
| Expression |
|---|
| chordthmALTVD.angdef |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0})
↦ (ℑ‘(log‘(𝑦 / 𝑥)))) |
| chordthmALTVD.A |
⊢ ( 𝜑 ▶ 𝐴 ∈ ℂ ) |
| chordthmALTVD.B |
⊢ ( 𝜑 ▶ 𝐵 ∈ ℂ ) |
| chordthmALTVD.C |
⊢ ( 𝜑 ▶ 𝐶 ∈ ℂ ) |
| chordthmALTVD.D |
⊢ ( 𝜑 ▶ 𝐷 ∈ ℂ ) |
| chordthmALTVD.P |
⊢ ( 𝜑 ▶ 𝑃 ∈ ℂ ) |
| chordthmALTVD.AneP |
⊢ ( 𝜑 ▶ 𝐴 ≠ 𝑃 ) |
| chordthmALTVD.BneP |
⊢ ( 𝜑 ▶ 𝐵 ≠ 𝑃 ) |
| chordthmALTVD.CneP |
⊢ ( 𝜑 ▶ 𝐶 ≠ 𝑃 ) |
| chordthmALTVD.DneP |
⊢ ( 𝜑 ▶ 𝐷 ≠ 𝑃 ) |
| chordthmALTVD.APB |
⊢ ( 𝜑 ▶ ((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = 𝜋 ) |
| chordthmALTVD.CPD |
⊢ ( 𝜑 ▶ ((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = 𝜋 ) |
| chordthmALTVD.Q |
⊢ ( 𝜑 ▶ 𝑄 ∈ ℂ ) |
| chordthmALTVD.ABcirc |
⊢ ( 𝜑 ▶ (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)) ) |
| chordthmALTVD.ACcirc |
⊢ ( 𝜑 ▶ (abs‘(𝐴 − 𝑄)) = (abs‘(𝐶 − 𝑄)) ) |
| chordthmALTVD.ADcirc |
⊢ ( 𝜑 ▶ (abs‘(𝐴 − 𝑄)) = (abs‘(𝐷 − 𝑄)) ) |
Assertion
| Ref
| Expression |
|---|
| chordthmALTVD |
⊢ ( 𝜑 ▶ ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))) ) |
Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝑥,𝐷,𝑦 𝑥,𝑃,𝑦
Allowed substitution hints: 𝜑(𝑥,𝑦) 𝑄(𝑥,𝑦) 𝐹(𝑥,𝑦)
Proof of Theorem chordthmALTVD
| Step | Hyp | Expression |
|---|
| h1 | | ⊢ ( 𝜑 ▶ ((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = 𝜋 )
| | h2 | | ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
| | h3 | | ⊢ ( 𝜑 ▶ 𝐶 ∈ ℂ )
| | h4 | | ⊢ ( 𝜑 ▶ 𝑃 ∈ ℂ )
| | h5 | | ⊢ ( 𝜑 ▶ 𝐷 ∈ ℂ )
| | h6 | | ⊢ ( 𝜑 ▶ 𝐶 ≠ 𝑃 )
| | h7 | | ⊢ ( 𝜑 ▶ 𝐷 ≠ 𝑃 )
| | 8 | 7 | ⊢ ( 𝜑 ▶ 𝑃 ≠ 𝐷 )
| | 9 | 2, 3, 4, 5, 6, 8 | ⊢ ( 𝜑 ▶ (((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = 𝜋 ↔ ∃𝑣 ∈ (0(,)1)𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) )
| | 10 | 1, 9 | ⊢ ( 𝜑 ▶ ∃𝑣 ∈ (0(,)1)𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)) )
| | 10b | 10 | ⊢ ( 𝜑 ▶ ∃𝑣(𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) )
| | h11 | | ⊢ ( 𝜑 ▶ ((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = 𝜋 )
| | h12 | | ⊢ ( 𝜑 ▶ 𝐴 ∈ ℂ )
| | h13 | | ⊢ ( 𝜑 ▶ 𝐵 ∈ ℂ )
| | h14 | | ⊢ ( 𝜑 ▶ 𝐴 ≠ 𝑃 )
| | h15 | | ⊢ ( 𝜑 ▶ 𝐵 ≠ 𝑃 )
| | 16 | 15 | ⊢ ( 𝜑 ▶ 𝑃 ≠ 𝐵 )
| | 17 | 2, 12, 4, 13, 14, 16 | ⊢ ( 𝜑 ▶ (((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = 𝜋 ↔ ∃𝑤 ∈ (0(,)1)𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) )
| | 18 | 11, 17 | ⊢ ( 𝜑 ▶ ∃𝑤 ∈ (0(,)1)𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)) )
| | 18b | 18 | ⊢ ( 𝜑 ▶ ∃𝑤(𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) )
| | h20 | | ⊢ ( 𝜑 ▶ (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)) )
| | h22 | | ⊢ ( 𝜑 ▶ (abs‘(𝐴 − 𝑄)) = (abs‘(𝐷 − 𝑄)) )
| | 24 | 20, 22 | ⊢ ( 𝜑 ▶ (abs‘(𝐵 − 𝑄)) = (abs‘(𝐷 − 𝑄)) )
| | 25 | 24 | ⊢ ( 𝜑 ▶ ((abs‘(𝐵 − 𝑄))↑2) = ((abs‘(𝐷 − 𝑄))↑2) )
| | 26 | 25 | ⊢ ( 𝜑 ▶ (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)) = (((abs‘(𝐷 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)) )
| | h29 | | ⊢ ( 𝜑 ▶ 𝑄 ∈ ℂ )
| | 31 | | ⊢ (0(,)1) ⊆ (0[,]1)
| | 32 | | ⊢ ( 𝑤 ∈ (0(,)1) ▶ 𝑤 ∈ (0(,)1) )
| | 33 | 32, 31 | ⊢ ( 𝑤 ∈ (0(,)1) ▶ 𝑤 ∈ (0[,]1) )
| | 34 | | ⊢ ( 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)) ▶ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)) )
| | 35 | 12, 13, 29, 33, 34, 20 | ⊢ ( ( 𝜑 , 𝑤 ∈ (0(,)1) , 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)) ) ▶ ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)) )
| | 35b | 35 | ⊢ ( ( 𝜑 , (𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) ) ▶ ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)) )
| | 38 | | ⊢ ( 𝑣 ∈ (0(,)1) ▶ 𝑣 ∈ (0(,)1) )
| | 39 | 38, 31 | ⊢ ( 𝑣 ∈ (0(,)1) ▶ 𝑣 ∈ (0[,]1) )
| | 40 | | ⊢ ( 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)) ▶ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)) )
| | h41 | | ⊢ ( 𝜑 ▶ (abs‘(𝐴 − 𝑄)) = (abs‘(𝐶 − 𝑄)) )
| | 43 | 22, 41 | ⊢ ( 𝜑 ▶ (abs‘(𝐶 − 𝑄)) = (abs‘(𝐷 − 𝑄)) )
| | 44 | 3, 5, 29, 39, 40, 43 | ⊢ ( ( 𝜑 , 𝑣 ∈ (0(,)1) , 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)) ) ▶ ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))) = (((abs‘(𝐷 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)) )
| | 44b | 44 | ⊢ ( ( 𝜑 , (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) ) ▶ ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))) = (((abs‘(𝐷 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)) )
| | 45 | 26, 35b, 44b | ⊢ ( ( 𝜑 , (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) , (𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) ) ▶ ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))) )
| | 45b | 45 | ⊢ ( ( 𝜑 , (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) ) ▶ ((𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷)))) )
| | 45c | 45b | ⊢ ( ( 𝜑 , (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) ) ▶ (∃𝑤(𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷)))) )
| | 46 | 18b, 45c | ⊢ ( ( 𝜑 , (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) ) ▶ ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))) )
| | 46b | 46 | ⊢ ( 𝜑 ▶ ((𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷)))) )
| | 46c | 46b | ⊢ ( 𝜑 ▶ (∃𝑣(𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷)))) )
| | qed | 10b, 46c | ⊢ ( 𝜑 ▶ ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))) )
|
|