Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	chordthmlem3.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	chordthmlem3.Q	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
	chordthmlem3.X	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	chordthmlem3.M	⊢ ( 𝜑 → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
	chordthmlem3.P	⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
	chordthmlem3.ABequidistQ	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
Assertion	chordthmlem3	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		chordthmlem3.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		chordthmlem3.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		chordthmlem3.Q	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
4		chordthmlem3.X	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5		chordthmlem3.M	⊢ ( 𝜑 → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
6		chordthmlem3.P	⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
7		chordthmlem3.ABequidistQ	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
8	1 2	addcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
9	8	halfcld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
10	5 9	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
11	3 10	subcld	⊢ ( 𝜑 → ( 𝑄 − 𝑀 ) ∈ ℂ )
12	11	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝑄 − 𝑀 ) ) ∈ ℝ )
13	12	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝑄 − 𝑀 ) ) ∈ ℂ )
14	13	sqcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) ∈ ℂ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) ∈ ℂ )
16	15	addridd	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + 0 ) = ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) )
17	4	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
18	17 1	mulcld	⊢ ( 𝜑 → ( 𝑋 · 𝐴 ) ∈ ℂ )
19		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
20	19 17	subcld	⊢ ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ )
21	20 2	mulcld	⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · 𝐵 ) ∈ ℂ )
22	18 21	addcld	⊢ ( 𝜑 → ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ∈ ℂ )
23	6 22	eqeltrd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → 𝑃 ∈ ℂ )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → 𝑃 = 𝑀 )
26	24 25	subeq0bd	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( 𝑃 − 𝑀 ) = 0 )
27	26	abs00bd	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑃 − 𝑀 ) ) = 0 )
28	27	sq0id	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) = 0 )
29	28	oveq2d	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + 0 ) )
30	3	adantr	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → 𝑄 ∈ ℂ )
31	30 24	abssubd	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑄 − 𝑃 ) ) = ( abs ‘ ( 𝑃 − 𝑄 ) ) )
32	25	oveq2d	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( 𝑄 − 𝑃 ) = ( 𝑄 − 𝑀 ) )
33	32	fveq2d	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑄 − 𝑃 ) ) = ( abs ‘ ( 𝑄 − 𝑀 ) ) )
34	31 33	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑃 − 𝑄 ) ) = ( abs ‘ ( 𝑄 − 𝑀 ) ) )
35	34	oveq1d	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) )
36	16 29 35	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )
37	23 10	subcld	⊢ ( 𝜑 → ( 𝑃 − 𝑀 ) ∈ ℂ )
38	37	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝑃 − 𝑀 ) ) ∈ ℝ )
39	38	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝑃 − 𝑀 ) ) ∈ ℂ )
40	39	sqcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ∈ ℂ )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ∈ ℂ )
42	41	addlidd	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 0 + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) = ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) )
43	3	adantr	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → 𝑄 ∈ ℂ )
44		simpr	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → 𝑄 = 𝑀 )
45	43 44	subeq0bd	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 𝑄 − 𝑀 ) = 0 )
46	45	abs00bd	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( abs ‘ ( 𝑄 − 𝑀 ) ) = 0 )
47	46	sq0id	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) = 0 )
48	47	oveq1d	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) = ( 0 + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )
49	44	oveq2d	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 𝑃 − 𝑄 ) = ( 𝑃 − 𝑀 ) )
50	49	fveq2d	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( abs ‘ ( 𝑃 − 𝑄 ) ) = ( abs ‘ ( 𝑃 − 𝑀 ) ) )
51	50	oveq1d	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) )
52	42 48 51	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )
53	23	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑃 ∈ ℂ )
54	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑄 ∈ ℂ )
55	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑀 ∈ ℂ )
56		simprl	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑃 ≠ 𝑀 )
57		simprr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑄 ≠ 𝑀 )
58		eqid	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
59	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝐴 ∈ ℂ )
60	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝐵 ∈ ℂ )
61	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑋 ∈ ℝ )
62	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) )
63	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) )
64	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) )
65	58 59 60 54 61 62 63 64 56 57	chordthmlem2	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } )
66		eqid	⊢ ( abs ‘ ( 𝑄 − 𝑀 ) ) = ( abs ‘ ( 𝑄 − 𝑀 ) )
67		eqid	⊢ ( abs ‘ ( 𝑃 − 𝑀 ) ) = ( abs ‘ ( 𝑃 − 𝑀 ) )
68		eqid	⊢ ( abs ‘ ( 𝑃 − 𝑄 ) ) = ( abs ‘ ( 𝑃 − 𝑄 ) )
69		eqid	⊢ ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) = ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) )
70	58 66 67 68 69	pythag	⊢ ( ( ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ∧ ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )
71	53 54 55 56 57 65 70	syl321anc	⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )
72	36 52 71	pm2.61da2ne	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) )