Theorem chordthmlem2 20125

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 20124, where P = B, and using angrtmuld 20101 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.)

Hypotheses

Ref	Expression
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

Ref	Expression
chordthmlem2	|- ( ph -> ( ( Q - M ) F ( P - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } )

Distinct variable groups:   x, y, Q   x, P, y   x, M, y   x, B, y   x, A, y

Allowed substitution hints:   ph( x, y)   F( x, y)   X( x, y)

Proof of Theorem chordthmlem2

Step	Hyp	Ref	Expression
1		chordthmlem2.angdef	. . 3 |- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		chordthmlem2.A	. . 3 |- ( ph -> A e. CC )
3		chordthmlem2.B	. . 3 |- ( ph -> B e. CC )
4		chordthmlem2.Q	. . 3 |- ( ph -> Q e. CC )
5		chordthmlem2.M	. . 3 |- ( ph -> M = ( ( A + B ) / 2 ) )
6		chordthmlem2.ABequidistQ	. . 3 |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )
7		2re 9811	. . . . . . . . . 10 |- 2 e. RR
8	7	a1i 12	. . . . . . . . 9 |- ( ph -> 2 e. RR )
9		2ne0 9825	. . . . . . . . . 10 |- 2 =/= 0
10	9	a1i 12	. . . . . . . . 9 |- ( ph -> 2 =/= 0 )
11	8, 10	rereccld 9583	. . . . . . . 8 |- ( ph -> ( 1 / 2 ) e. RR )
12		chordthmlem2.X	. . . . . . . 8 |- ( ph -> X e. RR )
13	11, 12	resubcld 9207	. . . . . . 7 |- ( ph -> ( ( 1 / 2 ) - X ) e. RR )
14	13	recnd 8857	. . . . . 6 |- ( ph -> ( ( 1 / 2 ) - X ) e. CC )
15	3, 2	subcld 9153	. . . . . 6 |- ( ph -> ( B - A ) e. CC )
16	11	recnd 8857	. . . . . . . . 9 |- ( ph -> ( 1 / 2 ) e. CC )
17	12	recnd 8857	. . . . . . . . 9 |- ( ph -> X e. CC )
18	16, 17, 15	subdird 9232	. . . . . . . 8 |- ( ph -> ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) - ( X x. ( B - A ) ) ) )
19		2cn 9812	. . . . . . . . . . . . . . 15 |- 2 e. CC
20	19	a1i 12	. . . . . . . . . . . . . 14 |- ( ph -> 2 e. CC )
21	3, 20, 10	divcan4d 9538	. . . . . . . . . . . . 13 |- ( ph -> ( ( B x. 2 ) / 2 ) = B )
22	3	times2d 9951	. . . . . . . . . . . . . 14 |- ( ph -> ( B x. 2 ) = ( B + B ) )
23	22	oveq1d 5835	. . . . . . . . . . . . 13 |- ( ph -> ( ( B x. 2 ) / 2 ) = ( ( B + B ) / 2 ) )
24	21, 23	eqtr3d 2319	. . . . . . . . . . . 12 |- ( ph -> B = ( ( B + B ) / 2 ) )
25	24, 5	oveq12d 5838	. . . . . . . . . . 11 |- ( ph -> ( B - M ) = ( ( ( B + B ) / 2 ) - ( ( A + B ) / 2 ) ) )
26	3, 3	addcld 8850	. . . . . . . . . . . 12 |- ( ph -> ( B + B ) e. CC )
27	2, 3	addcld 8850	. . . . . . . . . . . 12 |- ( ph -> ( A + B ) e. CC )
28	26, 27, 20, 10	divsubdird 9571	. . . . . . . . . . 11 |- ( ph -> ( ( ( B + B ) - ( A + B ) ) / 2 ) = ( ( ( B + B ) / 2 ) - ( ( A + B ) / 2 ) ) )
29	3, 2, 3	pnpcan2d 9191	. . . . . . . . . . . 12 |- ( ph -> ( ( B + B ) - ( A + B ) ) = ( B - A ) )
30	29	oveq1d 5835	. . . . . . . . . . 11 |- ( ph -> ( ( ( B + B ) - ( A + B ) ) / 2 ) = ( ( B - A ) / 2 ) )
31	25, 28, 30	3eqtr2d 2323	. . . . . . . . . 10 |- ( ph -> ( B - M ) = ( ( B - A ) / 2 ) )
32	15, 20, 10	divrec2d 9536	. . . . . . . . . 10 |- ( ph -> ( ( B - A ) / 2 ) = ( ( 1 / 2 ) x. ( B - A ) ) )
33	31, 32	eqtrd 2317	. . . . . . . . 9 |- ( ph -> ( B - M ) = ( ( 1 / 2 ) x. ( B - A ) ) )
34		chordthmlem2.P	. . . . . . . . . 10 |- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
35	17, 2	mulcld 8851	. . . . . . . . . . . . 13 |- ( ph -> ( X x. A ) e. CC )
36		ax-1cn 8791	. . . . . . . . . . . . . . . 16 |- 1 e. CC
37	36	a1i 12	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
38	37, 17	subcld 9153	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 - X ) e. CC )
39	38, 3	mulcld 8851	. . . . . . . . . . . . 13 |- ( ph -> ( ( 1 - X ) x. B ) e. CC )
40	35, 39	addcld 8850	. . . . . . . . . . . 12 |- ( ph -> ( ( X x. A ) + ( ( 1 - X ) x. B ) ) e. CC )
41	34, 40	eqeltrd 2359	. . . . . . . . . . 11 |- ( ph -> P e. CC )
42	2, 41, 3, 17	affineequiv 20118	. . . . . . . . . 10 |- ( ph -> ( P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) <-> ( B - P ) = ( X x. ( B - A ) ) ) )
43	34, 42	mpbid 203	. . . . . . . . 9 |- ( ph -> ( B - P ) = ( X x. ( B - A ) ) )
44	33, 43	oveq12d 5838	. . . . . . . 8 |- ( ph -> ( ( B - M ) - ( B - P ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) - ( X x. ( B - A ) ) ) )
45	27	halfcld 9952	. . . . . . . . . 10 |- ( ph -> ( ( A + B ) / 2 ) e. CC )
46	5, 45	eqeltrd 2359	. . . . . . . . 9 |- ( ph -> M e. CC )
47	3, 46, 41	nnncan1d 9187	. . . . . . . 8 |- ( ph -> ( ( B - M ) - ( B - P ) ) = ( P - M ) )
48	18, 44, 47	3eqtr2rd 2324	. . . . . . 7 |- ( ph -> ( P - M ) = ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) )
49		chordthmlem2.PneM	. . . . . . . 8 |- ( ph -> P =/= M )
50	41, 46, 49	subne0d 9162	. . . . . . 7 |- ( ph -> ( P - M ) =/= 0 )
51	48, 50	eqnetrrd 2468	. . . . . 6 |- ( ph -> ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) =/= 0 )
52	14, 15, 51	mulne0bbd 9418	. . . . 5 |- ( ph -> ( B - A ) =/= 0 )
53	3, 2, 52	subne0ad 9164	. . . 4 |- ( ph -> B =/= A )
54	53	necomd 2531	. . 3 |- ( ph -> A =/= B )
55		chordthmlem2.QneM	. . 3 |- ( ph -> Q =/= M )
56	1, 2, 3, 4, 5, 6, 54, 55	chordthmlem 20124	. 2 |- ( ph -> ( ( Q - M ) F ( B - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } )
57	4, 46	subcld 9153	. . 3 |- ( ph -> ( Q - M ) e. CC )
58	41, 46	subcld 9153	. . 3 |- ( ph -> ( P - M ) e. CC )
59	3, 46	subcld 9153	. . 3 |- ( ph -> ( B - M ) e. CC )
60	4, 46, 55	subne0d 9162	. . 3 |- ( ph -> ( Q - M ) =/= 0 )
61	20, 10	recne0d 9526	. . . . 5 |- ( ph -> ( 1 / 2 ) =/= 0 )
62	16, 15, 61, 52	mulne0d 9416	. . . 4 |- ( ph -> ( ( 1 / 2 ) x. ( B - A ) ) =/= 0 )
63	33, 62	eqnetrd 2466	. . 3 |- ( ph -> ( B - M ) =/= 0 )
64	33, 48	oveq12d 5838	. . . . 5 |- ( ph -> ( ( B - M ) / ( P - M ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) / ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) ) )
65	14, 15, 51	mulne0bad 9417	. . . . . 6 |- ( ph -> ( ( 1 / 2 ) - X ) =/= 0 )
66	16, 14, 15, 65, 52	divcan5rd 9559	. . . . 5 |- ( ph -> ( ( ( 1 / 2 ) x. ( B - A ) ) / ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) ) = ( ( 1 / 2 ) / ( ( 1 / 2 ) - X ) ) )
67	64, 66	eqtrd 2317	. . . 4 |- ( ph -> ( ( B - M ) / ( P - M ) ) = ( ( 1 / 2 ) / ( ( 1 / 2 ) - X ) ) )
68	11, 13, 65	redivcld 9584	. . . 4 |- ( ph -> ( ( 1 / 2 ) / ( ( 1 / 2 ) - X ) ) e. RR )
69	67, 68	eqeltrd 2359	. . 3 |- ( ph -> ( ( B - M ) / ( P - M ) ) e. RR )
70	1, 57, 58, 59, 60, 50, 63, 69	angrtmuld 20101	. 2 |- ( ph -> ( ( ( Q - M ) F ( P - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } <-> ( ( Q - M ) F ( B - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } ) )
71	56, 70	mpbird 225	1 |- ( ph -> ( ( Q - M ) F ( P - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } )

Syntax hints:   -> wi 6   = wceq 1624   e. wcel 1685   =/= wne 2448   \ cdif 3151   {csn 3642   {cpr 3643   ` cfv 5222  (class class class)co 5820   e. cmpt2 5822   CCcc 8731   RRcr 8732   0cc0 8733   1c1 8734   + caddc 8736   x. cmul 8738   - cmin 9033   -ucneg 9034   / cdiv 9419   2c2 9791   Imcim 11578   abscabs 11714   picpi 12343   logclog 19907

This theorem is referenced by:  chordthmlem3  20126

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7338  ax-cnex 8789  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-mulcom 8797  ax-addass 8798  ax-mulass 8799  ax-distr 8800  ax-i2m1 8801  ax-1ne0 8802  ax-1rid 8803  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807  ax-pre-lttrn 8808  ax-pre-ltadd 8809  ax-pre-mulgt0 8810  ax-pre-sup 8811  ax-addf 8812  ax-mulf 8813

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-fv 5230  df-isom 5231  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-of 6040  df-1st 6084  df-2nd 6085  df-iota 6253  df-riota 6300  df-recs 6384  df-rdg 6419  df-1o 6475  df-2o 6476  df-oadd 6479  df-er 6656  df-map 6770  df-pm 6771  df-ixp 6814  df-en 6860  df-dom 6861  df-sdom 6862  df-fin 6863  df-fi 7161  df-sup 7190  df-oi 7221  df-card 7568  df-cda 7790  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-sub 9035  df-neg 9036  df-div 9420  df-nn 9743  df-2 9800  df-3 9801  df-4 9802  df-5 9803  df-6 9804  df-7 9805  df-8 9806  df-9 9807  df-10 9808  df-n0 9962  df-z 10021  df-dec 10121  df-uz 10227  df-q 10313  df-rp 10351  df-xneg 10448  df-xadd 10449  df-xmul 10450  df-ioo 10655  df-ioc 10656  df-ico 10657  df-icc 10658  df-fz 10778  df-fzo 10866  df-fl 10920  df-mod 10969  df-seq 11042  df-exp 11100  df-fac 11284  df-bc 11311  df-hash 11333  df-shft 11557  df-cj 11579  df-re 11580  df-im 11581  df-sqr 11715  df-abs 11716  df-limsup 11940  df-clim 11957  df-rlim 11958  df-sum 12154  df-ef 12344  df-sin 12346  df-cos 12347  df-pi 12349  df-struct 13145  df-ndx 13146  df-slot 13147  df-base 13148  df-sets 13149  df-ress 13150  df-plusg 13216  df-mulr 13217  df-starv 13218  df-sca 13219  df-vsca 13220  df-tset 13222  df-ple 13223  df-ds 13225  df-hom 13227  df-cco 13228  df-rest 13322  df-topn 13323  df-topgen 13339  df-pt 13340  df-prds 13343  df-xrs 13398  df-0g 13399  df-gsum 13400  df-qtop 13405  df-imas 13406  df-xps 13408  df-mre 13483  df-mrc 13484  df-acs 13486  df-mnd 14362  df-submnd 14411  df-mulg 14487  df-cntz 14788  df-cmn 15086  df-xmet 16368  df-met 16369  df-bl 16370  df-mopn 16371  df-cnfld 16373  df-top 16631  df-bases 16633  df-topon 16634  df-topsp 16635  df-cld 16751  df-ntr 16752  df-cls 16753  df-nei 16830  df-lp 16863  df-perf 16864  df-cn 16952  df-cnp 16953  df-haus 17038  df-tx 17252  df-hmeo 17441  df-fbas 17515  df-fg 17516  df-fil 17536  df-fm 17628  df-flim 17629  df-flf 17630  df-xms 17880  df-ms 17881  df-tms 17882  df-cncf 18377  df-limc 19211  df-dv 19212  df-log 19909