Proof of Theorem mul4sqlem
Step | Hyp | Ref
| Expression |
1 | | mul4sq.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ[i]) |
2 | | gzcn 16485 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈
ℂ) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | | mul4sq.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℤ[i]) |
5 | | gzcn 16485 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℤ[i] → 𝐶 ∈
ℂ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
7 | 3, 6 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) |
8 | 7 | absvalsqd 15006 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶)))) |
9 | 7 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ) |
10 | 7, 9 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ) |
11 | 8, 10 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ) |
12 | | mul4sq.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ[i]) |
13 | | gzcn 16485 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℤ[i] → 𝐵 ∈
ℂ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
15 | | mul4sq.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℤ[i]) |
16 | | gzcn 16485 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℤ[i] → 𝐷 ∈
ℂ) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
18 | 14, 17 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ) |
19 | 18 | absvalsqd 15006 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷)))) |
20 | 18 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ) |
21 | 18, 20 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ) |
22 | 19, 21 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ) |
23 | 11, 22 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ) |
24 | 3 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘𝐴) ∈
ℂ) |
25 | 24, 6 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ) |
26 | 14 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘𝐵) ∈
ℂ) |
27 | 26, 17 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ) |
28 | 25, 27 | mulcld 10853 |
. . . . . . 7
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ) |
29 | 6 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘𝐶) ∈
ℂ) |
30 | 14, 29 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ) |
31 | 17 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘𝐷) ∈
ℂ) |
32 | 3, 31 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ) |
33 | 30, 32 | mulcld 10853 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ) |
34 | 28, 33 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ) |
35 | 3, 17 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ) |
36 | 35 | absvalsqd 15006 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷)))) |
37 | 35 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ) |
38 | 35, 37 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ) |
39 | 36, 38 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ) |
40 | 14, 6 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ) |
41 | 40 | absvalsqd 15006 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶)))) |
42 | 40 | cjcld 14759 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ) |
43 | 40, 42 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ) |
44 | 41, 43 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ) |
45 | 39, 44 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ) |
46 | 23, 34, 45 | ppncand 11229 |
. . . . 5
⊢ (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)))) |
47 | 14, 31 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ) |
48 | 25, 47 | addcld 10852 |
. . . . . . . 8
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ) |
49 | 48 | absvalsqd 15006 |
. . . . . . 7
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ·
(∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))) |
50 | 25, 47 | cjaddd 14783 |
. . . . . . . . 9
⊢ (𝜑 →
(∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) =
((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷))))) |
51 | 24, 6 | cjmuld 14784 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) ·
(∗‘𝐶))) |
52 | 3 | cjcjd 14762 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(∗‘(∗‘𝐴)) = 𝐴) |
53 | 52 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝜑 →
((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶))) |
54 | 51, 53 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 →
(∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶))) |
55 | 14, 31 | cjmuld 14784 |
. . . . . . . . . . 11
⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) ·
(∗‘(∗‘𝐷)))) |
56 | 17 | cjcjd 14762 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(∗‘(∗‘𝐷)) = 𝐷) |
57 | 56 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝐵) ·
(∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷)) |
58 | 55, 57 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷)) |
59 | 54, 58 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 →
((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) |
60 | 50, 59 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 →
(∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) |
61 | 60 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ·
(∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) |
62 | 3, 29 | mulcld 10853 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ) |
63 | 25, 62, 27 | adddid 10857 |
. . . . . . . . . 10
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))) |
64 | 6, 24, 3, 29 | mul4d 11044 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶)))) |
65 | 24, 6 | mulcomd 10854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴))) |
66 | 65 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶)))) |
67 | 3, 6 | mulcomd 10854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴)) |
68 | 3, 6 | cjmuld 14784 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶))) |
69 | 67, 68 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶)))) |
70 | 64, 66, 69 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶)))) |
71 | 70, 8 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2)) |
72 | 71 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))) |
73 | 63, 72 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))) |
74 | 47, 62, 27 | adddid 10857 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)))) |
75 | 3, 29 | mulcomd 10854 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴)) |
76 | 75 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴))) |
77 | 14, 31, 29, 3 | mul4d 11044 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴))) |
78 | 31, 3 | mulcomd 10854 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷))) |
79 | 78 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) |
80 | 76, 77, 79 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) |
81 | 14, 31, 17, 26 | mul4d 11044 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵)))) |
82 | 26, 17 | mulcomd 10854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵))) |
83 | 82 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵)))) |
84 | 14, 17 | cjmuld 14784 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷))) |
85 | 26, 31 | mulcomd 10854 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵))) |
86 | 84, 85 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵))) |
87 | 86 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵)))) |
88 | 81, 83, 87 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷)))) |
89 | 88, 19 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2)) |
90 | 80, 89 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))) |
91 | 74, 90 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))) |
92 | 73, 91 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))) |
93 | 62, 27 | addcld 10852 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ) |
94 | 25, 47, 93 | adddird 10858 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))) |
95 | 11, 22, 28, 33 | add42d 11061 |
. . . . . . . 8
⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))) |
96 | 92, 94, 95 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) |
97 | 49, 61, 96 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) |
98 | 24, 17 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ) |
99 | 98, 30 | subcld 11189 |
. . . . . . . 8
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ) |
100 | 99 | absvalsqd 15006 |
. . . . . . 7
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ·
(∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))))) |
101 | | cjsub 14712 |
. . . . . . . . . 10
⊢
((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) →
(∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) =
((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶))))) |
102 | 98, 30, 101 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 →
(∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) =
((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶))))) |
103 | 24, 17 | cjmuld 14784 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) ·
(∗‘𝐷))) |
104 | 52 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝜑 →
((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷))) |
105 | 103, 104 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 →
(∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷))) |
106 | 14, 29 | cjmuld 14784 |
. . . . . . . . . . 11
⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) ·
(∗‘(∗‘𝐶)))) |
107 | 6 | cjcjd 14762 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(∗‘(∗‘𝐶)) = 𝐶) |
108 | 107 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝐵) ·
(∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶)) |
109 | 106, 108 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶)) |
110 | 105, 109 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 →
((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) |
111 | 102, 110 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 →
(∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) |
112 | 111 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ·
(∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) |
113 | 26, 6 | mulcld 10853 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ) |
114 | 32, 113 | subcld 11189 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ) |
115 | 98, 30, 114 | subdird 11289 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))) |
116 | 98, 32, 113 | subdid 11288 |
. . . . . . . . . 10
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)))) |
117 | 17, 24, 3, 31 | mul4d 11044 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷)))) |
118 | 24, 17 | mulcomd 10854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴))) |
119 | 118 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷)))) |
120 | 3, 17 | mulcomd 10854 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴)) |
121 | 3, 17 | cjmuld 14784 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷))) |
122 | 120, 121 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷)))) |
123 | 117, 119,
122 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷)))) |
124 | 123, 36 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2)) |
125 | 26, 6 | mulcomd 10854 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵))) |
126 | 125 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵)))) |
127 | 24, 17, 6, 26 | mul4d 11044 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵)))) |
128 | 17, 26 | mulcomd 10854 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷)) |
129 | 128 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) |
130 | 126, 127,
129 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) |
131 | 124, 130 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))) |
132 | 116, 131 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))) |
133 | 30, 32, 113 | subdid 11288 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)))) |
134 | 125 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵)))) |
135 | 14, 29, 6, 26 | mul4d 11044 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵)))) |
136 | 29, 26 | mulcomd 10854 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶))) |
137 | 14, 6 | cjmuld 14784 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶))) |
138 | 136, 137 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶))) |
139 | 138 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶)))) |
140 | 134, 135,
139 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶)))) |
141 | 140, 41 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2)) |
142 | 141 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) |
143 | 133, 142 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) |
144 | 132, 143 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))) |
145 | 39, 28, 33, 44 | subadd4d 11237 |
. . . . . . . 8
⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) |
146 | 115, 144,
145 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) |
147 | 100, 112,
146 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) |
148 | 97, 147 | oveq12d 7231 |
. . . . 5
⊢ (𝜑 →
(((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) +
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))) |
149 | 3, 24 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ) |
150 | 14, 26 | mulcld 10853 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ) |
151 | 6, 29 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ) |
152 | 17, 31 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ) |
153 | 151, 152 | addcld 10852 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ) |
154 | 149, 150,
153 | adddird 10858 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))) |
155 | 68 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶)))) |
156 | 3, 6, 24, 29 | mul4d 11044 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶)))) |
157 | 8, 155, 156 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶)))) |
158 | 121 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷)))) |
159 | 3, 17, 24, 31 | mul4d 11044 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))) |
160 | 36, 158, 159 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))) |
161 | 157, 160 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))) |
162 | 149, 151,
152 | adddid 10857 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))) |
163 | 161, 162 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))) |
164 | 137 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶)))) |
165 | 14, 6, 26, 29 | mul4d 11044 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶)))) |
166 | 41, 164, 165 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶)))) |
167 | 84 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷)))) |
168 | 14, 17, 26, 31 | mul4d 11044 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))) |
169 | 19, 167, 168 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))) |
170 | 166, 169 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))) |
171 | 150, 151,
152 | adddid 10857 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))) |
172 | 170, 171 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))) |
173 | 163, 172 | oveq12d 7231 |
. . . . . . 7
⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))) |
174 | 154, 173 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)))) |
175 | | mul4sq.5 |
. . . . . . . 8
⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) |
176 | 3 | absvalsqd 15006 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))) |
177 | 14 | absvalsqd 15006 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵))) |
178 | 176, 177 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵)))) |
179 | 175, 178 | syl5eq 2790 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵)))) |
180 | | mul4sq.6 |
. . . . . . . 8
⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) |
181 | 6 | absvalsqd 15006 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶))) |
182 | 17 | absvalsqd 15006 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷))) |
183 | 181, 182 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) |
184 | 180, 183 | syl5eq 2790 |
. . . . . . 7
⊢ (𝜑 → 𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) |
185 | 179, 184 | oveq12d 7231 |
. . . . . 6
⊢ (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))) |
186 | 11, 22, 39, 44 | add42d 11061 |
. . . . . 6
⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)))) |
187 | 174, 185,
186 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)))) |
188 | 46, 148, 187 | 3eqtr4d 2787 |
. . . 4
⊢ (𝜑 →
(((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) +
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌)) |
189 | 188 | oveq1d 7228 |
. . 3
⊢ (𝜑 →
((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) +
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2))) |
190 | | mul4sq.7 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
191 | 190 | nncnd 11846 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
192 | 190 | nnne0d 11880 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≠ 0) |
193 | 48, 191, 192 | absdivd 15019 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀))) |
194 | 190 | nnred 11845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
195 | 190 | nnnn0d 12150 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
196 | 195 | nn0ge0d 12153 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑀) |
197 | 194, 196 | absidd 14986 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝑀) = 𝑀) |
198 | 197 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)) |
199 | 193, 198 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)) |
200 | 199 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 →
((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) =
(((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2)) |
201 | 48 | abscld 15000 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ) |
202 | 201 | recnd 10861 |
. . . . . . 7
⊢ (𝜑 →
(abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ) |
203 | 202, 191,
192 | sqdivd 13729 |
. . . . . 6
⊢ (𝜑 →
(((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) =
(((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2))) |
204 | 200, 203 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 →
((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) =
(((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2))) |
205 | 99, 191, 192 | absdivd 15019 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀))) |
206 | 197 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)) |
207 | 205, 206 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)) |
208 | 207 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 →
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) =
(((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2)) |
209 | 99 | abscld 15000 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ) |
210 | 209 | recnd 10861 |
. . . . . . 7
⊢ (𝜑 →
(abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ) |
211 | 210, 191,
192 | sqdivd 13729 |
. . . . . 6
⊢ (𝜑 →
(((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) =
(((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))) |
212 | 208, 211 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 →
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) =
(((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))) |
213 | 204, 212 | oveq12d 7231 |
. . . 4
⊢ (𝜑 →
(((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) +
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) =
((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) +
(((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))) |
214 | 23, 34 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ) |
215 | 97, 214 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈
ℂ) |
216 | 45, 34 | subcld 11189 |
. . . . . 6
⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ) |
217 | 147, 216 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 →
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈
ℂ) |
218 | 190 | nnsqcld 13811 |
. . . . . 6
⊢ (𝜑 → (𝑀↑2) ∈ ℕ) |
219 | 218 | nncnd 11846 |
. . . . 5
⊢ (𝜑 → (𝑀↑2) ∈ ℂ) |
220 | 218 | nnne0d 11880 |
. . . . 5
⊢ (𝜑 → (𝑀↑2) ≠ 0) |
221 | 215, 217,
219, 220 | divdird 11646 |
. . . 4
⊢ (𝜑 →
((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) +
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) =
((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) +
(((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))) |
222 | 213, 221 | eqtr4d 2780 |
. . 3
⊢ (𝜑 →
(((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) +
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) =
((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) +
((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2))) |
223 | 176, 149 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → ((abs‘𝐴)↑2) ∈
ℂ) |
224 | 177, 150 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → ((abs‘𝐵)↑2) ∈
ℂ) |
225 | 223, 224 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈
ℂ) |
226 | 175, 225 | eqeltrid 2842 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
227 | 184, 153 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ℂ) |
228 | 226, 191,
227, 191, 192, 192 | divmuldivd 11649 |
. . . 4
⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀))) |
229 | 191 | sqvald 13713 |
. . . . 5
⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀)) |
230 | 229 | oveq2d 7229 |
. . . 4
⊢ (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀))) |
231 | 228, 230 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2))) |
232 | 189, 222,
231 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 →
(((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) +
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀))) |
233 | 226, 48 | nncand 11194 |
. . . . . . 7
⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) |
234 | 149, 150,
25, 47 | addsub4d 11236 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))) |
235 | 179 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) |
236 | 24, 3, 6 | subdid 11288 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶))) |
237 | 24, 3 | mulcomd 10854 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴))) |
238 | 237 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶))) |
239 | 236, 238 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶))) |
240 | | cjsub 14712 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) →
(∗‘(𝐵 −
𝐷)) =
((∗‘𝐵) −
(∗‘𝐷))) |
241 | 14, 17, 240 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷))) |
242 | 241 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷)))) |
243 | 14, 26, 31 | subdid 11288 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))) |
244 | 242, 243 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))) |
245 | 239, 244 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))) |
246 | 234, 235,
245 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) |
247 | 246 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))) |
248 | 233, 247 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))) |
249 | 248 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀)) |
250 | 3, 6 | subcld 11189 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ) |
251 | 24, 250 | mulcld 10853 |
. . . . . . 7
⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) ∈ ℂ) |
252 | 14, 17 | subcld 11189 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℂ) |
253 | 252 | cjcld 14759 |
. . . . . . . 8
⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) ∈ ℂ) |
254 | 14, 253 | mulcld 10853 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) ∈ ℂ) |
255 | 251, 254 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) ∈ ℂ) |
256 | 226, 255,
191, 192 | divsubdird 11647 |
. . . . 5
⊢ (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀))) |
257 | 251, 254,
191, 192 | divdird 11646 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀))) |
258 | 24, 250, 191, 192 | divassd 11643 |
. . . . . . . 8
⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀))) |
259 | 14, 253, 191, 192 | divassd 11643 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀))) |
260 | 252, 191,
192 | cjdivd 14786 |
. . . . . . . . . . 11
⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀))) |
261 | 194 | cjred 14789 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘𝑀) = 𝑀) |
262 | 261 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀)) |
263 | 260, 262 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀)) |
264 | 263 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀))) |
265 | 259, 264 | eqtr4d 2780 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) |
266 | 258, 265 | oveq12d 7231 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) |
267 | 257, 266 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) |
268 | 267 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))) |
269 | 249, 256,
268 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))) |
270 | | mul4sq.10 |
. . . . . . 7
⊢ (𝜑 → (𝑋 / 𝑀) ∈
ℕ0) |
271 | 270 | nn0zd 12280 |
. . . . . 6
⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ) |
272 | | zgz 16486 |
. . . . . 6
⊢ ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i]) |
273 | 271, 272 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i]) |
274 | | gzcjcl 16489 |
. . . . . . . 8
⊢ (𝐴 ∈ ℤ[i] →
(∗‘𝐴) ∈
ℤ[i]) |
275 | 1, 274 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∗‘𝐴) ∈
ℤ[i]) |
276 | | mul4sq.8 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) |
277 | | gzmulcl 16491 |
. . . . . . 7
⊢
(((∗‘𝐴)
∈ ℤ[i] ∧ ((𝐴
− 𝐶) / 𝑀) ∈ ℤ[i]) →
((∗‘𝐴)
· ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) |
278 | 275, 276,
277 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) |
279 | | mul4sq.9 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) |
280 | | gzcjcl 16489 |
. . . . . . . 8
⊢ (((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i] →
(∗‘((𝐵 −
𝐷) / 𝑀)) ∈ ℤ[i]) |
281 | 279, 280 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) |
282 | | gzmulcl 16491 |
. . . . . . 7
⊢ ((𝐵 ∈ ℤ[i] ∧
(∗‘((𝐵 −
𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 ·
(∗‘((𝐵 −
𝐷) / 𝑀))) ∈ ℤ[i]) |
283 | 12, 281, 282 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) |
284 | | gzaddcl 16490 |
. . . . . 6
⊢
((((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 ·
(∗‘((𝐵 −
𝐷) / 𝑀))) ∈ ℤ[i]) →
(((∗‘𝐴)
· ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) |
285 | 278, 283,
284 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) |
286 | | gzsubcl 16493 |
. . . . 5
⊢ (((𝑋 / 𝑀) ∈ ℤ[i] ∧
(((∗‘𝐴)
· ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i]) |
287 | 273, 285,
286 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i]) |
288 | 269, 287 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i]) |
289 | 250 | cjcld 14759 |
. . . . . . . 8
⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) ∈ ℂ) |
290 | 14, 289 | mulcld 10853 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) ∈ ℂ) |
291 | 24, 252 | mulcld 10853 |
. . . . . . 7
⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) ∈ ℂ) |
292 | 290, 291,
191, 192 | divsubdird 11647 |
. . . . . 6
⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀))) |
293 | | cjsub 14712 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
(∗‘(𝐴 −
𝐶)) =
((∗‘𝐴) −
(∗‘𝐶))) |
294 | 3, 6, 293 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶))) |
295 | 294 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶)))) |
296 | 14, 24, 29 | subdid 11288 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶)))) |
297 | 295, 296 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶)))) |
298 | 24, 14, 17 | subdid 11288 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷))) |
299 | 24, 14 | mulcomd 10854 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴))) |
300 | 299 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) |
301 | 298, 300 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) |
302 | 297, 301 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))) |
303 | 14, 24 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ) |
304 | 303, 30, 98 | nnncan1d 11223 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) |
305 | 302, 304 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) |
306 | 305 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) |
307 | 292, 306 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) |
308 | 14, 289, 191, 192 | divassd 11643 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀))) |
309 | 250, 191,
192 | cjdivd 14786 |
. . . . . . . . 9
⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀))) |
310 | 261 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀)) |
311 | 309, 310 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀)) |
312 | 311 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀))) |
313 | 308, 312 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀)))) |
314 | 24, 252, 191, 192 | divassd 11643 |
. . . . . 6
⊢ (𝜑 → (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) |
315 | 313, 314 | oveq12d 7231 |
. . . . 5
⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))) |
316 | 307, 315 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))) |
317 | | gzcjcl 16489 |
. . . . . . 7
⊢ (((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i] →
(∗‘((𝐴 −
𝐶) / 𝑀)) ∈ ℤ[i]) |
318 | 276, 317 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) |
319 | | gzmulcl 16491 |
. . . . . 6
⊢ ((𝐵 ∈ ℤ[i] ∧
(∗‘((𝐴 −
𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 ·
(∗‘((𝐴 −
𝐶) / 𝑀))) ∈ ℤ[i]) |
320 | 12, 318, 319 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i]) |
321 | | gzmulcl 16491 |
. . . . . 6
⊢
(((∗‘𝐴)
∈ ℤ[i] ∧ ((𝐵
− 𝐷) / 𝑀) ∈ ℤ[i]) →
((∗‘𝐴)
· ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) |
322 | 275, 279,
321 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) |
323 | | gzsubcl 16493 |
. . . . 5
⊢ (((𝐵 ·
(∗‘((𝐴 −
𝐶) / 𝑀))) ∈ ℤ[i] ∧
((∗‘𝐴)
· ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 ·
(∗‘((𝐴 −
𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) |
324 | 320, 322,
323 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) |
325 | 316, 324 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) |
326 | | 4sq.1 |
. . . 4
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
327 | 326 | 4sqlem4a 16504 |
. . 3
⊢
((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧
((((∗‘𝐴)
· 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) →
(((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) +
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆) |
328 | 288, 325,
327 | syl2anc 587 |
. 2
⊢ (𝜑 →
(((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) +
((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆) |
329 | 232, 328 | eqeltrrd 2839 |
1
⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆) |