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 ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
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 ‘ ( 𝑈 / 𝑉 ) ) ) ) ) ) )