ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mul4sqlem GIF version

Theorem mul4sqlem 12338
Description: Lemma for mul4sq 12339: algebraic manipulations. The extra assumptions involving 𝑀 would let us 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 12317 . . . . . . . . . . 11 (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
31, 2syl 14 . . . . . . . . . 10 (𝜑𝐴 ∈ ℂ)
4 mul4sq.3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℤ[i])
5 gzcn 12317 . . . . . . . . . . 11 (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
64, 5syl 14 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
73, 6mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
87absvalsqd 11139 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
97cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
107, 9mulcld 7933 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
118, 10eqeltrd 2247 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12 mul4sq.2 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℤ[i])
13 gzcn 12317 . . . . . . . . . . 11 (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
1412, 13syl 14 . . . . . . . . . 10 (𝜑𝐵 ∈ ℂ)
15 mul4sq.4 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℤ[i])
16 gzcn 12317 . . . . . . . . . . 11 (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
1715, 16syl 14 . . . . . . . . . 10 (𝜑𝐷 ∈ ℂ)
1814, 17mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
1918absvalsqd 11139 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
2018cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
2118, 20mulcld 7933 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
2219, 21eqeltrd 2247 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
2311, 22addcld 7932 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
243cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘𝐴) ∈ ℂ)
2524, 6mulcld 7933 . . . . . . . 8 (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
2614cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘𝐵) ∈ ℂ)
2726, 17mulcld 7933 . . . . . . . 8 (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
2825, 27mulcld 7933 . . . . . . 7 (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
296cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘𝐶) ∈ ℂ)
3014, 29mulcld 7933 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
3117cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘𝐷) ∈ ℂ)
323, 31mulcld 7933 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
3330, 32mulcld 7933 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
3428, 33addcld 7932 . . . . . 6 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
353, 17mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
3635absvalsqd 11139 . . . . . . . 8 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
3735cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
3835, 37mulcld 7933 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
3936, 38eqeltrd 2247 . . . . . . 7 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
4014, 6mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
4140absvalsqd 11139 . . . . . . . 8 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
4240cjcld 10897 . . . . . . . . 9 (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
4340, 42mulcld 7933 . . . . . . . 8 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
4441, 43eqeltrd 2247 . . . . . . 7 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
4539, 44addcld 7932 . . . . . 6 (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
4623, 34, 45ppncand 8263 . . . . 5 (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
4714, 31mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
4825, 47addcld 7932 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
4948absvalsqd 11139 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
5025, 47cjaddd 10922 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
5124, 6cjmuld 10923 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
523cjcjd 10900 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
5352oveq1d 5866 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
5451, 53eqtrd 2203 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
5514, 31cjmuld 10923 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
5617cjcjd 10900 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
5756oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5855, 57eqtrd 2203 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
5954, 58oveq12d 5869 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6050, 59eqtrd 2203 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
6160oveq2d 5867 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
623, 29mulcld 7933 . . . . . . . . . . 11 (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
6325, 62, 27adddid 7937 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
646, 24, 3, 29mul4d 8067 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
6524, 6mulcomd 7934 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
6665oveq1d 5866 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
673, 6mulcomd 7934 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
683, 6cjmuld 10923 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
6967, 68oveq12d 5869 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
7064, 66, 693eqtr4d 2213 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
7170, 8eqtr4d 2206 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
7271oveq1d 5866 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7363, 72eqtrd 2203 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
7447, 62, 27adddid 7937 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
753, 29mulcomd 7934 . . . . . . . . . . . . 13 (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
7675oveq2d 5867 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
7714, 31, 29, 3mul4d 8067 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
7831, 3mulcomd 7934 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
7978oveq2d 5867 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8076, 77, 793eqtrd 2207 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
8114, 31, 17, 26mul4d 8067 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8226, 17mulcomd 7934 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
8382oveq2d 5867 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
8414, 17cjmuld 10923 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
8526, 31mulcomd 7934 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8684, 85eqtrd 2203 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
8786oveq2d 5867 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
8881, 83, 873eqtr4d 2213 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
8988, 19eqtr4d 2206 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
9080, 89oveq12d 5869 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9174, 90eqtrd 2203 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
9273, 91oveq12d 5869 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9362, 27addcld 7932 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
9425, 47, 93adddird 7938 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
9511, 22, 28, 33add42d 8082 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
9692, 94, 953eqtr4d 2213 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9749, 61, 963eqtrd 2207 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
9824, 17mulcld 7933 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
9998, 30subcld 8223 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
10099absvalsqd 11139 . . . . . . 7 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101 cjsub 10849 . . . . . . . . . 10 ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10298, 30, 101syl2anc 409 . . . . . . . . 9 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
10324, 17cjmuld 10923 . . . . . . . . . . 11 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
10452oveq1d 5866 . . . . . . . . . . 11 (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105103, 104eqtrd 2203 . . . . . . . . . 10 (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
10614, 29cjmuld 10923 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
1076cjcjd 10900 . . . . . . . . . . . 12 (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108107oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109106, 108eqtrd 2203 . . . . . . . . . 10 (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110105, 109oveq12d 5869 . . . . . . . . 9 (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111102, 110eqtrd 2203 . . . . . . . 8 (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112111oveq2d 5867 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
11326, 6mulcld 7933 . . . . . . . . . 10 (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
11432, 113subcld 8223 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
11598, 30, 114subdird 8327 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
11698, 32, 113subdid 8326 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
11717, 24, 3, 31mul4d 8067 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
11824, 17mulcomd 7934 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119118oveq1d 5866 . . . . . . . . . . . . 13 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
1203, 17mulcomd 7934 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
1213, 17cjmuld 10923 . . . . . . . . . . . . . 14 (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122120, 121oveq12d 5869 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123117, 119, 1223eqtr4d 2213 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124123, 36eqtr4d 2206 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
12526, 6mulcomd 7934 . . . . . . . . . . . . 13 (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126125oveq2d 5867 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
12724, 17, 6, 26mul4d 8067 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
12817, 26mulcomd 7934 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129128oveq2d 5867 . . . . . . . . . . . 12 (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130126, 127, 1293eqtrd 2207 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131124, 130oveq12d 5869 . . . . . . . . . 10 (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132116, 131eqtrd 2203 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
13330, 32, 113subdid 8326 . . . . . . . . . 10 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134125oveq2d 5867 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
13514, 29, 6, 26mul4d 8067 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
13629, 26mulcomd 7934 . . . . . . . . . . . . . . 15 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
13714, 6cjmuld 10923 . . . . . . . . . . . . . . 15 (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138136, 137eqtr4d 2206 . . . . . . . . . . . . . 14 (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139138oveq2d 5867 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140134, 135, 1393eqtrd 2207 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141140, 41eqtr4d 2206 . . . . . . . . . . 11 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142141oveq2d 5867 . . . . . . . . . 10 (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143133, 142eqtrd 2203 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144132, 143oveq12d 5869 . . . . . . . 8 (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
14539, 28, 33, 44subadd4d 8271 . . . . . . . 8 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146115, 144, 1453eqtrd 2207 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147100, 112, 1463eqtrd 2207 . . . . . 6 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
14897, 147oveq12d 5869 . . . . 5 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
1493, 24mulcld 7933 . . . . . . . 8 (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
15014, 26mulcld 7933 . . . . . . . 8 (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
1516, 29mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
15217, 31mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153151, 152addcld 7932 . . . . . . . 8 (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154149, 150, 153adddird 7938 . . . . . . 7 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
15568oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
1563, 6, 24, 29mul4d 8067 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
1578, 155, 1563eqtrd 2207 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158121oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
1593, 17, 24, 31mul4d 8067 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
16036, 158, 1593eqtrd 2207 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161157, 160oveq12d 5869 . . . . . . . . 9 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162149, 151, 152adddid 7937 . . . . . . . . 9 (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163161, 162eqtr4d 2206 . . . . . . . 8 (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164137oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
16514, 6, 26, 29mul4d 8067 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16641, 164, 1653eqtrd 2207 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
16784oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
16814, 17, 26, 31mul4d 8067 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
16919, 167, 1683eqtrd 2207 . . . . . . . . . 10 (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170166, 169oveq12d 5869 . . . . . . . . 9 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171150, 151, 152adddid 7937 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172170, 171eqtr4d 2206 . . . . . . . 8 (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173163, 172oveq12d 5869 . . . . . . 7 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174154, 173eqtr4d 2206 . . . . . 6 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175 mul4sq.5 . . . . . . . 8 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
1763absvalsqd 11139 . . . . . . . . 9 (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
17714absvalsqd 11139 . . . . . . . . 9 (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178176, 177oveq12d 5869 . . . . . . . 8 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179175, 178eqtrid 2215 . . . . . . 7 (𝜑𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180 mul4sq.6 . . . . . . . 8 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
1816absvalsqd 11139 . . . . . . . . 9 (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
18217absvalsqd 11139 . . . . . . . . 9 (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183181, 182oveq12d 5869 . . . . . . . 8 (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184180, 183eqtrid 2215 . . . . . . 7 (𝜑𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185179, 184oveq12d 5869 . . . . . 6 (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
18611, 22, 39, 44add42d 8082 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187174, 185, 1863eqtr4d 2213 . . . . 5 (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
18846, 148, 1873eqtr4d 2213 . . . 4 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189188oveq1d 5866 . . 3 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190 mul4sq.7 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
191190nncnd 8885 . . . . . . . . 9 (𝜑𝑀 ∈ ℂ)
192190nnap0d 8917 . . . . . . . . 9 (𝜑𝑀 # 0)
19348, 191, 192absdivapd 11152 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194190nnred 8884 . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
195190nnnn0d 9181 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ0)
196195nn0ge0d 9184 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑀)
197194, 196absidd 11124 . . . . . . . . 9 (𝜑 → (abs‘𝑀) = 𝑀)
198197oveq2d 5867 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199193, 198eqtrd 2203 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200199oveq1d 5866 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
20148abscld 11138 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202201recnd 7941 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203202, 191, 192sqdivapd 10615 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204200, 203eqtrd 2203 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
20599, 191, 192absdivapd 11152 . . . . . . . 8 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206197oveq2d 5867 . . . . . . . 8 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207205, 206eqtrd 2203 . . . . . . 7 (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208207oveq1d 5866 . . . . . 6 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
20999abscld 11138 . . . . . . . 8 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210209recnd 7941 . . . . . . 7 (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211210, 191, 192sqdivapd 10615 . . . . . 6 (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212208, 211eqtrd 2203 . . . . 5 (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213204, 212oveq12d 5869 . . . 4 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
21423, 34addcld 7932 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
21597, 214eqeltrd 2247 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
21645, 34subcld 8223 . . . . . 6 (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217147, 216eqeltrd 2247 . . . . 5 (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218190nnsqcld 10623 . . . . . 6 (𝜑 → (𝑀↑2) ∈ ℕ)
219218nncnd 8885 . . . . 5 (𝜑 → (𝑀↑2) ∈ ℂ)
220218nnap0d 8917 . . . . 5 (𝜑 → (𝑀↑2) # 0)
221215, 217, 219, 220divdirapd 8739 . . . 4 (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222213, 221eqtr4d 2206 . . 3 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223176, 149eqeltrd 2247 . . . . . . 7 (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224177, 150eqeltrd 2247 . . . . . . 7 (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225223, 224addcld 7932 . . . . . 6 (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226175, 225eqeltrid 2257 . . . . 5 (𝜑𝑋 ∈ ℂ)
227184, 153eqeltrd 2247 . . . . 5 (𝜑𝑌 ∈ ℂ)
228226, 191, 227, 191, 192, 192divmuldivapd 8742 . . . 4 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229191sqvald 10599 . . . . 5 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230229oveq2d 5867 . . . 4 (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231228, 230eqtr4d 2206 . . 3 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232189, 222, 2313eqtr4d 2213 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233226, 48nncand 8228 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234149, 150, 25, 47addsub4d 8270 . . . . . . . . 9 (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235179oveq1d 5866 . . . . . . . . 9 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
23624, 3, 6subdid 8326 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
23724, 3mulcomd 7934 . . . . . . . . . . . 12 (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238237oveq1d 5866 . . . . . . . . . . 11 (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239236, 238eqtrd 2203 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240 cjsub 10849 . . . . . . . . . . . . 13 ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
24114, 17, 240syl2anc 409 . . . . . . . . . . . 12 (𝜑 → (∗‘(𝐵𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242241oveq2d 5867 . . . . . . . . . . 11 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
24314, 26, 31subdid 8326 . . . . . . . . . . 11 (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244242, 243eqtrd 2203 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245239, 244oveq12d 5869 . . . . . . . . 9 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246234, 235, 2453eqtr4d 2213 . . . . . . . 8 (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))))
247246oveq2d 5867 . . . . . . 7 (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
248233, 247eqtr3d 2205 . . . . . 6 (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))))
249248oveq1d 5866 . . . . 5 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀))
2503, 6subcld 8223 . . . . . . . 8 (𝜑 → (𝐴𝐶) ∈ ℂ)
25124, 250mulcld 7933 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐴𝐶)) ∈ ℂ)
25214, 17subcld 8223 . . . . . . . . 9 (𝜑 → (𝐵𝐷) ∈ ℂ)
253252cjcld 10897 . . . . . . . 8 (𝜑 → (∗‘(𝐵𝐷)) ∈ ℂ)
25414, 253mulcld 7933 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐵𝐷))) ∈ ℂ)
255251, 254addcld 7932 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) ∈ ℂ)
256226, 255, 191, 192divsubdirapd 8740 . . . . 5 (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)))
257251, 254, 191, 192divdirapd 8739 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)))
25824, 250, 191, 192divassapd 8736 . . . . . . . 8 (𝜑 → (((∗‘𝐴) · (𝐴𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)))
25914, 253, 191, 192divassapd 8736 . . . . . . . . 9 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
260252, 191, 192cjdivapd 10925 . . . . . . . . . . 11 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / (∗‘𝑀)))
261194cjred 10928 . . . . . . . . . . . 12 (𝜑 → (∗‘𝑀) = 𝑀)
262261oveq2d 5867 . . . . . . . . . . 11 (𝜑 → ((∗‘(𝐵𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
263260, 262eqtrd 2203 . . . . . . . . . 10 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) = ((∗‘(𝐵𝐷)) / 𝑀))
264263oveq2d 5867 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵𝐷)) / 𝑀)))
265259, 264eqtr4d 2206 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))
266258, 265oveq12d 5869 . . . . . . 7 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
267257, 266eqtrd 2203 . . . . . 6 (𝜑 → ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))))
268267oveq2d 5867 . . . . 5 (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴𝐶)) + (𝐵 · (∗‘(𝐵𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
269249, 256, 2683eqtrd 2207 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))))
270 mul4sq.10 . . . . . . 7 (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
271270nn0zd 9325 . . . . . 6 (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272 zgz 12318 . . . . . 6 ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273271, 272syl 14 . . . . 5 (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274 gzcjcl 12321 . . . . . . . 8 (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
2751, 274syl 14 . . . . . . 7 (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276 mul4sq.8 . . . . . . 7 (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ[i])
277 gzmulcl 12323 . . . . . . 7 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
278275, 276, 277syl2anc 409 . . . . . 6 (𝜑 → ((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
279 mul4sq.9 . . . . . . . 8 (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ[i])
280 gzcjcl 12321 . . . . . . . 8 (((𝐵𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
281279, 280syl 14 . . . . . . 7 (𝜑 → (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
282 gzmulcl 12323 . . . . . . 7 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
28312, 281, 282syl2anc 409 . . . . . 6 (𝜑 → (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
284 gzaddcl 12322 . . . . . 6 ((((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
285278, 283, 284syl2anc 409 . . . . 5 (𝜑 → (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i])
286 gzsubcl 12325 . . . . 5 (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
287273, 285, 286syl2anc 409 . . . 4 (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵𝐷) / 𝑀))))) ∈ ℤ[i])
288269, 287eqeltrd 2247 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289250cjcld 10897 . . . . . . . 8 (𝜑 → (∗‘(𝐴𝐶)) ∈ ℂ)
29014, 289mulcld 7933 . . . . . . 7 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) ∈ ℂ)
29124, 252mulcld 7933 . . . . . . 7 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) ∈ ℂ)
292290, 291, 191, 192divsubdirapd 8740 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)))
293 cjsub 10849 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
2943, 6, 293syl2anc 409 . . . . . . . . . . 11 (𝜑 → (∗‘(𝐴𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295294oveq2d 5867 . . . . . . . . . 10 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
29614, 24, 29subdid 8326 . . . . . . . . . 10 (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297295, 296eqtrd 2203 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘(𝐴𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
29824, 14, 17subdid 8326 . . . . . . . . . 10 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
29924, 14mulcomd 7934 . . . . . . . . . . 11 (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300299oveq1d 5866 . . . . . . . . . 10 (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301298, 300eqtrd 2203 . . . . . . . . 9 (𝜑 → ((∗‘𝐴) · (𝐵𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302297, 301oveq12d 5869 . . . . . . . 8 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
30314, 24mulcld 7933 . . . . . . . . 9 (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304303, 30, 98nnncan1d 8257 . . . . . . . 8 (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305302, 304eqtrd 2203 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306305oveq1d 5866 . . . . . 6 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) − ((∗‘𝐴) · (𝐵𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307292, 306eqtr3d 2205 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
30814, 289, 191, 192divassapd 8736 . . . . . . 7 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
309250, 191, 192cjdivapd 10925 . . . . . . . . 9 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / (∗‘𝑀)))
310261oveq2d 5867 . . . . . . . . 9 (𝜑 → ((∗‘(𝐴𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
311309, 310eqtrd 2203 . . . . . . . 8 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) = ((∗‘(𝐴𝐶)) / 𝑀))
312311oveq2d 5867 . . . . . . 7 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴𝐶)) / 𝑀)))
313308, 312eqtr4d 2206 . . . . . 6 (𝜑 → ((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴𝐶) / 𝑀))))
31424, 252, 191, 192divassapd 8736 . . . . . 6 (𝜑 → (((∗‘𝐴) · (𝐵𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)))
315313, 314oveq12d 5869 . . . . 5 (𝜑 → (((𝐵 · (∗‘(𝐴𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
316307, 315eqtr3d 2205 . . . 4 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))))
317 gzcjcl 12321 . . . . . . 7 (((𝐴𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
318276, 317syl 14 . . . . . 6 (𝜑 → (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i])
319 gzmulcl 12323 . . . . . 6 ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
32012, 318, 319syl2anc 409 . . . . 5 (𝜑 → (𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i])
321 gzmulcl 12323 . . . . . 6 (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
322275, 279, 321syl2anc 409 . . . . 5 (𝜑 → ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i])
323 gzsubcl 12325 . . . . 5 (((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
324320, 322, 323syl2anc 409 . . . 4 (𝜑 → ((𝐵 · (∗‘((𝐴𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵𝐷) / 𝑀))) ∈ ℤ[i])
325316, 324eqeltrd 2247 . . 3 (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326 4sq.1 . . . 4 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
3273264sqlem4a 12336 . . 3 ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328288, 325, 327syl2anc 409 . 2 (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329232, 328eqeltrrd 2248 1 (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  wcel 2141  {cab 2156  wrex 2449  cfv 5196  (class class class)co 5851  cc 7765   + caddc 7770   · cmul 7772  cmin 8083   / cdiv 8582  cn 8871  2c2 8922  0cn0 9128  cz 9205  cexp 10468  ccj 10796  abscabs 10954  ℤ[i]cgz 12314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-mulrcl 7866  ax-addcom 7867  ax-mulcom 7868  ax-addass 7869  ax-mulass 7870  ax-distr 7871  ax-i2m1 7872  ax-0lt1 7873  ax-1rid 7874  ax-0id 7875  ax-rnegex 7876  ax-precex 7877  ax-cnre 7878  ax-pre-ltirr 7879  ax-pre-ltwlin 7880  ax-pre-lttrn 7881  ax-pre-apti 7882  ax-pre-ltadd 7883  ax-pre-mulgt0 7884  ax-pre-mulext 7885  ax-arch 7886  ax-caucvg 7887
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-recs 6282  df-frec 6368  df-pnf 7949  df-mnf 7950  df-xr 7951  df-ltxr 7952  df-le 7953  df-sub 8085  df-neg 8086  df-reap 8487  df-ap 8494  df-div 8583  df-inn 8872  df-2 8930  df-3 8931  df-4 8932  df-n0 9129  df-z 9206  df-uz 9481  df-rp 9604  df-seqfrec 10395  df-exp 10469  df-cj 10799  df-re 10800  df-im 10801  df-rsqrt 10955  df-abs 10956  df-gz 12315
This theorem is referenced by:  mul4sq  12339
  Copyright terms: Public domain W3C validator