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	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
	chordthmlem2.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	chordthmlem2.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	chordthmlem2.Q	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
	chordthmlem2.X	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	chordthmlem2.M	⊢ ( 𝜑 → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
	chordthmlem2.P	⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
	chordthmlem2.ABequidistQ	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
	chordthmlem2.PneM	⊢ ( 𝜑 → 𝑃 ≠ 𝑀 )
	chordthmlem2.QneM	⊢ ( 𝜑 → 𝑄 ≠ 𝑀 )
Assertion	chordthmlem2	⊢ ( 𝜑 → ( ( 𝑄 − 𝑀 ) 𝐹 ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )

Proof

Step	Hyp	Ref	Expression
1		chordthmlem2.angdef	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2		chordthmlem2.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3		chordthmlem2.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4		chordthmlem2.Q	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
5		chordthmlem2.X	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
6		chordthmlem2.M	⊢ ( 𝜑 → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
7		chordthmlem2.P	⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
8		chordthmlem2.ABequidistQ	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
9		chordthmlem2.PneM	⊢ ( 𝜑 → 𝑃 ≠ 𝑀 )
10		chordthmlem2.QneM	⊢ ( 𝜑 → 𝑄 ≠ 𝑀 )
11		2re	⊢ 2 ∈ ℝ
12	11	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
13		2ne0	⊢ 2 ≠ 0
14	13	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
15	12 14	rereccld	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
16	15 5	resubcld	⊢ ( 𝜑 → ( ( 1 / 2 ) − 𝑋 ) ∈ ℝ )
17	16	recnd	⊢ ( 𝜑 → ( ( 1 / 2 ) − 𝑋 ) ∈ ℂ )
18	3 2	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
19	15	recnd	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
20	5	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
21	19 20 18	subdird	⊢ ( 𝜑 → ( ( ( 1 / 2 ) − 𝑋 ) · ( 𝐵 − 𝐴 ) ) = ( ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) − ( 𝑋 · ( 𝐵 − 𝐴 ) ) ) )
22		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
23	3 22 14	divcan4d	⊢ ( 𝜑 → ( ( 𝐵 · 2 ) / 2 ) = 𝐵 )
24	3	times2d	⊢ ( 𝜑 → ( 𝐵 · 2 ) = ( 𝐵 + 𝐵 ) )
25	24	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 · 2 ) / 2 ) = ( ( 𝐵 + 𝐵 ) / 2 ) )
26	23 25	eqtr3d	⊢ ( 𝜑 → 𝐵 = ( ( 𝐵 + 𝐵 ) / 2 ) )
27	26 6	oveq12d	⊢ ( 𝜑 → ( 𝐵 − 𝑀 ) = ( ( ( 𝐵 + 𝐵 ) / 2 ) − ( ( 𝐴 + 𝐵 ) / 2 ) ) )
28	3 3	addcld	⊢ ( 𝜑 → ( 𝐵 + 𝐵 ) ∈ ℂ )
29	2 3	addcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
30	28 29 22 14	divsubdird	⊢ ( 𝜑 → ( ( ( 𝐵 + 𝐵 ) − ( 𝐴 + 𝐵 ) ) / 2 ) = ( ( ( 𝐵 + 𝐵 ) / 2 ) − ( ( 𝐴 + 𝐵 ) / 2 ) ) )
31	3 2 3	pnpcan2d	⊢ ( 𝜑 → ( ( 𝐵 + 𝐵 ) − ( 𝐴 + 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
32	31	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐵 + 𝐵 ) − ( 𝐴 + 𝐵 ) ) / 2 ) = ( ( 𝐵 − 𝐴 ) / 2 ) )
33	27 30 32	3eqtr2d	⊢ ( 𝜑 → ( 𝐵 − 𝑀 ) = ( ( 𝐵 − 𝐴 ) / 2 ) )
34	18 22 14	divrec2d	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / 2 ) = ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) )
35	33 34	eqtrd	⊢ ( 𝜑 → ( 𝐵 − 𝑀 ) = ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) )
36	20 2	mulcld	⊢ ( 𝜑 → ( 𝑋 · 𝐴 ) ∈ ℂ )
37		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
38	37 20	subcld	⊢ ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ )
39	38 3	mulcld	⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · 𝐵 ) ∈ ℂ )
40	36 39	addcld	⊢ ( 𝜑 → ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ∈ ℂ )
41	7 40	eqeltrd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
42	2 41 3 20	affineequiv	⊢ ( 𝜑 → ( 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ↔ ( 𝐵 − 𝑃 ) = ( 𝑋 · ( 𝐵 − 𝐴 ) ) ) )
43	7 42	mpbid	⊢ ( 𝜑 → ( 𝐵 − 𝑃 ) = ( 𝑋 · ( 𝐵 − 𝐴 ) ) )
44	35 43	oveq12d	⊢ ( 𝜑 → ( ( 𝐵 − 𝑀 ) − ( 𝐵 − 𝑃 ) ) = ( ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) − ( 𝑋 · ( 𝐵 − 𝐴 ) ) ) )
45	29	halfcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
46	6 45	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
47	3 46 41	nnncan1d	⊢ ( 𝜑 → ( ( 𝐵 − 𝑀 ) − ( 𝐵 − 𝑃 ) ) = ( 𝑃 − 𝑀 ) )
48	21 44 47	3eqtr2rd	⊢ ( 𝜑 → ( 𝑃 − 𝑀 ) = ( ( ( 1 / 2 ) − 𝑋 ) · ( 𝐵 − 𝐴 ) ) )
49	41 46 9	subne0d	⊢ ( 𝜑 → ( 𝑃 − 𝑀 ) ≠ 0 )
50	48 49	eqnetrrd	⊢ ( 𝜑 → ( ( ( 1 / 2 ) − 𝑋 ) · ( 𝐵 − 𝐴 ) ) ≠ 0 )
51	17 18 50	mulne0bbd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
52	3 2 51	subne0ad	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
53	52	necomd	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
54	1 2 3 4 6 8 53 10	chordthmlem	⊢ ( 𝜑 → ( ( 𝑄 − 𝑀 ) 𝐹 ( 𝐵 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )
55	4 46	subcld	⊢ ( 𝜑 → ( 𝑄 − 𝑀 ) ∈ ℂ )
56	41 46	subcld	⊢ ( 𝜑 → ( 𝑃 − 𝑀 ) ∈ ℂ )
57	3 46	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝑀 ) ∈ ℂ )
58	4 46 10	subne0d	⊢ ( 𝜑 → ( 𝑄 − 𝑀 ) ≠ 0 )
59	22 14	recne0d	⊢ ( 𝜑 → ( 1 / 2 ) ≠ 0 )
60	19 18 59 51	mulne0d	⊢ ( 𝜑 → ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) ≠ 0 )
61	35 60	eqnetrd	⊢ ( 𝜑 → ( 𝐵 − 𝑀 ) ≠ 0 )
62	35 48	oveq12d	⊢ ( 𝜑 → ( ( 𝐵 − 𝑀 ) / ( 𝑃 − 𝑀 ) ) = ( ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) / ( ( ( 1 / 2 ) − 𝑋 ) · ( 𝐵 − 𝐴 ) ) ) )
63	17 18 50	mulne0bad	⊢ ( 𝜑 → ( ( 1 / 2 ) − 𝑋 ) ≠ 0 )
64	19 17 18 63 51	divcan5rd	⊢ ( 𝜑 → ( ( ( 1 / 2 ) · ( 𝐵 − 𝐴 ) ) / ( ( ( 1 / 2 ) − 𝑋 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( 1 / 2 ) / ( ( 1 / 2 ) − 𝑋 ) ) )
65	62 64	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 − 𝑀 ) / ( 𝑃 − 𝑀 ) ) = ( ( 1 / 2 ) / ( ( 1 / 2 ) − 𝑋 ) ) )
66	15 16 63	redivcld	⊢ ( 𝜑 → ( ( 1 / 2 ) / ( ( 1 / 2 ) − 𝑋 ) ) ∈ ℝ )
67	65 66	eqeltrd	⊢ ( 𝜑 → ( ( 𝐵 − 𝑀 ) / ( 𝑃 − 𝑀 ) ) ∈ ℝ )
68	1 55 56 57 58 49 61 67	angrtmuld	⊢ ( 𝜑 → ( ( ( 𝑄 − 𝑀 ) 𝐹 ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ↔ ( ( 𝑄 − 𝑀 ) 𝐹 ( 𝐵 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) )
69	54 68	mpbird	⊢ ( 𝜑 → ( ( 𝑄 − 𝑀 ) 𝐹 ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )