Metamath Proof Explorer

Theorem lawcoslem1

Description: Lemma for lawcos . Here we prove the law for a point at the origin and two distinct points U and V, using an expanded version of the signed angle expression on the complex plane. (Contributed by David A. Wheeler, 11-Jun-2015)

Ref Expression
Hypotheses lawcoslem1.1 
|- ( ph -> U e. CC )
lawcoslem1.2 
|- ( ph -> V e. CC )
lawcoslem1.3 
|- ( ph -> U =/= 0 )
lawcoslem1.4 
|- ( ph -> V =/= 0 )
Assertion lawcoslem1 
|- ( ph -> ( ( abs ` ( U - V ) ) ^ 2 ) = ( ( ( ( abs ` U ) ^ 2 ) + ( ( abs ` V ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lawcoslem1.1 
 |-  ( ph -> U e. CC )
2 lawcoslem1.2 
 |-  ( ph -> V e. CC )
3 lawcoslem1.3 
 |-  ( ph -> U =/= 0 )
4 lawcoslem1.4 
 |-  ( ph -> V =/= 0 )
5 sqabssub 
 |-  ( ( U e. CC /\ V e. CC ) -> ( ( abs ` ( U - V ) ) ^ 2 ) = ( ( ( ( abs ` U ) ^ 2 ) + ( ( abs ` V ) ^ 2 ) ) - ( 2 x. ( Re ` ( U x. ( * ` V ) ) ) ) ) )
6 1 2 5 syl2anc 
 |-  ( ph -> ( ( abs ` ( U - V ) ) ^ 2 ) = ( ( ( ( abs ` U ) ^ 2 ) + ( ( abs ` V ) ^ 2 ) ) - ( 2 x. ( Re ` ( U x. ( * ` V ) ) ) ) ) )
7 1 2 4 absdivd 
 |-  ( ph -> ( abs ` ( U / V ) ) = ( ( abs ` U ) / ( abs ` V ) ) )
8 7 oveq2d 
 |-  ( ph -> ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) = ( ( Re ` ( U / V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) )
9 8 oveq2d 
 |-  ( ph -> ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) = ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) ) )
10 1 abscld 
 |-  ( ph -> ( abs ` U ) e. RR )
11 2 abscld 
 |-  ( ph -> ( abs ` V ) e. RR )
12 10 11 remulcld 
 |-  ( ph -> ( ( abs ` U ) x. ( abs ` V ) ) e. RR )
13 12 recnd 
 |-  ( ph -> ( ( abs ` U ) x. ( abs ` V ) ) e. CC )
14 1 2 4 divcld 
 |-  ( ph -> ( U / V ) e. CC )
15 14 recld 
 |-  ( ph -> ( Re ` ( U / V ) ) e. RR )
16 15 recnd 
 |-  ( ph -> ( Re ` ( U / V ) ) e. CC )
17 10 recnd 
 |-  ( ph -> ( abs ` U ) e. CC )
18 11 recnd 
 |-  ( ph -> ( abs ` V ) e. CC )
19 2 4 absne0d 
 |-  ( ph -> ( abs ` V ) =/= 0 )
20 17 18 19 divcld 
 |-  ( ph -> ( ( abs ` U ) / ( abs ` V ) ) e. CC )
21 1 3 absne0d 
 |-  ( ph -> ( abs ` U ) =/= 0 )
22 17 18 21 19 divne0d 
 |-  ( ph -> ( ( abs ` U ) / ( abs ` V ) ) =/= 0 )
23 13 16 20 22 div12d 
 |-  ( ph -> ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) ) = ( ( Re ` ( U / V ) ) x. ( ( ( abs ` U ) x. ( abs ` V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) ) )
24 9 23 eqtrd 
 |-  ( ph -> ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) = ( ( Re ` ( U / V ) ) x. ( ( ( abs ` U ) x. ( abs ` V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) ) )
25 13 17 18 21 19 divdiv2d 
 |-  ( ph -> ( ( ( abs ` U ) x. ( abs ` V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) = ( ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( abs ` V ) ) / ( abs ` U ) ) )
26 18 sqvald 
 |-  ( ph -> ( ( abs ` V ) ^ 2 ) = ( ( abs ` V ) x. ( abs ` V ) ) )
27 26 oveq1d 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) x. ( abs ` U ) ) = ( ( ( abs ` V ) x. ( abs ` V ) ) x. ( abs ` U ) ) )
28 17 18 18 mul31d 
 |-  ( ph -> ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( abs ` V ) ) = ( ( ( abs ` V ) x. ( abs ` V ) ) x. ( abs ` U ) ) )
29 27 28 eqtr4d 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) x. ( abs ` U ) ) = ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( abs ` V ) ) )
30 29 oveq1d 
 |-  ( ph -> ( ( ( ( abs ` V ) ^ 2 ) x. ( abs ` U ) ) / ( abs ` U ) ) = ( ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( abs ` V ) ) / ( abs ` U ) ) )
31 18 sqcld 
 |-  ( ph -> ( ( abs ` V ) ^ 2 ) e. CC )
