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

Theorem mul4sqlem 15863
Description: Lemma for mul4sq 15864: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 15871 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 15842 . . . . . . . . . . 11 (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
4 mul4sq.3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℤ[i])
5 gzcn 15842 . . . . . . . . . . 11 (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
73, 6mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
87absvalsqd 14388 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
97cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
107, 9mulcld 10261 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
118, 10eqeltrd 2849 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12 mul4sq.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℤ[i])
13 gzcn 15842 . . . . . . . . . . 11 (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
1412, 13syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
15 mul4sq.4 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℤ[i])
16 gzcn 15842 . . . . . . . . . . 11 (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
1814, 17mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
1918absvalsqd 14388 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
2018cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
2118, 20mulcld 10261 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
2219, 21eqeltrd 2849 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
2311, 22addcld 10260 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
243cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘𝐴) ∈ ℂ)
2524, 6mulcld 10261 . . . . . . . 8 (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
2614cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘𝐵) ∈ ℂ)
2726, 17mulcld 10261 . . . . . . . 8 (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
2825, 27mulcld 10261 . . . . . . 7 (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
296cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘𝐶) ∈ ℂ)
3014, 29mulcld 10261 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
3117cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘𝐷) ∈ ℂ)
323, 31mulcld 10261 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
3330, 32mulcld 10261 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
3428, 33addcld 10260 . . . . . 6 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
353, 17mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
3635absvalsqd 14388 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
3735cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
3835, 37mulcld 10261 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
3936, 38eqeltrd 2849 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
4014, 6mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
4140absvalsqd 14388 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
4240cjcld 14143 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
4340, 42mulcld 10261 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
4441, 43eqeltrd 2849 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
4539, 44addcld 10260 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
4623, 34, 45ppncand 10633 . . . . 5 (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
4714, 31mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
4825, 47addcld 10260 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
4948absvalsqd 14388 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
5025, 47cjaddd 14167 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
5124, 6cjmuld 14168 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
523cjcjd 14146 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
5352oveq1d 6807 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
5451, 53eqtrd 2804 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
5514, 31cjmuld 14168 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
5617cjcjd 14146 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
5756oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5855, 57eqtrd 2804 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5954, 58oveq12d 6810 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6050, 59eqtrd 2804 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6160oveq2d 6808 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
623, 29mulcld 10261 . . . . . . . . . . 11 (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
6325, 62, 27adddid 10265 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
646, 24, 3, 29mul4d 10449 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
6524, 6mulcomd 10262 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
6665oveq1d 6807 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
673, 6mulcomd 10262 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
683, 6cjmuld 14168 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
6967, 68oveq12d 6810 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
7064, 66, 693eqtr4d 2814 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
7170, 8eqtr4d 2807 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
7271oveq1d 6807 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7363, 72eqtrd 2804 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7447, 62, 27adddid 10265 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
753, 29mulcomd 10262 . . . . . . . . . . . . 13 (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
7675oveq2d 6808 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
7714, 31, 29, 3mul4d 10449 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
7831, 3mulcomd 10262 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
7978oveq2d 6808 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8076, 77, 793eqtrd 2808 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8114, 31, 17, 26mul4d 10449 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8226, 17mulcomd 10262 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
8382oveq2d 6808 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
8414, 17cjmuld 14168 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
8526, 31mulcomd 10262 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8684, 85eqtrd 2804 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8786oveq2d 6808 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8881, 83, 873eqtr4d 2814 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
8988, 19eqtr4d 2807 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
9080, 89oveq12d 6810 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9174, 90eqtrd 2804 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9273, 91oveq12d 6810 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9362, 27addcld 10260 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
9425, 47, 93adddird 10266 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
9511, 22, 28, 33add42d 10466 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9692, 94, 953eqtr4d 2814 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9749, 61, 963eqtrd 2808 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9824, 17mulcld 10261 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
9998, 30subcld 10593 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
10099absvalsqd 14388 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101 cjsub 14096 . . . . . . . . . 10 ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10298, 30, 101syl2anc 565 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10324, 17cjmuld 14168 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
10452oveq1d 6807 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105103, 104eqtrd 2804 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
10614, 29cjmuld 14168 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
1076cjcjd 14146 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108107oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109106, 108eqtrd 2804 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110105, 109oveq12d 6810 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111102, 110eqtrd 2804 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112111oveq2d 6808 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
11326, 6mulcld 10261 . . . . . . . . . 10 (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
11432, 113subcld 10593 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
11598, 30, 114subdird 10688 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
11698, 32, 113subdid 10687 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
11717, 24, 3, 31mul4d 10449 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
11824, 17mulcomd 10262 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119118oveq1d 6807 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
1203, 17mulcomd 10262 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
1213, 17cjmuld 14168 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122120, 121oveq12d 6810 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123117, 119, 1223eqtr4d 2814 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124123, 36eqtr4d 2807 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
12526, 6mulcomd 10262 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126125oveq2d 6808 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
12724, 17, 6, 26mul4d 10449 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
12817, 26mulcomd 10262 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129128oveq2d 6808 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130126, 127, 1293eqtrd 2808 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131124, 130oveq12d 6810 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132116, 131eqtrd 2804 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
13330, 32, 113subdid 10687 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134125oveq2d 6808 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
13514, 29, 6, 26mul4d 10449 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
13629, 26mulcomd 10262 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
13714, 6cjmuld 14168 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138136, 137eqtr4d 2807 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139138oveq2d 6808 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140134, 135, 1393eqtrd 2808 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141140, 41eqtr4d 2807 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142141oveq2d 6808 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143133, 142eqtrd 2804 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144132, 143oveq12d 6810 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
14539, 28, 33, 44subadd4d 10641 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146115, 144, 1453eqtrd 2808 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147100, 112, 1463eqtrd 2808 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
14897, 147oveq12d 6810 . . . . 5 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
1493, 24mulcld 10261 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
15014, 26mulcld 10261 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
1516, 29mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
15217, 31mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153151, 152addcld 10260 . . . . . . . 8 (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154149, 150, 153adddird 10266 . . . . . . 7 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
15568oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
1563, 6, 24, 29mul4d 10449 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
1578, 155, 1563eqtrd 2808 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158121oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
1593, 17, 24, 31mul4d 10449 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
16036, 158, 1593eqtrd 2808 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161157, 160oveq12d 6810 . . . . . . . . 9 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162149, 151, 152adddid 10265 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163161, 162eqtr4d 2807 . . . . . . . 8 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164137oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
16514, 6, 26, 29mul4d 10449 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16641, 164, 1653eqtrd 2808 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16784oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
16814, 17, 26, 31mul4d 10449 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
16919, 167, 1683eqtrd 2808 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170166, 169oveq12d 6810 . . . . . . . . 9 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171150, 151, 152adddid 10265 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172170, 171eqtr4d 2807 . . . . . . . 8 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173163, 172oveq12d 6810 . . . . . . 7 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174154, 173eqtr4d 2807 . . . . . 6 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175 mul4sq.5 . . . . . . . 8 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
1763absvalsqd 14388 . . . . . . . . 9 (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
17714absvalsqd 14388 . . . . . . . . 9 (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178176, 177oveq12d 6810 . . . . . . . 8 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179175, 178syl5eq 2816 . . . . . . 7 (𝜑𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180 mul4sq.6 . . . . . . . 8 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
1816absvalsqd 14388 . . . . . . . . 9 (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
18217absvalsqd 14388 . . . . . . . . 9 (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183181, 182oveq12d 6810 . . . . . . . 8 (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184180, 183syl5eq 2816 . . . . . . 7 (𝜑𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185179, 184oveq12d 6810 . . . . . 6 (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
18611, 22, 39, 44add42d 10466 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187174, 185, 1863eqtr4d 2814 . . . . 5 (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
18846, 148, 1873eqtr4d 2814 . . . 4 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189188oveq1d 6807 . . 3 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190 mul4sq.7 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
191190nncnd 11237 . . . . . . . . 9 (𝜑𝑀 ∈ ℂ)
192190nnne0d 11266 . . . . . . . . 9 (𝜑𝑀 ≠ 0)
19348, 191, 192absdivd 14401 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194190nnred 11236 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
195190nnnn0d 11552 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ0)
196195nn0ge0d 11555 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑀)
197194, 196absidd 14368 . . . . . . . . 9 (𝜑 → (abs‘𝑀) = 𝑀)
198197oveq2d 6808 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199193, 198eqtrd 2804 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200199oveq1d 6807 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
20148abscld 14382 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202201recnd 10269 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203202, 191, 192sqdivd 13227 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204200, 203eqtrd 2804 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
20599, 191, 192absdivd 14401 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206197oveq2d 6808 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207205, 206eqtrd 2804 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208207oveq1d 6807 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
20999abscld 14382 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210209recnd 10269 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211210, 191, 192sqdivd 13227 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212208, 211eqtrd 2804 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213204, 212oveq12d 6810 . . . 4 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
21423, 34addcld 10260 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
21597, 214eqeltrd 2849 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
21645, 34subcld 10593 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217147, 216eqeltrd 2849 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218190nnsqcld 13235 . . . . . 6 (𝜑 → (𝑀↑2) ∈ ℕ)
219218nncnd 11237 . . . . 5 (𝜑 → (𝑀↑2) ∈ ℂ)
220218nnne0d 11266 . . . . 5 (𝜑 → (𝑀↑2) ≠ 0)
221215, 217, 219, 220divdird 11040 . . . 4 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222213, 221eqtr4d 2807 . . 3 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223176, 149eqeltrd 2849 . . . . . . 7 (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224177, 150eqeltrd 2849 . . . . . . 7 (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225223, 224addcld 10260 . . . . . 6 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226175, 225syl5eqel 2853 . . . . 5 (𝜑𝑋 ∈ ℂ)
227184, 153eqeltrd 2849 . . . . 5 (𝜑𝑌 ∈ ℂ)
228226, 191, 227, 191, 192, 192divmuldivd 11043 . . . 4 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229191sqvald 13211 . . . . 5 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230229oveq2d 6808 . . . 4 (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231228, 230eqtr4d 2807 . . 3 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232189, 222, 2313eqtr4d 2814 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233226, 48nncand 10598 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234149, 150, 25, 47addsub4d 10640 . . . . . . . . 9 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235179oveq1d 6807 . . . . . . . . 9 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
23624, 3, 6subdid 10687 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
23724, 3mulcomd 10262 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238237oveq1d 6807 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239236, 238eqtrd 2804 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240 cjsub 14096 . . . . . . . . . . . . 13 ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
24114, 17, 240syl2anc 565 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242241oveq2d 6808 . . . . . . . . . . 11 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
24314, 26, 31subdid 10687 . . . . . . . . . . 11 (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244242, 243eqtrd 2804 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245239, 244oveq12d 6810 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246234, 235, 2453eqtr4d 2814 . . . . . . . 8 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))))
247246oveq2d 6808 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
248233, 247eqtr3d 2806 . . . . . 6 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
249248oveq1d 6807 . . . . 5 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀))
2503, 6subcld 10593 . . . . . . . 8 (𝜑 → (𝐴𝐶) ∈ ℂ)
25124, 250mulcld 10261 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) ∈ ℂ)
25214, 17subcld 10593 . . . . . . . . 9 (𝜑 → (𝐵𝐷) ∈ ℂ)
253252cjcld 14143 . . . . . . . 8 (𝜑 → (∗‘(𝐵𝐷)) ∈ ℂ)
25414, 253mulcld 10261 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) ∈ ℂ)
255251, 254addcld 10260 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) ∈ ℂ)
256226, 255, 191, 192divsubdird 11041 . . . . 5 (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)))
257251, 254, 191, 192divdird 11040 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)))
25824, 250, 191, 192divassd 11037 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)))
25914, 253, 191, 192divassd 11037 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
260252, 191, 192cjdivd 14170 . . . . . . . . . . 11 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / (∗‘𝑀)))
261194cjred 14173 . . . . . . . . . . . 12 (𝜑 → (∗‘𝑀) = 𝑀)
262261oveq2d 6808 . . . . . . . . . . 11 (𝜑 → ((∗‘(𝐵𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
263260, 262eqtrd 2804 . . . . . . . . . 10 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
264263oveq2d 6808 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
265259, 264eqtr4d 2807 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))
266258, 265oveq12d 6810 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
267257, 266eqtrd 2804 . . . . . 6 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
268267oveq2d 6808 . . . . 5 (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
269249, 256, 2683eqtrd 2808 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
270 mul4sq.10 . . . . . . 7 (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
271270nn0zd 11681 . . . . . 6 (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272 zgz 15843 . . . . . 6 ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273271, 272syl 17 . . . . 5 (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274 gzcjcl 15846 . . . . . . . 8 (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
2751, 274syl 17 . . . . . . 7 (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276 mul4sq.8 . . . . . . 7 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ[i])
277 gzmulcl 15848 . . . . . . 7 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
278275, 276, 277syl2anc 565 . . . . . 6 (𝜑 → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
279 mul4sq.9 . . . . . . . 8 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ[i])
280 gzcjcl 15846 . . . . . . . 8 (((𝐵𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
281279, 280syl 17 . . . . . . 7 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
282 gzmulcl 15848 . . . . . . 7 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
28312, 281, 282syl2anc 565 . . . . . 6 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
284 gzaddcl 15847 . . . . . 6 ((((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
285278, 283, 284syl2anc 565 . . . . 5 (𝜑 → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
286 gzsubcl 15850 . . . . 5 (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
287273, 285, 286syl2anc 565 . . . 4 (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
288269, 287eqeltrd 2849 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289250cjcld 14143 . . . . . . . 8 (𝜑 → (∗‘(𝐴𝐶)) ∈ ℂ)
29014, 289mulcld 10261 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) ∈ ℂ)
29124, 252mulcld 10261 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) ∈ ℂ)
292290, 291, 191, 192divsubdird 11041 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)))
293 cjsub 14096 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
2943, 6, 293syl2anc 565 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295294oveq2d 6808 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
29614, 24, 29subdid 10687 . . . . . . . . . 10 (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297295, 296eqtrd 2804 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
29824, 14, 17subdid 10687 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
29924, 14mulcomd 10262 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300299oveq1d 6807 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301298, 300eqtrd 2804 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302297, 301oveq12d 6810 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
30314, 24mulcld 10261 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304303, 30, 98nnncan1d 10627 . . . . . . . 8 (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305302, 304eqtrd 2804 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306305oveq1d 6807 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307292, 306eqtr3d 2806 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
30814, 289, 191, 192divassd 11037 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
309250, 191, 192cjdivd 14170 . . . . . . . . 9 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / (∗‘𝑀)))
310261oveq2d 6808 . . . . . . . . 9 (𝜑 → ((∗‘(𝐴𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
311309, 310eqtrd 2804 . . . . . . . 8 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
312311oveq2d 6808 . . . . . . 7 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
313308, 312eqtr4d 2807 . . . . . 6 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴𝐶) / 𝑀))))
31424, 252, 191, 192divassd 11037 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐵𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)))
315313, 314oveq12d 6810 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
316307, 315eqtr3d 2806 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
317 gzcjcl 15846 . . . . . . 7 (((𝐴𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
318276, 317syl 17 . . . . . 6 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
319 gzmulcl 15848 . . . . . 6 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
32012, 318, 319syl2anc 565 . . . . 5 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
321 gzmulcl 15848 . . . . . 6 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
322275, 279, 321syl2anc 565 . . . . 5 (𝜑 → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
323 gzsubcl 15850 . . . . 5 (((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
324320, 322, 323syl2anc 565 . . . 4 (𝜑 → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
325316, 324eqeltrd 2849 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326 4sq.1 . . . 4 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
3273264sqlem4a 15861 . . 3 ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328288, 325, 327syl2anc 565 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329232, 328eqeltrrd 2850 1 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2144  {cab 2756  wrex 3061  cfv 6031  (class class class)co 6792  cc 10135   + caddc 10140   · cmul 10142  cmin 10467   / cdiv 10885  cn 11221  2c2 11271  0cn0 11493  cz 11578  cexp 13066  ccj 14043  abscabs 14181  ℤ[i]cgz 15839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214  ax-pre-sup 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-er 7895  df-en 8109  df-dom 8110  df-sdom 8111  df-sup 8503  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-3 11281  df-n0 11494  df-z 11579  df-uz 11888  df-rp 12035  df-seq 13008  df-exp 13067  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-gz 15840
This theorem is referenced by:  mul4sq  15864  4sqlem17  15871
  Copyright terms: Public domain W3C validator