Metamath Proof Explorer

Theorem chordthmlem2

Description: If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem , where P = B, and using angrtmuld to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses chordthmlem2.angdef 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
chordthmlem2.A 
|- ( ph -> A e. CC )
chordthmlem2.B 
|- ( ph -> B e. CC )
chordthmlem2.Q 
|- ( ph -> Q e. CC )
chordthmlem2.X 
|- ( ph -> X e. RR )
chordthmlem2.M 
|- ( ph -> M = ( ( A + B ) / 2 ) )
chordthmlem2.P 
|- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
chordthmlem2.ABequidistQ 
|- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
chordthmlem2.PneM 
|- ( ph -> P =/= M )
chordthmlem2.QneM 
|- ( ph -> Q =/= M )
Assertion chordthmlem2 
|- ( ph -> ( ( Q - M ) F ( P - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )

Proof

Step Hyp Ref Expression
1 chordthmlem2.angdef 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 chordthmlem2.A 
 |-  ( ph -> A e. CC )
3 chordthmlem2.B 
 |-  ( ph -> B e. CC )
4 chordthmlem2.Q 
 |-  ( ph -> Q e. CC )
5 chordthmlem2.X 
 |-  ( ph -> X e. RR )
6 chordthmlem2.M 
 |-  ( ph -> M = ( ( A + B ) / 2 ) )
7 chordthmlem2.P 
 |-  ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
8 chordthmlem2.ABequidistQ 
 |-  ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
9 chordthmlem2.PneM 
 |-  ( ph -> P =/= M )
10 chordthmlem2.QneM 
 |-  ( ph -> Q =/= M )
11 2re 
 |-  2 e. RR
12 11 a1i 
 |-  ( ph -> 2 e. RR )
13 2ne0 
 |-  2 =/= 0
14 13 a1i 
 |-  ( ph -> 2 =/= 0 )
15 12 14 rereccld 
 |-  ( ph -> ( 1 / 2 ) e. RR )
16 15 5 resubcld 
 |-  ( ph -> ( ( 1 / 2 ) - X ) e. RR )
17 16 recnd 
 |-  ( ph -> ( ( 1 / 2 ) - X ) e. CC )
18 3 2 subcld 
 |-  ( ph -> ( B - A ) e. CC )
19 15 recnd 
 |-  ( ph -> ( 1 / 2 ) e. CC )
20 5 recnd 
 |-  ( ph -> X e. CC )
21 19 20 18 subdird 
 |-  ( ph -> ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) - ( X x. ( B - A ) ) ) )
22 2cnd 
 |-  ( ph -> 2 e. CC )
23 3 22 14 divcan4d 
 |-  ( ph -> ( ( B x. 2 ) / 2 ) = B )
24 3 times2d 
 |-  ( ph -> ( B x. 2 ) = ( B + B ) )
25 24 oveq1d 
 |-  ( ph -> ( ( B x. 2 ) / 2 ) = ( ( B + B ) / 2 ) )
26 23 25 eqtr3d 
 |-  ( ph -> B = ( ( B + B ) / 2 ) )
27 26 6 oveq12d 
 |-  ( ph -> ( B - M ) = ( ( ( B + B ) / 2 ) - ( ( A + B ) / 2 ) ) )
28 3 3 addcld 
 |-  ( ph -> ( B + B ) e. CC )
29 2 3 addcld 
 |-  ( ph -> ( A + B ) e. CC )
30 28 29 22 14 divsubdird 
 |-  ( ph -> ( ( ( B + B ) - ( A + B ) ) / 2 ) = ( ( ( B + B ) / 2 ) - ( ( A + B ) / 2 ) ) )
31 3 2 3 pnpcan2d 
 |-  ( ph -> ( ( B + B ) - ( A + B ) ) = ( B - A ) )
32 31 oveq1d 
 |-  ( ph -> ( ( ( B + B ) - ( A + B ) ) / 2 ) = ( ( B - A ) / 2 ) )
33 27 30 32 3eqtr2d 
 |-  ( ph -> ( B - M ) = ( ( B - A ) / 2 ) )
