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 φ A
chordthmlem5.B φ B
chordthmlem5.Q φ Q
chordthmlem5.X φ X 0 1
chordthmlem5.P φ P = X A + 1 X B
chordthmlem5.ABequidistQ φ A Q = B Q
Assertion chordthmlem5 φ P A P B = B Q 2 P Q 2

Proof

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