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 ( 𝜑𝐴 ∈ ℂ )
chordthmlem3.B ( 𝜑𝐵 ∈ ℂ )
chordthmlem3.Q ( 𝜑𝑄 ∈ ℂ )
chordthmlem3.X ( 𝜑𝑋 ∈ ℝ )
chordthmlem3.M ( 𝜑𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
chordthmlem3.P ( 𝜑𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
chordthmlem3.ABequidistQ ( 𝜑 → ( abs ‘ ( 𝐴𝑄 ) ) = ( abs ‘ ( 𝐵𝑄 ) ) )
Assertion chordthmlem3 ( 𝜑 → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 chordthmlem3.A ( 𝜑𝐴 ∈ ℂ )
2 chordthmlem3.B ( 𝜑𝐵 ∈ ℂ )
3 chordthmlem3.Q ( 𝜑𝑄 ∈ ℂ )
4 chordthmlem3.X ( 𝜑𝑋 ∈ ℝ )
5 chordthmlem3.M ( 𝜑𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
6 chordthmlem3.P ( 𝜑𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
7 chordthmlem3.ABequidistQ ( 𝜑 → ( abs ‘ ( 𝐴𝑄 ) ) = ( abs ‘ ( 𝐵𝑄 ) ) )
8 1 2 addcld ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
9 8 halfcld ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
10 5 9 eqeltrd ( 𝜑𝑀 ∈ ℂ )
11 3 10 subcld ( 𝜑 → ( 𝑄𝑀 ) ∈ ℂ )
12 11 abscld ( 𝜑 → ( abs ‘ ( 𝑄𝑀 ) ) ∈ ℝ )
13 12 recnd ( 𝜑 → ( abs ‘ ( 𝑄𝑀 ) ) ∈ ℂ )
14 13 sqcld ( 𝜑 → ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) ∈ ℂ )
15 14 adantr ( ( 𝜑𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) ∈ ℂ )
16 15 addid1d ( ( 𝜑𝑃 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + 0 ) = ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) )
17 4 recnd ( 𝜑𝑋 ∈ ℂ )
18 17 1 mulcld ( 𝜑 → ( 𝑋 · 𝐴 ) ∈ ℂ )
19 1cnd ( 𝜑 → 1 ∈ ℂ )
20 19 17 subcld ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ )
21 20 2 mulcld ( 𝜑 → ( ( 1 − 𝑋 ) · 𝐵 ) ∈ ℂ )
22 18 21 addcld ( 𝜑 → ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ∈ ℂ )
23 6 22 eqeltrd ( 𝜑𝑃 ∈ ℂ )
24 23 adantr ( ( 𝜑𝑃 = 𝑀 ) → 𝑃 ∈ ℂ )
25 simpr ( ( 𝜑𝑃 = 𝑀 ) → 𝑃 = 𝑀 )
26 24 25 subeq0bd ( ( 𝜑𝑃 = 𝑀 ) → ( 𝑃𝑀 ) = 0 )
27 26 abs00bd ( ( 𝜑𝑃 = 𝑀 ) → ( abs ‘ ( 𝑃𝑀 ) ) = 0 )
28 27 sq0id ( ( 𝜑𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) = 0 )
29 28 oveq2d ( ( 𝜑𝑃 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + 0 ) )
30 3 adantr ( ( 𝜑𝑃 = 𝑀 ) → 𝑄 ∈ ℂ )
31 30 24 abssubd ( ( 𝜑𝑃 = 𝑀 ) → ( abs ‘ ( 𝑄𝑃 ) ) = ( abs ‘ ( 𝑃𝑄 ) ) )
32 25 oveq2d ( ( 𝜑𝑃 = 𝑀 ) → ( 𝑄𝑃 ) = ( 𝑄𝑀 ) )
33 32 fveq2d ( ( 𝜑𝑃 = 𝑀 ) → ( abs ‘ ( 𝑄𝑃 ) ) = ( abs ‘ ( 𝑄𝑀 ) ) )
34 31 33 eqtr3d ( ( 𝜑𝑃 = 𝑀 ) → ( abs ‘ ( 𝑃𝑄 ) ) = ( abs ‘ ( 𝑄𝑀 ) ) )
35 34 oveq1d ( ( 𝜑𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) )
36 16 29 35 3eqtr4rd ( ( 𝜑𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )
37 23 10 subcld ( 𝜑 → ( 𝑃𝑀 ) ∈ ℂ )
38 37 abscld ( 𝜑 → ( abs ‘ ( 𝑃𝑀 ) ) ∈ ℝ )
39 38 recnd ( 𝜑 → ( abs ‘ ( 𝑃𝑀 ) ) ∈ ℂ )
40 39 sqcld ( 𝜑 → ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ∈ ℂ )
41 40 adantr ( ( 𝜑𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ∈ ℂ )
42 41 addid2d ( ( 𝜑𝑄 = 𝑀 ) → ( 0 + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) = ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) )
43 3 adantr ( ( 𝜑𝑄 = 𝑀 ) → 𝑄 ∈ ℂ )
44 simpr ( ( 𝜑𝑄 = 𝑀 ) → 𝑄 = 𝑀 )
45 43 44 subeq0bd ( ( 𝜑𝑄 = 𝑀 ) → ( 𝑄𝑀 ) = 0 )
46 45 abs00bd ( ( 𝜑𝑄 = 𝑀 ) → ( abs ‘ ( 𝑄𝑀 ) ) = 0 )
47 46 sq0id ( ( 𝜑𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) = 0 )
48 47 oveq1d ( ( 𝜑𝑄 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) = ( 0 + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )
49 44 oveq2d ( ( 𝜑𝑄 = 𝑀 ) → ( 𝑃𝑄 ) = ( 𝑃𝑀 ) )
50 49 fveq2d ( ( 𝜑𝑄 = 𝑀 ) → ( abs ‘ ( 𝑃𝑄 ) ) = ( abs ‘ ( 𝑃𝑀 ) ) )
51 50 oveq1d ( ( 𝜑𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) )
52 42 48 51 3eqtr4rd ( ( 𝜑𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )
53 23 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑃 ∈ ℂ )
54 3 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑄 ∈ ℂ )
55 10 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑀 ∈ ℂ )
56 simprl ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑃𝑀 )
57 simprr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑄𝑀 )
58 eqid ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
59 1 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝐴 ∈ ℂ )
60 2 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝐵 ∈ ℂ )
61 4 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑋 ∈ ℝ )
62 5 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
63 6 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
64 7 adantr ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → ( abs ‘ ( 𝐴𝑄 ) ) = ( abs ‘ ( 𝐵𝑄 ) ) )
65 58 59 60 54 61 62 63 64 56 57 chordthmlem2 ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → ( ( 𝑄𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )
66 eqid ( abs ‘ ( 𝑄𝑀 ) ) = ( abs ‘ ( 𝑄𝑀 ) )
67 eqid ( abs ‘ ( 𝑃𝑀 ) ) = ( abs ‘ ( 𝑃𝑀 ) )
68 eqid ( abs ‘ ( 𝑃𝑄 ) ) = ( abs ‘ ( 𝑃𝑄 ) )
69 eqid ( ( 𝑄𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃𝑀 ) ) = ( ( 𝑄𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃𝑀 ) )
70 58 66 67 68 69 pythag ( ( ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑃𝑀𝑄𝑀 ) ∧ ( ( 𝑄𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )
71 53 54 55 56 57 65 70 syl321anc ( ( 𝜑 ∧ ( 𝑃𝑀𝑄𝑀 ) ) → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )
72 36 52 71 pm2.61da2ne ( 𝜑 → ( ( abs ‘ ( 𝑃𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃𝑀 ) ) ↑ 2 ) ) )