mul4sqlem - Intuitionistic Logic Explorer

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

Theorem mul4sqlem 12562

Description: Lemma for mul4sq 12563: algebraic manipulations. The extra assumptions involving 𝑀 would let us know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.)

**Hypotheses**
Ref	Expression
4sq.1	⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
mul4sq.1	⊢ (𝜑 → 𝐴 ∈ ℤ[i])
mul4sq.2	⊢ (𝜑 → 𝐵 ∈ ℤ[i])
mul4sq.3	⊢ (𝜑 → 𝐶 ∈ ℤ[i])
mul4sq.4	⊢ (𝜑 → 𝐷 ∈ ℤ[i])
mul4sq.5	⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
mul4sq.6	⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
mul4sq.7	⊢ (𝜑 → 𝑀 ∈ ℕ)
mul4sq.8	⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])
mul4sq.9	⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])
mul4sq.10	⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ₀)

**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 12541	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
3	1, 2	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℂ)
4		mul4sq.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ[i])
5		gzcn 12541	. . . . . . . . . . 11 ⊢ (𝐶 ∈ ℤ[i] → 𝐶 ∈ ℂ)
6	4, 5	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ)
8	7	absvalsqd 11347	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
9	7	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) ∈ ℂ)
10	7, 9	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) ∈ ℂ)
11	8, 10	eqeltrd 2273	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) ∈ ℂ)
12		mul4sq.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ[i])
13		gzcn 12541	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ)
14	12, 13	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
15		mul4sq.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℤ[i])
16		gzcn 12541	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℤ[i] → 𝐷 ∈ ℂ)
17	15, 16	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18	14, 17	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ)
19	18	absvalsqd 11347	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
20	18	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) ∈ ℂ)
21	18, 20	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) ∈ ℂ)
22	19, 21	eqeltrd 2273	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) ∈ ℂ)
23	11, 22	addcld 8046	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) ∈ ℂ)
24	3	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ)
25	24, 6	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) ∈ ℂ)
26	14	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐵) ∈ ℂ)
27	26, 17	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) ∈ ℂ)
28	25, 27	mulcld 8047	. . . . . . 7 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) ∈ ℂ)
29	6	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐶) ∈ ℂ)
30	14, 29	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐶)) ∈ ℂ)
31	17	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘𝐷) ∈ ℂ)
32	3, 31	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐷)) ∈ ℂ)
33	30, 32	mulcld 8047	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) ∈ ℂ)
34	28, 33	addcld 8046	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))) ∈ ℂ)
35	3, 17	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ)
36	35	absvalsqd 11347	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
37	35	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) ∈ ℂ)
38	35, 37	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) ∈ ℂ)
39	36, 38	eqeltrd 2273	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) ∈ ℂ)
40	14, 6	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
41	40	absvalsqd 11347	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
42	40	cjcld 11105	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) ∈ ℂ)
43	40, 42	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) ∈ ℂ)
44	41, 43	eqeltrd 2273	. . . . . . 7 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) ∈ ℂ)
45	39, 44	addcld 8046	. . . . . 6 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) ∈ ℂ)
46	23, 34, 45	ppncand 8377	. . . . 5 ⊢ (𝜑 → (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
47	14, 31	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐷)) ∈ ℂ)
48	25, 47	addcld 8046	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) ∈ ℂ)
49	48	absvalsqd 11347	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))))
50	25, 47	cjaddd 11130	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))))
51	24, 6	cjmuld 11131	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = ((∗‘(∗‘𝐴)) · (∗‘𝐶)))
52	3	cjcjd 11108	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)
53	52	oveq1d 5937	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐶)) = (𝐴 · (∗‘𝐶)))
54	51, 53	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐶)) = (𝐴 · (∗‘𝐶)))
55	14, 31	cjmuld 11131	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · (∗‘(∗‘𝐷))))
56	17	cjcjd 11108	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐷)) = 𝐷)
57	56	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
58	55, 57	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐷))) = ((∗‘𝐵) · 𝐷))
59	54, 58	oveq12d 5940	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐶)) + (∗‘(𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
60	50, 59	eqtrd 2229	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))
61	60	oveq2d 5938	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · (∗‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))))
62	3, 29	mulcld 8047	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) ∈ ℂ)
63	25, 62, 27	adddid 8051	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
64	6, 24, 3, 29	mul4d 8181	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
65	24, 6	mulcomd 8048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐶) = (𝐶 · (∗‘𝐴)))
66	65	oveq1d 5937	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐶 · (∗‘𝐴)) · (𝐴 · (∗‘𝐶))))
67	3, 6	mulcomd 8048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐶 · 𝐴))
68	3, 6	cjmuld 11131	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐶)) = ((∗‘𝐴) · (∗‘𝐶)))
69	67, 68	oveq12d 5940	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐶 · 𝐴) · ((∗‘𝐴) · (∗‘𝐶))))
70	64, 66, 69	3eqtr4d 2239	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))))
71	70, 8	eqtr4d 2232	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) = ((abs‘(𝐴 · 𝐶))↑2))
72	71	oveq1d 5937	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · (𝐴 · (∗‘𝐶))) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
73	63, 72	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
74	47, 62, 27	adddid 8051	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))))
75	3, 29	mulcomd 8048	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · (∗‘𝐶)) = ((∗‘𝐶) · 𝐴))
76	75	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)))
77	14, 31, 29, 3	mul4d 8181	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐶) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)))
78	31, 3	mulcomd 8048	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐷) · 𝐴) = (𝐴 · (∗‘𝐷)))
79	78	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐷) · 𝐴)) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
80	76, 77, 79	3eqtrd 2233	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) = ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))
81	14, 31, 17, 26	mul4d 8181	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
82	26, 17	mulcomd 8048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐵) · 𝐷) = (𝐷 · (∗‘𝐵)))
83	82	oveq2d 5938	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · (∗‘𝐷)) · (𝐷 · (∗‘𝐵))))
84	14, 17	cjmuld 11131	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐵) · (∗‘𝐷)))
85	26, 31	mulcomd 8048	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
86	84, 85	eqtrd 2229	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐵 · 𝐷)) = ((∗‘𝐷) · (∗‘𝐵)))
87	86	oveq2d 5938	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐷) · (∗‘𝐵))))
88	81, 83, 87	3eqtr4d 2239	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))))
89	88, 19	eqtr4d 2232	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷)) = ((abs‘(𝐵 · 𝐷))↑2))
90	80, 89	oveq12d 5940	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐷)) · (𝐴 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐷)) · ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
91	74, 90	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2)))
92	73, 91	oveq12d 5940	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
93	62, 27	addcld 8046	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)) ∈ ℂ)
94	25, 47, 93	adddird 8052	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((∗‘𝐴) · 𝐶) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) + ((𝐵 · (∗‘𝐷)) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷)))))
95	11, 22, 28, 33	add42d 8196	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) = ((((abs‘(𝐴 · 𝐶))↑2) + (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) + (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) + ((abs‘(𝐵 · 𝐷))↑2))))
96	92, 94, 95	3eqtr4d 2239	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) · ((𝐴 · (∗‘𝐶)) + ((∗‘𝐵) · 𝐷))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
97	49, 61, 96	3eqtrd 2233	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
98	24, 17	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) ∈ ℂ)
99	98, 30	subcld 8337	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) ∈ ℂ)
100	99	absvalsqd 11347	. . . . . . 7 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))))
101		cjsub 11057	. . . . . . . . . 10 ⊢ ((((∗‘𝐴) · 𝐷) ∈ ℂ ∧ (𝐵 · (∗‘𝐶)) ∈ ℂ) → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
102	98, 30, 101	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))))
103	24, 17	cjmuld 11131	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = ((∗‘(∗‘𝐴)) · (∗‘𝐷)))
104	52	oveq1d 5937	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(∗‘𝐴)) · (∗‘𝐷)) = (𝐴 · (∗‘𝐷)))
105	103, 104	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((∗‘𝐴) · 𝐷)) = (𝐴 · (∗‘𝐷)))
106	14, 29	cjmuld 11131	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · (∗‘(∗‘𝐶))))
107	6	cjcjd 11108	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(∗‘𝐶)) = 𝐶)
108	107	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐵) · (∗‘(∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
109	106, 108	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘(𝐵 · (∗‘𝐶))) = ((∗‘𝐵) · 𝐶))
110	105, 109	oveq12d 5940	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘((∗‘𝐴) · 𝐷)) − (∗‘(𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
111	102, 110	eqtrd 2229	. . . . . . . 8 ⊢ (𝜑 → (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) = ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))
112	111	oveq2d 5938	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · (∗‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))))
113	26, 6	mulcld 8047	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) ∈ ℂ)
114	32, 113	subcld 8337	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)) ∈ ℂ)
115	98, 30, 114	subdird 8441	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))))
116	98, 32, 113	subdid 8440	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))))
117	17, 24, 3, 31	mul4d 8181	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
118	24, 17	mulcomd 8048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐴) · 𝐷) = (𝐷 · (∗‘𝐴)))
119	118	oveq1d 5937	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐷 · (∗‘𝐴)) · (𝐴 · (∗‘𝐷))))
120	3, 17	mulcomd 8048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐷) = (𝐷 · 𝐴))
121	3, 17	cjmuld 11131	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∗‘(𝐴 · 𝐷)) = ((∗‘𝐴) · (∗‘𝐷)))
122	120, 121	oveq12d 5940	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐷 · 𝐴) · ((∗‘𝐴) · (∗‘𝐷))))
123	117, 119, 122	3eqtr4d 2239	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))))
124	123, 36	eqtr4d 2232	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) = ((abs‘(𝐴 · 𝐷))↑2))
125	26, 6	mulcomd 8048	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∗‘𝐵) · 𝐶) = (𝐶 · (∗‘𝐵)))
126	125	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))))
127	24, 17, 6, 26	mul4d 8181	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · (𝐶 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))))
128	17, 26	mulcomd 8048	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (∗‘𝐵)) = ((∗‘𝐵) · 𝐷))
129	128	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) · (𝐷 · (∗‘𝐵))) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
130	126, 127, 129	3eqtrd 2233	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶)) = (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)))
131	124, 130	oveq12d 5940	. . . . . . . . . 10 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · (𝐴 · (∗‘𝐷))) − (((∗‘𝐴) · 𝐷) · ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
132	116, 131	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))))
133	30, 32, 113	subdid 8440	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))))
134	125	oveq2d 5938	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))))
135	14, 29, 6, 26	mul4d 8181	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · (𝐶 · (∗‘𝐵))) = ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))))
136	29, 26	mulcomd 8048	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = ((∗‘𝐵) · (∗‘𝐶)))
137	14, 6	cjmuld 11131	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∗‘(𝐵 · 𝐶)) = ((∗‘𝐵) · (∗‘𝐶)))
138	136, 137	eqtr4d 2232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((∗‘𝐶) · (∗‘𝐵)) = (∗‘(𝐵 · 𝐶)))
139	138	oveq2d 5938	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐶) · (∗‘𝐵))) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
140	134, 135, 139	3eqtrd 2233	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))))
141	140, 41	eqtr4d 2232	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶)) = ((abs‘(𝐵 · 𝐶))↑2))
142	141	oveq2d 5938	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((𝐵 · (∗‘𝐶)) · ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
143	133, 142	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2)))
144	132, 143	oveq12d 5940	. . . . . . . 8 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) − ((𝐵 · (∗‘𝐶)) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶)))) = ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))))
145	39, 28, 33, 44	subadd4d 8385	. . . . . . . 8 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) − (((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷))) − (((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))) − ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
146	115, 144, 145	3eqtrd 2233	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) · ((𝐴 · (∗‘𝐷)) − ((∗‘𝐵) · 𝐶))) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
147	100, 112, 146	3eqtrd 2233	. . . . . 6 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) = ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))))
148	97, 147	oveq12d 5940	. . . . 5 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) + ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷)))))))
149	3, 24	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℂ)
150	14, 26	mulcld 8047	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · (∗‘𝐵)) ∈ ℂ)
151	6, 29	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · (∗‘𝐶)) ∈ ℂ)
152	17, 31	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 · (∗‘𝐷)) ∈ ℂ)
153	151, 152	addcld 8046	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))) ∈ ℂ)
154	149, 150, 153	adddird 8052	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
155	68	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · (∗‘(𝐴 · 𝐶))) = ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))))
156	3, 6, 24, 29	mul4d 8181	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐶) · ((∗‘𝐴) · (∗‘𝐶))) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
157	8, 155, 156	3eqtrd 2233	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐶))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))))
158	121	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · (∗‘(𝐴 · 𝐷))) = ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))))
159	3, 17, 24, 31	mul4d 8181	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐷) · ((∗‘𝐴) · (∗‘𝐷))) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
160	36, 158, 159	3eqtrd 2233	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐴 · 𝐷))↑2) = ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷))))
161	157, 160	oveq12d 5940	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
162	149, 151, 152	adddid 8051	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) · (𝐶 · (∗‘𝐶))) + ((𝐴 · (∗‘𝐴)) · (𝐷 · (∗‘𝐷)))))
163	161, 162	eqtr4d 2232	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) = ((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
164	137	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · (∗‘(𝐵 · 𝐶))) = ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))))
165	14, 6, 26, 29	mul4d 8181	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐶) · ((∗‘𝐵) · (∗‘𝐶))) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
166	41, 164, 165	3eqtrd 2233	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐶))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))))
167	84	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · (∗‘(𝐵 · 𝐷))) = ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))))
168	14, 17, 26, 31	mul4d 8181	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐷) · ((∗‘𝐵) · (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
169	19, 167, 168	3eqtrd 2233	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(𝐵 · 𝐷))↑2) = ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷))))
170	166, 169	oveq12d 5940	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
171	150, 151, 152	adddid 8051	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = (((𝐵 · (∗‘𝐵)) · (𝐶 · (∗‘𝐶))) + ((𝐵 · (∗‘𝐵)) · (𝐷 · (∗‘𝐷)))))
172	170, 171	eqtr4d 2232	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) = ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
173	163, 172	oveq12d 5940	. . . . . . 7 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))) = (((𝐴 · (∗‘𝐴)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) + ((𝐵 · (∗‘𝐵)) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))))
174	154, 173	eqtr4d 2232	. . . . . 6 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
175		mul4sq.5	. . . . . . . 8 ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))
176	3	absvalsqd 11347	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
177	14	absvalsqd 11347	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐵)↑2) = (𝐵 · (∗‘𝐵)))
178	176, 177	oveq12d 5940	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
179	175, 178	eqtrid 2241	. . . . . . 7 ⊢ (𝜑 → 𝑋 = ((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))))
180		mul4sq.6	. . . . . . . 8 ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))
181	6	absvalsqd 11347	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐶)↑2) = (𝐶 · (∗‘𝐶)))
182	17	absvalsqd 11347	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘𝐷)↑2) = (𝐷 · (∗‘𝐷)))
183	181, 182	oveq12d 5940	. . . . . . . 8 ⊢ (𝜑 → (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
184	180, 183	eqtrid 2241	. . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷))))
185	179, 184	oveq12d 5940	. . . . . 6 ⊢ (𝜑 → (𝑋 · 𝑌) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) · ((𝐶 · (∗‘𝐶)) + (𝐷 · (∗‘𝐷)))))
186	11, 22, 39, 44	add42d 8196	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐴 · 𝐷))↑2)) + (((abs‘(𝐵 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2))))
187	174, 185, 186	3eqtr4d 2239	. . . . 5 ⊢ (𝜑 → (𝑋 · 𝑌) = ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + (((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2))))
188	46, 148, 187	3eqtr4d 2239	. . . 4 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) = (𝑋 · 𝑌))
189	188	oveq1d 5937	. . 3 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀↑2)))
190		mul4sq.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
191	190	nncnd 9004	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
192	190	nnap0d 9036	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 # 0)
193	48, 191, 192	absdivapd 11360	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)))
194	190	nnred 9003	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
195	190	nnnn0d 9302	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
196	195	nn0ge0d 9305	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑀)
197	194, 196	absidd 11332	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝑀) = 𝑀)
198	197	oveq2d 5938	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
199	193, 198	eqtrd 2229	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀))
200	199	oveq1d 5937	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2))
201	48	abscld 11346	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℝ)
202	201	recnd 8055	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) ∈ ℂ)
203	202, 191, 192	sqdivapd 10778	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
204	200, 203	eqtrd 2229	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)))
205	99, 191, 192	absdivapd 11360	. . . . . . . 8 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)))
206	197	oveq2d 5938	. . . . . . . 8 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / (abs‘𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
207	205, 206	eqtrd 2229	. . . . . . 7 ⊢ (𝜑 → (abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀)) = ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀))
208	207	oveq1d 5937	. . . . . 6 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2))
209	99	abscld 11346	. . . . . . . 8 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℝ)
210	209	recnd 8055	. . . . . . 7 ⊢ (𝜑 → (abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) ∈ ℂ)
211	210, 191, 192	sqdivapd 10778	. . . . . 6 ⊢ (𝜑 → (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶)))) / 𝑀)↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
212	208, 211	eqtrd 2229	. . . . 5 ⊢ (𝜑 → ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2) = (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2)))
213	204, 212	oveq12d 5940	. . . 4 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
214	23, 34	addcld 8046	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐶))↑2) + ((abs‘(𝐵 · 𝐷))↑2)) + ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
215	97, 214	eqeltrd 2273	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) ∈ ℂ)
216	45, 34	subcld 8337	. . . . . 6 ⊢ (𝜑 → ((((abs‘(𝐴 · 𝐷))↑2) + ((abs‘(𝐵 · 𝐶))↑2)) − ((((∗‘𝐴) · 𝐶) · ((∗‘𝐵) · 𝐷)) + ((𝐵 · (∗‘𝐶)) · (𝐴 · (∗‘𝐷))))) ∈ ℂ)
217	147, 216	eqeltrd 2273	. . . . 5 ⊢ (𝜑 → ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) ∈ ℂ)
218	190	nnsqcld 10786	. . . . . 6 ⊢ (𝜑 → (𝑀↑2) ∈ ℕ)
219	218	nncnd 9004	. . . . 5 ⊢ (𝜑 → (𝑀↑2) ∈ ℂ)
220	218	nnap0d 9036	. . . . 5 ⊢ (𝜑 → (𝑀↑2) # 0)
221	215, 217, 219, 220	divdirapd 8856	. . . 4 ⊢ (𝜑 → ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) / (𝑀↑2)) + (((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2) / (𝑀↑2))))
222	213, 221	eqtr4d 2232	. . 3 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((((abs‘(((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))↑2) + ((abs‘(((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))↑2)) / (𝑀↑2)))
223	176, 149	eqeltrd 2273	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐴)↑2) ∈ ℂ)
224	177, 150	eqeltrd 2273	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐵)↑2) ∈ ℂ)
225	223, 224	addcld 8046	. . . . . 6 ⊢ (𝜑 → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ ℂ)
226	175, 225	eqeltrid 2283	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ ℂ)
227	184, 153	eqeltrd 2273	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ ℂ)
228	226, 191, 227, 191, 192, 192	divmuldivapd 8859	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
229	191	sqvald 10762	. . . . 5 ⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
230	229	oveq2d 5938	. . . 4 ⊢ (𝜑 → ((𝑋 · 𝑌) / (𝑀↑2)) = ((𝑋 · 𝑌) / (𝑀 · 𝑀)))
231	228, 230	eqtr4d 2232	. . 3 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) = ((𝑋 · 𝑌) / (𝑀↑2)))
232	189, 222, 231	3eqtr4d 2239	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) = ((𝑋 / 𝑀) · (𝑌 / 𝑀)))
233	226, 48	nncand 8342	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))
234	149, 150, 25, 47	addsub4d 8384	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
235	179	oveq1d 5937	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((𝐴 · (∗‘𝐴)) + (𝐵 · (∗‘𝐵))) − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))))
236	24, 3, 6	subdid 8440	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)))
237	24, 3	mulcomd 8048	. . . . . . . . . . . 12 ⊢ (𝜑 → ((∗‘𝐴) · 𝐴) = (𝐴 · (∗‘𝐴)))
238	237	oveq1d 5937	. . . . . . . . . . 11 ⊢ (𝜑 → (((∗‘𝐴) · 𝐴) − ((∗‘𝐴) · 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
239	236, 238	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) = ((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)))
240		cjsub 11057	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
241	14, 17, 240	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) = ((∗‘𝐵) − (∗‘𝐷)))
242	241	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = (𝐵 · ((∗‘𝐵) − (∗‘𝐷))))
243	14, 26, 31	subdid 8440	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · ((∗‘𝐵) − (∗‘𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
244	242, 243	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) = ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷))))
245	239, 244	oveq12d 5940	. . . . . . . . 9 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) = (((𝐴 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐶)) + ((𝐵 · (∗‘𝐵)) − (𝐵 · (∗‘𝐷)))))
246	234, 235, 245	3eqtr4d 2239	. . . . . . . 8 ⊢ (𝜑 → (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷)))) = (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))))
247	246	oveq2d 5938	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝑋 − (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
248	233, 247	eqtr3d 2231	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) = (𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))))
249	248	oveq1d 5937	. . . . 5 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀))
250	3, 6	subcld 8337	. . . . . . . 8 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ)
251	24, 250	mulcld 8047	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐴 − 𝐶)) ∈ ℂ)
252	14, 17	subcld 8337	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℂ)
253	252	cjcld 11105	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐵 − 𝐷)) ∈ ℂ)
254	14, 253	mulcld 8047	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐵 − 𝐷))) ∈ ℂ)
255	251, 254	addcld 8046	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) ∈ ℂ)
256	226, 255, 191, 192	divsubdirapd 8857	. . . . 5 ⊢ (𝜑 → ((𝑋 − (((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷))))) / 𝑀) = ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)))
257	251, 254, 191, 192	divdirapd 8856	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)))
258	24, 250, 191, 192	divassapd 8853	. . . . . . . 8 ⊢ (𝜑 → (((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) = ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)))
259	14, 253, 191, 192	divassapd 8853	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
260	252, 191, 192	cjdivapd 11133	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)))
261	194	cjred 11136	. . . . . . . . . . . 12 ⊢ (𝜑 → (∗‘𝑀) = 𝑀)
262	261	oveq2d 5938	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘(𝐵 − 𝐷)) / (∗‘𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
263	260, 262	eqtrd 2229	. . . . . . . . . 10 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) = ((∗‘(𝐵 − 𝐷)) / 𝑀))
264	263	oveq2d 5938	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) = (𝐵 · ((∗‘(𝐵 − 𝐷)) / 𝑀)))
265	259, 264	eqtr4d 2232	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀) = (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))
266	258, 265	oveq12d 5940	. . . . . . 7 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) / 𝑀) + ((𝐵 · (∗‘(𝐵 − 𝐷))) / 𝑀)) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
267	257, 266	eqtrd 2229	. . . . . 6 ⊢ (𝜑 → ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀) = (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))))
268	267	oveq2d 5938	. . . . 5 ⊢ (𝜑 → ((𝑋 / 𝑀) − ((((∗‘𝐴) · (𝐴 − 𝐶)) + (𝐵 · (∗‘(𝐵 − 𝐷)))) / 𝑀)) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
269	249, 256, 268	3eqtrd 2233	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) = ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))))
270		mul4sq.10	. . . . . . 7 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ₀)
271	270	nn0zd 9446	. . . . . 6 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ)
272		zgz 12542	. . . . . 6 ⊢ ((𝑋 / 𝑀) ∈ ℤ → (𝑋 / 𝑀) ∈ ℤ[i])
273	271, 272	syl 14	. . . . 5 ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℤ[i])
274		gzcjcl 12545	. . . . . . . 8 ⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
275	1, 274	syl 14	. . . . . . 7 ⊢ (𝜑 → (∗‘𝐴) ∈ ℤ[i])
276		mul4sq.8	. . . . . . 7 ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])
277		gzmulcl 12547	. . . . . . 7 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
278	275, 276, 277	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
279		mul4sq.9	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])
280		gzcjcl 12545	. . . . . . . 8 ⊢ (((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i] → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
281	279, 280	syl 14	. . . . . . 7 ⊢ (𝜑 → (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
282		gzmulcl 12547	. . . . . . 7 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
283	12, 281, 282	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
284		gzaddcl 12546	. . . . . 6 ⊢ ((((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i] ∧ (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i]) → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
285	278, 283, 284	syl2anc 411	. . . . 5 ⊢ (𝜑 → (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i])
286		gzsubcl 12549	. . . . 5 ⊢ (((𝑋 / 𝑀) ∈ ℤ[i] ∧ (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀)))) ∈ ℤ[i]) → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
287	273, 285, 286	syl2anc 411	. . . 4 ⊢ (𝜑 → ((𝑋 / 𝑀) − (((∗‘𝐴) · ((𝐴 − 𝐶) / 𝑀)) + (𝐵 · (∗‘((𝐵 − 𝐷) / 𝑀))))) ∈ ℤ[i])
288	269, 287	eqeltrd 2273	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i])
289	250	cjcld 11105	. . . . . . . 8 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) ∈ ℂ)
290	14, 289	mulcld 8047	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) ∈ ℂ)
291	24, 252	mulcld 8047	. . . . . . 7 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) ∈ ℂ)
292	290, 291, 191, 192	divsubdirapd 8857	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)))
293		cjsub 11057	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
294	3, 6, 293	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → (∗‘(𝐴 − 𝐶)) = ((∗‘𝐴) − (∗‘𝐶)))
295	294	oveq2d 5938	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = (𝐵 · ((∗‘𝐴) − (∗‘𝐶))))
296	14, 24, 29	subdid 8440	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 · ((∗‘𝐴) − (∗‘𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
297	295, 296	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘(𝐴 − 𝐶))) = ((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))))
298	24, 14, 17	subdid 8440	. . . . . . . . . 10 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)))
299	24, 14	mulcomd 8048	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗‘𝐴) · 𝐵) = (𝐵 · (∗‘𝐴)))
300	299	oveq1d 5937	. . . . . . . . . 10 ⊢ (𝜑 → (((∗‘𝐴) · 𝐵) − ((∗‘𝐴) · 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
301	298, 300	eqtrd 2229	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘𝐴) · (𝐵 − 𝐷)) = ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷)))
302	297, 301	oveq12d 5940	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))))
303	14, 24	mulcld 8047	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 · (∗‘𝐴)) ∈ ℂ)
304	303, 30, 98	nnncan1d 8371	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · (∗‘𝐴)) − (𝐵 · (∗‘𝐶))) − ((𝐵 · (∗‘𝐴)) − ((∗‘𝐴) · 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
305	302, 304	eqtrd 2229	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) = (((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))))
306	305	oveq1d 5937	. . . . . 6 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) − ((∗‘𝐴) · (𝐵 − 𝐷))) / 𝑀) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
307	292, 306	eqtr3d 2231	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))
308	14, 289, 191, 192	divassapd 8853	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
309	250, 191, 192	cjdivapd 11133	. . . . . . . . 9 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)))
310	261	oveq2d 5938	. . . . . . . . 9 ⊢ (𝜑 → ((∗‘(𝐴 − 𝐶)) / (∗‘𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
311	309, 310	eqtrd 2229	. . . . . . . 8 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) = ((∗‘(𝐴 − 𝐶)) / 𝑀))
312	311	oveq2d 5938	. . . . . . 7 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) = (𝐵 · ((∗‘(𝐴 − 𝐶)) / 𝑀)))
313	308, 312	eqtr4d 2232	. . . . . 6 ⊢ (𝜑 → ((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) = (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))))
314	24, 252, 191, 192	divassapd 8853	. . . . . 6 ⊢ (𝜑 → (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀) = ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)))
315	313, 314	oveq12d 5940	. . . . 5 ⊢ (𝜑 → (((𝐵 · (∗‘(𝐴 − 𝐶))) / 𝑀) − (((∗‘𝐴) · (𝐵 − 𝐷)) / 𝑀)) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
316	307, 315	eqtr3d 2231	. . . 4 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) = ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))))
317		gzcjcl 12545	. . . . . . 7 ⊢ (((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i] → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
318	276, 317	syl 14	. . . . . 6 ⊢ (𝜑 → (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i])
319		gzmulcl 12547	. . . . . 6 ⊢ ((𝐵 ∈ ℤ[i] ∧ (∗‘((𝐴 − 𝐶) / 𝑀)) ∈ ℤ[i]) → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
320	12, 318, 319	syl2anc 411	. . . . 5 ⊢ (𝜑 → (𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i])
321		gzmulcl 12547	. . . . . 6 ⊢ (((∗‘𝐴) ∈ ℤ[i] ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
322	275, 279, 321	syl2anc 411	. . . . 5 ⊢ (𝜑 → ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i])
323		gzsubcl 12549	. . . . 5 ⊢ (((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) ∈ ℤ[i] ∧ ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀)) ∈ ℤ[i]) → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
324	320, 322, 323	syl2anc 411	. . . 4 ⊢ (𝜑 → ((𝐵 · (∗‘((𝐴 − 𝐶) / 𝑀))) − ((∗‘𝐴) · ((𝐵 − 𝐷) / 𝑀))) ∈ ℤ[i])
325	316, 324	eqeltrd 2273	. . 3 ⊢ (𝜑 → ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i])
326		4sq.1	. . . 4 ⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
327	326	4sqlem4a 12560	. . 3 ⊢ ((((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀) ∈ ℤ[i] ∧ ((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀) ∈ ℤ[i]) → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
328	288, 325, 327	syl2anc 411	. 2 ⊢ (𝜑 → (((abs‘((((∗‘𝐴) · 𝐶) + (𝐵 · (∗‘𝐷))) / 𝑀))↑2) + ((abs‘((((∗‘𝐴) · 𝐷) − (𝐵 · (∗‘𝐶))) / 𝑀))↑2)) ∈ 𝑆)
329	232, 328	eqeltrrd 2274	1 ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: → wi 4 = wceq 1364 ∈ wcel 2167 {cab 2182 ∃wrex 2476 ‘cfv 5258 (class class class)co 5922 ℂcc 7877 + caddc 7882 · cmul 7884 − cmin 8197 / cdiv 8699 ℕcn 8990 2c2 9041 ℕ₀cn0 9249 ℤcz 9326 ↑cexp 10630 ∗ccj 11004 abscabs 11162 ℤ[i]cgz 12538

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-rp 9729 df-seqfrec 10540 df-exp 10631 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-gz 12539

This theorem is referenced by: mul4sq 12563 4sqlem17 12576

W3C validator