32 31 17 21 divcan4d 
 |-  ( ph -> ( ( ( ( abs ` V ) ^ 2 ) x. ( abs ` U ) ) / ( abs ` U ) ) = ( ( abs ` V ) ^ 2 ) )
33 25 30 32 3eqtr2rd 
 |-  ( ph -> ( ( abs ` V ) ^ 2 ) = ( ( ( abs ` U ) x. ( abs ` V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) )
34 33 oveq2d 
 |-  ( ph -> ( ( Re ` ( U / V ) ) x. ( ( abs ` V ) ^ 2 ) ) = ( ( Re ` ( U / V ) ) x. ( ( ( abs ` U ) x. ( abs ` V ) ) / ( ( abs ` U ) / ( abs ` V ) ) ) ) )
35 16 31 mulcomd 
 |-  ( ph -> ( ( Re ` ( U / V ) ) x. ( ( abs ` V ) ^ 2 ) ) = ( ( ( abs ` V ) ^ 2 ) x. ( Re ` ( U / V ) ) ) )
36 11 resqcld 
 |-  ( ph -> ( ( abs ` V ) ^ 2 ) e. RR )
37 36 14 remul2d 
 |-  ( ph -> ( Re ` ( ( ( abs ` V ) ^ 2 ) x. ( U / V ) ) ) = ( ( ( abs ` V ) ^ 2 ) x. ( Re ` ( U / V ) ) ) )
38 35 37 eqtr4d 
 |-  ( ph -> ( ( Re ` ( U / V ) ) x. ( ( abs ` V ) ^ 2 ) ) = ( Re ` ( ( ( abs ` V ) ^ 2 ) x. ( U / V ) ) ) )
39 1 31 2 4 div12d 
 |-  ( ph -> ( U x. ( ( ( abs ` V ) ^ 2 ) / V ) ) = ( ( ( abs ` V ) ^ 2 ) x. ( U / V ) ) )
40 31 2 4 divrecd 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) / V ) = ( ( ( abs ` V ) ^ 2 ) x. ( 1 / V ) ) )
41 recval 
 |-  ( ( V e. CC /\ V =/= 0 ) -> ( 1 / V ) = ( ( * ` V ) / ( ( abs ` V ) ^ 2 ) ) )
42 2 4 41 syl2anc 
 |-  ( ph -> ( 1 / V ) = ( ( * ` V ) / ( ( abs ` V ) ^ 2 ) ) )
43 42 oveq2d 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) x. ( 1 / V ) ) = ( ( ( abs ` V ) ^ 2 ) x. ( ( * ` V ) / ( ( abs ` V ) ^ 2 ) ) ) )
44 2 cjcld 
 |-  ( ph -> ( * ` V ) e. CC )
45 sqne0 
 |-  ( ( abs ` V ) e. CC -> ( ( ( abs ` V ) ^ 2 ) =/= 0 <-> ( abs ` V ) =/= 0 ) )
46 18 45 syl 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) =/= 0 <-> ( abs ` V ) =/= 0 ) )
47 19 46 mpbird 
 |-  ( ph -> ( ( abs ` V ) ^ 2 ) =/= 0 )
48 44 31 47 divcan2d 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) x. ( ( * ` V ) / ( ( abs ` V ) ^ 2 ) ) ) = ( * ` V ) )
49 43 48 eqtrd 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) x. ( 1 / V ) ) = ( * ` V ) )
50 40 49 eqtrd 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) / V ) = ( * ` V ) )
51 50 oveq2d 
 |-  ( ph -> ( U x. ( ( ( abs ` V ) ^ 2 ) / V ) ) = ( U x. ( * ` V ) ) )
52 39 51 eqtr3d 
 |-  ( ph -> ( ( ( abs ` V ) ^ 2 ) x. ( U / V ) ) = ( U x. ( * ` V ) ) )
53 52 fveq2d 
 |-  ( ph -> ( Re ` ( ( ( abs ` V ) ^ 2 ) x. ( U / V ) ) ) = ( Re ` ( U x. ( * ` V ) ) ) )
54 38 53 eqtrd 
 |-  ( ph -> ( ( Re ` ( U / V ) ) x. ( ( abs ` V ) ^ 2 ) ) = ( Re ` ( U x. ( * ` V ) ) ) )
55 24 34 54 3eqtr2rd 
 |-  ( ph -> ( Re ` ( U x. ( * ` V ) ) ) = ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) )
56 55 oveq2d 
 |-  ( ph -> ( 2 x. ( Re ` ( U x. ( * ` V ) ) ) ) = ( 2 x. ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) ) )
57 56 oveq2d 
 |-  ( ph -> ( ( ( ( abs ` U ) ^ 2 ) + ( ( abs ` V ) ^ 2 ) ) - ( 2 x. ( Re ` ( U x. ( * ` V ) ) ) ) ) = ( ( ( ( abs ` U ) ^ 2 ) + ( ( abs ` V ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) ) ) )
58 6 57 eqtrd 
 |-  ( ph -> ( ( abs ` ( U - V ) ) ^ 2 ) = ( ( ( ( abs ` U ) ^ 2 ) + ( ( abs ` V ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` U ) x. ( abs ` V ) ) x. ( ( Re ` ( U / V ) ) / ( abs ` ( U / V ) ) ) ) ) ) )