Metamath Proof Explorer

Theorem 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 ) ) )