34 18 22 14 divrec2d 
 |-  ( ph -> ( ( B - A ) / 2 ) = ( ( 1 / 2 ) x. ( B - A ) ) )
35 33 34 eqtrd 
 |-  ( ph -> ( B - M ) = ( ( 1 / 2 ) x. ( B - A ) ) )
36 20 2 mulcld 
 |-  ( ph -> ( X x. A ) e. CC )
37 1cnd 
 |-  ( ph -> 1 e. CC )
38 37 20 subcld 
 |-  ( ph -> ( 1 - X ) e. CC )
39 38 3 mulcld 
 |-  ( ph -> ( ( 1 - X ) x. B ) e. CC )
40 36 39 addcld 
 |-  ( ph -> ( ( X x. A ) + ( ( 1 - X ) x. B ) ) e. CC )
41 7 40 eqeltrd 
 |-  ( ph -> P e. CC )
42 2 41 3 20 affineequiv 
 |-  ( ph -> ( P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) <-> ( B - P ) = ( X x. ( B - A ) ) ) )
43 7 42 mpbid 
 |-  ( ph -> ( B - P ) = ( X x. ( B - A ) ) )
44 35 43 oveq12d 
 |-  ( ph -> ( ( B - M ) - ( B - P ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) - ( X x. ( B - A ) ) ) )
45 29 halfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. CC )
46 6 45 eqeltrd 
 |-  ( ph -> M e. CC )
47 3 46 41 nnncan1d 
 |-  ( ph -> ( ( B - M ) - ( B - P ) ) = ( P - M ) )
48 21 44 47 3eqtr2rd 
 |-  ( ph -> ( P - M ) = ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) )
49 41 46 9 subne0d 
 |-  ( ph -> ( P - M ) =/= 0 )
50 48 49 eqnetrrd 
 |-  ( ph -> ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) =/= 0 )
51 17 18 50 mulne0bbd 
 |-  ( ph -> ( B - A ) =/= 0 )
52 3 2 51 subne0ad 
 |-  ( ph -> B =/= A )
53 52 necomd 
 |-  ( ph -> A =/= B )
54 1 2 3 4 6 8 53 10 chordthmlem 
 |-  ( ph -> ( ( Q - M ) F ( B - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )
55 4 46 subcld 
 |-  ( ph -> ( Q - M ) e. CC )
56 41 46 subcld 
 |-  ( ph -> ( P - M ) e. CC )
57 3 46 subcld 
 |-  ( ph -> ( B - M ) e. CC )
58 4 46 10 subne0d 
 |-  ( ph -> ( Q - M ) =/= 0 )
59 22 14 recne0d 
 |-  ( ph -> ( 1 / 2 ) =/= 0 )
60 19 18 59 51 mulne0d 
 |-  ( ph -> ( ( 1 / 2 ) x. ( B - A ) ) =/= 0 )
61 35 60 eqnetrd 
 |-  ( ph -> ( B - M ) =/= 0 )
62 35 48 oveq12d 
 |-  ( ph -> ( ( B - M ) / ( P - M ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) / ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) ) )
63 17 18 50 mulne0bad 
 |-  ( ph -> ( ( 1 / 2 ) - X ) =/= 0 )
64 19 17 18 63 51 divcan5rd 
 |-  ( ph -> ( ( ( 1 / 2 ) x. ( B - A ) ) / ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) ) = ( ( 1 / 2 ) / ( ( 1 / 2 ) - X ) ) )
65 62 64 eqtrd 
 |-  ( ph -> ( ( B - M ) / ( P - M ) ) = ( ( 1 / 2 ) / ( ( 1 / 2 ) - X ) ) )
66 15 16 63 redivcld 
 |-  ( ph -> ( ( 1 / 2 ) / ( ( 1 / 2 ) - X ) ) e. RR )
67 65 66 eqeltrd 
 |-  ( ph -> ( ( B - M ) / ( P - M ) ) e. RR )
68 1 55 56 57 58 49 61 67 angrtmuld 
 |-  ( ph -> ( ( ( Q - M ) F ( P - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( ( Q - M ) F ( B - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
69 54 68 mpbird 
 |-  ( ph -> ( ( Q - M ) F ( P - M ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } )