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 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
lawcos.2 
|- X = ( abs ` ( B - C ) )
lawcos.3 
|- Y = ( abs ` ( A - C ) )
lawcos.4 
|- Z = ( abs ` ( A - B ) )
lawcos.5 
|- O = ( ( B - C ) F ( A - C ) )
Assertion lawcos 
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Z ^ 2 ) = ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lawcos.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 lawcos.2 
 |-  X = ( abs ` ( B - C ) )
3 lawcos.3 
 |-  Y = ( abs ` ( A - C ) )
4 lawcos.4 
 |-  Z = ( abs ` ( A - B ) )
5 lawcos.5 
 |-  O = ( ( B - C ) F ( A - C ) )
6 subcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A - C ) e. CC )
7 6 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - C ) e. CC )
8 7 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( A - C ) e. CC )
9 subcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
10 9 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
11 10 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( B - C ) e. CC )
12 subeq0 
 |-  ( ( A e. CC /\ C e. CC ) -> ( ( A - C ) = 0 <-> A = C ) )
13 12 necon3bid 
 |-  ( ( A e. CC /\ C e. CC ) -> ( ( A - C ) =/= 0 <-> A =/= C ) )
14 13 bicomd 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A =/= C <-> ( A - C ) =/= 0 ) )
15 14 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A =/= C <-> ( A - C ) =/= 0 ) )
16 15 biimpa 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ A =/= C ) -> ( A - C ) =/= 0 )
17 16 adantrr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( A - C ) =/= 0 )
18 subeq0 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B - C ) = 0 <-> B = C ) )
19 18 necon3bid 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B - C ) =/= 0 <-> B =/= C ) )
20 19 bicomd 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B =/= C <-> ( B - C ) =/= 0 ) )
21 20 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B =/= C <-> ( B - C ) =/= 0 ) )
22 21 biimpa 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ B =/= C ) -> ( B - C ) =/= 0 )
23 22 adantrl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( B - C ) =/= 0 )
24 8 11 17 23 lawcoslem1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( abs ` ( ( A - C ) - ( B - C ) ) ) ^ 2 ) = ( ( ( ( abs ` ( A - C ) ) ^ 2 ) + ( ( abs ` ( B - C ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - C ) ) x. ( abs ` ( B - C ) ) ) x. ( ( Re ` ( ( A - C ) / ( B - C ) ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) ) ) ) )
25 nnncan2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) - ( B - C ) ) = ( A - B ) )
26 25 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( abs ` ( ( A - C ) - ( B - C ) ) ) = ( abs ` ( A - B ) ) )
27 4 26 eqtr4id 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> Z = ( abs ` ( ( A - C ) - ( B - C ) ) ) )
28 27 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( Z ^ 2 ) = ( ( abs ` ( ( A - C ) - ( B - C ) ) ) ^ 2 ) )
29 28 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Z ^ 2 ) = ( ( abs ` ( ( A - C ) - ( B - C ) ) ) ^ 2 ) )
30 2 oveq1i 
 |-  ( X ^ 2 ) = ( ( abs ` ( B - C ) ) ^ 2 )
31 3 oveq1i 
 |-  ( Y ^ 2 ) = ( ( abs ` ( A - C ) ) ^ 2 )
32 30 31 oveq12i 
 |-  ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( abs ` ( B - C ) ) ^ 2 ) + ( ( abs ` ( A - C ) ) ^ 2 ) )
33 8 abscld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( abs ` ( A - C ) ) e. RR )
34 33 recnd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( abs ` ( A - C ) ) e. CC )
35 34 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( abs ` ( A - C ) ) ^ 2 ) e. CC )
36 11 abscld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( abs ` ( B - C ) ) e. RR )
37 36 recnd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( abs ` ( B - C ) ) e. CC )
38 37 sqcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( abs ` ( B - C ) ) ^ 2 ) e. CC )
39 35 38 addcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( ( abs ` ( A - C ) ) ^ 2 ) + ( ( abs ` ( B - C ) ) ^ 2 ) ) = ( ( ( abs ` ( B - C ) ) ^ 2 ) + ( ( abs ` ( A - C ) ) ^ 2 ) ) )
40 32 39 eqtr4id 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( abs ` ( A - C ) ) ^ 2 ) + ( ( abs ` ( B - C ) ) ^ 2 ) ) )
41 2 3 oveq12i 
 |-  ( X x. Y ) = ( ( abs ` ( B - C ) ) x. ( abs ` ( A - C ) ) )
