Theorem chordthmALTVD
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
StepHypExpression
h1  (   𝜑   ▶   ((𝐶𝑃)𝐹(𝐷𝑃)) = 𝜋   )
h2  𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
h3  (   𝜑   ▶   𝐶 ∈ ℂ   )
h4  (   𝜑   ▶   𝑃 ∈ ℂ   )
h5  (   𝜑   ▶   𝐷 ∈ ℂ   )
h6  (   𝜑   ▶   𝐶𝑃   )
h7  (   𝜑   ▶   𝐷𝑃   )
87 (   𝜑   ▶   𝑃𝐷   )
92, 3, 4, 5, 6, 8 (   𝜑   ▶   (((𝐶𝑃)𝐹(𝐷𝑃)) = 𝜋 ↔ ∃𝑣 ∈ (0(,)1)𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   )
101, 9 (   𝜑   ▶   𝑣 ∈ (0(,)1)𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))   )
10b10 (   𝜑   ▶   𝑣(𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   )
h11  (   𝜑   ▶   ((𝐴𝑃)𝐹(𝐵𝑃)) = 𝜋   )
h12  (   𝜑   ▶   𝐴 ∈ ℂ   )
h13  (   𝜑   ▶   𝐵 ∈ ℂ   )
h14  (   𝜑   ▶   𝐴𝑃   )
h15  (   𝜑   ▶   𝐵𝑃   )
1615 (   𝜑   ▶   𝑃𝐵   )
172, 12, 4, 13, 14, 16 (   𝜑   ▶   (((𝐴𝑃)𝐹(𝐵𝑃)) = 𝜋 ↔ ∃𝑤 ∈ (0(,)1)𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)))   )
1811, 17 (   𝜑   ▶   𝑤 ∈ (0(,)1)𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))   )
18b18 (   𝜑   ▶   𝑤(𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)))   )
h20  (   𝜑   ▶   (abs‘(𝐴𝑄)) = (abs‘(𝐵𝑄))   )
h22  (   𝜑   ▶   (abs‘(𝐴𝑄)) = (abs‘(𝐷𝑄))   )
2420, 22 (   𝜑   ▶   (abs‘(𝐵𝑄)) = (abs‘(𝐷𝑄))   )
2524 (   𝜑   ▶   ((abs‘(𝐵𝑄))↑2) = ((abs‘(𝐷𝑄))↑2)   )
2625 (   𝜑   ▶   (((abs‘(𝐵𝑄))↑2) − ((abs‘(𝑃𝑄))↑2)) = (((abs‘(𝐷𝑄))↑2) − ((abs‘(𝑃𝑄))↑2))   )
h29  (   𝜑   ▶   𝑄 ∈ ℂ   )
31  (0(,)1) ⊆ (0[,]1)
32  (   𝑤 ∈ (0(,)1)   ▶   𝑤 ∈ (0(,)1)   )
3332, 31 (   𝑤 ∈ (0(,)1)   ▶   𝑤 ∈ (0[,]1)   )
34  (   𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))   ▶   𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))   )
3512, 13, 29, 33, 34, 20 (   (   𝜑   ,   𝑤 ∈ (0(,)1)   ,   𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))   )   ▶   ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = (((abs‘(𝐵𝑄))↑2) − ((abs‘(𝑃𝑄))↑2))   )
35b35 (   (   𝜑   ,   (𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)))   )   ▶   ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = (((abs‘(𝐵𝑄))↑2) − ((abs‘(𝑃𝑄))↑2))   )
38  (   𝑣 ∈ (0(,)1)   ▶   𝑣 ∈ (0(,)1)   )
3938, 31 (   𝑣 ∈ (0(,)1)   ▶   𝑣 ∈ (0[,]1)   )
40  (   𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))   ▶   𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))   )
h41  (   𝜑   ▶   (abs‘(𝐴𝑄)) = (abs‘(𝐶𝑄))   )
4322, 41 (   𝜑   ▶   (abs‘(𝐶𝑄)) = (abs‘(𝐷𝑄))   )
443, 5, 29, 39, 40, 43 (   (   𝜑   ,   𝑣 ∈ (0(,)1)   ,   𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))   )   ▶   ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷))) = (((abs‘(𝐷𝑄))↑2) − ((abs‘(𝑃𝑄))↑2))   )
44b44 (   (   𝜑   ,   (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   )   ▶   ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷))) = (((abs‘(𝐷𝑄))↑2) − ((abs‘(𝑃𝑄))↑2))   )
4526, 35b, 44b (   (   𝜑   ,   (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   ,   (𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵)))   )   ▶   ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷)))   )
45b45 (   (   𝜑   ,   (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   )   ▶   ((𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) → ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷))))   )
45c45b (   (   𝜑   ,   (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   )   ▶   (∃𝑤(𝑤 ∈ (0(,)1) ∧ 𝑃 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐵))) → ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷))))   )
4618b, 45c (   (   𝜑   ,   (𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷)))   )   ▶   ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷)))   )
46b46 (   𝜑   ▶   ((𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) → ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷))))   )
46c46b (   𝜑   ▶   (∃𝑣(𝑣 ∈ (0(,)1) ∧ 𝑃 = ((𝑣 · 𝐶) + ((1 − 𝑣) · 𝐷))) → ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷))))   )
qed10b, 46c (   𝜑   ▶   ((abs‘(𝑃𝐴)) · (abs‘(𝑃𝐵))) = ((abs‘(𝑃𝐶)) · (abs‘(𝑃𝐷)))   )
  Copyright terms: Public domain W3C validator