Metamath Proof Explorer


Theorem chordthmlem

Description: If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right angles. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses chordthmlem.angdef 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
chordthmlem.A ( 𝜑𝐴 ∈ ℂ )
chordthmlem.B ( 𝜑𝐵 ∈ ℂ )
chordthmlem.Q ( 𝜑𝑄 ∈ ℂ )
chordthmlem.M ( 𝜑𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
chordthmlem.ABequidistQ ( 𝜑 → ( abs ‘ ( 𝐴𝑄 ) ) = ( abs ‘ ( 𝐵𝑄 ) ) )
chordthmlem.AneB ( 𝜑𝐴𝐵 )
chordthmlem.QneM ( 𝜑𝑄𝑀 )
Assertion chordthmlem ( 𝜑 → ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )

Proof

Step Hyp Ref Expression
1 chordthmlem.angdef 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 chordthmlem.A ( 𝜑𝐴 ∈ ℂ )
3 chordthmlem.B ( 𝜑𝐵 ∈ ℂ )
4 chordthmlem.Q ( 𝜑𝑄 ∈ ℂ )
5 chordthmlem.M ( 𝜑𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
6 chordthmlem.ABequidistQ ( 𝜑 → ( abs ‘ ( 𝐴𝑄 ) ) = ( abs ‘ ( 𝐵𝑄 ) ) )
7 chordthmlem.AneB ( 𝜑𝐴𝐵 )
8 chordthmlem.QneM ( 𝜑𝑄𝑀 )
9 negpitopissre ( - π (,] π ) ⊆ ℝ
10 2 3 addcld ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
11 10 halfcld ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
12 5 11 eqeltrd ( 𝜑𝑀 ∈ ℂ )
13 4 12 subcld ( 𝜑 → ( 𝑄𝑀 ) ∈ ℂ )
14 4 12 8 subne0d ( 𝜑 → ( 𝑄𝑀 ) ≠ 0 )
15 3 12 subcld ( 𝜑 → ( 𝐵𝑀 ) ∈ ℂ )
16 5 oveq1d ( 𝜑 → ( 𝑀 · 2 ) = ( ( ( 𝐴 + 𝐵 ) / 2 ) · 2 ) )
17 12 times2d ( 𝜑 → ( 𝑀 · 2 ) = ( 𝑀 + 𝑀 ) )
18 2cnd ( 𝜑 → 2 ∈ ℂ )
19 2ne0 2 ≠ 0
20 19 a1i ( 𝜑 → 2 ≠ 0 )
21 10 18 20 divcan1d ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) / 2 ) · 2 ) = ( 𝐴 + 𝐵 ) )
22 16 17 21 3eqtr3d ( 𝜑 → ( 𝑀 + 𝑀 ) = ( 𝐴 + 𝐵 ) )
23 2 3 3 7 addneintr2d ( 𝜑 → ( 𝐴 + 𝐵 ) ≠ ( 𝐵 + 𝐵 ) )
24 22 23 eqnetrd ( 𝜑 → ( 𝑀 + 𝑀 ) ≠ ( 𝐵 + 𝐵 ) )
25 24 neneqd ( 𝜑 → ¬ ( 𝑀 + 𝑀 ) = ( 𝐵 + 𝐵 ) )
26 oveq12 ( ( 𝑀 = 𝐵𝑀 = 𝐵 ) → ( 𝑀 + 𝑀 ) = ( 𝐵 + 𝐵 ) )
27 26 anidms ( 𝑀 = 𝐵 → ( 𝑀 + 𝑀 ) = ( 𝐵 + 𝐵 ) )
28 25 27 nsyl ( 𝜑 → ¬ 𝑀 = 𝐵 )
29 28 neqned ( 𝜑𝑀𝐵 )
30 29 necomd ( 𝜑𝐵𝑀 )
31 3 12 30 subne0d ( 𝜑 → ( 𝐵𝑀 ) ≠ 0 )
32 1 13 14 15 31 angcld ( 𝜑 → ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ ( - π (,] π ) )
33 9 32 sselid ( 𝜑 → ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ ℝ )
34 33 recnd ( 𝜑 → ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ ℂ )
35 34 coscld ( 𝜑 → ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) ∈ ℂ )
36 3 12 negsubdi2d ( 𝜑 → - ( 𝐵𝑀 ) = ( 𝑀𝐵 ) )
37 12 12 2 3 addsubeq4d ( 𝜑 → ( ( 𝑀 + 𝑀 ) = ( 𝐴 + 𝐵 ) ↔ ( 𝐴𝑀 ) = ( 𝑀𝐵 ) ) )
38 22 37 mpbid ( 𝜑 → ( 𝐴𝑀 ) = ( 𝑀𝐵 ) )
39 36 38 eqtr4d ( 𝜑 → - ( 𝐵𝑀 ) = ( 𝐴𝑀 ) )
40 39 oveq2d ( 𝜑 → ( ( 𝑄𝑀 ) 𝐹 - ( 𝐵𝑀 ) ) = ( ( 𝑄𝑀 ) 𝐹 ( 𝐴𝑀 ) ) )
41 40 fveq2d ( 𝜑 → ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 - ( 𝐵𝑀 ) ) ) = ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐴𝑀 ) ) ) )
42 1 13 14 15 31 cosangneg2d ( 𝜑 → ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 - ( 𝐵𝑀 ) ) ) = - ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) )
43 2 2 3 7 addneintrd ( 𝜑 → ( 𝐴 + 𝐴 ) ≠ ( 𝐴 + 𝐵 ) )
44 43 22 neeqtrrd ( 𝜑 → ( 𝐴 + 𝐴 ) ≠ ( 𝑀 + 𝑀 ) )
45 44 necomd ( 𝜑 → ( 𝑀 + 𝑀 ) ≠ ( 𝐴 + 𝐴 ) )
46 45 neneqd ( 𝜑 → ¬ ( 𝑀 + 𝑀 ) = ( 𝐴 + 𝐴 ) )
47 oveq12 ( ( 𝑀 = 𝐴𝑀 = 𝐴 ) → ( 𝑀 + 𝑀 ) = ( 𝐴 + 𝐴 ) )
48 47 anidms ( 𝑀 = 𝐴 → ( 𝑀 + 𝑀 ) = ( 𝐴 + 𝐴 ) )
49 46 48 nsyl ( 𝜑 → ¬ 𝑀 = 𝐴 )
50 49 neqned ( 𝜑𝑀𝐴 )
51 eqidd ( 𝜑 → ( abs ‘ ( 𝑄𝑀 ) ) = ( abs ‘ ( 𝑄𝑀 ) ) )
52 2 12 subcld ( 𝜑 → ( 𝐴𝑀 ) ∈ ℂ )
53 52 absnegd ( 𝜑 → ( abs ‘ - ( 𝐴𝑀 ) ) = ( abs ‘ ( 𝐴𝑀 ) ) )
54 2 12 negsubdi2d ( 𝜑 → - ( 𝐴𝑀 ) = ( 𝑀𝐴 ) )
55 54 fveq2d ( 𝜑 → ( abs ‘ - ( 𝐴𝑀 ) ) = ( abs ‘ ( 𝑀𝐴 ) ) )
56 38 fveq2d ( 𝜑 → ( abs ‘ ( 𝐴𝑀 ) ) = ( abs ‘ ( 𝑀𝐵 ) ) )
57 53 55 56 3eqtr3d ( 𝜑 → ( abs ‘ ( 𝑀𝐴 ) ) = ( abs ‘ ( 𝑀𝐵 ) ) )
58 1 4 12 2 4 12 3 8 50 8 29 51 57 6 ssscongptld ( 𝜑 → ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐴𝑀 ) ) ) = ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) )
59 41 42 58 3eqtr3rd ( 𝜑 → ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) = - ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) )
60 35 59 eqnegad ( 𝜑 → ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) = 0 )
61 coseq0negpitopi ( ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ ( - π (,] π ) → ( ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) = 0 ↔ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
62 32 61 syl ( 𝜑 → ( ( cos ‘ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ) = 0 ↔ ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
63 60 62 mpbid ( 𝜑 → ( ( 𝑄𝑀 ) 𝐹 ( 𝐵𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )