Metamath Proof Explorer

Theorem chordthmlem3

Description: If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ2 = QM2 + PM2. This follows from chordthmlem2 and the Pythagorean theorem ( pythag ) in the case where P and Q are unequal to M. If either P or Q equals M, the result is trivial. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses chordthmlem3.A 
|- ( ph -> A e. CC )
chordthmlem3.B 
|- ( ph -> B e. CC )
chordthmlem3.Q 
|- ( ph -> Q e. CC )
chordthmlem3.X 
|- ( ph -> X e. RR )
chordthmlem3.M 
|- ( ph -> M = ( ( A + B ) / 2 ) )
chordthmlem3.P 
|- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
chordthmlem3.ABequidistQ 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
Assertion chordthmlem3 
|- ( ph -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 chordthmlem3.A 
 |-  ( ph -> A e. CC )
2 chordthmlem3.B 
 |-  ( ph -> B e. CC )
3 chordthmlem3.Q 
 |-  ( ph -> Q e. CC )
4 chordthmlem3.X 
 |-  ( ph -> X e. RR )
5 chordthmlem3.M 
 |-  ( ph -> M = ( ( A + B ) / 2 ) )
6 chordthmlem3.P 
 |-  ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
7 chordthmlem3.ABequidistQ 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
8 1 2 addcld 
 |-  ( ph -> ( A + B ) e. CC )
9 8 halfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. CC )
10 5 9 eqeltrd 
 |-  ( ph -> M e. CC )
11 3 10 subcld 
 |-  ( ph -> ( Q - M ) e. CC )
12 11 abscld 
 |-  ( ph -> ( abs ` ( Q - M ) ) e. RR )
13 12 recnd 
 |-  ( ph -> ( abs ` ( Q - M ) ) e. CC )
14 13 sqcld 
 |-  ( ph -> ( ( abs ` ( Q - M ) ) ^ 2 ) e. CC )
15 14 adantr 
 |-  ( ( ph /\ P = M ) -> ( ( abs ` ( Q - M ) ) ^ 2 ) e. CC )
16 15 addid1d 
 |-  ( ( ph /\ P = M ) -> ( ( ( abs ` ( Q - M ) ) ^ 2 ) + 0 ) = ( ( abs ` ( Q - M ) ) ^ 2 ) )
17 4 recnd 
 |-  ( ph -> X e. CC )
18 17 1 mulcld 
 |-  ( ph -> ( X x. A ) e. CC )
19 1cnd 
 |-  ( ph -> 1 e. CC )
20 19 17 subcld 
 |-  ( ph -> ( 1 - X ) e. CC )
21 20 2 mulcld 
 |-  ( ph -> ( ( 1 - X ) x. B ) e. CC )
22 18 21 addcld 
 |-  ( ph -> ( ( X x. A ) + ( ( 1 - X ) x. B ) ) e. CC )
23 6 22 eqeltrd 
 |-  ( ph -> P e. CC )
24 23 adantr 
 |-  ( ( ph /\ P = M ) -> P e. CC )
25 simpr 
 |-  ( ( ph /\ P = M ) -> P = M )
26 24 25 subeq0bd 
 |-  ( ( ph /\ P = M ) -> ( P - M ) = 0 )
27 26 abs00bd 
 |-  ( ( ph /\ P = M ) -> ( abs ` ( P - M ) ) = 0 )
28 27 sq0id 
 |-  ( ( ph /\ P = M ) -> ( ( abs ` ( P - M ) ) ^ 2 ) = 0 )
29 28 oveq2d 
 |-  ( ( ph /\ P = M ) -> ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + 0 ) )
30 3 adantr 
 |-  ( ( ph /\ P = M ) -> Q e. CC )
31 30 24 abssubd 
 |-  ( ( ph /\ P = M ) -> ( abs ` ( Q - P ) ) = ( abs ` ( P - Q ) ) )
32 25 oveq2d 
 |-  ( ( ph /\ P = M ) -> ( Q - P ) = ( Q - M ) )
33 32 fveq2d 
 |-  ( ( ph /\ P = M ) -> ( abs ` ( Q - P ) ) = ( abs ` ( Q - M ) ) )
