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 addridd ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( ( 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 addlidd ⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 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 ) ) )