pythag

Description: Pythagorean theorem. Given three distinct points A, B, and C that form a right triangle (with the right angle at C), prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where F is the signed angle construct (as used in ang180 ), X is the distance of line segment BC, Y is the distance of line segment AC, Z is the distance of line segment AB (the hypotenuse), and O is the signed right angle m/__ BCA. We use the law of cosines lawcos to prove this, along with simple trigonometry facts like coshalfpi and cosneg . (Contributed by David A. Wheeler, 13-Jun-2015)

	Ref	Expression
Hypotheses	lawcos.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
	lawcos.2	⊢ 𝑋 = ( abs ‘ ( 𝐵 − 𝐶 ) )
	lawcos.3	⊢ 𝑌 = ( abs ‘ ( 𝐴 − 𝐶 ) )
	lawcos.4	⊢ 𝑍 = ( abs ‘ ( 𝐴 − 𝐵 ) )
	lawcos.5	⊢ 𝑂 = ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) )
Assertion	pythag	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝑍 ↑ 2 ) = ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lawcos.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2		lawcos.2	⊢ 𝑋 = ( abs ‘ ( 𝐵 − 𝐶 ) )
3		lawcos.3	⊢ 𝑌 = ( abs ‘ ( 𝐴 − 𝐶 ) )
4		lawcos.4	⊢ 𝑍 = ( abs ‘ ( 𝐴 − 𝐵 ) )
5		lawcos.5	⊢ 𝑂 = ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) )
6	1 2 3 4 5	lawcos	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝑍 ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) )
7	6	3adant3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝑍 ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) )
8		elpri	⊢ ( 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } → ( 𝑂 = ( π / 2 ) ∨ 𝑂 = - ( π / 2 ) ) )
9		fveq2	⊢ ( 𝑂 = ( π / 2 ) → ( cos ‘ 𝑂 ) = ( cos ‘ ( π / 2 ) ) )
10		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
11	9 10	eqtrdi	⊢ ( 𝑂 = ( π / 2 ) → ( cos ‘ 𝑂 ) = 0 )
12		fveq2	⊢ ( 𝑂 = - ( π / 2 ) → ( cos ‘ 𝑂 ) = ( cos ‘ - ( π / 2 ) ) )
13		cosneghalfpi	⊢ ( cos ‘ - ( π / 2 ) ) = 0
14	12 13	eqtrdi	⊢ ( 𝑂 = - ( π / 2 ) → ( cos ‘ 𝑂 ) = 0 )
15	11 14	jaoi	⊢ ( ( 𝑂 = ( π / 2 ) ∨ 𝑂 = - ( π / 2 ) ) → ( cos ‘ 𝑂 ) = 0 )
16	8 15	syl	⊢ ( 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } → ( cos ‘ 𝑂 ) = 0 )
17	16	3ad2ant3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( cos ‘ 𝑂 ) = 0 )
18	17	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) = ( ( 𝑋 · 𝑌 ) · 0 ) )
19		subcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
20	19	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
21	20	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
22	21	abscld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
23	22	recnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℂ )
24	2 23	eqeltrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → 𝑋 ∈ ℂ )
25		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
26	25	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
27	26	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
28	27	abscld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
29	28	recnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℂ )
30	3 29	eqeltrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → 𝑌 ∈ ℂ )
31	24 30	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝑋 · 𝑌 ) ∈ ℂ )
32	31	mul01d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( 𝑋 · 𝑌 ) · 0 ) = 0 )
33	18 32	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) = 0 )
34	33	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) = ( 2 · 0 ) )
35		2t0e0	⊢ ( 2 · 0 ) = 0
36	34 35	eqtrdi	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) = 0 )
37	36	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − 0 ) )
38	24	sqcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝑋 ↑ 2 ) ∈ ℂ )
39	30	sqcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝑌 ↑ 2 ) ∈ ℂ )
40	38 39	addcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ∈ ℂ )
41	40	subid1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − 0 ) = ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
42	7 37 41	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝑂 ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( 𝑍 ↑ 2 ) = ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )

Metamath Proof Explorer

Theorem pythag

Proof