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 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
chordthmlem.A 
|- ( ph -> A e. CC )
chordthmlem.B 
|- ( ph -> B e. CC )
chordthmlem.Q 
|- ( ph -> Q e. CC )
chordthmlem.M 
|- ( ph -> M = ( ( A + B ) / 2 ) )
chordthmlem.ABequidistQ 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
chordthmlem.AneB 
|- ( ph -> A =/= B )
chordthmlem.QneM 
|- ( ph -> Q =/= M )
Assertion chordthmlem 
|- ( ph -> ( ( Q - M ) F ( B - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )

Proof

Step Hyp Ref Expression
1 chordthmlem.angdef 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 chordthmlem.A 
 |-  ( ph -> A e. CC )
3 chordthmlem.B 
 |-  ( ph -> B e. CC )
4 chordthmlem.Q 
 |-  ( ph -> Q e. CC )
5 chordthmlem.M 
 |-  ( ph -> M = ( ( A + B ) / 2 ) )
6 chordthmlem.ABequidistQ 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
7 chordthmlem.AneB 
 |-  ( ph -> A =/= B )
8 chordthmlem.QneM 
 |-  ( ph -> Q =/= M )
9 negpitopissre 
 |-  ( -u _pi (,] _pi ) C_ RR
10 2 3 addcld 
 |-  ( ph -> ( A + B ) e. CC )
11 10 halfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. CC )
12 5 11 eqeltrd 
 |-  ( ph -> M e. CC )
13 4 12 subcld 
 |-  ( ph -> ( Q - M ) e. CC )
14 4 12 8 subne0d 
 |-  ( ph -> ( Q - M ) =/= 0 )
15 3 12 subcld 
 |-  ( ph -> ( B - M ) e. CC )
16 5 oveq1d 
 |-  ( ph -> ( M x. 2 ) = ( ( ( A + B ) / 2 ) x. 2 ) )
17 12 times2d 
 |-  ( ph -> ( M x. 2 ) = ( M + M ) )
18 2cnd 
 |-  ( ph -> 2 e. CC )
19 2ne0 
 |-  2 =/= 0
20 19 a1i 
 |-  ( ph -> 2 =/= 0 )
21 10 18 20 divcan1d 
 |-  ( ph -> ( ( ( A + B ) / 2 ) x. 2 ) = ( A + B ) )
22 16 17 21 3eqtr3d 
 |-  ( ph -> ( M + M ) = ( A + B ) )
23 2 3 3 7 addneintr2d 
 |-  ( ph -> ( A + B ) =/= ( B + B ) )
24 22 23 eqnetrd 
 |-  ( ph -> ( M + M ) =/= ( B + B ) )
25 24 neneqd 
 |-  ( ph -> -. ( M + M ) = ( B + B ) )
26 oveq12 
 |-  ( ( M = B /\ M = B ) -> ( M + M ) = ( B + B ) )
27 26 anidms 
 |-  ( M = B -> ( M + M ) = ( B + B ) )
28 25 27 nsyl 
 |-  ( ph -> -. M = B )
29 28 neqned 
 |-  ( ph -> M =/= B )
30 29 necomd 
 |-  ( ph -> B =/= M )
31 3 12 30 subne0d 
 |-  ( ph -> ( B - M ) =/= 0 )
32 1 13 14 15 31 angcld 
 |-  ( ph -> ( ( Q - M ) F ( B - M ) ) e. ( -u _pi (,] _pi ) )
33 9 32 sselid 
 |-  ( ph -> ( ( Q - M ) F ( B - M ) ) e. RR )
34 33 recnd 
 |-  ( ph -> ( ( Q - M ) F ( B - M ) ) e. CC )
35 34 coscld 
 |-  ( ph -> ( cos ` ( ( Q - M ) F ( B - M ) ) ) e. CC )
36 3 12 negsubdi2d 
 |-  ( ph -> -u ( B - M ) = ( M - B ) )
37 12 12 2 3 addsubeq4d 
 |-  ( ph -> ( ( M + M ) = ( A + B ) <-> ( A - M ) = ( M - B ) ) )
38 22 37 mpbid 
 |-  ( ph -> ( A - M ) = ( M - B ) )
39 36 38 eqtr4d 
 |-  ( ph -> -u ( B - M ) = ( A - M ) )
40 39 oveq2d 
 |-  ( ph -> ( ( Q - M ) F -u ( B - M ) ) = ( ( Q - M ) F ( A - M ) ) )
41 40 fveq2d 
 |-  ( ph -> ( cos ` ( ( Q - M ) F -u ( B - M ) ) ) = ( cos ` ( ( Q - M ) F ( A - M ) ) ) )
42 1 13 14 15 31 cosangneg2d 
 |-  ( ph -> ( cos ` ( ( Q - M ) F -u ( B - M ) ) ) = -u ( cos ` ( ( Q - M ) F ( B - M ) ) ) )
43 2 2 3 7 addneintrd 
 |-  ( ph -> ( A + A ) =/= ( A + B ) )
44 43 22 neeqtrrd 
 |-  ( ph -> ( A + A ) =/= ( M + M ) )
45 44 necomd 
 |-  ( ph -> ( M + M ) =/= ( A + A ) )
46 45 neneqd 
 |-  ( ph -> -. ( M + M ) = ( A + A ) )
47 oveq12 
 |-  ( ( M = A /\ M = A ) -> ( M + M ) = ( A + A ) )
48 47 anidms 
 |-  ( M = A -> ( M + M ) = ( A + A ) )
49 46 48 nsyl 
 |-  ( ph -> -. M = A )
50 49 neqned 
 |-  ( ph -> M =/= A )
51 eqidd 
 |-  ( ph -> ( abs ` ( Q - M ) ) = ( abs ` ( Q - M ) ) )
52 2 12 subcld 
 |-  ( ph -> ( A - M ) e. CC )
53 52 absnegd 
 |-  ( ph -> ( abs ` -u ( A - M ) ) = ( abs ` ( A - M ) ) )
54 2 12 negsubdi2d 
 |-  ( ph -> -u ( A - M ) = ( M - A ) )
55 54 fveq2d 
 |-  ( ph -> ( abs ` -u ( A - M ) ) = ( abs ` ( M - A ) ) )
56 38 fveq2d 
 |-  ( ph -> ( abs ` ( A - M ) ) = ( abs ` ( M - B ) ) )
57 53 55 56 3eqtr3d 
 |-  ( ph -> ( abs ` ( M - A ) ) = ( abs ` ( M - B ) ) )
58 1 4 12 2 4 12 3 8 50 8 29 51 57 6 ssscongptld 
 |-  ( ph -> ( cos ` ( ( Q - M ) F ( A - M ) ) ) = ( cos ` ( ( Q - M ) F ( B - M ) ) ) )
59 41 42 58 3eqtr3rd 
 |-  ( ph -> ( cos ` ( ( Q - M ) F ( B - M ) ) ) = -u ( cos ` ( ( Q - M ) F ( B - M ) ) ) )
60 35 59 eqnegad 
 |-  ( ph -> ( cos ` ( ( Q - M ) F ( B - M ) ) ) = 0 )
61 coseq0negpitopi 
 |-  ( ( ( Q - M ) F ( B - M ) ) e. ( -u _pi (,] _pi ) -> ( ( cos ` ( ( Q - M ) F ( B - M ) ) ) = 0 <-> ( ( Q - M ) F ( B - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
62 32 61 syl 
 |-  ( ph -> ( ( cos ` ( ( Q - M ) F ( B - M ) ) ) = 0 <-> ( ( Q - M ) F ( B - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
63 60 62 mpbid 
 |-  ( ph -> ( ( Q - M ) F ( B - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )