# 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 ${⊢}{\phi }\to {U}\in ℂ$
lawcoslem1.2 ${⊢}{\phi }\to {V}\in ℂ$
lawcoslem1.3 ${⊢}{\phi }\to {U}\ne 0$
lawcoslem1.4 ${⊢}{\phi }\to {V}\ne 0$
Assertion lawcoslem1 ${⊢}{\phi }\to {\left|{U}-{V}\right|}^{2}={\left|{U}\right|}^{2}+{\left|{V}\right|}^{2}-2\left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)$

### Proof

Step Hyp Ref Expression
1 lawcoslem1.1 ${⊢}{\phi }\to {U}\in ℂ$
2 lawcoslem1.2 ${⊢}{\phi }\to {V}\in ℂ$
3 lawcoslem1.3 ${⊢}{\phi }\to {U}\ne 0$
4 lawcoslem1.4 ${⊢}{\phi }\to {V}\ne 0$
5 sqabssub ${⊢}\left({U}\in ℂ\wedge {V}\in ℂ\right)\to {\left|{U}-{V}\right|}^{2}={\left|{U}\right|}^{2}+{\left|{V}\right|}^{2}-2\Re \left({U}\stackrel{‾}{{V}}\right)$
6 1 2 5 syl2anc ${⊢}{\phi }\to {\left|{U}-{V}\right|}^{2}={\left|{U}\right|}^{2}+{\left|{V}\right|}^{2}-2\Re \left({U}\stackrel{‾}{{V}}\right)$
7 1 2 4 absdivd ${⊢}{\phi }\to \left|\frac{{U}}{{V}}\right|=\frac{\left|{U}\right|}{\left|{V}\right|}$
8 7 oveq2d ${⊢}{\phi }\to \frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}=\frac{\Re \left(\frac{{U}}{{V}}\right)}{\frac{\left|{U}\right|}{\left|{V}\right|}}$
9 8 oveq2d ${⊢}{\phi }\to \left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)=\left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\frac{\left|{U}\right|}{\left|{V}\right|}}\right)$
10 1 abscld ${⊢}{\phi }\to \left|{U}\right|\in ℝ$
11 2 abscld ${⊢}{\phi }\to \left|{V}\right|\in ℝ$
12 10 11 remulcld ${⊢}{\phi }\to \left|{U}\right|\left|{V}\right|\in ℝ$
13 12 recnd ${⊢}{\phi }\to \left|{U}\right|\left|{V}\right|\in ℂ$
14 1 2 4 divcld ${⊢}{\phi }\to \frac{{U}}{{V}}\in ℂ$
15 14 recld ${⊢}{\phi }\to \Re \left(\frac{{U}}{{V}}\right)\in ℝ$
16 15 recnd ${⊢}{\phi }\to \Re \left(\frac{{U}}{{V}}\right)\in ℂ$
17 10 recnd ${⊢}{\phi }\to \left|{U}\right|\in ℂ$
18 11 recnd ${⊢}{\phi }\to \left|{V}\right|\in ℂ$
19 2 4 absne0d ${⊢}{\phi }\to \left|{V}\right|\ne 0$
20 17 18 19 divcld ${⊢}{\phi }\to \frac{\left|{U}\right|}{\left|{V}\right|}\in ℂ$
21 1 3 absne0d ${⊢}{\phi }\to \left|{U}\right|\ne 0$
22 17 18 21 19 divne0d ${⊢}{\phi }\to \frac{\left|{U}\right|}{\left|{V}\right|}\ne 0$
23 13 16 20 22 div12d ${⊢}{\phi }\to \left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\frac{\left|{U}\right|}{\left|{V}\right|}}\right)=\Re \left(\frac{{U}}{{V}}\right)\left(\frac{\left|{U}\right|\left|{V}\right|}{\frac{\left|{U}\right|}{\left|{V}\right|}}\right)$
24 9 23 eqtrd ${⊢}{\phi }\to \left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)=\Re \left(\frac{{U}}{{V}}\right)\left(\frac{\left|{U}\right|\left|{V}\right|}{\frac{\left|{U}\right|}{\left|{V}\right|}}\right)$
25 13 17 18 21 19 divdiv2d ${⊢}{\phi }\to \frac{\left|{U}\right|\left|{V}\right|}{\frac{\left|{U}\right|}{\left|{V}\right|}}=\frac{\left|{U}\right|\left|{V}\right|\left|{V}\right|}{\left|{U}\right|}$
26 18 sqvald ${⊢}{\phi }\to {\left|{V}\right|}^{2}=\left|{V}\right|\left|{V}\right|$
27 26 oveq1d ${⊢}{\phi }\to {\left|{V}\right|}^{2}\left|{U}\right|=\left|{V}\right|\left|{V}\right|\left|{U}\right|$
28 17 18 18 mul31d ${⊢}{\phi }\to \left|{U}\right|\left|{V}\right|\left|{V}\right|=\left|{V}\right|\left|{V}\right|\left|{U}\right|$
29 27 28 eqtr4d ${⊢}{\phi }\to {\left|{V}\right|}^{2}\left|{U}\right|=\left|{U}\right|\left|{V}\right|\left|{V}\right|$
30 29 oveq1d ${⊢}{\phi }\to \frac{{\left|{V}\right|}^{2}\left|{U}\right|}{\left|{U}\right|}=\frac{\left|{U}\right|\left|{V}\right|\left|{V}\right|}{\left|{U}\right|}$
31 18 sqcld ${⊢}{\phi }\to {\left|{V}\right|}^{2}\in ℂ$
32 31 17 21 divcan4d ${⊢}{\phi }\to \frac{{\left|{V}\right|}^{2}\left|{U}\right|}{\left|{U}\right|}={\left|{V}\right|}^{2}$
33 25 30 32 3eqtr2rd ${⊢}{\phi }\to {\left|{V}\right|}^{2}=\frac{\left|{U}\right|\left|{V}\right|}{\frac{\left|{U}\right|}{\left|{V}\right|}}$
34 33 oveq2d ${⊢}{\phi }\to \Re \left(\frac{{U}}{{V}}\right){\left|{V}\right|}^{2}=\Re \left(\frac{{U}}{{V}}\right)\left(\frac{\left|{U}\right|\left|{V}\right|}{\frac{\left|{U}\right|}{\left|{V}\right|}}\right)$
35 16 31 mulcomd ${⊢}{\phi }\to \Re \left(\frac{{U}}{{V}}\right){\left|{V}\right|}^{2}={\left|{V}\right|}^{2}\Re \left(\frac{{U}}{{V}}\right)$
36 11 resqcld ${⊢}{\phi }\to {\left|{V}\right|}^{2}\in ℝ$
37 36 14 remul2d ${⊢}{\phi }\to \Re \left({\left|{V}\right|}^{2}\left(\frac{{U}}{{V}}\right)\right)={\left|{V}\right|}^{2}\Re \left(\frac{{U}}{{V}}\right)$
38 35 37 eqtr4d ${⊢}{\phi }\to \Re \left(\frac{{U}}{{V}}\right){\left|{V}\right|}^{2}=\Re \left({\left|{V}\right|}^{2}\left(\frac{{U}}{{V}}\right)\right)$
39 1 31 2 4 div12d ${⊢}{\phi }\to {U}\left(\frac{{\left|{V}\right|}^{2}}{{V}}\right)={\left|{V}\right|}^{2}\left(\frac{{U}}{{V}}\right)$
40 31 2 4 divrecd ${⊢}{\phi }\to \frac{{\left|{V}\right|}^{2}}{{V}}={\left|{V}\right|}^{2}\left(\frac{1}{{V}}\right)$
41 recval ${⊢}\left({V}\in ℂ\wedge {V}\ne 0\right)\to \frac{1}{{V}}=\frac{\stackrel{‾}{{V}}}{{\left|{V}\right|}^{2}}$
42 2 4 41 syl2anc ${⊢}{\phi }\to \frac{1}{{V}}=\frac{\stackrel{‾}{{V}}}{{\left|{V}\right|}^{2}}$
43 42 oveq2d ${⊢}{\phi }\to {\left|{V}\right|}^{2}\left(\frac{1}{{V}}\right)={\left|{V}\right|}^{2}\left(\frac{\stackrel{‾}{{V}}}{{\left|{V}\right|}^{2}}\right)$
44 2 cjcld ${⊢}{\phi }\to \stackrel{‾}{{V}}\in ℂ$
45 sqne0 ${⊢}\left|{V}\right|\in ℂ\to \left({\left|{V}\right|}^{2}\ne 0↔\left|{V}\right|\ne 0\right)$
46 18 45 syl ${⊢}{\phi }\to \left({\left|{V}\right|}^{2}\ne 0↔\left|{V}\right|\ne 0\right)$
47 19 46 mpbird ${⊢}{\phi }\to {\left|{V}\right|}^{2}\ne 0$
48 44 31 47 divcan2d ${⊢}{\phi }\to {\left|{V}\right|}^{2}\left(\frac{\stackrel{‾}{{V}}}{{\left|{V}\right|}^{2}}\right)=\stackrel{‾}{{V}}$
49 43 48 eqtrd ${⊢}{\phi }\to {\left|{V}\right|}^{2}\left(\frac{1}{{V}}\right)=\stackrel{‾}{{V}}$
50 40 49 eqtrd ${⊢}{\phi }\to \frac{{\left|{V}\right|}^{2}}{{V}}=\stackrel{‾}{{V}}$
51 50 oveq2d ${⊢}{\phi }\to {U}\left(\frac{{\left|{V}\right|}^{2}}{{V}}\right)={U}\stackrel{‾}{{V}}$
52 39 51 eqtr3d ${⊢}{\phi }\to {\left|{V}\right|}^{2}\left(\frac{{U}}{{V}}\right)={U}\stackrel{‾}{{V}}$
53 52 fveq2d ${⊢}{\phi }\to \Re \left({\left|{V}\right|}^{2}\left(\frac{{U}}{{V}}\right)\right)=\Re \left({U}\stackrel{‾}{{V}}\right)$
54 38 53 eqtrd ${⊢}{\phi }\to \Re \left(\frac{{U}}{{V}}\right){\left|{V}\right|}^{2}=\Re \left({U}\stackrel{‾}{{V}}\right)$
55 24 34 54 3eqtr2rd ${⊢}{\phi }\to \Re \left({U}\stackrel{‾}{{V}}\right)=\left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)$
56 55 oveq2d ${⊢}{\phi }\to 2\Re \left({U}\stackrel{‾}{{V}}\right)=2\left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)$
57 56 oveq2d ${⊢}{\phi }\to {\left|{U}\right|}^{2}+{\left|{V}\right|}^{2}-2\Re \left({U}\stackrel{‾}{{V}}\right)={\left|{U}\right|}^{2}+{\left|{V}\right|}^{2}-2\left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)$
58 6 57 eqtrd ${⊢}{\phi }\to {\left|{U}-{V}\right|}^{2}={\left|{U}\right|}^{2}+{\left|{V}\right|}^{2}-2\left|{U}\right|\left|{V}\right|\left(\frac{\Re \left(\frac{{U}}{{V}}\right)}{\left|\frac{{U}}{{V}}\right|}\right)$