Proof of Theorem lawcoslem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lawcoslem1.1 | . . 3
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 2 |  | lawcoslem1.2 | . . 3
⊢ (𝜑 → 𝑉 ∈ ℂ) | 
| 3 |  | sqabssub 15323 | . . 3
⊢ ((𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ) →
((abs‘(𝑈 −
𝑉))↑2) =
((((abs‘𝑈)↑2) +
((abs‘𝑉)↑2))
− (2 · (ℜ‘(𝑈 · (∗‘𝑉)))))) | 
| 4 | 1, 2, 3 | syl2anc 584 | . 2
⊢ (𝜑 → ((abs‘(𝑈 − 𝑉))↑2) = ((((abs‘𝑈)↑2) + ((abs‘𝑉)↑2)) − (2 ·
(ℜ‘(𝑈 ·
(∗‘𝑉)))))) | 
| 5 |  | lawcoslem1.4 | . . . . . . . . 9
⊢ (𝜑 → 𝑉 ≠ 0) | 
| 6 | 1, 2, 5 | absdivd 15495 | . . . . . . . 8
⊢ (𝜑 → (abs‘(𝑈 / 𝑉)) = ((abs‘𝑈) / (abs‘𝑉))) | 
| 7 | 6 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉))) = ((ℜ‘(𝑈 / 𝑉)) / ((abs‘𝑈) / (abs‘𝑉)))) | 
| 8 | 7 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (((abs‘𝑈) · (abs‘𝑉)) ·
((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉)))) = (((abs‘𝑈) · (abs‘𝑉)) · ((ℜ‘(𝑈 / 𝑉)) / ((abs‘𝑈) / (abs‘𝑉))))) | 
| 9 | 1 | abscld 15476 | . . . . . . . . 9
⊢ (𝜑 → (abs‘𝑈) ∈
ℝ) | 
| 10 | 2 | abscld 15476 | . . . . . . . . 9
⊢ (𝜑 → (abs‘𝑉) ∈
ℝ) | 
| 11 | 9, 10 | remulcld 11292 | . . . . . . . 8
⊢ (𝜑 → ((abs‘𝑈) · (abs‘𝑉)) ∈
ℝ) | 
| 12 | 11 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → ((abs‘𝑈) · (abs‘𝑉)) ∈
ℂ) | 
| 13 | 1, 2, 5 | divcld 12044 | . . . . . . . . 9
⊢ (𝜑 → (𝑈 / 𝑉) ∈ ℂ) | 
| 14 | 13 | recld 15234 | . . . . . . . 8
⊢ (𝜑 → (ℜ‘(𝑈 / 𝑉)) ∈ ℝ) | 
| 15 | 14 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (ℜ‘(𝑈 / 𝑉)) ∈ ℂ) | 
| 16 | 9 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝑈) ∈
ℂ) | 
| 17 | 10 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝑉) ∈
ℂ) | 
| 18 | 2, 5 | absne0d 15487 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝑉) ≠ 0) | 
| 19 | 16, 17, 18 | divcld 12044 | . . . . . . 7
⊢ (𝜑 → ((abs‘𝑈) / (abs‘𝑉)) ∈ ℂ) | 
| 20 |  | lawcoslem1.3 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ≠ 0) | 
| 21 | 1, 20 | absne0d 15487 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝑈) ≠ 0) | 
| 22 | 16, 17, 21, 18 | divne0d 12060 | . . . . . . 7
⊢ (𝜑 → ((abs‘𝑈) / (abs‘𝑉)) ≠ 0) | 
| 23 | 12, 15, 19, 22 | div12d 12080 | . . . . . 6
⊢ (𝜑 → (((abs‘𝑈) · (abs‘𝑉)) ·
((ℜ‘(𝑈 / 𝑉)) / ((abs‘𝑈) / (abs‘𝑉)))) = ((ℜ‘(𝑈 / 𝑉)) · (((abs‘𝑈) · (abs‘𝑉)) / ((abs‘𝑈) / (abs‘𝑉))))) | 
| 24 | 8, 23 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (((abs‘𝑈) · (abs‘𝑉)) ·
((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉)))) = ((ℜ‘(𝑈 / 𝑉)) · (((abs‘𝑈) · (abs‘𝑉)) / ((abs‘𝑈) / (abs‘𝑉))))) | 
| 25 | 12, 16, 17, 21, 18 | divdiv2d 12076 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝑈) · (abs‘𝑉)) / ((abs‘𝑈) / (abs‘𝑉))) = ((((abs‘𝑈) · (abs‘𝑉)) · (abs‘𝑉)) / (abs‘𝑈))) | 
| 26 | 17 | sqvald 14184 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝑉)↑2) = ((abs‘𝑉) · (abs‘𝑉))) | 
| 27 | 26 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝑉)↑2) ·
(abs‘𝑈)) =
(((abs‘𝑉) ·
(abs‘𝑉)) ·
(abs‘𝑈))) | 
| 28 | 16, 17, 17 | mul31d 11473 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝑈) · (abs‘𝑉)) · (abs‘𝑉)) = (((abs‘𝑉) · (abs‘𝑉)) · (abs‘𝑈))) | 
| 29 | 27, 28 | eqtr4d 2779 | . . . . . . . 8
⊢ (𝜑 → (((abs‘𝑉)↑2) ·
(abs‘𝑈)) =
(((abs‘𝑈) ·
(abs‘𝑉)) ·
(abs‘𝑉))) | 
| 30 | 29 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝑉)↑2) ·
(abs‘𝑈)) /
(abs‘𝑈)) =
((((abs‘𝑈) ·
(abs‘𝑉)) ·
(abs‘𝑉)) /
(abs‘𝑈))) | 
| 31 | 17 | sqcld 14185 | . . . . . . . 8
⊢ (𝜑 → ((abs‘𝑉)↑2) ∈
ℂ) | 
| 32 | 31, 16, 21 | divcan4d 12050 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝑉)↑2) ·
(abs‘𝑈)) /
(abs‘𝑈)) =
((abs‘𝑉)↑2)) | 
| 33 | 25, 30, 32 | 3eqtr2rd 2783 | . . . . . 6
⊢ (𝜑 → ((abs‘𝑉)↑2) = (((abs‘𝑈) · (abs‘𝑉)) / ((abs‘𝑈) / (abs‘𝑉)))) | 
| 34 | 33 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → ((ℜ‘(𝑈 / 𝑉)) · ((abs‘𝑉)↑2)) = ((ℜ‘(𝑈 / 𝑉)) · (((abs‘𝑈) · (abs‘𝑉)) / ((abs‘𝑈) / (abs‘𝑉))))) | 
| 35 | 15, 31 | mulcomd 11283 | . . . . . . 7
⊢ (𝜑 → ((ℜ‘(𝑈 / 𝑉)) · ((abs‘𝑉)↑2)) = (((abs‘𝑉)↑2) · (ℜ‘(𝑈 / 𝑉)))) | 
| 36 | 10 | resqcld 14166 | . . . . . . . 8
⊢ (𝜑 → ((abs‘𝑉)↑2) ∈
ℝ) | 
| 37 | 36, 13 | remul2d 15267 | . . . . . . 7
⊢ (𝜑 →
(ℜ‘(((abs‘𝑉)↑2) · (𝑈 / 𝑉))) = (((abs‘𝑉)↑2) · (ℜ‘(𝑈 / 𝑉)))) | 
| 38 | 35, 37 | eqtr4d 2779 | . . . . . 6
⊢ (𝜑 → ((ℜ‘(𝑈 / 𝑉)) · ((abs‘𝑉)↑2)) =
(ℜ‘(((abs‘𝑉)↑2) · (𝑈 / 𝑉)))) | 
| 39 | 1, 31, 2, 5 | div12d 12080 | . . . . . . . 8
⊢ (𝜑 → (𝑈 · (((abs‘𝑉)↑2) / 𝑉)) = (((abs‘𝑉)↑2) · (𝑈 / 𝑉))) | 
| 40 | 31, 2, 5 | divrecd 12047 | . . . . . . . . . 10
⊢ (𝜑 → (((abs‘𝑉)↑2) / 𝑉) = (((abs‘𝑉)↑2) · (1 / 𝑉))) | 
| 41 |  | recval 15362 | . . . . . . . . . . . . 13
⊢ ((𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) → (1 / 𝑉) = ((∗‘𝑉) / ((abs‘𝑉)↑2))) | 
| 42 | 2, 5, 41 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (1 / 𝑉) = ((∗‘𝑉) / ((abs‘𝑉)↑2))) | 
| 43 | 42 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝑉)↑2) · (1 / 𝑉)) = (((abs‘𝑉)↑2) ·
((∗‘𝑉) /
((abs‘𝑉)↑2)))) | 
| 44 | 2 | cjcld 15236 | . . . . . . . . . . . 12
⊢ (𝜑 → (∗‘𝑉) ∈
ℂ) | 
| 45 |  | sqne0 14164 | . . . . . . . . . . . . . 14
⊢
((abs‘𝑉)
∈ ℂ → (((abs‘𝑉)↑2) ≠ 0 ↔ (abs‘𝑉) ≠ 0)) | 
| 46 | 17, 45 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘𝑉)↑2) ≠ 0 ↔
(abs‘𝑉) ≠
0)) | 
| 47 | 18, 46 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝑉)↑2) ≠
0) | 
| 48 | 44, 31, 47 | divcan2d 12046 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝑉)↑2) ·
((∗‘𝑉) /
((abs‘𝑉)↑2))) =
(∗‘𝑉)) | 
| 49 | 43, 48 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (((abs‘𝑉)↑2) · (1 / 𝑉)) = (∗‘𝑉)) | 
| 50 | 40, 49 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝑉)↑2) / 𝑉) = (∗‘𝑉)) | 
| 51 | 50 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (𝑈 · (((abs‘𝑉)↑2) / 𝑉)) = (𝑈 · (∗‘𝑉))) | 
| 52 | 39, 51 | eqtr3d 2778 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝑉)↑2) · (𝑈 / 𝑉)) = (𝑈 · (∗‘𝑉))) | 
| 53 | 52 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 →
(ℜ‘(((abs‘𝑉)↑2) · (𝑈 / 𝑉))) = (ℜ‘(𝑈 · (∗‘𝑉)))) | 
| 54 | 38, 53 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → ((ℜ‘(𝑈 / 𝑉)) · ((abs‘𝑉)↑2)) = (ℜ‘(𝑈 · (∗‘𝑉)))) | 
| 55 | 24, 34, 54 | 3eqtr2rd 2783 | . . . 4
⊢ (𝜑 → (ℜ‘(𝑈 · (∗‘𝑉))) = (((abs‘𝑈) · (abs‘𝑉)) ·
((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉))))) | 
| 56 | 55 | oveq2d 7448 | . . 3
⊢ (𝜑 → (2 ·
(ℜ‘(𝑈 ·
(∗‘𝑉)))) = (2
· (((abs‘𝑈)
· (abs‘𝑉))
· ((ℜ‘(𝑈
/ 𝑉)) / (abs‘(𝑈 / 𝑉)))))) | 
| 57 | 56 | oveq2d 7448 | . 2
⊢ (𝜑 → ((((abs‘𝑈)↑2) + ((abs‘𝑉)↑2)) − (2 ·
(ℜ‘(𝑈 ·
(∗‘𝑉))))) =
((((abs‘𝑈)↑2) +
((abs‘𝑉)↑2))
− (2 · (((abs‘𝑈) · (abs‘𝑉)) · ((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉))))))) | 
| 58 | 4, 57 | eqtrd 2776 | 1
⊢ (𝜑 → ((abs‘(𝑈 − 𝑉))↑2) = ((((abs‘𝑈)↑2) + ((abs‘𝑉)↑2)) − (2 ·
(((abs‘𝑈) ·
(abs‘𝑉)) ·
((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉))))))) |