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. (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	sseldi	$⊢ φ \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