Theorem mul4sqlem 16882

Description: Lemma for mul4sq 16883: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 16890 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

Step	Hyp	Ref	Expression
1		mul4sq.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℤ[i])
2		gzcn 16861	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		mul4sq.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ[i])
5		gzcn 16861	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
8	7	absvalsqd 15385	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
9	7	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
10	7, 9	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
11	8, 10	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12		mul4sq.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ[i])
13		gzcn 16861	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
14	12, 13	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
15		mul4sq.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℤ[i])
16		gzcn 16861	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18	14, 17	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
19	18	absvalsqd 15385	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
20	18	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
21	18, 20	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
22	19, 21	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
23	11, 22	addcld 11229	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
24	3	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
25	24, 6	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
26	14	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐵) ∈ ℂ)
27	26, 17	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
28	25, 27	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
29	6	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐶) ∈ ℂ)
30	14, 29	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
31	17	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
32	3, 31	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
33	30, 32	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
34	28, 33	addcld 11229	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
35	3, 17	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
36	35	absvalsqd 15385	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
37	35	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
38	35, 37	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
39	36, 38	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
40	14, 6	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
41	40	absvalsqd 15385	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
42	40	cjcld 15139	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
43	40, 42	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
44	41, 43	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
45	39, 44	addcld 11229	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
46	23, 34, 45	ppncand 11607	. . . . 5 ⊢ (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
47	14, 31	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
48	25, 47	addcld 11229	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
49	48	absvalsqd 15385	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
50	25, 47	cjaddd 15163	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
51	24, 6	cjmuld 15164	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
52	3	cjcjd 15142	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
53	52	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
54	51, 53	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
55	14, 31	cjmuld 15164	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
56	17	cjcjd 15142	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
57	56	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
58	55, 57	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
59	54, 58	oveq12d 7423	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
60	50, 59	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
61	60	oveq2d 7421	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
62	3, 29	mulcld 11230	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
63	25, 62, 27	adddid 11234	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
64	6, 24, 3, 29	mul4d 11422	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
65	24, 6	mulcomd 11231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
66	65	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
67	3, 6	mulcomd 11231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
68	3, 6	cjmuld 15164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
69	67, 68	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
70	64, 66, 69	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
71	70, 8	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
72	71	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
73	63, 72	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
74	47, 62, 27	adddid 11234	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
75	3, 29	mulcomd 11231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
76	75	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
77	14, 31, 29, 3	mul4d 11422	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
78	31, 3	mulcomd 11231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
79	78	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
80	76, 77, 79	3eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
81	14, 31, 17, 26	mul4d 11422	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
82	26, 17	mulcomd 11231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
83	82	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
84	14, 17	cjmuld 15164	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
85	26, 31	mulcomd 11231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
86	84, 85	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
87	86	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
88	81, 83, 87	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
89	88, 19	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
90	80, 89	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
91	74, 90	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
92	73, 91	oveq12d 7423	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
93	62, 27	addcld 11229	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
94	25, 47, 93	adddird 11235	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
95	11, 22, 28, 33	add42d 11439	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
96	92, 94, 95	3eqtr4d 2782	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
97	49, 61, 96	3eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
98	24, 17	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
99	98, 30	subcld 11567	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
100	99	absvalsqd 15385	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101		cjsub 15092	. . . . . . . . . 10 ⊢ ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
102	98, 30, 101	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
103	24, 17	cjmuld 15164	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
104	52	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105	103, 104	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
106	14, 29	cjmuld 15164	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
107	6	cjcjd 15142	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108	107	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109	106, 108	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110	105, 109	oveq12d 7423	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111	102, 110	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112	111	oveq2d 7421	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
113	26, 6	mulcld 11230	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
114	32, 113	subcld 11567	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
115	98, 30, 114	subdird 11667	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
116	98, 32, 113	subdid 11666	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
117	17, 24, 3, 31	mul4d 11422	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
118	24, 17	mulcomd 11231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119	118	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
120	3, 17	mulcomd 11231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
121	3, 17	cjmuld 15164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122	120, 121	oveq12d 7423	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123	117, 119, 122	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124	123, 36	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
125	26, 6	mulcomd 11231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126	125	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
127	24, 17, 6, 26	mul4d 11422	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
128	17, 26	mulcomd 11231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129	128	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130	126, 127, 129	3eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131	124, 130	oveq12d 7423	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132	116, 131	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
133	30, 32, 113	subdid 11666	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134	125	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
135	14, 29, 6, 26	mul4d 11422	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
136	29, 26	mulcomd 11231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
137	14, 6	cjmuld 15164	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138	136, 137	eqtr4d 2775	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139	138	oveq2d 7421	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140	134, 135, 139	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141	140, 41	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142	141	oveq2d 7421	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143	133, 142	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144	132, 143	oveq12d 7423	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
145	39, 28, 33, 44	subadd4d 11615	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146	115, 144, 145	3eqtrd 2776	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147	100, 112, 146	3eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
148	97, 147	oveq12d 7423	. . . . 5 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
149	3, 24	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
150	14, 26	mulcld 11230	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
151	6, 29	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
152	17, 31	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153	151, 152	addcld 11229	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154	149, 150, 153	adddird 11235	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
155	68	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
156	3, 6, 24, 29	mul4d 11422	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
157	8, 155, 156	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158	121	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
159	3, 17, 24, 31	mul4d 11422	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
160	36, 158, 159	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161	157, 160	oveq12d 7423	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162	149, 151, 152	adddid 11234	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163	161, 162	eqtr4d 2775	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164	137	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
165	14, 6, 26, 29	mul4d 11422	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
166	41, 164, 165	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
167	84	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
168	14, 17, 26, 31	mul4d 11422	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
169	19, 167, 168	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170	166, 169	oveq12d 7423	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171	150, 151, 152	adddid 11234	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172	170, 171	eqtr4d 2775	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173	163, 172	oveq12d 7423	. . . . . . 7 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174	154, 173	eqtr4d 2775	. . . . . 6 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175		mul4sq.5	. . . . . . . 8 ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
176	3	absvalsqd 15385	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
177	14	absvalsqd 15385	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178	176, 177	oveq12d 7423	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179	175, 178	eqtrid 2784	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180		mul4sq.6	. . . . . . . 8 ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
181	6	absvalsqd 15385	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
182	17	absvalsqd 15385	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183	181, 182	oveq12d 7423	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184	180, 183	eqtrid 2784	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185	179, 184	oveq12d 7423	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
186	11, 22, 39, 44	add42d 11439	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187	174, 185, 186	3eqtr4d 2782	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
188	46, 148, 187	3eqtr4d 2782	. . . 4 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189	188	oveq1d 7420	. . 3 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190		mul4sq.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
191	190	nncnd 12224	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
192	190	nnne0d 12258	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≠ 0)
193	48, 191, 192	absdivd 15398	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194	190	nnred 12223	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
195	190	nnnn0d 12528	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
196	195	nn0ge0d 12531	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑀)
197	194, 196	absidd 15365	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝑀) = 𝑀)
198	197	oveq2d 7421	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199	193, 198	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200	199	oveq1d 7420	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
201	48	abscld 15379	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202	201	recnd 11238	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203	202, 191, 192	sqdivd 14120	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204	200, 203	eqtrd 2772	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
205	99, 191, 192	absdivd 15398	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206	197	oveq2d 7421	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207	205, 206	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208	207	oveq1d 7420	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
209	99	abscld 15379	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210	209	recnd 11238	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211	210, 191, 192	sqdivd 14120	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212	208, 211	eqtrd 2772	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213	204, 212	oveq12d 7423	. . . 4 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
214	23, 34	addcld 11229	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
215	97, 214	eqeltrd 2833	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
216	45, 34	subcld 11567	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217	147, 216	eqeltrd 2833	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218	190	nnsqcld 14203	. . . . . 6 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
219	218	nncnd 12224	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ∈ ℂ)
220	218	nnne0d 12258	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ≠ 0)
221	215, 217, 219, 220	divdird 12024	. . . 4 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222	213, 221	eqtr4d 2775	. . 3 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223	176, 149	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224	177, 150	eqeltrd 2833	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225	223, 224	addcld 11229	. . . . . 6 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226	175, 225	eqeltrid 2837	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℂ)
227	184, 153	eqeltrd 2833	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ℂ)
228	226, 191, 227, 191, 192, 192	divmuldivd 12027	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229	191	sqvald 14104	. . . . 5 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230	229	oveq2d 7421	. . . 4 ⊢ (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231	228, 230	eqtr4d 2775	. . 3 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232	189, 222, 231	3eqtr4d 2782	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233	226, 48	nncand 11572	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234	149, 150, 25, 47	addsub4d 11614	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235	179	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
236	24, 3, 6	subdid 11666	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
237	24, 3	mulcomd 11231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238	237	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239	236, 238	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240		cjsub 15092	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
241	14, 17, 240	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242	241	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
243	14, 26, 31	subdid 11666	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244	242, 243	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245	239, 244	oveq12d 7423	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246	234, 235, 245	3eqtr4d 2782	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))
247	246	oveq2d 7421	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
248	233, 247	eqtr3d 2774	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
249	248	oveq1d 7420	. . . . 5 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀))
250	3, 6	subcld 11567	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
251	24, 250	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) ∈ ℂ)
252	14, 17	subcld 11567	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℂ)
253	252	cjcld 15139	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) ∈ ℂ)
254	14, 253	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) ∈ ℂ)
255	251, 254	addcld 11229	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) ∈ ℂ)
256	226, 255, 191, 192	divsubdird 12025	. . . . 5 ⊢ (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)))
257	251, 254, 191, 192	divdird 12024	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)))
258	24, 250, 191, 192	divassd 12021	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)))
259	14, 253, 191, 192	divassd 12021	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
260	252, 191, 192	cjdivd 15166	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)))
261	194	cjred 15169	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘𝑀) = 𝑀)
262	261	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
263	260, 262	eqtrd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
264	263	oveq2d 7421	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
265	259, 264	eqtr4d 2775	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))
266	258, 265	oveq12d 7423	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
267	257, 266	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
268	267	oveq2d 7421	. . . . 5 ⊢ (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
269	249, 256, 268	3eqtrd 2776	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
270		mul4sq.10	. . . . . . 7 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)
271	270	nn0zd 12580	. . . . . 6 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272		zgz 16862	. . . . . 6 ⊢ ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273	271, 272	syl 17	. . . . 5 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274		gzcjcl 16865	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
275	1, 274	syl 17	. . . . . . 7 ⊢ (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276		mul4sq.8	. . . . . . 7 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])
277		gzmulcl 16867	. . . . . . 7 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
278	275, 276, 277	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
279		mul4sq.9	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])
280		gzcjcl 16865	. . . . . . . 8 ⊢ (((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
281	279, 280	syl 17	. . . . . . 7 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
282		gzmulcl 16867	. . . . . . 7 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
283	12, 281, 282	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
284		gzaddcl 16866	. . . . . 6 ⊢ ((((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
285	278, 283, 284	syl2anc 584	. . . . 5 ⊢ (𝜑 → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
286		gzsubcl 16869	. . . . 5 ⊢ (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
287	273, 285, 286	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
288	269, 287	eqeltrd 2833	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289	250	cjcld 15139	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) ∈ ℂ)
290	14, 289	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) ∈ ℂ)
291	24, 252	mulcld 11230	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) ∈ ℂ)
292	290, 291, 191, 192	divsubdird 12025	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)))
293		cjsub 15092	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
294	3, 6, 293	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295	294	oveq2d 7421	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
296	14, 24, 29	subdid 11666	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297	295, 296	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
298	24, 14, 17	subdid 11666	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
299	24, 14	mulcomd 11231	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300	299	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301	298, 300	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302	297, 301	oveq12d 7423	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
303	14, 24	mulcld 11230	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304	303, 30, 98	nnncan1d 11601	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305	302, 304	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306	305	oveq1d 7420	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307	292, 306	eqtr3d 2774	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
308	14, 289, 191, 192	divassd 12021	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
309	250, 191, 192	cjdivd 15166	. . . . . . . . 9 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)))
310	261	oveq2d 7421	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
311	309, 310	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
312	311	oveq2d 7421	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
313	308, 312	eqtr4d 2775	. . . . . 6 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))))
314	24, 252, 191, 192	divassd 12021	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))
315	313, 314	oveq12d 7423	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
316	307, 315	eqtr3d 2774	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
317		gzcjcl 16865	. . . . . . 7 ⊢ (((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
318	276, 317	syl 17	. . . . . 6 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
319		gzmulcl 16867	. . . . . 6 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
320	12, 318, 319	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
321		gzmulcl 16867	. . . . . 6 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
322	275, 279, 321	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
323		gzsubcl 16869	. . . . 5 ⊢ (((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
324	320, 322, 323	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
325	316, 324	eqeltrd 2833	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326		4sq.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
327	326	4sqlem4a 16880	. . 3 ⊢ ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328	288, 325, 327	syl2anc 584	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329	232, 328	eqeltrrd 2834	1 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  {cab 2709  ∃wrex 3070  ‘cfv 6540  (class class class)co 7405  ℂcc 11104   + caddc 11109   · cmul 11111   − cmin 11440   / cdiv 11867  ℕcn 12208  2c2 12263  ℕ₀cn0 12468  ℤcz 12554  ↑cexp 14023  ∗ccj 15039  abscabs 15177  ℤ[i]cgz 16858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-sup 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-gz 16859

This theorem is referenced by:  mul4sq  16883  4sqlem17  16890