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

Theorem mul4sqlem 15581
Description: Lemma for mul4sq 15582: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 15589 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 15560 . . . . . . . . . . 11 (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
31, 2syl 17 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
4 mul4sq.3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℤ[i])
5 gzcn 15560 . . . . . . . . . . 11 (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
73, 6mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
87absvalsqd 14115 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
97cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
107, 9mulcld 10004 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
118, 10eqeltrd 2698 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12 mul4sq.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℤ[i])
13 gzcn 15560 . . . . . . . . . . 11 (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
1412, 13syl 17 . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
15 mul4sq.4 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℤ[i])
16 gzcn 15560 . . . . . . . . . . 11 (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
1814, 17mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
1918absvalsqd 14115 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
2018cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
2118, 20mulcld 10004 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
2219, 21eqeltrd 2698 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
2311, 22addcld 10003 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
243cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘𝐴) ∈ ℂ)
2524, 6mulcld 10004 . . . . . . . 8 (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
2614cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘𝐵) ∈ ℂ)
2726, 17mulcld 10004 . . . . . . . 8 (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
2825, 27mulcld 10004 . . . . . . 7 (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
296cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘𝐶) ∈ ℂ)
3014, 29mulcld 10004 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
3117cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘𝐷) ∈ ℂ)
323, 31mulcld 10004 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
3330, 32mulcld 10004 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
3428, 33addcld 10003 . . . . . 6 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
353, 17mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
3635absvalsqd 14115 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
3735cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
3835, 37mulcld 10004 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
3936, 38eqeltrd 2698 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
4014, 6mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
4140absvalsqd 14115 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
4240cjcld 13870 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
4340, 42mulcld 10004 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
4441, 43eqeltrd 2698 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
4539, 44addcld 10003 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
4623, 34, 45ppncand 10376 . . . . 5 (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
4714, 31mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
4825, 47addcld 10003 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
4948absvalsqd 14115 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
5025, 47cjaddd 13894 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
5124, 6cjmuld 13895 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
523cjcjd 13873 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
5352oveq1d 6619 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
5451, 53eqtrd 2655 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
5514, 31cjmuld 13895 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
5617cjcjd 13873 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
5756oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5855, 57eqtrd 2655 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5954, 58oveq12d 6622 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6050, 59eqtrd 2655 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6160oveq2d 6620 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
623, 29mulcld 10004 . . . . . . . . . . 11 (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
6325, 62, 27adddid 10008 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
646, 24, 3, 29mul4d 10192 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
6524, 6mulcomd 10005 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
6665oveq1d 6619 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
673, 6mulcomd 10005 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
683, 6cjmuld 13895 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
6967, 68oveq12d 6622 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
7064, 66, 693eqtr4d 2665 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
7170, 8eqtr4d 2658 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
7271oveq1d 6619 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7363, 72eqtrd 2655 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7447, 62, 27adddid 10008 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
753, 29mulcomd 10005 . . . . . . . . . . . . 13 (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
7675oveq2d 6620 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
7714, 31, 29, 3mul4d 10192 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
7831, 3mulcomd 10005 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
7978oveq2d 6620 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8076, 77, 793eqtrd 2659 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8114, 31, 17, 26mul4d 10192 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8226, 17mulcomd 10005 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
8382oveq2d 6620 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
8414, 17cjmuld 13895 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
8526, 31mulcomd 10005 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8684, 85eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8786oveq2d 6620 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8881, 83, 873eqtr4d 2665 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
8988, 19eqtr4d 2658 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
9080, 89oveq12d 6622 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9174, 90eqtrd 2655 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9273, 91oveq12d 6622 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9362, 27addcld 10003 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
9425, 47, 93adddird 10009 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
9511, 22, 28, 33add42d 10209 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9692, 94, 953eqtr4d 2665 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9749, 61, 963eqtrd 2659 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9824, 17mulcld 10004 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
9998, 30subcld 10336 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
10099absvalsqd 14115 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101 cjsub 13823 . . . . . . . . . 10 ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10298, 30, 101syl2anc 692 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10324, 17cjmuld 13895 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
10452oveq1d 6619 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105103, 104eqtrd 2655 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
10614, 29cjmuld 13895 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
1076cjcjd 13873 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108107oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109106, 108eqtrd 2655 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110105, 109oveq12d 6622 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111102, 110eqtrd 2655 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112111oveq2d 6620 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
11326, 6mulcld 10004 . . . . . . . . . 10 (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
11432, 113subcld 10336 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
11598, 30, 114subdird 10431 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
11698, 32, 113subdid 10430 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
11717, 24, 3, 31mul4d 10192 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
11824, 17mulcomd 10005 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119118oveq1d 6619 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
1203, 17mulcomd 10005 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
1213, 17cjmuld 13895 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122120, 121oveq12d 6622 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123117, 119, 1223eqtr4d 2665 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124123, 36eqtr4d 2658 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
12526, 6mulcomd 10005 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126125oveq2d 6620 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
12724, 17, 6, 26mul4d 10192 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
12817, 26mulcomd 10005 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129128oveq2d 6620 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130126, 127, 1293eqtrd 2659 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131124, 130oveq12d 6622 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132116, 131eqtrd 2655 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
13330, 32, 113subdid 10430 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134125oveq2d 6620 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
13514, 29, 6, 26mul4d 10192 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
13629, 26mulcomd 10005 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
13714, 6cjmuld 13895 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138136, 137eqtr4d 2658 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139138oveq2d 6620 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140134, 135, 1393eqtrd 2659 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141140, 41eqtr4d 2658 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142141oveq2d 6620 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143133, 142eqtrd 2655 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144132, 143oveq12d 6622 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
14539, 28, 33, 44subadd4d 10384 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146115, 144, 1453eqtrd 2659 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147100, 112, 1463eqtrd 2659 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
14897, 147oveq12d 6622 . . . . 5 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
1493, 24mulcld 10004 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
15014, 26mulcld 10004 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
1516, 29mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
15217, 31mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153151, 152addcld 10003 . . . . . . . 8 (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154149, 150, 153adddird 10009 . . . . . . 7 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
15568oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
1563, 6, 24, 29mul4d 10192 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
1578, 155, 1563eqtrd 2659 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158121oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
1593, 17, 24, 31mul4d 10192 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
16036, 158, 1593eqtrd 2659 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161157, 160oveq12d 6622 . . . . . . . . 9 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162149, 151, 152adddid 10008 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163161, 162eqtr4d 2658 . . . . . . . 8 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164137oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
16514, 6, 26, 29mul4d 10192 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16641, 164, 1653eqtrd 2659 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16784oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
16814, 17, 26, 31mul4d 10192 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
16919, 167, 1683eqtrd 2659 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170166, 169oveq12d 6622 . . . . . . . . 9 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171150, 151, 152adddid 10008 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172170, 171eqtr4d 2658 . . . . . . . 8 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173163, 172oveq12d 6622 . . . . . . 7 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174154, 173eqtr4d 2658 . . . . . 6 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175 mul4sq.5 . . . . . . . 8 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
1763absvalsqd 14115 . . . . . . . . 9 (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
17714absvalsqd 14115 . . . . . . . . 9 (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178176, 177oveq12d 6622 . . . . . . . 8 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179175, 178syl5eq 2667 . . . . . . 7 (𝜑𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180 mul4sq.6 . . . . . . . 8 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
1816absvalsqd 14115 . . . . . . . . 9 (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
18217absvalsqd 14115 . . . . . . . . 9 (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183181, 182oveq12d 6622 . . . . . . . 8 (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184180, 183syl5eq 2667 . . . . . . 7 (𝜑𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185179, 184oveq12d 6622 . . . . . 6 (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
18611, 22, 39, 44add42d 10209 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187174, 185, 1863eqtr4d 2665 . . . . 5 (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
18846, 148, 1873eqtr4d 2665 . . . 4 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189188oveq1d 6619 . . 3 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190 mul4sq.7 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
191190nncnd 10980 . . . . . . . . 9 (𝜑𝑀 ∈ ℂ)
192190nnne0d 11009 . . . . . . . . 9 (𝜑𝑀 ≠ 0)
19348, 191, 192absdivd 14128 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194190nnred 10979 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
195190nnnn0d 11295 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ0)
196195nn0ge0d 11298 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑀)
197194, 196absidd 14095 . . . . . . . . 9 (𝜑 → (abs‘𝑀) = 𝑀)
198197oveq2d 6620 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199193, 198eqtrd 2655 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200199oveq1d 6619 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
20148abscld 14109 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202201recnd 10012 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203202, 191, 192sqdivd 12961 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204200, 203eqtrd 2655 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
20599, 191, 192absdivd 14128 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206197oveq2d 6620 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207205, 206eqtrd 2655 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208207oveq1d 6619 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
20999abscld 14109 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210209recnd 10012 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211210, 191, 192sqdivd 12961 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212208, 211eqtrd 2655 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213204, 212oveq12d 6622 . . . 4 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
21423, 34addcld 10003 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
21597, 214eqeltrd 2698 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
21645, 34subcld 10336 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217147, 216eqeltrd 2698 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218190nnsqcld 12969 . . . . . 6 (𝜑 → (𝑀↑2) ∈ ℕ)
219218nncnd 10980 . . . . 5 (𝜑 → (𝑀↑2) ∈ ℂ)
220218nnne0d 11009 . . . . 5 (𝜑 → (𝑀↑2) ≠ 0)
221215, 217, 219, 220divdird 10783 . . . 4 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222213, 221eqtr4d 2658 . . 3 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223176, 149eqeltrd 2698 . . . . . . 7 (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224177, 150eqeltrd 2698 . . . . . . 7 (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225223, 224addcld 10003 . . . . . 6 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226175, 225syl5eqel 2702 . . . . 5 (𝜑𝑋 ∈ ℂ)
227184, 153eqeltrd 2698 . . . . 5 (𝜑𝑌 ∈ ℂ)
228226, 191, 227, 191, 192, 192divmuldivd 10786 . . . 4 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229191sqvald 12945 . . . . 5 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230229oveq2d 6620 . . . 4 (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231228, 230eqtr4d 2658 . . 3 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232189, 222, 2313eqtr4d 2665 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233226, 48nncand 10341 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234149, 150, 25, 47addsub4d 10383 . . . . . . . . 9 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235179oveq1d 6619 . . . . . . . . 9 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
23624, 3, 6subdid 10430 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
23724, 3mulcomd 10005 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238237oveq1d 6619 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239236, 238eqtrd 2655 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240 cjsub 13823 . . . . . . . . . . . . 13 ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
24114, 17, 240syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242241oveq2d 6620 . . . . . . . . . . 11 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
24314, 26, 31subdid 10430 . . . . . . . . . . 11 (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244242, 243eqtrd 2655 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245239, 244oveq12d 6622 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246234, 235, 2453eqtr4d 2665 . . . . . . . 8 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))))
247246oveq2d 6620 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
248233, 247eqtr3d 2657 . . . . . 6 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
249248oveq1d 6619 . . . . 5 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀))
2503, 6subcld 10336 . . . . . . . 8 (𝜑 → (𝐴𝐶) ∈ ℂ)
25124, 250mulcld 10004 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) ∈ ℂ)
25214, 17subcld 10336 . . . . . . . . 9 (𝜑 → (𝐵𝐷) ∈ ℂ)
253252cjcld 13870 . . . . . . . 8 (𝜑 → (∗‘(𝐵𝐷)) ∈ ℂ)
25414, 253mulcld 10004 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) ∈ ℂ)
255251, 254addcld 10003 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) ∈ ℂ)
256226, 255, 191, 192divsubdird 10784 . . . . 5 (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)))
257251, 254, 191, 192divdird 10783 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)))
25824, 250, 191, 192divassd 10780 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)))
25914, 253, 191, 192divassd 10780 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
260252, 191, 192cjdivd 13897 . . . . . . . . . . 11 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / (∗‘𝑀)))
261194cjred 13900 . . . . . . . . . . . 12 (𝜑 → (∗‘𝑀) = 𝑀)
262261oveq2d 6620 . . . . . . . . . . 11 (𝜑 → ((∗‘(𝐵𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
263260, 262eqtrd 2655 . . . . . . . . . 10 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
264263oveq2d 6620 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
265259, 264eqtr4d 2658 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))
266258, 265oveq12d 6622 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
267257, 266eqtrd 2655 . . . . . 6 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
268267oveq2d 6620 . . . . 5 (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
269249, 256, 2683eqtrd 2659 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
270 mul4sq.10 . . . . . . 7 (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
271270nn0zd 11424 . . . . . 6 (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272 zgz 15561 . . . . . 6 ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273271, 272syl 17 . . . . 5 (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274 gzcjcl 15564 . . . . . . . 8 (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
2751, 274syl 17 . . . . . . 7 (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276 mul4sq.8 . . . . . . 7 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ[i])
277 gzmulcl 15566 . . . . . . 7 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
278275, 276, 277syl2anc 692 . . . . . 6 (𝜑 → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
279 mul4sq.9 . . . . . . . 8 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ[i])
280 gzcjcl 15564 . . . . . . . 8 (((𝐵𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
281279, 280syl 17 . . . . . . 7 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
282 gzmulcl 15566 . . . . . . 7 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
28312, 281, 282syl2anc 692 . . . . . 6 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
284 gzaddcl 15565 . . . . . 6 ((((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
285278, 283, 284syl2anc 692 . . . . 5 (𝜑 → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
286 gzsubcl 15568 . . . . 5 (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
287273, 285, 286syl2anc 692 . . . 4 (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
288269, 287eqeltrd 2698 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289250cjcld 13870 . . . . . . . 8 (𝜑 → (∗‘(𝐴𝐶)) ∈ ℂ)
29014, 289mulcld 10004 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) ∈ ℂ)
29124, 252mulcld 10004 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) ∈ ℂ)
292290, 291, 191, 192divsubdird 10784 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)))
293 cjsub 13823 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
2943, 6, 293syl2anc 692 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295294oveq2d 6620 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
29614, 24, 29subdid 10430 . . . . . . . . . 10 (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297295, 296eqtrd 2655 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
29824, 14, 17subdid 10430 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
29924, 14mulcomd 10005 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300299oveq1d 6619 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301298, 300eqtrd 2655 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302297, 301oveq12d 6622 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
30314, 24mulcld 10004 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304303, 30, 98nnncan1d 10370 . . . . . . . 8 (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305302, 304eqtrd 2655 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306305oveq1d 6619 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307292, 306eqtr3d 2657 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
30814, 289, 191, 192divassd 10780 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
309250, 191, 192cjdivd 13897 . . . . . . . . 9 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / (∗‘𝑀)))
310261oveq2d 6620 . . . . . . . . 9 (𝜑 → ((∗‘(𝐴𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
311309, 310eqtrd 2655 . . . . . . . 8 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
312311oveq2d 6620 . . . . . . 7 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
313308, 312eqtr4d 2658 . . . . . 6 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴𝐶) / 𝑀))))
31424, 252, 191, 192divassd 10780 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐵𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)))
315313, 314oveq12d 6622 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
316307, 315eqtr3d 2657 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
317 gzcjcl 15564 . . . . . . 7 (((𝐴𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
318276, 317syl 17 . . . . . 6 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
319 gzmulcl 15566 . . . . . 6 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
32012, 318, 319syl2anc 692 . . . . 5 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
321 gzmulcl 15566 . . . . . 6 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
322275, 279, 321syl2anc 692 . . . . 5 (𝜑 → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
323 gzsubcl 15568 . . . . 5 (((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
324320, 322, 323syl2anc 692 . . . 4 (𝜑 → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
325316, 324eqeltrd 2698 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326 4sq.1 . . . 4 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
3273264sqlem4a 15579 . . 3 ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328288, 325, 327syl2anc 692 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329232, 328eqeltrrd 2699 1 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  {cab 2607  wrex 2908  cfv 5847  (class class class)co 6604  cc 9878   + caddc 9883   · cmul 9885  cmin 10210   / cdiv 10628  cn 10964  2c2 11014  0cn0 11236  cz 11321  cexp 12800  ccj 13770  abscabs 13908  ℤ[i]cgz 15557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-sup 8292  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-z 11322  df-uz 11632  df-rp 11777  df-seq 12742  df-exp 12801  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-gz 15558
This theorem is referenced by:  mul4sq  15582  4sqlem17  15589
  Copyright terms: Public domain W3C validator