42 34 37 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( abs ` ( A - C ) ) x. ( abs ` ( B - C ) ) ) = ( ( abs ` ( B - C ) ) x. ( abs ` ( A - C ) ) ) )
43 41 42 eqtr4id 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( X x. Y ) = ( ( abs ` ( A - C ) ) x. ( abs ` ( B - C ) ) ) )
44 5 fveq2i 
 |-  ( cos ` O ) = ( cos ` ( ( B - C ) F ( A - C ) ) )
45 1 11 23 8 17 angvald 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( B - C ) F ( A - C ) ) = ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) )
46 45 fveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( cos ` ( ( B - C ) F ( A - C ) ) ) = ( cos ` ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) )
47 44 46 eqtrid 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( cos ` O ) = ( cos ` ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) )
48 8 11 23 divcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( A - C ) / ( B - C ) ) e. CC )
49 8 11 17 23 divne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( A - C ) / ( B - C ) ) =/= 0 )
50 48 49 logcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( log ` ( ( A - C ) / ( B - C ) ) ) e. CC )
51 50 imcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) e. RR )
52 recosval 
 |-  ( ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) e. RR -> ( cos ` ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) = ( Re ` ( exp ` ( _i x. ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) ) ) )
53 51 52 syl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( cos ` ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) = ( Re ` ( exp ` ( _i x. ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) ) ) )
54 47 53 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( cos ` O ) = ( Re ` ( exp ` ( _i x. ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) ) ) )
55 efiarg 
 |-  ( ( ( ( A - C ) / ( B - C ) ) e. CC /\ ( ( A - C ) / ( B - C ) ) =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) ) = ( ( ( A - C ) / ( B - C ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) )
56 48 49 55 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( exp ` ( _i x. ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) ) = ( ( ( A - C ) / ( B - C ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) )
57 56 fveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Re ` ( exp ` ( _i x. ( Im ` ( log ` ( ( A - C ) / ( B - C ) ) ) ) ) ) ) = ( Re ` ( ( ( A - C ) / ( B - C ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) ) )
58 48 abscld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( abs ` ( ( A - C ) / ( B - C ) ) ) e. RR )
59 48 49 absne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( abs ` ( ( A - C ) / ( B - C ) ) ) =/= 0 )
60 58 48 59 redivd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Re ` ( ( ( A - C ) / ( B - C ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) ) = ( ( Re ` ( ( A - C ) / ( B - C ) ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) )
61 54 57 60 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( cos ` O ) = ( ( Re ` ( ( A - C ) / ( B - C ) ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) )
62 43 61 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( X x. Y ) x. ( cos ` O ) ) = ( ( ( abs ` ( A - C ) ) x. ( abs ` ( B - C ) ) ) x. ( ( Re ` ( ( A - C ) / ( B - C ) ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) ) )
63 62 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) = ( 2 x. ( ( ( abs ` ( A - C ) ) x. ( abs ` ( B - C ) ) ) x. ( ( Re ` ( ( A - C ) / ( B - C ) ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) ) ) )
64 40 63 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) = ( ( ( ( abs ` ( A - C ) ) ^ 2 ) + ( ( abs ` ( B - C ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - C ) ) x. ( abs ` ( B - C ) ) ) x. ( ( Re ` ( ( A - C ) / ( B - C ) ) ) / ( abs ` ( ( A - C ) / ( B - C ) ) ) ) ) ) ) )
65 24 29 64 3eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Z ^ 2 ) = ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) )