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 ) } )