MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul4sqlem Structured version   Visualization version   GIF version

Theorem mul4sqlem 15851
Description: Lemma for mul4sq 15852: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 15859 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.)
Hypotheses
Ref Expression
4sq.1 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
mul4sq.1 (𝜑𝐴 ∈ ℤ[i])
mul4sq.2 (𝜑𝐵 ∈ ℤ[i])
mul4sq.3 (𝜑𝐶 ∈ ℤ[i])
mul4sq.4 (𝜑𝐷 ∈ ℤ[i])
mul4sq.5 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
mul4sq.6 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
mul4sq.7 (𝜑𝑀 ∈ ℕ)
mul4sq.8 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ[i])
mul4sq.9 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ[i])
mul4sq.10 (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
Assertion
Ref Expression
mul4sqlem (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Distinct variable groups:   𝑤,𝑛,𝑥,𝑦,𝑧   𝐵,𝑛   𝐴,𝑛   𝐶,𝑛   𝐷,𝑛   𝑛,𝑀   𝜑,𝑛   𝑆,𝑛
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐴(𝑥,𝑦,𝑧,𝑤)   𝐵(𝑥,𝑦,𝑧,𝑤)   𝐶(𝑥,𝑦,𝑧,𝑤)   𝐷(𝑥,𝑦,𝑧,𝑤)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝑀(𝑥,𝑦,𝑧,𝑤)   𝑋(𝑥,𝑦,𝑧,𝑤,𝑛)   𝑌(𝑥,𝑦,𝑧,𝑤,𝑛)

Proof of Theorem mul4sqlem
StepHypRef Expression
1 mul4sq.1 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℤ[i])
2 gzcn 15830 . . . . . . . . . . 11 (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
4 mul4sq.3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℤ[i])
5 gzcn 15830 . . . . . . . . . . 11 (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
73, 6mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
87absvalsqd 14372 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
97cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
107, 9mulcld 10244 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
118, 10eqeltrd 2831 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12 mul4sq.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℤ[i])
13 gzcn 15830 . . . . . . . . . . 11 (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
1412, 13syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
15 mul4sq.4 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℤ[i])
16 gzcn 15830 . . . . . . . . . . 11 (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
1814, 17mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
1918absvalsqd 14372 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
2018cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
2118, 20mulcld 10244 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
2219, 21eqeltrd 2831 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
2311, 22addcld 10243 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
243cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘𝐴) ∈ ℂ)
2524, 6mulcld 10244 . . . . . . . 8 (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
2614cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘𝐵) ∈ ℂ)
2726, 17mulcld 10244 . . . . . . . 8 (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
2825, 27mulcld 10244 . . . . . . 7 (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
296cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘𝐶) ∈ ℂ)
3014, 29mulcld 10244 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
3117cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘𝐷) ∈ ℂ)
323, 31mulcld 10244 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
3330, 32mulcld 10244 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
3428, 33addcld 10243 . . . . . 6 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
353, 17mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
3635absvalsqd 14372 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
3735cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
3835, 37mulcld 10244 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
3936, 38eqeltrd 2831 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
4014, 6mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
4140absvalsqd 14372 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
4240cjcld 14127 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
4340, 42mulcld 10244 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
4441, 43eqeltrd 2831 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
4539, 44addcld 10243 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
4623, 34, 45ppncand 10616 . . . . 5 (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
4714, 31mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
4825, 47addcld 10243 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
4948absvalsqd 14372 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
5025, 47cjaddd 14151 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
5124, 6cjmuld 14152 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
523cjcjd 14130 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
5352oveq1d 6820 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
5451, 53eqtrd 2786 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
5514, 31cjmuld 14152 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
5617cjcjd 14130 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
5756oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5855, 57eqtrd 2786 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5954, 58oveq12d 6823 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6050, 59eqtrd 2786 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6160oveq2d 6821 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
623, 29mulcld 10244 . . . . . . . . . . 11 (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
6325, 62, 27adddid 10248 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
646, 24, 3, 29mul4d 10432 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
6524, 6mulcomd 10245 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
6665oveq1d 6820 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
673, 6mulcomd 10245 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
683, 6cjmuld 14152 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
6967, 68oveq12d 6823 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
7064, 66, 693eqtr4d 2796 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
7170, 8eqtr4d 2789 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
7271oveq1d 6820 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7363, 72eqtrd 2786 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7447, 62, 27adddid 10248 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
753, 29mulcomd 10245 . . . . . . . . . . . . 13 (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
7675oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
7714, 31, 29, 3mul4d 10432 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
7831, 3mulcomd 10245 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
7978oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8076, 77, 793eqtrd 2790 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8114, 31, 17, 26mul4d 10432 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8226, 17mulcomd 10245 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
8382oveq2d 6821 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
8414, 17cjmuld 14152 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
8526, 31mulcomd 10245 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8684, 85eqtrd 2786 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8786oveq2d 6821 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8881, 83, 873eqtr4d 2796 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
8988, 19eqtr4d 2789 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
9080, 89oveq12d 6823 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9174, 90eqtrd 2786 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9273, 91oveq12d 6823 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9362, 27addcld 10243 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
9425, 47, 93adddird 10249 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
9511, 22, 28, 33add42d 10449 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9692, 94, 953eqtr4d 2796 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9749, 61, 963eqtrd 2790 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9824, 17mulcld 10244 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
9998, 30subcld 10576 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
10099absvalsqd 14372 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101 cjsub 14080 . . . . . . . . . 10 ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10298, 30, 101syl2anc 696 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10324, 17cjmuld 14152 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
10452oveq1d 6820 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105103, 104eqtrd 2786 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
10614, 29cjmuld 14152 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
1076cjcjd 14130 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108107oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109106, 108eqtrd 2786 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110105, 109oveq12d 6823 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111102, 110eqtrd 2786 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112111oveq2d 6821 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
11326, 6mulcld 10244 . . . . . . . . . 10 (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
11432, 113subcld 10576 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
11598, 30, 114subdird 10671 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
11698, 32, 113subdid 10670 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
11717, 24, 3, 31mul4d 10432 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
11824, 17mulcomd 10245 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119118oveq1d 6820 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
1203, 17mulcomd 10245 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
1213, 17cjmuld 14152 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122120, 121oveq12d 6823 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123117, 119, 1223eqtr4d 2796 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124123, 36eqtr4d 2789 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
12526, 6mulcomd 10245 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126125oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
12724, 17, 6, 26mul4d 10432 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
12817, 26mulcomd 10245 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129128oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130126, 127, 1293eqtrd 2790 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131124, 130oveq12d 6823 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132116, 131eqtrd 2786 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
13330, 32, 113subdid 10670 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134125oveq2d 6821 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
13514, 29, 6, 26mul4d 10432 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
13629, 26mulcomd 10245 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
13714, 6cjmuld 14152 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138136, 137eqtr4d 2789 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139138oveq2d 6821 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140134, 135, 1393eqtrd 2790 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141140, 41eqtr4d 2789 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142141oveq2d 6821 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143133, 142eqtrd 2786 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144132, 143oveq12d 6823 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
14539, 28, 33, 44subadd4d 10624 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146115, 144, 1453eqtrd 2790 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147100, 112, 1463eqtrd 2790 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
14897, 147oveq12d 6823 . . . . 5 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
1493, 24mulcld 10244 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
15014, 26mulcld 10244 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
1516, 29mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
15217, 31mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153151, 152addcld 10243 . . . . . . . 8 (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154149, 150, 153adddird 10249 . . . . . . 7 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
15568oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
1563, 6, 24, 29mul4d 10432 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
1578, 155, 1563eqtrd 2790 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158121oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
1593, 17, 24, 31mul4d 10432 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
16036, 158, 1593eqtrd 2790 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161157, 160oveq12d 6823 . . . . . . . . 9 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162149, 151, 152adddid 10248 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163161, 162eqtr4d 2789 . . . . . . . 8 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164137oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
16514, 6, 26, 29mul4d 10432 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16641, 164, 1653eqtrd 2790 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16784oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
16814, 17, 26, 31mul4d 10432 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
16919, 167, 1683eqtrd 2790 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170166, 169oveq12d 6823 . . . . . . . . 9 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171150, 151, 152adddid 10248 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172170, 171eqtr4d 2789 . . . . . . . 8 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173163, 172oveq12d 6823 . . . . . . 7 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174154, 173eqtr4d 2789 . . . . . 6 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175 mul4sq.5 . . . . . . . 8 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
1763absvalsqd 14372 . . . . . . . . 9 (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
17714absvalsqd 14372 . . . . . . . . 9 (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178176, 177oveq12d 6823 . . . . . . . 8 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179175, 178syl5eq 2798 . . . . . . 7 (𝜑𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180 mul4sq.6 . . . . . . . 8 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
1816absvalsqd 14372 . . . . . . . . 9 (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
18217absvalsqd 14372 . . . . . . . . 9 (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183181, 182oveq12d 6823 . . . . . . . 8 (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184180, 183syl5eq 2798 . . . . . . 7 (𝜑𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185179, 184oveq12d 6823 . . . . . 6 (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
18611, 22, 39, 44add42d 10449 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187174, 185, 1863eqtr4d 2796 . . . . 5 (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
18846, 148, 1873eqtr4d 2796 . . . 4 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189188oveq1d 6820 . . 3 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190 mul4sq.7 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
191190nncnd 11220 . . . . . . . . 9 (𝜑𝑀 ∈ ℂ)
192190nnne0d 11249 . . . . . . . . 9 (𝜑𝑀 ≠ 0)
19348, 191, 192absdivd 14385 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194190nnred 11219 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
195190nnnn0d 11535 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ0)
196195nn0ge0d 11538 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑀)
197194, 196absidd 14352 . . . . . . . . 9 (𝜑 → (abs‘𝑀) = 𝑀)
198197oveq2d 6821 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199193, 198eqtrd 2786 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200199oveq1d 6820 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
20148abscld 14366 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202201recnd 10252 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203202, 191, 192sqdivd 13207 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204200, 203eqtrd 2786 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
20599, 191, 192absdivd 14385 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206197oveq2d 6821 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207205, 206eqtrd 2786 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208207oveq1d 6820 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
20999abscld 14366 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210209recnd 10252 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211210, 191, 192sqdivd 13207 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212208, 211eqtrd 2786 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213204, 212oveq12d 6823 . . . 4 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
21423, 34addcld 10243 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
21597, 214eqeltrd 2831 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
21645, 34subcld 10576 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217147, 216eqeltrd 2831 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218190nnsqcld 13215 . . . . . 6 (𝜑 → (𝑀↑2) ∈ ℕ)
219218nncnd 11220 . . . . 5 (𝜑 → (𝑀↑2) ∈ ℂ)
220218nnne0d 11249 . . . . 5 (𝜑 → (𝑀↑2) ≠ 0)
221215, 217, 219, 220divdird 11023 . . . 4 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222213, 221eqtr4d 2789 . . 3 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223176, 149eqeltrd 2831 . . . . . . 7 (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224177, 150eqeltrd 2831 . . . . . . 7 (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225223, 224addcld 10243 . . . . . 6 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226175, 225syl5eqel 2835 . . . . 5 (𝜑𝑋 ∈ ℂ)
227184, 153eqeltrd 2831 . . . . 5 (𝜑𝑌 ∈ ℂ)
228226, 191, 227, 191, 192, 192divmuldivd 11026 . . . 4 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229191sqvald 13191 . . . . 5 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230229oveq2d 6821 . . . 4 (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231228, 230eqtr4d 2789 . . 3 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232189, 222, 2313eqtr4d 2796 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233226, 48nncand 10581 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234149, 150, 25, 47addsub4d 10623 . . . . . . . . 9 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235179oveq1d 6820 . . . . . . . . 9 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
23624, 3, 6subdid 10670 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
23724, 3mulcomd 10245 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238237oveq1d 6820 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239236, 238eqtrd 2786 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240 cjsub 14080 . . . . . . . . . . . . 13 ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
24114, 17, 240syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242241oveq2d 6821 . . . . . . . . . . 11 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
24314, 26, 31subdid 10670 . . . . . . . . . . 11 (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244242, 243eqtrd 2786 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245239, 244oveq12d 6823 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246234, 235, 2453eqtr4d 2796 . . . . . . . 8 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))))
247246oveq2d 6821 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
248233, 247eqtr3d 2788 . . . . . 6 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
249248oveq1d 6820 . . . . 5 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀))
2503, 6subcld 10576 . . . . . . . 8 (𝜑 → (𝐴𝐶) ∈ ℂ)
25124, 250mulcld 10244 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) ∈ ℂ)
25214, 17subcld 10576 . . . . . . . . 9 (𝜑 → (𝐵𝐷) ∈ ℂ)
253252cjcld 14127 . . . . . . . 8 (𝜑 → (∗‘(𝐵𝐷)) ∈ ℂ)
25414, 253mulcld 10244 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) ∈ ℂ)
255251, 254addcld 10243 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) ∈ ℂ)
256226, 255, 191, 192divsubdird 11024 . . . . 5 (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)))
257251, 254, 191, 192divdird 11023 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)))
25824, 250, 191, 192divassd 11020 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)))
25914, 253, 191, 192divassd 11020 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
260252, 191, 192cjdivd 14154 . . . . . . . . . . 11 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / (∗‘𝑀)))
261194cjred 14157 . . . . . . . . . . . 12 (𝜑 → (∗‘𝑀) = 𝑀)
262261oveq2d 6821 . . . . . . . . . . 11 (𝜑 → ((∗‘(𝐵𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
263260, 262eqtrd 2786 . . . . . . . . . 10 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
264263oveq2d 6821 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
265259, 264eqtr4d 2789 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))
266258, 265oveq12d 6823 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
267257, 266eqtrd 2786 . . . . . 6 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
268267oveq2d 6821 . . . . 5 (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
269249, 256, 2683eqtrd 2790 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
270 mul4sq.10 . . . . . . 7 (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
271270nn0zd 11664 . . . . . 6 (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272 zgz 15831 . . . . . 6 ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273271, 272syl 17 . . . . 5 (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274 gzcjcl 15834 . . . . . . . 8 (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
2751, 274syl 17 . . . . . . 7 (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276 mul4sq.8 . . . . . . 7 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ[i])
277 gzmulcl 15836 . . . . . . 7 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
278275, 276, 277syl2anc 696 . . . . . 6 (𝜑 → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
279 mul4sq.9 . . . . . . . 8 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ[i])
280 gzcjcl 15834 . . . . . . . 8 (((𝐵𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
281279, 280syl 17 . . . . . . 7 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
282 gzmulcl 15836 . . . . . . 7 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
28312, 281, 282syl2anc 696 . . . . . 6 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
284 gzaddcl 15835 . . . . . 6 ((((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
285278, 283, 284syl2anc 696 . . . . 5 (𝜑 → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
286 gzsubcl 15838 . . . . 5 (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
287273, 285, 286syl2anc 696 . . . 4 (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
288269, 287eqeltrd 2831 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289250cjcld 14127 . . . . . . . 8 (𝜑 → (∗‘(𝐴𝐶)) ∈ ℂ)
29014, 289mulcld 10244 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) ∈ ℂ)
29124, 252mulcld 10244 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) ∈ ℂ)
292290, 291, 191, 192divsubdird 11024 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)))
293 cjsub 14080 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
2943, 6, 293syl2anc 696 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295294oveq2d 6821 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
29614, 24, 29subdid 10670 . . . . . . . . . 10 (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297295, 296eqtrd 2786 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
29824, 14, 17subdid 10670 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
29924, 14mulcomd 10245 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300299oveq1d 6820 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301298, 300eqtrd 2786 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302297, 301oveq12d 6823 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
30314, 24mulcld 10244 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304303, 30, 98nnncan1d 10610 . . . . . . . 8 (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305302, 304eqtrd 2786 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306305oveq1d 6820 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307292, 306eqtr3d 2788 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
30814, 289, 191, 192divassd 11020 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
309250, 191, 192cjdivd 14154 . . . . . . . . 9 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / (∗‘𝑀)))
310261oveq2d 6821 . . . . . . . . 9 (𝜑 → ((∗‘(𝐴𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
311309, 310eqtrd 2786 . . . . . . . 8 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
312311oveq2d 6821 . . . . . . 7 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
313308, 312eqtr4d 2789 . . . . . 6 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴𝐶) / 𝑀))))
31424, 252, 191, 192divassd 11020 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐵𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)))
315313, 314oveq12d 6823 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
316307, 315eqtr3d 2788 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
317 gzcjcl 15834 . . . . . . 7 (((𝐴𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
318276, 317syl 17 . . . . . 6 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
319 gzmulcl 15836 . . . . . 6 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
32012, 318, 319syl2anc 696 . . . . 5 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
321 gzmulcl 15836 . . . . . 6 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
322275, 279, 321syl2anc 696 . . . . 5 (𝜑 → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
323 gzsubcl 15838 . . . . 5 (((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
324320, 322, 323syl2anc 696 . . . 4 (𝜑 → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
325316, 324eqeltrd 2831 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326 4sq.1 . . . 4 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
3273264sqlem4a 15849 . . 3 ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328288, 325, 327syl2anc 696 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329232, 328eqeltrrd 2832 1 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  wcel 2131  {cab 2738  wrex 3043  cfv 6041  (class class class)co 6805  cc 10118   + caddc 10123   · cmul 10125  cmin 10450   / cdiv 10868  cn 11204  2c2 11254  0cn0 11476  cz 11561  cexp 13046  ccj 14027  abscabs 14165  ℤ[i]cgz 15827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-er 7903  df-en 8114  df-dom 8115  df-sdom 8116  df-sup 8505  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-n0 11477  df-z 11562  df-uz 11872  df-rp 12018  df-seq 12988  df-exp 13047  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-gz 15828
This theorem is referenced by:  mul4sq  15852  4sqlem17  15859
  Copyright terms: Public domain W3C validator