Theorem mul4sqlem 12390

Description: Lemma for mul4sq 12391: 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

Step	Hyp	Ref	Expression
1		mul4sq.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℤ[i])
2		gzcn 12369	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
3	1, 2	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		mul4sq.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ[i])
5		gzcn 12369	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
6	4, 5	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
8	7	absvalsqd 11190	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
9	7	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
10	7, 9	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
11	8, 10	eqeltrd 2254	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12		mul4sq.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ[i])
13		gzcn 12369	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
15		mul4sq.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℤ[i])
16		gzcn 12369	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
17	15, 16	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18	14, 17	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
19	18	absvalsqd 11190	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
20	18	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
21	18, 20	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
22	19, 21	eqeltrd 2254	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
23	11, 22	addcld 7976	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
24	3	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
25	24, 6	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
26	14	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐵) ∈ ℂ)
27	26, 17	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
28	25, 27	mulcld 7977	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
29	6	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐶) ∈ ℂ)
30	14, 29	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
31	17	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
32	3, 31	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
33	30, 32	mulcld 7977	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
34	28, 33	addcld 7976	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
35	3, 17	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
36	35	absvalsqd 11190	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
37	35	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
38	35, 37	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
39	36, 38	eqeltrd 2254	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
40	14, 6	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
41	40	absvalsqd 11190	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
42	40	cjcld 10948	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
43	40, 42	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
44	41, 43	eqeltrd 2254	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
45	39, 44	addcld 7976	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
46	23, 34, 45	ppncand 8307	. . . . 5 ⊢ (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
47	14, 31	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
48	25, 47	addcld 7976	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
49	48	absvalsqd 11190	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
50	25, 47	cjaddd 10973	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
51	24, 6	cjmuld 10974	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
52	3	cjcjd 10951	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
53	52	oveq1d 5889	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
54	51, 53	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
55	14, 31	cjmuld 10974	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
56	17	cjcjd 10951	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
57	56	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
58	55, 57	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
59	54, 58	oveq12d 5892	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
60	50, 59	eqtrd 2210	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
61	60	oveq2d 5890	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
62	3, 29	mulcld 7977	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
63	25, 62, 27	adddid 7981	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
64	6, 24, 3, 29	mul4d 8111	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
65	24, 6	mulcomd 7978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
66	65	oveq1d 5889	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
67	3, 6	mulcomd 7978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
68	3, 6	cjmuld 10974	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
69	67, 68	oveq12d 5892	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
70	64, 66, 69	3eqtr4d 2220	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
71	70, 8	eqtr4d 2213	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
72	71	oveq1d 5889	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
73	63, 72	eqtrd 2210	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
74	47, 62, 27	adddid 7981	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
75	3, 29	mulcomd 7978	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
76	75	oveq2d 5890	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
77	14, 31, 29, 3	mul4d 8111	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
78	31, 3	mulcomd 7978	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
79	78	oveq2d 5890	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
80	76, 77, 79	3eqtrd 2214	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
81	14, 31, 17, 26	mul4d 8111	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
82	26, 17	mulcomd 7978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
83	82	oveq2d 5890	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
84	14, 17	cjmuld 10974	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
85	26, 31	mulcomd 7978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
86	84, 85	eqtrd 2210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
87	86	oveq2d 5890	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
88	81, 83, 87	3eqtr4d 2220	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
89	88, 19	eqtr4d 2213	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
90	80, 89	oveq12d 5892	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
91	74, 90	eqtrd 2210	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
92	73, 91	oveq12d 5892	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
93	62, 27	addcld 7976	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
94	25, 47, 93	adddird 7982	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
95	11, 22, 28, 33	add42d 8126	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
96	92, 94, 95	3eqtr4d 2220	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
97	49, 61, 96	3eqtrd 2214	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
98	24, 17	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
99	98, 30	subcld 8267	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
100	99	absvalsqd 11190	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101		cjsub 10900	. . . . . . . . . 10 ⊢ ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
102	98, 30, 101	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
103	24, 17	cjmuld 10974	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
104	52	oveq1d 5889	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105	103, 104	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
106	14, 29	cjmuld 10974	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
107	6	cjcjd 10951	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108	107	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109	106, 108	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110	105, 109	oveq12d 5892	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111	102, 110	eqtrd 2210	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112	111	oveq2d 5890	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
113	26, 6	mulcld 7977	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
114	32, 113	subcld 8267	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
115	98, 30, 114	subdird 8371	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
116	98, 32, 113	subdid 8370	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
117	17, 24, 3, 31	mul4d 8111	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
118	24, 17	mulcomd 7978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119	118	oveq1d 5889	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
120	3, 17	mulcomd 7978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
121	3, 17	cjmuld 10974	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122	120, 121	oveq12d 5892	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123	117, 119, 122	3eqtr4d 2220	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124	123, 36	eqtr4d 2213	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
125	26, 6	mulcomd 7978	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126	125	oveq2d 5890	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
127	24, 17, 6, 26	mul4d 8111	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
128	17, 26	mulcomd 7978	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129	128	oveq2d 5890	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130	126, 127, 129	3eqtrd 2214	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131	124, 130	oveq12d 5892	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132	116, 131	eqtrd 2210	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
133	30, 32, 113	subdid 8370	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134	125	oveq2d 5890	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
135	14, 29, 6, 26	mul4d 8111	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
136	29, 26	mulcomd 7978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
137	14, 6	cjmuld 10974	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138	136, 137	eqtr4d 2213	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139	138	oveq2d 5890	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140	134, 135, 139	3eqtrd 2214	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141	140, 41	eqtr4d 2213	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142	141	oveq2d 5890	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143	133, 142	eqtrd 2210	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144	132, 143	oveq12d 5892	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
145	39, 28, 33, 44	subadd4d 8315	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146	115, 144, 145	3eqtrd 2214	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147	100, 112, 146	3eqtrd 2214	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
148	97, 147	oveq12d 5892	. . . . 5 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
149	3, 24	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
150	14, 26	mulcld 7977	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
151	6, 29	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
152	17, 31	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153	151, 152	addcld 7976	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154	149, 150, 153	adddird 7982	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
155	68	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
156	3, 6, 24, 29	mul4d 8111	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
157	8, 155, 156	3eqtrd 2214	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158	121	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
159	3, 17, 24, 31	mul4d 8111	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
160	36, 158, 159	3eqtrd 2214	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161	157, 160	oveq12d 5892	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162	149, 151, 152	adddid 7981	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163	161, 162	eqtr4d 2213	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164	137	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
165	14, 6, 26, 29	mul4d 8111	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
166	41, 164, 165	3eqtrd 2214	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
167	84	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
168	14, 17, 26, 31	mul4d 8111	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
169	19, 167, 168	3eqtrd 2214	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170	166, 169	oveq12d 5892	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171	150, 151, 152	adddid 7981	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172	170, 171	eqtr4d 2213	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173	163, 172	oveq12d 5892	. . . . . . 7 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174	154, 173	eqtr4d 2213	. . . . . 6 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175		mul4sq.5	. . . . . . . 8 ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
176	3	absvalsqd 11190	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
177	14	absvalsqd 11190	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178	176, 177	oveq12d 5892	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179	175, 178	eqtrid 2222	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180		mul4sq.6	. . . . . . . 8 ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
181	6	absvalsqd 11190	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
182	17	absvalsqd 11190	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183	181, 182	oveq12d 5892	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184	180, 183	eqtrid 2222	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185	179, 184	oveq12d 5892	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
186	11, 22, 39, 44	add42d 8126	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187	174, 185, 186	3eqtr4d 2220	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
188	46, 148, 187	3eqtr4d 2220	. . . 4 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189	188	oveq1d 5889	. . 3 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190		mul4sq.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
191	190	nncnd 8932	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
192	190	nnap0d 8964	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 # 0)
193	48, 191, 192	absdivapd 11203	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194	190	nnred 8931	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
195	190	nnnn0d 9228	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
196	195	nn0ge0d 9231	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑀)
197	194, 196	absidd 11175	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝑀) = 𝑀)
198	197	oveq2d 5890	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199	193, 198	eqtrd 2210	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200	199	oveq1d 5889	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
201	48	abscld 11189	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202	201	recnd 7985	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203	202, 191, 192	sqdivapd 10666	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204	200, 203	eqtrd 2210	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
205	99, 191, 192	absdivapd 11203	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206	197	oveq2d 5890	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207	205, 206	eqtrd 2210	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208	207	oveq1d 5889	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
209	99	abscld 11189	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210	209	recnd 7985	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211	210, 191, 192	sqdivapd 10666	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212	208, 211	eqtrd 2210	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213	204, 212	oveq12d 5892	. . . 4 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
214	23, 34	addcld 7976	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
215	97, 214	eqeltrd 2254	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
216	45, 34	subcld 8267	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217	147, 216	eqeltrd 2254	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218	190	nnsqcld 10674	. . . . . 6 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
219	218	nncnd 8932	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ∈ ℂ)
220	218	nnap0d 8964	. . . . 5 ⊢ (𝜑 → (𝑀↑2) # 0)
221	215, 217, 219, 220	divdirapd 8785	. . . 4 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222	213, 221	eqtr4d 2213	. . 3 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223	176, 149	eqeltrd 2254	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224	177, 150	eqeltrd 2254	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225	223, 224	addcld 7976	. . . . . 6 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226	175, 225	eqeltrid 2264	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℂ)
227	184, 153	eqeltrd 2254	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ℂ)
228	226, 191, 227, 191, 192, 192	divmuldivapd 8788	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229	191	sqvald 10650	. . . . 5 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230	229	oveq2d 5890	. . . 4 ⊢ (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231	228, 230	eqtr4d 2213	. . 3 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232	189, 222, 231	3eqtr4d 2220	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233	226, 48	nncand 8272	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234	149, 150, 25, 47	addsub4d 8314	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235	179	oveq1d 5889	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
236	24, 3, 6	subdid 8370	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
237	24, 3	mulcomd 7978	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238	237	oveq1d 5889	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239	236, 238	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240		cjsub 10900	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
241	14, 17, 240	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242	241	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
243	14, 26, 31	subdid 8370	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244	242, 243	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245	239, 244	oveq12d 5892	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246	234, 235, 245	3eqtr4d 2220	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))
247	246	oveq2d 5890	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
248	233, 247	eqtr3d 2212	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
249	248	oveq1d 5889	. . . . 5 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀))
250	3, 6	subcld 8267	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
251	24, 250	mulcld 7977	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) ∈ ℂ)
252	14, 17	subcld 8267	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℂ)
253	252	cjcld 10948	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) ∈ ℂ)
254	14, 253	mulcld 7977	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) ∈ ℂ)
255	251, 254	addcld 7976	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) ∈ ℂ)
256	226, 255, 191, 192	divsubdirapd 8786	. . . . 5 ⊢ (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)))
257	251, 254, 191, 192	divdirapd 8785	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)))
258	24, 250, 191, 192	divassapd 8782	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)))
259	14, 253, 191, 192	divassapd 8782	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
260	252, 191, 192	cjdivapd 10976	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)))
261	194	cjred 10979	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘𝑀) = 𝑀)
262	261	oveq2d 5890	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
263	260, 262	eqtrd 2210	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
264	263	oveq2d 5890	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
265	259, 264	eqtr4d 2213	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))
266	258, 265	oveq12d 5892	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
267	257, 266	eqtrd 2210	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
268	267	oveq2d 5890	. . . . 5 ⊢ (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
269	249, 256, 268	3eqtrd 2214	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
270		mul4sq.10	. . . . . . 7 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
271	270	nn0zd 9372	. . . . . 6 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272		zgz 12370	. . . . . 6 ⊢ ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273	271, 272	syl 14	. . . . 5 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274		gzcjcl 12373	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
275	1, 274	syl 14	. . . . . . 7 ⊢ (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276		mul4sq.8	. . . . . . 7 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])
277		gzmulcl 12375	. . . . . . 7 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
278	275, 276, 277	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
279		mul4sq.9	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])
280		gzcjcl 12373	. . . . . . . 8 ⊢ (((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
281	279, 280	syl 14	. . . . . . 7 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
282		gzmulcl 12375	. . . . . . 7 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
283	12, 281, 282	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
284		gzaddcl 12374	. . . . . 6 ⊢ ((((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
285	278, 283, 284	syl2anc 411	. . . . 5 ⊢ (𝜑 → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
286		gzsubcl 12377	. . . . 5 ⊢ (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
287	273, 285, 286	syl2anc 411	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
288	269, 287	eqeltrd 2254	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289	250	cjcld 10948	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) ∈ ℂ)
290	14, 289	mulcld 7977	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) ∈ ℂ)
291	24, 252	mulcld 7977	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) ∈ ℂ)
292	290, 291, 191, 192	divsubdirapd 8786	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)))
293		cjsub 10900	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
294	3, 6, 293	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295	294	oveq2d 5890	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
296	14, 24, 29	subdid 8370	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297	295, 296	eqtrd 2210	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
298	24, 14, 17	subdid 8370	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
299	24, 14	mulcomd 7978	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300	299	oveq1d 5889	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301	298, 300	eqtrd 2210	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302	297, 301	oveq12d 5892	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
303	14, 24	mulcld 7977	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304	303, 30, 98	nnncan1d 8301	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305	302, 304	eqtrd 2210	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306	305	oveq1d 5889	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307	292, 306	eqtr3d 2212	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
308	14, 289, 191, 192	divassapd 8782	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
309	250, 191, 192	cjdivapd 10976	. . . . . . . . 9 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)))
310	261	oveq2d 5890	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
311	309, 310	eqtrd 2210	. . . . . . . 8 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
312	311	oveq2d 5890	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
313	308, 312	eqtr4d 2213	. . . . . 6 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))))
314	24, 252, 191, 192	divassapd 8782	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))
315	313, 314	oveq12d 5892	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
316	307, 315	eqtr3d 2212	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
317		gzcjcl 12373	. . . . . . 7 ⊢ (((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
318	276, 317	syl 14	. . . . . 6 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
319		gzmulcl 12375	. . . . . 6 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
320	12, 318, 319	syl2anc 411	. . . . 5 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
321		gzmulcl 12375	. . . . . 6 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
322	275, 279, 321	syl2anc 411	. . . . 5 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
323		gzsubcl 12377	. . . . 5 ⊢ (((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
324	320, 322, 323	syl2anc 411	. . . 4 ⊢ (𝜑 → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
325	316, 324	eqeltrd 2254	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326		4sq.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
327	326	4sqlem4a 12388	. . 3 ⊢ ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328	288, 325, 327	syl2anc 411	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329	232, 328	eqeltrrd 2255	1 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  {cab 2163  ∃wrex 2456  ‘cfv 5216  (class class class)co 5874  ℂcc 7808   + caddc 7813   · cmul 7815   − cmin 8127   / cdiv 8628  ℕcn 8918  2c2 8969  ℕ₀cn0 9175  ℤcz 9252  ↑cexp 10518  ∗ccj 10847  abscabs 11005  ℤ[i]cgz 12366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-frec 6391  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-n0 9176  df-z 9253  df-uz 9528  df-rp 9653  df-seqfrec 10445  df-exp 10519  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-gz 12367

This theorem is referenced by:  mul4sq  12391