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 
|- ( ph -> A e. CC )
chordthmlem5.B 
|- ( ph -> B e. CC )
chordthmlem5.Q 
|- ( ph -> Q e. CC )
chordthmlem5.X 
|- ( ph -> X e. ( 0 [,] 1 ) )
chordthmlem5.P 
|- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
chordthmlem5.ABequidistQ 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
Assertion chordthmlem5 
|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 chordthmlem5.A 
 |-  ( ph -> A e. CC )
2 chordthmlem5.B 
 |-  ( ph -> B e. CC )
3 chordthmlem5.Q 
 |-  ( ph -> Q e. CC )
4 chordthmlem5.X 
 |-  ( ph -> X e. ( 0 [,] 1 ) )
5 chordthmlem5.P 
 |-  ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
6 chordthmlem5.ABequidistQ 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
7 1 2 addcld 
 |-  ( ph -> ( A + B ) e. CC )
8 7 halfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. CC )
9 3 8 subcld 
 |-  ( ph -> ( Q - ( ( A + B ) / 2 ) ) e. CC )
10 9 abscld 
 |-  ( ph -> ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) e. RR )
11 10 recnd 
 |-  ( ph -> ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) e. CC )
12 11 sqcld 
 |-  ( ph -> ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) e. CC )
13 2 8 subcld 
 |-  ( ph -> ( B - ( ( A + B ) / 2 ) ) e. CC )
14 13 abscld 
 |-  ( ph -> ( abs ` ( B - ( ( A + B ) / 2 ) ) ) e. RR )
15 14 recnd 
 |-  ( ph -> ( abs ` ( B - ( ( A + B ) / 2 ) ) ) e. CC )
16 15 sqcld 
 |-  ( ph -> ( ( abs ` ( B - ( ( A + B ) / 2 ) ) ) ^ 2 ) e. CC )
17 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
18 17 4 sselid 
 |-  ( ph -> X e. RR )
19 18 recnd 
 |-  ( ph -> X e. CC )
20 19 1 mulcld 
 |-  ( ph -> ( X x. A ) e. CC )
21 1cnd 
 |-  ( ph -> 1 e. CC )
22 21 19 subcld 
 |-  ( ph -> ( 1 - X ) e. CC )
23 22 2 mulcld 
 |-  ( ph -> ( ( 1 - X ) x. B ) e. CC )
24 20 23 addcld 
 |-  ( ph -> ( ( X x. A ) + ( ( 1 - X ) x. B ) ) e. CC )
25 5 24 eqeltrd 
 |-  ( ph -> P e. CC )
26 25 8 subcld 
 |-  ( ph -> ( P - ( ( A + B ) / 2 ) ) e. CC )
27 26 abscld 
 |-  ( ph -> ( abs ` ( P - ( ( A + B ) / 2 ) ) ) e. RR )
28 27 recnd 
 |-  ( ph -> ( abs ` ( P - ( ( A + B ) / 2 ) ) ) e. CC )
29 28 sqcld 
 |-  ( ph -> ( ( abs ` ( P - ( ( A + B ) / 2 ) ) ) ^ 2 ) e. CC )
30 12 16 29 pnpcand 
 |-  ( ph -> ( ( ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) + ( ( abs ` ( B - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) - ( ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) + ( ( abs ` ( P - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) ) = ( ( ( abs ` ( B - ( ( A + B ) / 2 ) ) ) ^ 2 ) - ( ( abs ` ( P - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) )
31 0red 
 |-  ( ph -> 0 e. RR )
32 eqidd 
 |-  ( ph -> ( ( A + B ) / 2 ) = ( ( A + B ) / 2 ) )
33 1 mul02d 
 |-  ( ph -> ( 0 x. A ) = 0 )
34 21 subid1d 
 |-  ( ph -> ( 1 - 0 ) = 1 )
35 34 oveq1d 
 |-  ( ph -> ( ( 1 - 0 ) x. B ) = ( 1 x. B ) )
36 2 mulid2d 
 |-  ( ph -> ( 1 x. B ) = B )
37 35 36 eqtrd 
 |-  ( ph -> ( ( 1 - 0 ) x. B ) = B )
38 33 37 oveq12d 
 |-  ( ph -> ( ( 0 x. A ) + ( ( 1 - 0 ) x. B ) ) = ( 0 + B ) )
39 2 addid2d 
 |-  ( ph -> ( 0 + B ) = B )
40 38 39 eqtr2d 
 |-  ( ph -> B = ( ( 0 x. A ) + ( ( 1 - 0 ) x. B ) ) )
41 1 2 3 31 32 40 6 chordthmlem3 
 |-  ( ph -> ( ( abs ` ( B - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) + ( ( abs ` ( B - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) )
42 1 2 3 18 32 5 6 chordthmlem3 
 |-  ( ph -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) + ( ( abs ` ( P - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) )
43 41 42 oveq12d 
 |-  ( ph -> ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) = ( ( ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) + ( ( abs ` ( B - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) - ( ( ( abs ` ( Q - ( ( A + B ) / 2 ) ) ) ^ 2 ) + ( ( abs ` ( P - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) ) )
44 1 2 4 32 5 chordthmlem4 
 |-  ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - ( ( A + B ) / 2 ) ) ) ^ 2 ) - ( ( abs ` ( P - ( ( A + B ) / 2 ) ) ) ^ 2 ) ) )
45 30 43 44 3eqtr4rd 
 |-  ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )