Metamath Proof Explorer

Theorem chordthmALT

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'sElements, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm . https://us.metamath.org/other/completeusersproof/chordthmaltvd.html is a Virtual Deduction User's Proof transcription of chordthm . That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT Metamath proof. (Contributed by Alan Sare, 19-Sep-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses chordthmALT.angdef ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
chordthmALT.A ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
chordthmALT.B ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
chordthmALT.C ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
chordthmALT.D ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
chordthmALT.P ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
chordthmALT.AneP ⊢ ( 𝜑 → 𝐴 ≠ 𝑃 )
chordthmALT.BneP ⊢ ( 𝜑 → 𝐵 ≠ 𝑃 )
chordthmALT.CneP ⊢ ( 𝜑 → 𝐶 ≠ 𝑃 )
chordthmALT.DneP ⊢ ( 𝜑 → 𝐷 ≠ 𝑃 )
chordthmALT.APB ⊢ ( 𝜑 → ( ( 𝐴 − 𝑃 ) 𝐹 ( 𝐵 − 𝑃 ) ) = π )
chordthmALT.CPD ⊢ ( 𝜑 → ( ( 𝐶 − 𝑃 ) 𝐹 ( 𝐷 − 𝑃 ) ) = π )
chordthmALT.Q ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
chordthmALT.ABcirc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
chordthmALT.ACcirc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐶 − 𝑄 ) ) )
chordthmALT.ADcirc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) )
Assertion chordthmALT ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 chordthmALT.angdef ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 chordthmALT.A ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3 chordthmALT.B ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4 chordthmALT.C ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 chordthmALT.D ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
6 chordthmALT.P ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
7 chordthmALT.AneP ⊢ ( 𝜑 → 𝐴 ≠ 𝑃 )
8 chordthmALT.BneP ⊢ ( 𝜑 → 𝐵 ≠ 𝑃 )
9 chordthmALT.CneP ⊢ ( 𝜑 → 𝐶 ≠ 𝑃 )
10 chordthmALT.DneP ⊢ ( 𝜑 → 𝐷 ≠ 𝑃 )
11 chordthmALT.APB ⊢ ( 𝜑 → ( ( 𝐴 − 𝑃 ) 𝐹 ( 𝐵 − 𝑃 ) ) = π )
12 chordthmALT.CPD ⊢ ( 𝜑 → ( ( 𝐶 − 𝑃 ) 𝐹 ( 𝐷 − 𝑃 ) ) = π )
13 chordthmALT.Q ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
14 chordthmALT.ABcirc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
15 chordthmALT.ACcirc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐶 − 𝑄 ) ) )
16 chordthmALT.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 df-rex ⊢ ( ∃ 𝑣 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) )
21 20 biimpi ⊢ ( ∃ 𝑣 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) → ∃ 𝑣 ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) )
22 19 21 syl ⊢ ( 𝜑 → ∃ 𝑣 ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) )
23 8 necomd ⊢ ( 𝜑 → 𝑃 ≠ 𝐵 )
24 1 2 6 3 7 23 angpieqvd ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝑃 ) 𝐹 ( 𝐵 − 𝑃 ) ) = π ↔ ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) )
25 11 24 mpbid ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) )
26 df-rex ⊢ ( ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) )
27 26 biimpi ⊢ ( ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) → ∃ 𝑤 ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) )
28 25 27 syl ⊢ ( 𝜑 → ∃ 𝑤 ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ∃ 𝑤 ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) )
30 14 16 eqtr3d ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) )
31 30 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) )
32 31 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
34 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → 𝐴 ∈ ℂ )
35 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → 𝐵 ∈ ℂ )
36 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → 𝑄 ∈ ℂ )
37 ioossicc ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
38 id ⊢ ( 𝑤 ∈ ( 0 (,) 1 ) → 𝑤 ∈ ( 0 (,) 1 ) )
39 37 38 sselid ⊢ ( 𝑤 ∈ ( 0 (,) 1 ) → 𝑤 ∈ ( 0 [,] 1 ) )
40 39 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → 𝑤 ∈ ( 0 [,] 1 ) )
41 id ⊢ ( 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) → 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) )
42 41 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) )
43 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
44 34 35 36 40 42 43 chordthmlem5 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
45 44 3expb ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
46 45 3adant2 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
47 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → 𝐶 ∈ ℂ )
48 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → 𝐷 ∈ ℂ )
49 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → 𝑄 ∈ ℂ )
50 id ⊢ ( 𝑣 ∈ ( 0 (,) 1 ) → 𝑣 ∈ ( 0 (,) 1 ) )
51 37 50 sselid ⊢ ( 𝑣 ∈ ( 0 (,) 1 ) → 𝑣 ∈ ( 0 [,] 1 ) )
52 51 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → 𝑣 ∈ ( 0 [,] 1 ) )
53 id ⊢ ( 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) → 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) )
54 53 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) )
55 15 16 eqtr3d ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) )
56 55 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → ( abs ‘ ( 𝐶 − 𝑄 ) ) = ( abs ‘ ( 𝐷 − 𝑄 ) ) )
57 47 48 49 52 54 56 chordthmlem5 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
58 57 3expb ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
59 58 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) = ( ( ( abs ‘ ( 𝐷 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )
60 33 46 59 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ∧ ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) )
61 60 3expia ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ( ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) )
62 61 exlimdv ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ( ∃ 𝑤 ( 𝑤 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐵 ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) )
63 29 62 mpd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) )
64 63 ex ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) )
65 64 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ( 𝑣 ∈ ( 0 (,) 1 ) ∧ 𝑃 = ( ( 𝑣 · 𝐶 ) + ( ( 1 − 𝑣 ) · 𝐷 ) ) ) → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) ) )
66 22 65 mpd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( abs ‘ ( 𝑃 − 𝐶 ) ) · ( abs ‘ ( 𝑃 − 𝐷 ) ) ) )