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 16289

Description: Lemma for mul4sq 16290: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 16297 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 16268	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
3	1, 2	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		mul4sq.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ[i])
5		gzcn 16268	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
8	7	absvalsqd 14802	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
9	7	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
10	7, 9	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
11	8, 10	eqeltrd 2913	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12		mul4sq.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ[i])
13		gzcn 16268	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
14	12, 13	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
15		mul4sq.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℤ[i])
16		gzcn 16268	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18	14, 17	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
19	18	absvalsqd 14802	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
20	18	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
21	18, 20	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
22	19, 21	eqeltrd 2913	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
23	11, 22	addcld 10660	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
24	3	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
25	24, 6	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
26	14	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐵) ∈ ℂ)
27	26, 17	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
28	25, 27	mulcld 10661	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
29	6	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐶) ∈ ℂ)
30	14, 29	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
31	17	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
32	3, 31	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
33	30, 32	mulcld 10661	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
34	28, 33	addcld 10660	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
35	3, 17	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
36	35	absvalsqd 14802	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
37	35	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
38	35, 37	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
39	36, 38	eqeltrd 2913	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
40	14, 6	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
41	40	absvalsqd 14802	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
42	40	cjcld 14555	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
43	40, 42	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
44	41, 43	eqeltrd 2913	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
45	39, 44	addcld 10660	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
46	23, 34, 45	ppncand 11037	. . . . 5 ⊢ (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
47	14, 31	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
48	25, 47	addcld 10660	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
49	48	absvalsqd 14802	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
50	25, 47	cjaddd 14579	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
51	24, 6	cjmuld 14580	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
52	3	cjcjd 14558	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
53	52	oveq1d 7171	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
54	51, 53	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
55	14, 31	cjmuld 14580	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
56	17	cjcjd 14558	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
57	56	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
58	55, 57	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
59	54, 58	oveq12d 7174	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
60	50, 59	eqtrd 2856	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
61	60	oveq2d 7172	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
62	3, 29	mulcld 10661	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
63	25, 62, 27	adddid 10665	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
64	6, 24, 3, 29	mul4d 10852	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
65	24, 6	mulcomd 10662	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
66	65	oveq1d 7171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
67	3, 6	mulcomd 10662	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
68	3, 6	cjmuld 14580	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
69	67, 68	oveq12d 7174	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
70	64, 66, 69	3eqtr4d 2866	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
71	70, 8	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
72	71	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
73	63, 72	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
74	47, 62, 27	adddid 10665	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
75	3, 29	mulcomd 10662	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
76	75	oveq2d 7172	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
77	14, 31, 29, 3	mul4d 10852	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
78	31, 3	mulcomd 10662	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
79	78	oveq2d 7172	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
80	76, 77, 79	3eqtrd 2860	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
81	14, 31, 17, 26	mul4d 10852	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
82	26, 17	mulcomd 10662	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
83	82	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
84	14, 17	cjmuld 14580	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
85	26, 31	mulcomd 10662	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
86	84, 85	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
87	86	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
88	81, 83, 87	3eqtr4d 2866	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
89	88, 19	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
90	80, 89	oveq12d 7174	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
91	74, 90	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
92	73, 91	oveq12d 7174	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
93	62, 27	addcld 10660	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
94	25, 47, 93	adddird 10666	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
95	11, 22, 28, 33	add42d 10869	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
96	92, 94, 95	3eqtr4d 2866	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
97	49, 61, 96	3eqtrd 2860	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
98	24, 17	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
99	98, 30	subcld 10997	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
100	99	absvalsqd 14802	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101		cjsub 14508	. . . . . . . . . 10 ⊢ ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
102	98, 30, 101	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
103	24, 17	cjmuld 14580	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
104	52	oveq1d 7171	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105	103, 104	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
106	14, 29	cjmuld 14580	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
107	6	cjcjd 14558	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108	107	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109	106, 108	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110	105, 109	oveq12d 7174	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111	102, 110	eqtrd 2856	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112	111	oveq2d 7172	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
113	26, 6	mulcld 10661	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
114	32, 113	subcld 10997	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
115	98, 30, 114	subdird 11097	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
116	98, 32, 113	subdid 11096	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
117	17, 24, 3, 31	mul4d 10852	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
118	24, 17	mulcomd 10662	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119	118	oveq1d 7171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
120	3, 17	mulcomd 10662	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
121	3, 17	cjmuld 14580	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122	120, 121	oveq12d 7174	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123	117, 119, 122	3eqtr4d 2866	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124	123, 36	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
125	26, 6	mulcomd 10662	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126	125	oveq2d 7172	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
127	24, 17, 6, 26	mul4d 10852	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
128	17, 26	mulcomd 10662	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129	128	oveq2d 7172	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130	126, 127, 129	3eqtrd 2860	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131	124, 130	oveq12d 7174	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132	116, 131	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
133	30, 32, 113	subdid 11096	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134	125	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
135	14, 29, 6, 26	mul4d 10852	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
136	29, 26	mulcomd 10662	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
137	14, 6	cjmuld 14580	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138	136, 137	eqtr4d 2859	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139	138	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140	134, 135, 139	3eqtrd 2860	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141	140, 41	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142	141	oveq2d 7172	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143	133, 142	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144	132, 143	oveq12d 7174	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
145	39, 28, 33, 44	subadd4d 11045	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146	115, 144, 145	3eqtrd 2860	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147	100, 112, 146	3eqtrd 2860	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
148	97, 147	oveq12d 7174	. . . . 5 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
149	3, 24	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
150	14, 26	mulcld 10661	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
151	6, 29	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
152	17, 31	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153	151, 152	addcld 10660	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154	149, 150, 153	adddird 10666	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
155	68	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
156	3, 6, 24, 29	mul4d 10852	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
157	8, 155, 156	3eqtrd 2860	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158	121	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
159	3, 17, 24, 31	mul4d 10852	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
160	36, 158, 159	3eqtrd 2860	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161	157, 160	oveq12d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162	149, 151, 152	adddid 10665	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163	161, 162	eqtr4d 2859	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164	137	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
165	14, 6, 26, 29	mul4d 10852	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
166	41, 164, 165	3eqtrd 2860	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
167	84	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
168	14, 17, 26, 31	mul4d 10852	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
169	19, 167, 168	3eqtrd 2860	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170	166, 169	oveq12d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171	150, 151, 152	adddid 10665	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172	170, 171	eqtr4d 2859	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173	163, 172	oveq12d 7174	. . . . . . 7 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174	154, 173	eqtr4d 2859	. . . . . 6 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175		mul4sq.5	. . . . . . . 8 ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
176	3	absvalsqd 14802	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
177	14	absvalsqd 14802	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178	176, 177	oveq12d 7174	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179	175, 178	syl5eq 2868	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180		mul4sq.6	. . . . . . . 8 ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
181	6	absvalsqd 14802	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
182	17	absvalsqd 14802	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183	181, 182	oveq12d 7174	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184	180, 183	syl5eq 2868	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185	179, 184	oveq12d 7174	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
186	11, 22, 39, 44	add42d 10869	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187	174, 185, 186	3eqtr4d 2866	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
188	46, 148, 187	3eqtr4d 2866	. . . 4 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189	188	oveq1d 7171	. . 3 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190		mul4sq.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
191	190	nncnd 11654	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
192	190	nnne0d 11688	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≠ 0)
193	48, 191, 192	absdivd 14815	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194	190	nnred 11653	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
195	190	nnnn0d 11956	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
196	195	nn0ge0d 11959	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑀)
197	194, 196	absidd 14782	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝑀) = 𝑀)
198	197	oveq2d 7172	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199	193, 198	eqtrd 2856	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200	199	oveq1d 7171	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
201	48	abscld 14796	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202	201	recnd 10669	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203	202, 191, 192	sqdivd 13524	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204	200, 203	eqtrd 2856	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
205	99, 191, 192	absdivd 14815	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206	197	oveq2d 7172	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207	205, 206	eqtrd 2856	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208	207	oveq1d 7171	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
209	99	abscld 14796	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210	209	recnd 10669	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211	210, 191, 192	sqdivd 13524	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212	208, 211	eqtrd 2856	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213	204, 212	oveq12d 7174	. . . 4 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
214	23, 34	addcld 10660	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
215	97, 214	eqeltrd 2913	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
216	45, 34	subcld 10997	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217	147, 216	eqeltrd 2913	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218	190	nnsqcld 13606	. . . . . 6 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
219	218	nncnd 11654	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ∈ ℂ)
220	218	nnne0d 11688	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ≠ 0)
221	215, 217, 219, 220	divdird 11454	. . . 4 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222	213, 221	eqtr4d 2859	. . 3 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223	176, 149	eqeltrd 2913	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224	177, 150	eqeltrd 2913	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225	223, 224	addcld 10660	. . . . . 6 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226	175, 225	eqeltrid 2917	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℂ)
227	184, 153	eqeltrd 2913	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ℂ)
228	226, 191, 227, 191, 192, 192	divmuldivd 11457	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229	191	sqvald 13508	. . . . 5 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230	229	oveq2d 7172	. . . 4 ⊢ (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231	228, 230	eqtr4d 2859	. . 3 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232	189, 222, 231	3eqtr4d 2866	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233	226, 48	nncand 11002	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234	149, 150, 25, 47	addsub4d 11044	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235	179	oveq1d 7171	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
236	24, 3, 6	subdid 11096	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
237	24, 3	mulcomd 10662	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238	237	oveq1d 7171	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239	236, 238	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240		cjsub 14508	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
241	14, 17, 240	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242	241	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
243	14, 26, 31	subdid 11096	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244	242, 243	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245	239, 244	oveq12d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246	234, 235, 245	3eqtr4d 2866	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))
247	246	oveq2d 7172	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
248	233, 247	eqtr3d 2858	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
249	248	oveq1d 7171	. . . . 5 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀))
250	3, 6	subcld 10997	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
251	24, 250	mulcld 10661	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) ∈ ℂ)
252	14, 17	subcld 10997	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℂ)
253	252	cjcld 14555	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) ∈ ℂ)
254	14, 253	mulcld 10661	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) ∈ ℂ)
255	251, 254	addcld 10660	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) ∈ ℂ)
256	226, 255, 191, 192	divsubdird 11455	. . . . 5 ⊢ (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)))
257	251, 254, 191, 192	divdird 11454	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)))
258	24, 250, 191, 192	divassd 11451	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)))
259	14, 253, 191, 192	divassd 11451	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
260	252, 191, 192	cjdivd 14582	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)))
261	194	cjred 14585	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘𝑀) = 𝑀)
262	261	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
263	260, 262	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
264	263	oveq2d 7172	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
265	259, 264	eqtr4d 2859	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))
266	258, 265	oveq12d 7174	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
267	257, 266	eqtrd 2856	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
268	267	oveq2d 7172	. . . . 5 ⊢ (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
269	249, 256, 268	3eqtrd 2860	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
270		mul4sq.10	. . . . . . 7 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ₀)
271	270	nn0zd 12086	. . . . . 6 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272		zgz 16269	. . . . . 6 ⊢ ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273	271, 272	syl 17	. . . . 5 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274		gzcjcl 16272	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
275	1, 274	syl 17	. . . . . . 7 ⊢ (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276		mul4sq.8	. . . . . . 7 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])
277		gzmulcl 16274	. . . . . . 7 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
278	275, 276, 277	syl2anc 586	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
279		mul4sq.9	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])
280		gzcjcl 16272	. . . . . . . 8 ⊢ (((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
281	279, 280	syl 17	. . . . . . 7 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
282		gzmulcl 16274	. . . . . . 7 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
283	12, 281, 282	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
284		gzaddcl 16273	. . . . . 6 ⊢ ((((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
285	278, 283, 284	syl2anc 586	. . . . 5 ⊢ (𝜑 → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
286		gzsubcl 16276	. . . . 5 ⊢ (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
287	273, 285, 286	syl2anc 586	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
288	269, 287	eqeltrd 2913	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289	250	cjcld 14555	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) ∈ ℂ)
290	14, 289	mulcld 10661	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) ∈ ℂ)
291	24, 252	mulcld 10661	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) ∈ ℂ)
292	290, 291, 191, 192	divsubdird 11455	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)))
293		cjsub 14508	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
294	3, 6, 293	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295	294	oveq2d 7172	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
296	14, 24, 29	subdid 11096	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297	295, 296	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
298	24, 14, 17	subdid 11096	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
299	24, 14	mulcomd 10662	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300	299	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301	298, 300	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302	297, 301	oveq12d 7174	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
303	14, 24	mulcld 10661	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304	303, 30, 98	nnncan1d 11031	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305	302, 304	eqtrd 2856	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306	305	oveq1d 7171	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307	292, 306	eqtr3d 2858	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
308	14, 289, 191, 192	divassd 11451	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
309	250, 191, 192	cjdivd 14582	. . . . . . . . 9 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)))
310	261	oveq2d 7172	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
311	309, 310	eqtrd 2856	. . . . . . . 8 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
312	311	oveq2d 7172	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
313	308, 312	eqtr4d 2859	. . . . . 6 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))))
314	24, 252, 191, 192	divassd 11451	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))
315	313, 314	oveq12d 7174	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
316	307, 315	eqtr3d 2858	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
317		gzcjcl 16272	. . . . . . 7 ⊢ (((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
318	276, 317	syl 17	. . . . . 6 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
319		gzmulcl 16274	. . . . . 6 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
320	12, 318, 319	syl2anc 586	. . . . 5 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
321		gzmulcl 16274	. . . . . 6 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
322	275, 279, 321	syl2anc 586	. . . . 5 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
323		gzsubcl 16276	. . . . 5 ⊢ (((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
324	320, 322, 323	syl2anc 586	. . . 4 ⊢ (𝜑 → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
325	316, 324	eqeltrd 2913	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326		4sq.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
327	326	4sqlem4a 16287	. . 3 ⊢ ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328	288, 325, 327	syl2anc 586	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329	232, 328	eqeltrrd 2914	1 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 {cab 2799 ∃wrex 3139 ‘cfv 6355 (class class class)co 7156 ℂcc 10535 + caddc 10540 · cmul 10542 − cmin 10870 / cdiv 11297 ℕcn 11638 2c2 11693 ℕ₀cn0 11898 ℤcz 11982 ↑cexp 13430 ∗ccj 14455 abscabs 14593 ℤ[i]cgz 16265

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-sup 8906 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-n0 11899 df-z 11983 df-uz 12245 df-rp 12391 df-seq 13371 df-exp 13431 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-gz 16266

This theorem is referenced by: mul4sq 16290 4sqlem17 16297

W3C validator