Metamath Proof Explorer

Theorem lawcos

Description: Law of cosines (also known as the Al-Kashi theorem or the generalized Pythagorean theorem, or the cosine formula or cosine rule). Given three distinct points A, B, and 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, and O is the signed angle m/__ BCA on the complex plane. We translate triangle ABC to move C to the origin (C-C), B to U=(B-C), and A to V=(A-C), then use lemma lawcoslem1 to prove this algebraically simpler case. The Metamath convention is to use a signed angle; in this case the sign doesn't matter because we use the cosine of the angle (see cosneg ). The Pythagorean theorem pythag is a special case of the law of cosines. The theorem's expression and approach were suggested by Mario Carneiro. This is Metamath 100 proof #94. (Contributed by David A. Wheeler, 12-Jun-2015)

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

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 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
7 6 3adant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
9 subcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
10 9 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
12 subeq0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) = 0 ↔ 𝐴 = 𝐶 ) )
13 12 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) ≠ 0 ↔ 𝐴 ≠ 𝐶 ) )
14 13 bicomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ≠ 𝐶 ↔ ( 𝐴 − 𝐶 ) ≠ 0 ) )
15 14 3adant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ≠ 𝐶 ↔ ( 𝐴 − 𝐶 ) ≠ 0 ) )
16 15 biimpa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 − 𝐶 ) ≠ 0 )
17 16 adantrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐴 − 𝐶 ) ≠ 0 )
18 subeq0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) = 0 ↔ 𝐵 = 𝐶 ) )
19 18 necon3bid ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 − 𝐶 ) ≠ 0 ↔ 𝐵 ≠ 𝐶 ) )
20 19 bicomd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ≠ 𝐶 ↔ ( 𝐵 − 𝐶 ) ≠ 0 ) )
21 20 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ≠ 𝐶 ↔ ( 𝐵 − 𝐶 ) ≠ 0 ) )
22 21 biimpa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 − 𝐶 ) ≠ 0 )
23 22 adantrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝐵 − 𝐶 ) ≠ 0 )
24 8 11 17 23 lawcoslem1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( abs ‘ ( ( 𝐴 − 𝐶 ) − ( 𝐵 − 𝐶 ) ) ) ↑ 2 ) = ( ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) ) − ( 2 · ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) · ( abs ‘ ( 𝐵 − 𝐶 ) ) ) · ( ( ℜ ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) ) )
25 nnncan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) − ( 𝐵 − 𝐶 ) ) = ( 𝐴 − 𝐵 ) )
26 25 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( abs ‘ ( ( 𝐴 − 𝐶 ) − ( 𝐵 − 𝐶 ) ) ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
27 4 26 eqtr4id ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝑍 = ( abs ‘ ( ( 𝐴 − 𝐶 ) − ( 𝐵 − 𝐶 ) ) ) )
28 27 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑍 ↑ 2 ) = ( ( abs ‘ ( ( 𝐴 − 𝐶 ) − ( 𝐵 − 𝐶 ) ) ) ↑ 2 ) )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝑍 ↑ 2 ) = ( ( abs ‘ ( ( 𝐴 − 𝐶 ) − ( 𝐵 − 𝐶 ) ) ) ↑ 2 ) )
30 2 oveq1i ⊢ ( 𝑋 ↑ 2 ) = ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 )
31 3 oveq1i ⊢ ( 𝑌 ↑ 2 ) = ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 )
32 30 31 oveq12i ⊢ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) )
33 8 abscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
34 33 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℂ )
35 34 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) ∈ ℂ )
36 11 abscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
37 36 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℂ )
38 37 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) ∈ ℂ )
39 35 38 addcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) ) )
40 32 39 eqtr4id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) ) )
41 2 3 oveq12i ⊢ ( 𝑋 · 𝑌 ) = ( ( abs ‘ ( 𝐵 − 𝐶 ) ) · ( abs ‘ ( 𝐴 − 𝐶 ) ) )
42 34 37 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( abs ‘ ( 𝐴 − 𝐶 ) ) · ( abs ‘ ( 𝐵 − 𝐶 ) ) ) = ( ( abs ‘ ( 𝐵 − 𝐶 ) ) · ( abs ‘ ( 𝐴 − 𝐶 ) ) ) )
43 41 42 eqtr4id ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝑋 · 𝑌 ) = ( ( abs ‘ ( 𝐴 − 𝐶 ) ) · ( abs ‘ ( 𝐵 − 𝐶 ) ) ) )
44 5 fveq2i ⊢ ( cos ‘ 𝑂 ) = ( cos ‘ ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) ) )
45 1 11 23 8 17 angvald ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) ) = ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) )
46 45 fveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( cos ‘ ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) )
47 44 46 eqtrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( cos ‘ 𝑂 ) = ( cos ‘ ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) )
48 8 11 23 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ∈ ℂ )
49 8 11 17 23 divne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ≠ 0 )
50 48 49 logcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ∈ ℂ )
51 50 imcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ∈ ℝ )
52 recosval ⊢ ( ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ∈ ℝ → ( cos ‘ ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) ) )
53 51 52 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( cos ‘ ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) ) )
54 47 53 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( cos ‘ 𝑂 ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) ) )
55 efiarg ⊢ ( ( ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ∈ ℂ ∧ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) = ( ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) )
56 48 49 55 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) = ( ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) )
57 56 fveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) ) = ( ℜ ‘ ( ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) )
58 48 abscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ∈ ℝ )
59 48 49 absne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ≠ 0 )
60 58 48 59 redivd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ℜ ‘ ( ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) = ( ( ℜ ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) )
61 54 57 60 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( cos ‘ 𝑂 ) = ( ( ℜ ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) )
62 43 61 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) = ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) · ( abs ‘ ( 𝐵 − 𝐶 ) ) ) · ( ( ℜ ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) )
63 62 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) = ( 2 · ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) · ( abs ‘ ( 𝐵 − 𝐶 ) ) ) · ( ( ℜ ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) )
64 40 63 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) = ( ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐵 − 𝐶 ) ) ↑ 2 ) ) − ( 2 · ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) · ( abs ‘ ( 𝐵 − 𝐶 ) ) ) · ( ( ℜ ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) / ( abs ‘ ( ( 𝐴 − 𝐶 ) / ( 𝐵 − 𝐶 ) ) ) ) ) ) ) )
65 24 29 64 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝑍 ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) )