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 \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	chordthmlem.A	$⊢ φ \to A \in ℂ$
	chordthmlem.B	$⊢ φ \to B \in ℂ$
	chordthmlem.Q	$⊢ φ \to Q \in ℂ$
	chordthmlem.M	$⊢ φ \to M = \frac{A + B}{2}$
	chordthmlem.ABequidistQ	$⊢ φ \to \|A - Q\| = \|B - Q\|$
	chordthmlem.AneB	$⊢ φ \to A \neq B$
	chordthmlem.QneM	$⊢ φ \to Q \neq M$
Assertion	chordthmlem	$⊢ φ \to (Q - M) F (B - M) \in \{\frac{π}{2}, - \frac{π}{2}\}$

Proof

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

Metamath Proof Explorer

Theorem chordthmlem

Proof