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	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
	lawcoslem1.2	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
	lawcoslem1.3	⊢ ( 𝜑 → 𝑈 ≠ 0 )
	lawcoslem1.4	⊢ ( 𝜑 → 𝑉 ≠ 0 )
Assertion	lawcoslem1	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑈 − 𝑉 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝑈 ) ↑ 2 ) + ( ( abs ‘ 𝑉 ) ↑ 2 ) ) − ( 2 · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lawcoslem1.1	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
2		lawcoslem1.2	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
3		lawcoslem1.3	⊢ ( 𝜑 → 𝑈 ≠ 0 )
4		lawcoslem1.4	⊢ ( 𝜑 → 𝑉 ≠ 0 )
5		sqabssub	⊢ ( ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ) → ( ( abs ‘ ( 𝑈 − 𝑉 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝑈 ) ↑ 2 ) + ( ( abs ‘ 𝑉 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) ) ) )
6	1 2 5	syl2anc	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑈 − 𝑉 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝑈 ) ↑ 2 ) + ( ( abs ‘ 𝑉 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) ) ) )
7	1 2 4	absdivd	⊢ ( 𝜑 → ( abs ‘ ( 𝑈 / 𝑉 ) ) = ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) )
8	7	oveq2d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) = ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) )
9	8	oveq2d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) = ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) ) )
10	1	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℝ )
11	2	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℝ )
12	10 11	remulcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) ∈ ℝ )
13	12	recnd	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) ∈ ℂ )
14	1 2 4	divcld	⊢ ( 𝜑 → ( 𝑈 / 𝑉 ) ∈ ℂ )
15	14	recld	⊢ ( 𝜑 → ( ℜ ‘ ( 𝑈 / 𝑉 ) ) ∈ ℝ )
16	15	recnd	⊢ ( 𝜑 → ( ℜ ‘ ( 𝑈 / 𝑉 ) ) ∈ ℂ )
17	10	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℂ )
18	11	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℂ )
19	2 4	absne0d	⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ≠ 0 )
20	17 18 19	divcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ∈ ℂ )
21	1 3	absne0d	⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ≠ 0 )
22	17 18 21 19	divne0d	⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ≠ 0 )
23	13 16 20 22	div12d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) ) = ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) ) )
24	9 23	eqtrd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) = ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) ) )
25	13 17 18 21 19	divdiv2d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) = ( ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( abs ‘ 𝑉 ) ) / ( abs ‘ 𝑈 ) ) )
26	18	sqvald	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) ↑ 2 ) = ( ( abs ‘ 𝑉 ) · ( abs ‘ 𝑉 ) ) )
27	26	oveq1d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( abs ‘ 𝑈 ) ) = ( ( ( abs ‘ 𝑉 ) · ( abs ‘ 𝑉 ) ) · ( abs ‘ 𝑈 ) ) )
28	17 18 18	mul31d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( abs ‘ 𝑉 ) ) = ( ( ( abs ‘ 𝑉 ) · ( abs ‘ 𝑉 ) ) · ( abs ‘ 𝑈 ) ) )
29	27 28	eqtr4d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( abs ‘ 𝑈 ) ) = ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( abs ‘ 𝑉 ) ) )
30	29	oveq1d	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( abs ‘ 𝑈 ) ) / ( abs ‘ 𝑈 ) ) = ( ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( abs ‘ 𝑉 ) ) / ( abs ‘ 𝑈 ) ) )
31	18	sqcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) ↑ 2 ) ∈ ℂ )
32	31 17 21	divcan4d	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( abs ‘ 𝑈 ) ) / ( abs ‘ 𝑈 ) ) = ( ( abs ‘ 𝑉 ) ↑ 2 ) )
33	25 30 32	3eqtr2rd	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) ↑ 2 ) = ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) )
34	33	oveq2d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( abs ‘ 𝑉 ) ↑ 2 ) ) = ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) / ( ( abs ‘ 𝑈 ) / ( abs ‘ 𝑉 ) ) ) ) )
35	16 31	mulcomd	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( abs ‘ 𝑉 ) ↑ 2 ) ) = ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( ℜ ‘ ( 𝑈 / 𝑉 ) ) ) )
36	11	resqcld	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) ↑ 2 ) ∈ ℝ )
37	36 14	remul2d	⊢ ( 𝜑 → ( ℜ ‘ ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 𝑈 / 𝑉 ) ) ) = ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( ℜ ‘ ( 𝑈 / 𝑉 ) ) ) )
38	35 37	eqtr4d	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( abs ‘ 𝑉 ) ↑ 2 ) ) = ( ℜ ‘ ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 𝑈 / 𝑉 ) ) ) )
39	1 31 2 4	div12d	⊢ ( 𝜑 → ( 𝑈 · ( ( ( abs ‘ 𝑉 ) ↑ 2 ) / 𝑉 ) ) = ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 𝑈 / 𝑉 ) ) )
40	31 2 4	divrecd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) / 𝑉 ) = ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 1 / 𝑉 ) ) )
41		recval	⊢ ( ( 𝑉 ∈ ℂ ∧ 𝑉 ≠ 0 ) → ( 1 / 𝑉 ) = ( ( ∗ ‘ 𝑉 ) / ( ( abs ‘ 𝑉 ) ↑ 2 ) ) )
42	2 4 41	syl2anc	⊢ ( 𝜑 → ( 1 / 𝑉 ) = ( ( ∗ ‘ 𝑉 ) / ( ( abs ‘ 𝑉 ) ↑ 2 ) ) )
43	42	oveq2d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 1 / 𝑉 ) ) = ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( ( ∗ ‘ 𝑉 ) / ( ( abs ‘ 𝑉 ) ↑ 2 ) ) ) )
44	2	cjcld	⊢ ( 𝜑 → ( ∗ ‘ 𝑉 ) ∈ ℂ )
45		sqne0	⊢ ( ( abs ‘ 𝑉 ) ∈ ℂ → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) ≠ 0 ↔ ( abs ‘ 𝑉 ) ≠ 0 ) )
46	18 45	syl	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) ≠ 0 ↔ ( abs ‘ 𝑉 ) ≠ 0 ) )
47	19 46	mpbird	⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) ↑ 2 ) ≠ 0 )
48	44 31 47	divcan2d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( ( ∗ ‘ 𝑉 ) / ( ( abs ‘ 𝑉 ) ↑ 2 ) ) ) = ( ∗ ‘ 𝑉 ) )
49	43 48	eqtrd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 1 / 𝑉 ) ) = ( ∗ ‘ 𝑉 ) )
50	40 49	eqtrd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) / 𝑉 ) = ( ∗ ‘ 𝑉 ) )
51	50	oveq2d	⊢ ( 𝜑 → ( 𝑈 · ( ( ( abs ‘ 𝑉 ) ↑ 2 ) / 𝑉 ) ) = ( 𝑈 · ( ∗ ‘ 𝑉 ) ) )
52	39 51	eqtr3d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 𝑈 / 𝑉 ) ) = ( 𝑈 · ( ∗ ‘ 𝑉 ) ) )
53	52	fveq2d	⊢ ( 𝜑 → ( ℜ ‘ ( ( ( abs ‘ 𝑉 ) ↑ 2 ) · ( 𝑈 / 𝑉 ) ) ) = ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) )
54	38 53	eqtrd	⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) · ( ( abs ‘ 𝑉 ) ↑ 2 ) ) = ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) )
55	24 34 54	3eqtr2rd	⊢ ( 𝜑 → ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) = ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) )
56	55	oveq2d	⊢ ( 𝜑 → ( 2 · ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) ) = ( 2 · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) ) )
57	56	oveq2d	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝑈 ) ↑ 2 ) + ( ( abs ‘ 𝑉 ) ↑ 2 ) ) − ( 2 · ( ℜ ‘ ( 𝑈 · ( ∗ ‘ 𝑉 ) ) ) ) ) = ( ( ( ( abs ‘ 𝑈 ) ↑ 2 ) + ( ( abs ‘ 𝑉 ) ↑ 2 ) ) − ( 2 · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) ) ) )
58	6 57	eqtrd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑈 − 𝑉 ) ) ↑ 2 ) = ( ( ( ( abs ‘ 𝑈 ) ↑ 2 ) + ( ( abs ‘ 𝑉 ) ↑ 2 ) ) − ( 2 · ( ( ( abs ‘ 𝑈 ) · ( abs ‘ 𝑉 ) ) · ( ( ℜ ‘ ( 𝑈 / 𝑉 ) ) / ( abs ‘ ( 𝑈 / 𝑉 ) ) ) ) ) ) )