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\bar{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\bar{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{\bar{V}}{{\left|V\right|}^2}$$
42	2 4 41	syl2anc	$$⊢\phi \to \frac{1}{V}=\frac{\bar{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{\bar{V}}{{\left|V\right|}^2}\right)$$
44	2	cjcld	$$⊢\phi \to \bar{V}\in ℂ$$
45		sqne0	$$⊢\left|V\right|\in ℂ\to \left({\left|V\right|}^2\ne 0\leftrightarrow \left|V\right|\ne 0\right)$$
46	18 45	syl	$$⊢\phi \to \left({\left|V\right|}^2\ne 0\leftrightarrow \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{\bar{V}}{{\left|V\right|}^2}\right)=\bar{V}$$
49	43 48	eqtrd	$$⊢\phi \to {\left|V\right|}^2\left(\frac{1}{V}\right)=\bar{V}$$
50	40 49	eqtrd	$$⊢\phi \to \frac{{\left|V\right|}^2}{V}=\bar{V}$$
51	50	oveq2d	$$⊢\phi \to U\left(\frac{{\left|V\right|}^2}{V}\right)=U\bar{V}$$
52	39 51	eqtr3d	$$⊢\phi \to {\left|V\right|}^2\left(\frac{U}{V}\right)=U\bar{V}$$
53	52	fveq2d	$$⊢\phi \to \Re \left({\left|V\right|}^2\left(\frac{U}{V}\right)\right)=\Re \left(U\bar{V}\right)$$
54	38 53	eqtrd	$$⊢\phi \to \Re \left(\frac{U}{V}\right){\left|V\right|}^2=\Re \left(U\bar{V}\right)$$
55	24 34 54	3eqtr2rd	$$⊢\phi \to \Re \left(U\bar{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\bar{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\bar{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)$$