mul4sqlem - Metamath Proof Explorer

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

Theorem mul4sqlem 16582

Description: Lemma for mul4sq 16583: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 16590 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	⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ₀)

**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 16561	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		mul4sq.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ[i])
5		gzcn 16561	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
8	7	absvalsqd 15082	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
9	7	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
10	7, 9	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
11	8, 10	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12		mul4sq.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ[i])
13		gzcn 16561	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
14	12, 13	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
15		mul4sq.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℤ[i])
16		gzcn 16561	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18	14, 17	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
19	18	absvalsqd 15082	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
20	18	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
21	18, 20	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
22	19, 21	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
23	11, 22	addcld 10925	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
24	3	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
25	24, 6	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
26	14	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐵) ∈ ℂ)
27	26, 17	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
28	25, 27	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
29	6	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐶) ∈ ℂ)
30	14, 29	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
31	17	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
32	3, 31	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
33	30, 32	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
34	28, 33	addcld 10925	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
35	3, 17	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
36	35	absvalsqd 15082	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
37	35	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
38	35, 37	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
39	36, 38	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
40	14, 6	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
41	40	absvalsqd 15082	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
42	40	cjcld 14835	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
43	40, 42	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
44	41, 43	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
45	39, 44	addcld 10925	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
46	23, 34, 45	ppncand 11302	. . . . 5 ⊢ (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
47	14, 31	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
48	25, 47	addcld 10925	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
49	48	absvalsqd 15082	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
50	25, 47	cjaddd 14859	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
51	24, 6	cjmuld 14860	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
52	3	cjcjd 14838	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
53	52	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
54	51, 53	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
55	14, 31	cjmuld 14860	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
56	17	cjcjd 14838	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
57	56	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
58	55, 57	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
59	54, 58	oveq12d 7273	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
60	50, 59	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
61	60	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
62	3, 29	mulcld 10926	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
63	25, 62, 27	adddid 10930	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
64	6, 24, 3, 29	mul4d 11117	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
65	24, 6	mulcomd 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
66	65	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
67	3, 6	mulcomd 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
68	3, 6	cjmuld 14860	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
69	67, 68	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
70	64, 66, 69	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
71	70, 8	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
72	71	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
73	63, 72	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
74	47, 62, 27	adddid 10930	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
75	3, 29	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
76	75	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
77	14, 31, 29, 3	mul4d 11117	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
78	31, 3	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
79	78	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
80	76, 77, 79	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
81	14, 31, 17, 26	mul4d 11117	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
82	26, 17	mulcomd 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
83	82	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
84	14, 17	cjmuld 14860	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
85	26, 31	mulcomd 10927	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
86	84, 85	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
87	86	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
88	81, 83, 87	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
89	88, 19	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
90	80, 89	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
91	74, 90	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
92	73, 91	oveq12d 7273	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
93	62, 27	addcld 10925	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
94	25, 47, 93	adddird 10931	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
95	11, 22, 28, 33	add42d 11134	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
96	92, 94, 95	3eqtr4d 2788	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
97	49, 61, 96	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
98	24, 17	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
99	98, 30	subcld 11262	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
100	99	absvalsqd 15082	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101		cjsub 14788	. . . . . . . . . 10 ⊢ ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
102	98, 30, 101	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
103	24, 17	cjmuld 14860	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
104	52	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105	103, 104	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
106	14, 29	cjmuld 14860	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
107	6	cjcjd 14838	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108	107	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109	106, 108	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110	105, 109	oveq12d 7273	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111	102, 110	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112	111	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
113	26, 6	mulcld 10926	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
114	32, 113	subcld 11262	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
115	98, 30, 114	subdird 11362	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
116	98, 32, 113	subdid 11361	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
117	17, 24, 3, 31	mul4d 11117	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
118	24, 17	mulcomd 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119	118	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
120	3, 17	mulcomd 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
121	3, 17	cjmuld 14860	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122	120, 121	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123	117, 119, 122	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124	123, 36	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
125	26, 6	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126	125	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
127	24, 17, 6, 26	mul4d 11117	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
128	17, 26	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129	128	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130	126, 127, 129	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131	124, 130	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132	116, 131	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
133	30, 32, 113	subdid 11361	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134	125	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
135	14, 29, 6, 26	mul4d 11117	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
136	29, 26	mulcomd 10927	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
137	14, 6	cjmuld 14860	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138	136, 137	eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139	138	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140	134, 135, 139	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141	140, 41	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142	141	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143	133, 142	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144	132, 143	oveq12d 7273	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
145	39, 28, 33, 44	subadd4d 11310	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146	115, 144, 145	3eqtrd 2782	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147	100, 112, 146	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
148	97, 147	oveq12d 7273	. . . . 5 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
149	3, 24	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
150	14, 26	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
151	6, 29	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
152	17, 31	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153	151, 152	addcld 10925	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154	149, 150, 153	adddird 10931	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
155	68	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
156	3, 6, 24, 29	mul4d 11117	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
157	8, 155, 156	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158	121	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
159	3, 17, 24, 31	mul4d 11117	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
160	36, 158, 159	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161	157, 160	oveq12d 7273	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162	149, 151, 152	adddid 10930	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163	161, 162	eqtr4d 2781	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164	137	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
165	14, 6, 26, 29	mul4d 11117	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
166	41, 164, 165	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
167	84	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
168	14, 17, 26, 31	mul4d 11117	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
169	19, 167, 168	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170	166, 169	oveq12d 7273	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171	150, 151, 152	adddid 10930	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172	170, 171	eqtr4d 2781	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173	163, 172	oveq12d 7273	. . . . . . 7 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174	154, 173	eqtr4d 2781	. . . . . 6 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175		mul4sq.5	. . . . . . . 8 ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
176	3	absvalsqd 15082	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
177	14	absvalsqd 15082	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178	176, 177	oveq12d 7273	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179	175, 178	eqtrid 2790	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180		mul4sq.6	. . . . . . . 8 ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
181	6	absvalsqd 15082	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
182	17	absvalsqd 15082	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183	181, 182	oveq12d 7273	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184	180, 183	eqtrid 2790	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185	179, 184	oveq12d 7273	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
186	11, 22, 39, 44	add42d 11134	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187	174, 185, 186	3eqtr4d 2788	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
188	46, 148, 187	3eqtr4d 2788	. . . 4 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189	188	oveq1d 7270	. . 3 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190		mul4sq.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
191	190	nncnd 11919	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
192	190	nnne0d 11953	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≠ 0)
193	48, 191, 192	absdivd 15095	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194	190	nnred 11918	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
195	190	nnnn0d 12223	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
196	195	nn0ge0d 12226	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑀)
197	194, 196	absidd 15062	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝑀) = 𝑀)
198	197	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199	193, 198	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200	199	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
201	48	abscld 15076	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202	201	recnd 10934	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203	202, 191, 192	sqdivd 13805	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204	200, 203	eqtrd 2778	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
205	99, 191, 192	absdivd 15095	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206	197	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207	205, 206	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208	207	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
209	99	abscld 15076	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210	209	recnd 10934	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211	210, 191, 192	sqdivd 13805	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212	208, 211	eqtrd 2778	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213	204, 212	oveq12d 7273	. . . 4 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
214	23, 34	addcld 10925	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
215	97, 214	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
216	45, 34	subcld 11262	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217	147, 216	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218	190	nnsqcld 13887	. . . . . 6 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
219	218	nncnd 11919	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ∈ ℂ)
220	218	nnne0d 11953	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ≠ 0)
221	215, 217, 219, 220	divdird 11719	. . . 4 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222	213, 221	eqtr4d 2781	. . 3 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223	176, 149	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224	177, 150	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225	223, 224	addcld 10925	. . . . . 6 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226	175, 225	eqeltrid 2843	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℂ)
227	184, 153	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ℂ)
228	226, 191, 227, 191, 192, 192	divmuldivd 11722	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229	191	sqvald 13789	. . . . 5 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230	229	oveq2d 7271	. . . 4 ⊢ (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231	228, 230	eqtr4d 2781	. . 3 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232	189, 222, 231	3eqtr4d 2788	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233	226, 48	nncand 11267	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234	149, 150, 25, 47	addsub4d 11309	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235	179	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
236	24, 3, 6	subdid 11361	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
237	24, 3	mulcomd 10927	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238	237	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239	236, 238	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240		cjsub 14788	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
241	14, 17, 240	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242	241	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
243	14, 26, 31	subdid 11361	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244	242, 243	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245	239, 244	oveq12d 7273	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246	234, 235, 245	3eqtr4d 2788	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))
247	246	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
248	233, 247	eqtr3d 2780	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
249	248	oveq1d 7270	. . . . 5 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀))
250	3, 6	subcld 11262	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
251	24, 250	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) ∈ ℂ)
252	14, 17	subcld 11262	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℂ)
253	252	cjcld 14835	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) ∈ ℂ)
254	14, 253	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) ∈ ℂ)
255	251, 254	addcld 10925	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) ∈ ℂ)
256	226, 255, 191, 192	divsubdird 11720	. . . . 5 ⊢ (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)))
257	251, 254, 191, 192	divdird 11719	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)))
258	24, 250, 191, 192	divassd 11716	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)))
259	14, 253, 191, 192	divassd 11716	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
260	252, 191, 192	cjdivd 14862	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)))
261	194	cjred 14865	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘𝑀) = 𝑀)
262	261	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
263	260, 262	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
264	263	oveq2d 7271	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
265	259, 264	eqtr4d 2781	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))
266	258, 265	oveq12d 7273	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
267	257, 266	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
268	267	oveq2d 7271	. . . . 5 ⊢ (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
269	249, 256, 268	3eqtrd 2782	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
270		mul4sq.10	. . . . . . 7 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ₀)
271	270	nn0zd 12353	. . . . . 6 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272		zgz 16562	. . . . . 6 ⊢ ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273	271, 272	syl 17	. . . . 5 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274		gzcjcl 16565	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
275	1, 274	syl 17	. . . . . . 7 ⊢ (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276		mul4sq.8	. . . . . . 7 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])
277		gzmulcl 16567	. . . . . . 7 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
278	275, 276, 277	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
279		mul4sq.9	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])
280		gzcjcl 16565	. . . . . . . 8 ⊢ (((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
281	279, 280	syl 17	. . . . . . 7 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
282		gzmulcl 16567	. . . . . . 7 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
283	12, 281, 282	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
284		gzaddcl 16566	. . . . . 6 ⊢ ((((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
285	278, 283, 284	syl2anc 583	. . . . 5 ⊢ (𝜑 → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
286		gzsubcl 16569	. . . . 5 ⊢ (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
287	273, 285, 286	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
288	269, 287	eqeltrd 2839	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289	250	cjcld 14835	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) ∈ ℂ)
290	14, 289	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) ∈ ℂ)
291	24, 252	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) ∈ ℂ)
292	290, 291, 191, 192	divsubdird 11720	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)))
293		cjsub 14788	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
294	3, 6, 293	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295	294	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
296	14, 24, 29	subdid 11361	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297	295, 296	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
298	24, 14, 17	subdid 11361	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
299	24, 14	mulcomd 10927	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300	299	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301	298, 300	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302	297, 301	oveq12d 7273	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
303	14, 24	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304	303, 30, 98	nnncan1d 11296	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305	302, 304	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306	305	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307	292, 306	eqtr3d 2780	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
308	14, 289, 191, 192	divassd 11716	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
309	250, 191, 192	cjdivd 14862	. . . . . . . . 9 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)))
310	261	oveq2d 7271	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
311	309, 310	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
312	311	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
313	308, 312	eqtr4d 2781	. . . . . 6 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))))
314	24, 252, 191, 192	divassd 11716	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))
315	313, 314	oveq12d 7273	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
316	307, 315	eqtr3d 2780	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
317		gzcjcl 16565	. . . . . . 7 ⊢ (((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
318	276, 317	syl 17	. . . . . 6 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
319		gzmulcl 16567	. . . . . 6 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
320	12, 318, 319	syl2anc 583	. . . . 5 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
321		gzmulcl 16567	. . . . . 6 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
322	275, 279, 321	syl2anc 583	. . . . 5 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
323		gzsubcl 16569	. . . . 5 ⊢ (((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
324	320, 322, 323	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
325	316, 324	eqeltrd 2839	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326		4sq.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
327	326	4sqlem4a 16580	. . 3 ⊢ ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328	288, 325, 327	syl2anc 583	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329	232, 328	eqeltrrd 2840	1 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2108 {cab 2715 ∃wrex 3064 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 + caddc 10805 · cmul 10807 − cmin 11135 / cdiv 11562 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤcz 12249 ↑cexp 13710 ∗ccj 14735 abscabs 14873 ℤ[i]cgz 16558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-gz 16559

This theorem is referenced by: mul4sq 16583 4sqlem17 16590

W3C validator