chordthmlem3

Description: If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ² = QM² + PM². This follows from chordthmlem2 and the Pythagorean theorem ( pythag ) in the case where P and Q are unequal to M. If either P or Q equals M, the result is trivial. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	chordthmlem3.A	$⊢ φ \to A \in ℂ$
	chordthmlem3.B	$⊢ φ \to B \in ℂ$
	chordthmlem3.Q	$⊢ φ \to Q \in ℂ$
	chordthmlem3.X	$⊢ φ \to X \in ℝ$
	chordthmlem3.M	$⊢ φ \to M = \frac{A + B}{2}$
	chordthmlem3.P	$⊢ φ \to P = X A + (1 - X) B$
	chordthmlem3.ABequidistQ	$⊢ φ \to \|A - Q\| = \|B - Q\|$
Assertion	chordthmlem3	$⊢ φ \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2} + {\|P - M\|}^{2}$

Proof

Step	Hyp	Ref	Expression
1		chordthmlem3.A	$⊢ φ \to A \in ℂ$
2		chordthmlem3.B	$⊢ φ \to B \in ℂ$
3		chordthmlem3.Q	$⊢ φ \to Q \in ℂ$
4		chordthmlem3.X	$⊢ φ \to X \in ℝ$
5		chordthmlem3.M	$⊢ φ \to M = \frac{A + B}{2}$
6		chordthmlem3.P	$⊢ φ \to P = X A + (1 - X) B$
7		chordthmlem3.ABequidistQ	$⊢ φ \to \|A - Q\| = \|B - Q\|$
8	1 2	addcld	$⊢ φ \to A + B \in ℂ$
9	8	halfcld	$⊢ φ \to \frac{A + B}{2} \in ℂ$
10	5 9	eqeltrd	$⊢ φ \to M \in ℂ$
11	3 10	subcld	$⊢ φ \to Q - M \in ℂ$
12	11	abscld	$⊢ φ \to \|Q - M\| \in ℝ$
13	12	recnd	$⊢ φ \to \|Q - M\| \in ℂ$
14	13	sqcld	$⊢ φ \to {\|Q - M\|}^{2} \in ℂ$
15	14	adantr	$⊢ (φ \land P = M) \to {\|Q - M\|}^{2} \in ℂ$
16	15	addridd	$⊢ (φ \land P = M) \to {\|Q - M\|}^{2} + 0 = {\|Q - M\|}^{2}$
17	4	recnd	$⊢ φ \to X \in ℂ$
18	17 1	mulcld	$⊢ φ \to X A \in ℂ$
19		1cnd	$⊢ φ \to 1 \in ℂ$
20	19 17	subcld	$⊢ φ \to 1 - X \in ℂ$
21	20 2	mulcld	$⊢ φ \to (1 - X) B \in ℂ$
22	18 21	addcld	$⊢ φ \to X A + (1 - X) B \in ℂ$
23	6 22	eqeltrd	$⊢ φ \to P \in ℂ$
24	23	adantr	$⊢ (φ \land P = M) \to P \in ℂ$
25		simpr	$⊢ (φ \land P = M) \to P = M$
26	24 25	subeq0bd	$⊢ (φ \land P = M) \to P - M = 0$
27	26	abs00bd	$⊢ (φ \land P = M) \to \|P - M\| = 0$
28	27	sq0id	$⊢ (φ \land P = M) \to {\|P - M\|}^{2} = 0$
29	28	oveq2d	$⊢ (φ \land P = M) \to {\|Q - M\|}^{2} + {\|P - M\|}^{2} = {\|Q - M\|}^{2} + 0$
30	3	adantr	$⊢ (φ \land P = M) \to Q \in ℂ$
31	30 24	abssubd	$⊢ (φ \land P = M) \to \|Q - P\| = \|P - Q\|$
32	25	oveq2d	$⊢ (φ \land P = M) \to Q - P = Q - M$
33	32	fveq2d	$⊢ (φ \land P = M) \to \|Q - P\| = \|Q - M\|$
34	31 33	eqtr3d	$⊢ (φ \land P = M) \to \|P - Q\| = \|Q - M\|$
35	34	oveq1d	$⊢ (φ \land P = M) \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2}$
36	16 29 35	3eqtr4rd	$⊢ (φ \land P = M) \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2} + {\|P - M\|}^{2}$
37	23 10	subcld	$⊢ φ \to P - M \in ℂ$
38	37	abscld	$⊢ φ \to \|P - M\| \in ℝ$
39	38	recnd	$⊢ φ \to \|P - M\| \in ℂ$
40	39	sqcld	$⊢ φ \to {\|P - M\|}^{2} \in ℂ$
41	40	adantr	$⊢ (φ \land Q = M) \to {\|P - M\|}^{2} \in ℂ$
42	41	addlidd	$⊢ (φ \land Q = M) \to 0 + {\|P - M\|}^{2} = {\|P - M\|}^{2}$
43	3	adantr	$⊢ (φ \land Q = M) \to Q \in ℂ$
44		simpr	$⊢ (φ \land Q = M) \to Q = M$
45	43 44	subeq0bd	$⊢ (φ \land Q = M) \to Q - M = 0$
46	45	abs00bd	$⊢ (φ \land Q = M) \to \|Q - M\| = 0$
47	46	sq0id	$⊢ (φ \land Q = M) \to {\|Q - M\|}^{2} = 0$
48	47	oveq1d	$⊢ (φ \land Q = M) \to {\|Q - M\|}^{2} + {\|P - M\|}^{2} = 0 + {\|P - M\|}^{2}$
49	44	oveq2d	$⊢ (φ \land Q = M) \to P - Q = P - M$
50	49	fveq2d	$⊢ (φ \land Q = M) \to \|P - Q\| = \|P - M\|$
51	50	oveq1d	$⊢ (φ \land Q = M) \to {\|P - Q\|}^{2} = {\|P - M\|}^{2}$
52	42 48 51	3eqtr4rd	$⊢ (φ \land Q = M) \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2} + {\|P - M\|}^{2}$
53	23	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to P \in ℂ$
54	3	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to Q \in ℂ$
55	10	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to M \in ℂ$
56		simprl	$⊢ (φ \land (P \neq M \land Q \neq M)) \to P \neq M$
57		simprr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to Q \neq M$
58		eqid	$⊢ (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x}))) = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
59	1	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to A \in ℂ$
60	2	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to B \in ℂ$
61	4	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to X \in ℝ$
62	5	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to M = \frac{A + B}{2}$
63	6	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to P = X A + (1 - X) B$
64	7	adantr	$⊢ (φ \land (P \neq M \land Q \neq M)) \to \|A - Q\| = \|B - Q\|$
65	58 59 60 54 61 62 63 64 56 57	chordthmlem2	$⊢ (φ \land (P \neq M \land Q \neq M)) \to (Q - M) (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x}))) (P - M) \in \{\frac{π}{2}, - \frac{π}{2}\}$
66		eqid	$⊢ \|Q - M\| = \|Q - M\|$
67		eqid	$⊢ \|P - M\| = \|P - M\|$
68		eqid	$⊢ \|P - Q\| = \|P - Q\|$
69		eqid	$⊢ (Q - M) (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x}))) (P - M) = (Q - M) (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x}))) (P - M)$
70	58 66 67 68 69	pythag	$⊢ ((P \in ℂ \land Q \in ℂ \land M \in ℂ) \land (P \neq M \land Q \neq M) \land (Q - M) (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x}))) (P - M) \in \{\frac{π}{2}, - \frac{π}{2}\}) \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2} + {\|P - M\|}^{2}$
71	53 54 55 56 57 65 70	syl321anc	$⊢ (φ \land (P \neq M \land Q \neq M)) \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2} + {\|P - M\|}^{2}$
72	36 52 71	pm2.61da2ne	$⊢ φ \to {\|P - Q\|}^{2} = {\|Q - M\|}^{2} + {\|P - M\|}^{2}$

Metamath Proof Explorer

Theorem chordthmlem3

Proof