34 31 33 eqtr3d 
 |-  ( ( ph /\ P = M ) -> ( abs ` ( P - Q ) ) = ( abs ` ( Q - M ) ) )
35 34 oveq1d 
 |-  ( ( ph /\ P = M ) -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( abs ` ( Q - M ) ) ^ 2 ) )
36 16 29 35 3eqtr4rd 
 |-  ( ( ph /\ P = M ) -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )
37 23 10 subcld 
 |-  ( ph -> ( P - M ) e. CC )
38 37 abscld 
 |-  ( ph -> ( abs ` ( P - M ) ) e. RR )
39 38 recnd 
 |-  ( ph -> ( abs ` ( P - M ) ) e. CC )
40 39 sqcld 
 |-  ( ph -> ( ( abs ` ( P - M ) ) ^ 2 ) e. CC )
41 40 adantr 
 |-  ( ( ph /\ Q = M ) -> ( ( abs ` ( P - M ) ) ^ 2 ) e. CC )
42 41 addid2d 
 |-  ( ( ph /\ Q = M ) -> ( 0 + ( ( abs ` ( P - M ) ) ^ 2 ) ) = ( ( abs ` ( P - M ) ) ^ 2 ) )
43 3 adantr 
 |-  ( ( ph /\ Q = M ) -> Q e. CC )
44 simpr 
 |-  ( ( ph /\ Q = M ) -> Q = M )
45 43 44 subeq0bd 
 |-  ( ( ph /\ Q = M ) -> ( Q - M ) = 0 )
46 45 abs00bd 
 |-  ( ( ph /\ Q = M ) -> ( abs ` ( Q - M ) ) = 0 )
47 46 sq0id 
 |-  ( ( ph /\ Q = M ) -> ( ( abs ` ( Q - M ) ) ^ 2 ) = 0 )
48 47 oveq1d 
 |-  ( ( ph /\ Q = M ) -> ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) = ( 0 + ( ( abs ` ( P - M ) ) ^ 2 ) ) )
49 44 oveq2d 
 |-  ( ( ph /\ Q = M ) -> ( P - Q ) = ( P - M ) )
50 49 fveq2d 
 |-  ( ( ph /\ Q = M ) -> ( abs ` ( P - Q ) ) = ( abs ` ( P - M ) ) )
51 50 oveq1d 
 |-  ( ( ph /\ Q = M ) -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( abs ` ( P - M ) ) ^ 2 ) )
52 42 48 51 3eqtr4rd 
 |-  ( ( ph /\ Q = M ) -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )
53 23 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> P e. CC )
54 3 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> Q e. CC )
55 10 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> M e. CC )
56 simprl 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> P =/= M )
57 simprr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> Q =/= M )
58 eqid 
 |-  ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
59 1 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> A e. CC )
60 2 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> B e. CC )
61 4 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> X e. RR )
62 5 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> M = ( ( A + B ) / 2 ) )
63 6 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
64 7 adantr 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
65 58 59 60 54 61 62 63 64 56 57 chordthmlem2 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> ( ( Q - M ) ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) ( P - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
66 eqid 
 |-  ( abs ` ( Q - M ) ) = ( abs ` ( Q - M ) )
67 eqid 
 |-  ( abs ` ( P - M ) ) = ( abs ` ( P - M ) )
68 eqid 
 |-  ( abs ` ( P - Q ) ) = ( abs ` ( P - Q ) )
69 eqid 
 |-  ( ( Q - M ) ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) ( P - M ) ) = ( ( Q - M ) ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) ( P - M ) )
70 58 66 67 68 69 pythag 
 |-  ( ( ( P e. CC /\ Q e. CC /\ M e. CC ) /\ ( P =/= M /\ Q =/= M ) /\ ( ( Q - M ) ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) ) ( P - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )
71 53 54 55 56 57 65 70 syl321anc 
 |-  ( ( ph /\ ( P =/= M /\ Q =/= M ) ) -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )
72 36 52 71 pm2.61da2ne 
 |-  ( ph -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )