Metamath Proof Explorer

Theorem chordthmlem5

Description: If P is on the segment AB and AQ = BQ, then PA x. PB = BQ2 - PQ2. This follows from two uses of chordthmlem3 to show that PQ2 = QM2 + PM2 and BQ2 = QM2 + BM2, so BQ2 - PQ2 = (QM2 + BM2) - (QM2 + PM2) = BM2 - PM2, which equals PA x. PB by chordthmlem4 . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses chordthmlem5.A ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
chordthmlem5.B ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
chordthmlem5.Q ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
chordthmlem5.X ⊢ ( 𝜑 → 𝑋 ∈ ( 0 [,] 1 ) )
chordthmlem5.P ⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
chordthmlem5.ABequidistQ ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
Assertion chordthmlem5 ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 chordthmlem5.A ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 chordthmlem5.B ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 chordthmlem5.Q ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
4 chordthmlem5.X ⊢ ( 𝜑 → 𝑋 ∈ ( 0 [,] 1 ) )
5 chordthmlem5.P ⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
6 chordthmlem5.ABequidistQ ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
7 1 2 addcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
8 7 halfcld ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
9 3 8 subcld ⊢ ( 𝜑 → ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
10 9 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
11 10 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℂ )
12 11 sqcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ∈ ℂ )
13 2 8 subcld ⊢ ( 𝜑 → ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
14 13 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
15 14 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℂ )
16 15 sqcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ∈ ℂ )
17 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
18 17 4 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
20 19 1 mulcld ⊢ ( 𝜑 → ( 𝑋 · 𝐴 ) ∈ ℂ )
21 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
22 21 19 subcld ⊢ ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ )
23 22 2 mulcld ⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · 𝐵 ) ∈ ℂ )
24 20 23 addcld ⊢ ( 𝜑 → ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ∈ ℂ )
25 5 24 eqeltrd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
26 25 8 subcld ⊢ ( 𝜑 → ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
27 26 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
28 27 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℂ )
29 28 sqcld ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ∈ ℂ )
30 12 16 29 pnpcand ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) − ( ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) ) = ( ( ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) )
31 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
32 eqidd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) = ( ( 𝐴 + 𝐵 ) / 2 ) )
33 1 mul02d ⊢ ( 𝜑 → ( 0 · 𝐴 ) = 0 )
34 21 subid1d ⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
35 34 oveq1d ⊢ ( 𝜑 → ( ( 1 − 0 ) · 𝐵 ) = ( 1 · 𝐵 ) )
36 2 mullidd ⊢ ( 𝜑 → ( 1 · 𝐵 ) = 𝐵 )
37 35 36 eqtrd ⊢ ( 𝜑 → ( ( 1 − 0 ) · 𝐵 ) = 𝐵 )
38 33 37 oveq12d ⊢ ( 𝜑 → ( ( 0 · 𝐴 ) + ( ( 1 − 0 ) · 𝐵 ) ) = ( 0 + 𝐵 ) )
39 2 addlidd ⊢ ( 𝜑 → ( 0 + 𝐵 ) = 𝐵 )
40 38 39 eqtr2d ⊢ ( 𝜑 → 𝐵 = ( ( 0 · 𝐴 ) + ( ( 1 − 0 ) · 𝐵 ) ) )
41 1 2 3 31 32 40 6 chordthmlem3 ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) )
42 1 2 3 18 32 5 6 chordthmlem3 ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) )
43 41 42 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) − ( ( ( abs ‘ ( 𝑄 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) ) )
44 1 2 4 32 5 chordthmlem4 ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ↑ 2 ) ) )
45 30 43 44 3eqtr4rd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝐴 ) ) · ( abs ‘ ( 𝑃 − 𝐵 ) ) ) = ( ( ( abs ‘ ( 𝐵 − 𝑄 ) ) ↑ 2 ) − ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) ) )