mul4sqlem

Description: Lemma for mul4sq : algebraic manipulations. The extra assumptions involving M are for a part of 4sqlem17 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by M . (Contributed by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Hypotheses	4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
	mul4sq.1	$⊢ φ \to A \in ℤ [i]$
	mul4sq.2	$⊢ φ \to B \in ℤ [i]$
	mul4sq.3	$⊢ φ \to C \in ℤ [i]$
	mul4sq.4	$⊢ φ \to D \in ℤ [i]$
	mul4sq.5	$⊢ X = {\|A\|}^{2} + {\|B\|}^{2}$
	mul4sq.6	$⊢ Y = {\|C\|}^{2} + {\|D\|}^{2}$
	mul4sq.7	$⊢ φ \to M \in ℕ$
	mul4sq.8	$⊢ φ \to \frac{A - C}{M} \in ℤ [i]$
	mul4sq.9	$⊢ φ \to \frac{B - D}{M} \in ℤ [i]$
	mul4sq.10	$⊢ φ \to \frac{X}{M} \in ℕ_{0}$
Assertion	mul4sqlem	$⊢ φ \to (\frac{X}{M}) (\frac{Y}{M}) \in S$

Proof

Step	Hyp	Ref	Expression
1		4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
2		mul4sq.1	$⊢ φ \to A \in ℤ [i]$
3		mul4sq.2	$⊢ φ \to B \in ℤ [i]$
4		mul4sq.3	$⊢ φ \to C \in ℤ [i]$
5		mul4sq.4	$⊢ φ \to D \in ℤ [i]$
6		mul4sq.5	$⊢ X = {\|A\|}^{2} + {\|B\|}^{2}$
7		mul4sq.6	$⊢ Y = {\|C\|}^{2} + {\|D\|}^{2}$
8		mul4sq.7	$⊢ φ \to M \in ℕ$
9		mul4sq.8	$⊢ φ \to \frac{A - C}{M} \in ℤ [i]$
10		mul4sq.9	$⊢ φ \to \frac{B - D}{M} \in ℤ [i]$
11		mul4sq.10	$⊢ φ \to \frac{X}{M} \in ℕ_{0}$
12		gzcn	$⊢ A \in ℤ [i] \to A \in ℂ$
13	2 12	syl	$⊢ φ \to A \in ℂ$
14		gzcn	$⊢ C \in ℤ [i] \to C \in ℂ$
15	4 14	syl	$⊢ φ \to C \in ℂ$
16	13 15	mulcld	$⊢ φ \to A C \in ℂ$
17	16	absvalsqd	$⊢ φ \to {\|A C\|}^{2} = A C \overline{A C}$
18	16	cjcld	$⊢ φ \to \overline{A C} \in ℂ$
19	16 18	mulcld	$⊢ φ \to A C \overline{A C} \in ℂ$
20	17 19	eqeltrd	$⊢ φ \to {\|A C\|}^{2} \in ℂ$
21		gzcn	$⊢ B \in ℤ [i] \to B \in ℂ$
22	3 21	syl	$⊢ φ \to B \in ℂ$
23		gzcn	$⊢ D \in ℤ [i] \to D \in ℂ$
24	5 23	syl	$⊢ φ \to D \in ℂ$
25	22 24	mulcld	$⊢ φ \to B D \in ℂ$
26	25	absvalsqd	$⊢ φ \to {\|B D\|}^{2} = B D \overline{B D}$
27	25	cjcld	$⊢ φ \to \overline{B D} \in ℂ$
28	25 27	mulcld	$⊢ φ \to B D \overline{B D} \in ℂ$
29	26 28	eqeltrd	$⊢ φ \to {\|B D\|}^{2} \in ℂ$
30	20 29	addcld	$⊢ φ \to {\|A C\|}^{2} + {\|B D\|}^{2} \in ℂ$
31	13	cjcld	$⊢ φ \to \overline{A} \in ℂ$
32	31 15	mulcld	$⊢ φ \to \overline{A} C \in ℂ$
33	22	cjcld	$⊢ φ \to \overline{B} \in ℂ$
34	33 24	mulcld	$⊢ φ \to \overline{B} D \in ℂ$
35	32 34	mulcld	$⊢ φ \to \overline{A} C \overline{B} D \in ℂ$
36	15	cjcld	$⊢ φ \to \overline{C} \in ℂ$
37	22 36	mulcld	$⊢ φ \to B \overline{C} \in ℂ$
38	24	cjcld	$⊢ φ \to \overline{D} \in ℂ$
39	13 38	mulcld	$⊢ φ \to A \overline{D} \in ℂ$
40	37 39	mulcld	$⊢ φ \to B \overline{C} A \overline{D} \in ℂ$
41	35 40	addcld	$⊢ φ \to \overline{A} C \overline{B} D + B \overline{C} A \overline{D} \in ℂ$
42	13 24	mulcld	$⊢ φ \to A D \in ℂ$
43	42	absvalsqd	$⊢ φ \to {\|A D\|}^{2} = A D \overline{A D}$
44	42	cjcld	$⊢ φ \to \overline{A D} \in ℂ$
45	42 44	mulcld	$⊢ φ \to A D \overline{A D} \in ℂ$
46	43 45	eqeltrd	$⊢ φ \to {\|A D\|}^{2} \in ℂ$
47	22 15	mulcld	$⊢ φ \to B C \in ℂ$
48	47	absvalsqd	$⊢ φ \to {\|B C\|}^{2} = B C \overline{B C}$
49	47	cjcld	$⊢ φ \to \overline{B C} \in ℂ$
50	47 49	mulcld	$⊢ φ \to B C \overline{B C} \in ℂ$
51	48 50	eqeltrd	$⊢ φ \to {\|B C\|}^{2} \in ℂ$
52	46 51	addcld	$⊢ φ \to {\|A D\|}^{2} + {\|B C\|}^{2} \in ℂ$
53	30 41 52	ppncand	$⊢ φ \to ({\|A C\|}^{2} + {\|B D\|}^{2}) + (\overline{A} C \overline{B} D + B \overline{C} A \overline{D}) + ({\|A D\|}^{2} + {\|B C\|}^{2} - (\overline{A} C \overline{B} D + B \overline{C} A \overline{D})) = {\|A C\|}^{2} + {\|B D\|}^{2} + {\|A D\|}^{2} + {\|B C\|}^{2}$
54	22 38	mulcld	$⊢ φ \to B \overline{D} \in ℂ$
55	32 54	addcld	$⊢ φ \to \overline{A} C + B \overline{D} \in ℂ$
56	55	absvalsqd	$⊢ φ \to {\|\overline{A} C + B \overline{D}\|}^{2} = (\overline{A} C + B \overline{D}) \overline{\overline{A} C + B \overline{D}}$
57	32 54	cjaddd	$⊢ φ \to \overline{\overline{A} C + B \overline{D}} = \overline{\overline{A} C} + \overline{B \overline{D}}$
58	31 15	cjmuld	$⊢ φ \to \overline{\overline{A} C} = \overline{\overline{A}} \overline{C}$
59	13	cjcjd	$⊢ φ \to \overline{\overline{A}} = A$
60	59	oveq1d	$⊢ φ \to \overline{\overline{A}} \overline{C} = A \overline{C}$
61	58 60	eqtrd	$⊢ φ \to \overline{\overline{A} C} = A \overline{C}$
62	22 38	cjmuld	$⊢ φ \to \overline{B \overline{D}} = \overline{B} \overline{\overline{D}}$
63	24	cjcjd	$⊢ φ \to \overline{\overline{D}} = D$
64	63	oveq2d	$⊢ φ \to \overline{B} \overline{\overline{D}} = \overline{B} D$
65	62 64	eqtrd	$⊢ φ \to \overline{B \overline{D}} = \overline{B} D$
66	61 65	oveq12d	$⊢ φ \to \overline{\overline{A} C} + \overline{B \overline{D}} = A \overline{C} + \overline{B} D$
67	57 66	eqtrd	$⊢ φ \to \overline{\overline{A} C + B \overline{D}} = A \overline{C} + \overline{B} D$
68	67	oveq2d	$⊢ φ \to (\overline{A} C + B \overline{D}) \overline{\overline{A} C + B \overline{D}} = (\overline{A} C + B \overline{D}) (A \overline{C} + \overline{B} D)$
69	13 36	mulcld	$⊢ φ \to A \overline{C} \in ℂ$
70	32 69 34	adddid	$⊢ φ \to \overline{A} C (A \overline{C} + \overline{B} D) = \overline{A} C A \overline{C} + \overline{A} C \overline{B} D$
71	15 31 13 36	mul4d	$⊢ φ \to C \overline{A} A \overline{C} = C A \overline{A} \overline{C}$
72	31 15	mulcomd	$⊢ φ \to \overline{A} C = C \overline{A}$
73	72	oveq1d	$⊢ φ \to \overline{A} C A \overline{C} = C \overline{A} A \overline{C}$
74	13 15	mulcomd	$⊢ φ \to A C = C A$
75	13 15	cjmuld	$⊢ φ \to \overline{A C} = \overline{A} \overline{C}$
76	74 75	oveq12d	$⊢ φ \to A C \overline{A C} = C A \overline{A} \overline{C}$
77	71 73 76	3eqtr4d	$⊢ φ \to \overline{A} C A \overline{C} = A C \overline{A C}$
78	77 17	eqtr4d	$⊢ φ \to \overline{A} C A \overline{C} = {\|A C\|}^{2}$
79	78	oveq1d	$⊢ φ \to \overline{A} C A \overline{C} + \overline{A} C \overline{B} D = {\|A C\|}^{2} + \overline{A} C \overline{B} D$
80	70 79	eqtrd	$⊢ φ \to \overline{A} C (A \overline{C} + \overline{B} D) = {\|A C\|}^{2} + \overline{A} C \overline{B} D$
81	54 69 34	adddid	$⊢ φ \to B \overline{D} (A \overline{C} + \overline{B} D) = B \overline{D} A \overline{C} + B \overline{D} \overline{B} D$
82	13 36	mulcomd	$⊢ φ \to A \overline{C} = \overline{C} A$
83	82	oveq2d	$⊢ φ \to B \overline{D} A \overline{C} = B \overline{D} \overline{C} A$
84	22 38 36 13	mul4d	$⊢ φ \to B \overline{D} \overline{C} A = B \overline{C} \overline{D} A$
85	38 13	mulcomd	$⊢ φ \to \overline{D} A = A \overline{D}$
86	85	oveq2d	$⊢ φ \to B \overline{C} \overline{D} A = B \overline{C} A \overline{D}$
87	83 84 86	3eqtrd	$⊢ φ \to B \overline{D} A \overline{C} = B \overline{C} A \overline{D}$
88	22 38 24 33	mul4d	$⊢ φ \to B \overline{D} D \overline{B} = B D \overline{D} \overline{B}$
89	33 24	mulcomd	$⊢ φ \to \overline{B} D = D \overline{B}$
90	89	oveq2d	$⊢ φ \to B \overline{D} \overline{B} D = B \overline{D} D \overline{B}$
91	22 24	cjmuld	$⊢ φ \to \overline{B D} = \overline{B} \overline{D}$
92	33 38	mulcomd	$⊢ φ \to \overline{B} \overline{D} = \overline{D} \overline{B}$
93	91 92	eqtrd	$⊢ φ \to \overline{B D} = \overline{D} \overline{B}$
94	93	oveq2d	$⊢ φ \to B D \overline{B D} = B D \overline{D} \overline{B}$
95	88 90 94	3eqtr4d	$⊢ φ \to B \overline{D} \overline{B} D = B D \overline{B D}$
96	95 26	eqtr4d	$⊢ φ \to B \overline{D} \overline{B} D = {\|B D\|}^{2}$
97	87 96	oveq12d	$⊢ φ \to B \overline{D} A \overline{C} + B \overline{D} \overline{B} D = B \overline{C} A \overline{D} + {\|B D\|}^{2}$
98	81 97	eqtrd	$⊢ φ \to B \overline{D} (A \overline{C} + \overline{B} D) = B \overline{C} A \overline{D} + {\|B D\|}^{2}$
99	80 98	oveq12d	$⊢ φ \to \overline{A} C (A \overline{C} + \overline{B} D) + B \overline{D} (A \overline{C} + \overline{B} D) = {\|A C\|}^{2} + \overline{A} C \overline{B} D + B \overline{C} A \overline{D} + {\|B D\|}^{2}$
100	69 34	addcld	$⊢ φ \to A \overline{C} + \overline{B} D \in ℂ$
101	32 54 100	adddird	$⊢ φ \to (\overline{A} C + B \overline{D}) (A \overline{C} + \overline{B} D) = \overline{A} C (A \overline{C} + \overline{B} D) + B \overline{D} (A \overline{C} + \overline{B} D)$
102	20 29 35 40	add42d	$⊢ φ \to {\|A C\|}^{2} + {\|B D\|}^{2} + \overline{A} C \overline{B} D + B \overline{C} A \overline{D} = {\|A C\|}^{2} + \overline{A} C \overline{B} D + B \overline{C} A \overline{D} + {\|B D\|}^{2}$
103	99 101 102	3eqtr4d	$⊢ φ \to (\overline{A} C + B \overline{D}) (A \overline{C} + \overline{B} D) = {\|A C\|}^{2} + {\|B D\|}^{2} + \overline{A} C \overline{B} D + B \overline{C} A \overline{D}$
104	56 68 103	3eqtrd	$⊢ φ \to {\|\overline{A} C + B \overline{D}\|}^{2} = {\|A C\|}^{2} + {\|B D\|}^{2} + \overline{A} C \overline{B} D + B \overline{C} A \overline{D}$
105	31 24	mulcld	$⊢ φ \to \overline{A} D \in ℂ$
106	105 37	subcld	$⊢ φ \to \overline{A} D - B \overline{C} \in ℂ$
107	106	absvalsqd	$⊢ φ \to {\|\overline{A} D - B \overline{C}\|}^{2} = (\overline{A} D - B \overline{C}) \overline{\overline{A} D - B \overline{C}}$
108		cjsub	$⊢ (\overline{A} D \in ℂ \land B \overline{C} \in ℂ) \to \overline{\overline{A} D - B \overline{C}} = \overline{\overline{A} D} - \overline{B \overline{C}}$
109	105 37 108	syl2anc	$⊢ φ \to \overline{\overline{A} D - B \overline{C}} = \overline{\overline{A} D} - \overline{B \overline{C}}$
110	31 24	cjmuld	$⊢ φ \to \overline{\overline{A} D} = \overline{\overline{A}} \overline{D}$
111	59	oveq1d	$⊢ φ \to \overline{\overline{A}} \overline{D} = A \overline{D}$
112	110 111	eqtrd	$⊢ φ \to \overline{\overline{A} D} = A \overline{D}$
113	22 36	cjmuld	$⊢ φ \to \overline{B \overline{C}} = \overline{B} \overline{\overline{C}}$
114	15	cjcjd	$⊢ φ \to \overline{\overline{C}} = C$
115	114	oveq2d	$⊢ φ \to \overline{B} \overline{\overline{C}} = \overline{B} C$
116	113 115	eqtrd	$⊢ φ \to \overline{B \overline{C}} = \overline{B} C$
117	112 116	oveq12d	$⊢ φ \to \overline{\overline{A} D} - \overline{B \overline{C}} = A \overline{D} - \overline{B} C$
118	109 117	eqtrd	$⊢ φ \to \overline{\overline{A} D - B \overline{C}} = A \overline{D} - \overline{B} C$
119	118	oveq2d	$⊢ φ \to (\overline{A} D - B \overline{C}) \overline{\overline{A} D - B \overline{C}} = (\overline{A} D - B \overline{C}) (A \overline{D} - \overline{B} C)$
120	33 15	mulcld	$⊢ φ \to \overline{B} C \in ℂ$
121	39 120	subcld	$⊢ φ \to A \overline{D} - \overline{B} C \in ℂ$
122	105 37 121	subdird	$⊢ φ \to (\overline{A} D - B \overline{C}) (A \overline{D} - \overline{B} C) = \overline{A} D (A \overline{D} - \overline{B} C) - B \overline{C} (A \overline{D} - \overline{B} C)$
123	105 39 120	subdid	$⊢ φ \to \overline{A} D (A \overline{D} - \overline{B} C) = \overline{A} D A \overline{D} - \overline{A} D \overline{B} C$
124	24 31 13 38	mul4d	$⊢ φ \to D \overline{A} A \overline{D} = D A \overline{A} \overline{D}$
125	31 24	mulcomd	$⊢ φ \to \overline{A} D = D \overline{A}$
126	125	oveq1d	$⊢ φ \to \overline{A} D A \overline{D} = D \overline{A} A \overline{D}$
127	13 24	mulcomd	$⊢ φ \to A D = D A$
128	13 24	cjmuld	$⊢ φ \to \overline{A D} = \overline{A} \overline{D}$
129	127 128	oveq12d	$⊢ φ \to A D \overline{A D} = D A \overline{A} \overline{D}$
130	124 126 129	3eqtr4d	$⊢ φ \to \overline{A} D A \overline{D} = A D \overline{A D}$
131	130 43	eqtr4d	$⊢ φ \to \overline{A} D A \overline{D} = {\|A D\|}^{2}$
132	33 15	mulcomd	$⊢ φ \to \overline{B} C = C \overline{B}$
133	132	oveq2d	$⊢ φ \to \overline{A} D \overline{B} C = \overline{A} D C \overline{B}$
134	31 24 15 33	mul4d	$⊢ φ \to \overline{A} D C \overline{B} = \overline{A} C D \overline{B}$
135	24 33	mulcomd	$⊢ φ \to D \overline{B} = \overline{B} D$
136	135	oveq2d	$⊢ φ \to \overline{A} C D \overline{B} = \overline{A} C \overline{B} D$
137	133 134 136	3eqtrd	$⊢ φ \to \overline{A} D \overline{B} C = \overline{A} C \overline{B} D$
138	131 137	oveq12d	$⊢ φ \to \overline{A} D A \overline{D} - \overline{A} D \overline{B} C = {\|A D\|}^{2} - \overline{A} C \overline{B} D$
139	123 138	eqtrd	$⊢ φ \to \overline{A} D (A \overline{D} - \overline{B} C) = {\|A D\|}^{2} - \overline{A} C \overline{B} D$
140	37 39 120	subdid	$⊢ φ \to B \overline{C} (A \overline{D} - \overline{B} C) = B \overline{C} A \overline{D} - B \overline{C} \overline{B} C$
141	132	oveq2d	$⊢ φ \to B \overline{C} \overline{B} C = B \overline{C} C \overline{B}$
142	22 36 15 33	mul4d	$⊢ φ \to B \overline{C} C \overline{B} = B C \overline{C} \overline{B}$
143	36 33	mulcomd	$⊢ φ \to \overline{C} \overline{B} = \overline{B} \overline{C}$
144	22 15	cjmuld	$⊢ φ \to \overline{B C} = \overline{B} \overline{C}$
145	143 144	eqtr4d	$⊢ φ \to \overline{C} \overline{B} = \overline{B C}$
146	145	oveq2d	$⊢ φ \to B C \overline{C} \overline{B} = B C \overline{B C}$
147	141 142 146	3eqtrd	$⊢ φ \to B \overline{C} \overline{B} C = B C \overline{B C}$
148	147 48	eqtr4d	$⊢ φ \to B \overline{C} \overline{B} C = {\|B C\|}^{2}$
149	148	oveq2d	$⊢ φ \to B \overline{C} A \overline{D} - B \overline{C} \overline{B} C = B \overline{C} A \overline{D} - {\|B C\|}^{2}$
150	140 149	eqtrd	$⊢ φ \to B \overline{C} (A \overline{D} - \overline{B} C) = B \overline{C} A \overline{D} - {\|B C\|}^{2}$
151	139 150	oveq12d	$⊢ φ \to \overline{A} D (A \overline{D} - \overline{B} C) - B \overline{C} (A \overline{D} - \overline{B} C) = {\|A D\|}^{2} - \overline{A} C \overline{B} D - (B \overline{C} A \overline{D} - {\|B C\|}^{2})$
152	46 35 40 51	subadd4d	$⊢ φ \to {\|A D\|}^{2} - \overline{A} C \overline{B} D - (B \overline{C} A \overline{D} - {\|B C\|}^{2}) = {\|A D\|}^{2} + {\|B C\|}^{2} - (\overline{A} C \overline{B} D + B \overline{C} A \overline{D})$
153	122 151 152	3eqtrd	$⊢ φ \to (\overline{A} D - B \overline{C}) (A \overline{D} - \overline{B} C) = {\|A D\|}^{2} + {\|B C\|}^{2} - (\overline{A} C \overline{B} D + B \overline{C} A \overline{D})$
154	107 119 153	3eqtrd	$⊢ φ \to {\|\overline{A} D - B \overline{C}\|}^{2} = {\|A D\|}^{2} + {\|B C\|}^{2} - (\overline{A} C \overline{B} D + B \overline{C} A \overline{D})$
155	104 154	oveq12d	$⊢ φ \to {\|\overline{A} C + B \overline{D}\|}^{2} + {\|\overline{A} D - B \overline{C}\|}^{2} = ({\|A C\|}^{2} + {\|B D\|}^{2}) + (\overline{A} C \overline{B} D + B \overline{C} A \overline{D}) + ({\|A D\|}^{2} + {\|B C\|}^{2} - (\overline{A} C \overline{B} D + B \overline{C} A \overline{D}))$
156	13 31	mulcld	$⊢ φ \to A \overline{A} \in ℂ$
157	22 33	mulcld	$⊢ φ \to B \overline{B} \in ℂ$
158	15 36	mulcld	$⊢ φ \to C \overline{C} \in ℂ$
159	24 38	mulcld	$⊢ φ \to D \overline{D} \in ℂ$
160	158 159	addcld	$⊢ φ \to C \overline{C} + D \overline{D} \in ℂ$
161	156 157 160	adddird	$⊢ φ \to (A \overline{A} + B \overline{B}) (C \overline{C} + D \overline{D}) = A \overline{A} (C \overline{C} + D \overline{D}) + B \overline{B} (C \overline{C} + D \overline{D})$
162	75	oveq2d	$⊢ φ \to A C \overline{A C} = A C \overline{A} \overline{C}$
163	13 15 31 36	mul4d	$⊢ φ \to A C \overline{A} \overline{C} = A \overline{A} C \overline{C}$
164	17 162 163	3eqtrd	$⊢ φ \to {\|A C\|}^{2} = A \overline{A} C \overline{C}$
165	128	oveq2d	$⊢ φ \to A D \overline{A D} = A D \overline{A} \overline{D}$
166	13 24 31 38	mul4d	$⊢ φ \to A D \overline{A} \overline{D} = A \overline{A} D \overline{D}$
167	43 165 166	3eqtrd	$⊢ φ \to {\|A D\|}^{2} = A \overline{A} D \overline{D}$
168	164 167	oveq12d	$⊢ φ \to {\|A C\|}^{2} + {\|A D\|}^{2} = A \overline{A} C \overline{C} + A \overline{A} D \overline{D}$
169	156 158 159	adddid	$⊢ φ \to A \overline{A} (C \overline{C} + D \overline{D}) = A \overline{A} C \overline{C} + A \overline{A} D \overline{D}$
170	168 169	eqtr4d	$⊢ φ \to {\|A C\|}^{2} + {\|A D\|}^{2} = A \overline{A} (C \overline{C} + D \overline{D})$
171	144	oveq2d	$⊢ φ \to B C \overline{B C} = B C \overline{B} \overline{C}$
172	22 15 33 36	mul4d	$⊢ φ \to B C \overline{B} \overline{C} = B \overline{B} C \overline{C}$
173	48 171 172	3eqtrd	$⊢ φ \to {\|B C\|}^{2} = B \overline{B} C \overline{C}$
174	91	oveq2d	$⊢ φ \to B D \overline{B D} = B D \overline{B} \overline{D}$
175	22 24 33 38	mul4d	$⊢ φ \to B D \overline{B} \overline{D} = B \overline{B} D \overline{D}$
176	26 174 175	3eqtrd	$⊢ φ \to {\|B D\|}^{2} = B \overline{B} D \overline{D}$
177	173 176	oveq12d	$⊢ φ \to {\|B C\|}^{2} + {\|B D\|}^{2} = B \overline{B} C \overline{C} + B \overline{B} D \overline{D}$
178	157 158 159	adddid	$⊢ φ \to B \overline{B} (C \overline{C} + D \overline{D}) = B \overline{B} C \overline{C} + B \overline{B} D \overline{D}$
179	177 178	eqtr4d	$⊢ φ \to {\|B C\|}^{2} + {\|B D\|}^{2} = B \overline{B} (C \overline{C} + D \overline{D})$
180	170 179	oveq12d	$⊢ φ \to {\|A C\|}^{2} + {\|A D\|}^{2} + {\|B C\|}^{2} + {\|B D\|}^{2} = A \overline{A} (C \overline{C} + D \overline{D}) + B \overline{B} (C \overline{C} + D \overline{D})$
181	161 180	eqtr4d	$⊢ φ \to (A \overline{A} + B \overline{B}) (C \overline{C} + D \overline{D}) = {\|A C\|}^{2} + {\|A D\|}^{2} + {\|B C\|}^{2} + {\|B D\|}^{2}$
182	13	absvalsqd	$⊢ φ \to {\|A\|}^{2} = A \overline{A}$
183	22	absvalsqd	$⊢ φ \to {\|B\|}^{2} = B \overline{B}$
184	182 183	oveq12d	$⊢ φ \to {\|A\|}^{2} + {\|B\|}^{2} = A \overline{A} + B \overline{B}$
185	6 184	syl5eq	$⊢ φ \to X = A \overline{A} + B \overline{B}$
186	15	absvalsqd	$⊢ φ \to {\|C\|}^{2} = C \overline{C}$
187	24	absvalsqd	$⊢ φ \to {\|D\|}^{2} = D \overline{D}$
188	186 187	oveq12d	$⊢ φ \to {\|C\|}^{2} + {\|D\|}^{2} = C \overline{C} + D \overline{D}$
189	7 188	syl5eq	$⊢ φ \to Y = C \overline{C} + D \overline{D}$
190	185 189	oveq12d	$⊢ φ \to X Y = (A \overline{A} + B \overline{B}) (C \overline{C} + D \overline{D})$
191	20 29 46 51	add42d	$⊢ φ \to {\|A C\|}^{2} + {\|B D\|}^{2} + {\|A D\|}^{2} + {\|B C\|}^{2} = {\|A C\|}^{2} + {\|A D\|}^{2} + {\|B C\|}^{2} + {\|B D\|}^{2}$
192	181 190 191	3eqtr4d	$⊢ φ \to X Y = {\|A C\|}^{2} + {\|B D\|}^{2} + {\|A D\|}^{2} + {\|B C\|}^{2}$
193	53 155 192	3eqtr4d	$⊢ φ \to {\|\overline{A} C + B \overline{D}\|}^{2} + {\|\overline{A} D - B \overline{C}\|}^{2} = X Y$
194	193	oveq1d	$⊢ φ \to \frac{{\|\overline{A} C + B \overline{D}\|}^{2} + {\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}} = \frac{X Y}{M^{2}}$
195	8	nncnd	$⊢ φ \to M \in ℂ$
196	8	nnne0d	$⊢ φ \to M \neq 0$
197	55 195 196	absdivd	$⊢ φ \to \|\frac{\overline{A} C + B \overline{D}}{M}\| = \frac{\|\overline{A} C + B \overline{D}\|}{\|M\|}$
198	8	nnred	$⊢ φ \to M \in ℝ$
199	8	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
200	199	nn0ge0d	$⊢ φ \to 0 \leq M$
201	198 200	absidd	$⊢ φ \to \|M\| = M$
202	201	oveq2d	$⊢ φ \to \frac{\|\overline{A} C + B \overline{D}\|}{\|M\|} = \frac{\|\overline{A} C + B \overline{D}\|}{M}$
203	197 202	eqtrd	$⊢ φ \to \|\frac{\overline{A} C + B \overline{D}}{M}\| = \frac{\|\overline{A} C + B \overline{D}\|}{M}$
204	203	oveq1d	$⊢ φ \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} = {(\frac{\|\overline{A} C + B \overline{D}\|}{M})}^{2}$
205	55	abscld	$⊢ φ \to \|\overline{A} C + B \overline{D}\| \in ℝ$
206	205	recnd	$⊢ φ \to \|\overline{A} C + B \overline{D}\| \in ℂ$
207	206 195 196	sqdivd	$⊢ φ \to {(\frac{\|\overline{A} C + B \overline{D}\|}{M})}^{2} = \frac{{\|\overline{A} C + B \overline{D}\|}^{2}}{M^{2}}$
208	204 207	eqtrd	$⊢ φ \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} = \frac{{\|\overline{A} C + B \overline{D}\|}^{2}}{M^{2}}$
209	106 195 196	absdivd	$⊢ φ \to \|\frac{\overline{A} D - B \overline{C}}{M}\| = \frac{\|\overline{A} D - B \overline{C}\|}{\|M\|}$
210	201	oveq2d	$⊢ φ \to \frac{\|\overline{A} D - B \overline{C}\|}{\|M\|} = \frac{\|\overline{A} D - B \overline{C}\|}{M}$
211	209 210	eqtrd	$⊢ φ \to \|\frac{\overline{A} D - B \overline{C}}{M}\| = \frac{\|\overline{A} D - B \overline{C}\|}{M}$
212	211	oveq1d	$⊢ φ \to {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} = {(\frac{\|\overline{A} D - B \overline{C}\|}{M})}^{2}$
213	106	abscld	$⊢ φ \to \|\overline{A} D - B \overline{C}\| \in ℝ$
214	213	recnd	$⊢ φ \to \|\overline{A} D - B \overline{C}\| \in ℂ$
215	214 195 196	sqdivd	$⊢ φ \to {(\frac{\|\overline{A} D - B \overline{C}\|}{M})}^{2} = \frac{{\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}}$
216	212 215	eqtrd	$⊢ φ \to {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} = \frac{{\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}}$
217	208 216	oveq12d	$⊢ φ \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} + {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} = (\frac{{\|\overline{A} C + B \overline{D}\|}^{2}}{M^{2}}) + (\frac{{\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}})$
218	30 41	addcld	$⊢ φ \to {\|A C\|}^{2} + {\|B D\|}^{2} + \overline{A} C \overline{B} D + B \overline{C} A \overline{D} \in ℂ$
219	104 218	eqeltrd	$⊢ φ \to {\|\overline{A} C + B \overline{D}\|}^{2} \in ℂ$
220	52 41	subcld	$⊢ φ \to {\|A D\|}^{2} + {\|B C\|}^{2} - (\overline{A} C \overline{B} D + B \overline{C} A \overline{D}) \in ℂ$
221	154 220	eqeltrd	$⊢ φ \to {\|\overline{A} D - B \overline{C}\|}^{2} \in ℂ$
222	8	nnsqcld	$⊢ φ \to M^{2} \in ℕ$
223	222	nncnd	$⊢ φ \to M^{2} \in ℂ$
224	222	nnne0d	$⊢ φ \to M^{2} \neq 0$
225	219 221 223 224	divdird	$⊢ φ \to \frac{{\|\overline{A} C + B \overline{D}\|}^{2} + {\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}} = (\frac{{\|\overline{A} C + B \overline{D}\|}^{2}}{M^{2}}) + (\frac{{\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}})$
226	217 225	eqtr4d	$⊢ φ \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} + {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} = \frac{{\|\overline{A} C + B \overline{D}\|}^{2} + {\|\overline{A} D - B \overline{C}\|}^{2}}{M^{2}}$
227	182 156	eqeltrd	$⊢ φ \to {\|A\|}^{2} \in ℂ$
228	183 157	eqeltrd	$⊢ φ \to {\|B\|}^{2} \in ℂ$
229	227 228	addcld	$⊢ φ \to {\|A\|}^{2} + {\|B\|}^{2} \in ℂ$
230	6 229	eqeltrid	$⊢ φ \to X \in ℂ$
231	189 160	eqeltrd	$⊢ φ \to Y \in ℂ$
232	230 195 231 195 196 196	divmuldivd	$⊢ φ \to (\frac{X}{M}) (\frac{Y}{M}) = \frac{X Y}{M \cdot M}$
233	195	sqvald	$⊢ φ \to M^{2} = M \cdot M$
234	233	oveq2d	$⊢ φ \to \frac{X Y}{M^{2}} = \frac{X Y}{M \cdot M}$
235	232 234	eqtr4d	$⊢ φ \to (\frac{X}{M}) (\frac{Y}{M}) = \frac{X Y}{M^{2}}$
236	194 226 235	3eqtr4d	$⊢ φ \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} + {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} = (\frac{X}{M}) (\frac{Y}{M})$
237	230 55	nncand	$⊢ φ \to X - (X - (\overline{A} C + B \overline{D})) = \overline{A} C + B \overline{D}$
238	156 157 32 54	addsub4d	$⊢ φ \to A \overline{A} + B \overline{B} - (\overline{A} C + B \overline{D}) = (A \overline{A} - \overline{A} C) + B \overline{B} - B \overline{D}$
239	185	oveq1d	$⊢ φ \to X - (\overline{A} C + B \overline{D}) = A \overline{A} + B \overline{B} - (\overline{A} C + B \overline{D})$
240	31 13 15	subdid	$⊢ φ \to \overline{A} (A - C) = \overline{A} A - \overline{A} C$
241	31 13	mulcomd	$⊢ φ \to \overline{A} A = A \overline{A}$
242	241	oveq1d	$⊢ φ \to \overline{A} A - \overline{A} C = A \overline{A} - \overline{A} C$
243	240 242	eqtrd	$⊢ φ \to \overline{A} (A - C) = A \overline{A} - \overline{A} C$
244		cjsub	$⊢ (B \in ℂ \land D \in ℂ) \to \overline{B - D} = \overline{B} - \overline{D}$
245	22 24 244	syl2anc	$⊢ φ \to \overline{B - D} = \overline{B} - \overline{D}$
246	245	oveq2d	$⊢ φ \to B \overline{B - D} = B (\overline{B} - \overline{D})$
247	22 33 38	subdid	$⊢ φ \to B (\overline{B} - \overline{D}) = B \overline{B} - B \overline{D}$
248	246 247	eqtrd	$⊢ φ \to B \overline{B - D} = B \overline{B} - B \overline{D}$
249	243 248	oveq12d	$⊢ φ \to \overline{A} (A - C) + B \overline{B - D} = (A \overline{A} - \overline{A} C) + B \overline{B} - B \overline{D}$
250	238 239 249	3eqtr4d	$⊢ φ \to X - (\overline{A} C + B \overline{D}) = \overline{A} (A - C) + B \overline{B - D}$
251	250	oveq2d	$⊢ φ \to X - (X - (\overline{A} C + B \overline{D})) = X - (\overline{A} (A - C) + B \overline{B - D})$
252	237 251	eqtr3d	$⊢ φ \to \overline{A} C + B \overline{D} = X - (\overline{A} (A - C) + B \overline{B - D})$
253	252	oveq1d	$⊢ φ \to \frac{\overline{A} C + B \overline{D}}{M} = \frac{X - (\overline{A} (A - C) + B \overline{B - D})}{M}$
254	13 15	subcld	$⊢ φ \to A - C \in ℂ$
255	31 254	mulcld	$⊢ φ \to \overline{A} (A - C) \in ℂ$
256	22 24	subcld	$⊢ φ \to B - D \in ℂ$
257	256	cjcld	$⊢ φ \to \overline{B - D} \in ℂ$
258	22 257	mulcld	$⊢ φ \to B \overline{B - D} \in ℂ$
259	255 258	addcld	$⊢ φ \to \overline{A} (A - C) + B \overline{B - D} \in ℂ$
260	230 259 195 196	divsubdird	$⊢ φ \to \frac{X - (\overline{A} (A - C) + B \overline{B - D})}{M} = (\frac{X}{M}) - (\frac{\overline{A} (A - C) + B \overline{B - D}}{M})$
261	255 258 195 196	divdird	$⊢ φ \to \frac{\overline{A} (A - C) + B \overline{B - D}}{M} = (\frac{\overline{A} (A - C)}{M}) + (\frac{B \overline{B - D}}{M})$
262	31 254 195 196	divassd	$⊢ φ \to \frac{\overline{A} (A - C)}{M} = \overline{A} (\frac{A - C}{M})$
263	22 257 195 196	divassd	$⊢ φ \to \frac{B \overline{B - D}}{M} = B (\frac{\overline{B - D}}{M})$
264	256 195 196	cjdivd	$⊢ φ \to \overline{\frac{B - D}{M}} = \frac{\overline{B - D}}{\overline{M}}$
265	198	cjred	$⊢ φ \to \overline{M} = M$
266	265	oveq2d	$⊢ φ \to \frac{\overline{B - D}}{\overline{M}} = \frac{\overline{B - D}}{M}$
267	264 266	eqtrd	$⊢ φ \to \overline{\frac{B - D}{M}} = \frac{\overline{B - D}}{M}$
268	267	oveq2d	$⊢ φ \to B \overline{\frac{B - D}{M}} = B (\frac{\overline{B - D}}{M})$
269	263 268	eqtr4d	$⊢ φ \to \frac{B \overline{B - D}}{M} = B \overline{\frac{B - D}{M}}$
270	262 269	oveq12d	$⊢ φ \to (\frac{\overline{A} (A - C)}{M}) + (\frac{B \overline{B - D}}{M}) = \overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}}$
271	261 270	eqtrd	$⊢ φ \to \frac{\overline{A} (A - C) + B \overline{B - D}}{M} = \overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}}$
272	271	oveq2d	$⊢ φ \to (\frac{X}{M}) - (\frac{\overline{A} (A - C) + B \overline{B - D}}{M}) = (\frac{X}{M}) - (\overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}})$
273	253 260 272	3eqtrd	$⊢ φ \to \frac{\overline{A} C + B \overline{D}}{M} = (\frac{X}{M}) - (\overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}})$
274	11	nn0zd	$⊢ φ \to \frac{X}{M} \in ℤ$
275		zgz	$⊢ \frac{X}{M} \in ℤ \to \frac{X}{M} \in ℤ [i]$
276	274 275	syl	$⊢ φ \to \frac{X}{M} \in ℤ [i]$
277		gzcjcl	$⊢ A \in ℤ [i] \to \overline{A} \in ℤ [i]$
278	2 277	syl	$⊢ φ \to \overline{A} \in ℤ [i]$
279		gzmulcl	$⊢ (\overline{A} \in ℤ [i] \land \frac{A - C}{M} \in ℤ [i]) \to \overline{A} (\frac{A - C}{M}) \in ℤ [i]$
280	278 9 279	syl2anc	$⊢ φ \to \overline{A} (\frac{A - C}{M}) \in ℤ [i]$
281		gzcjcl	$⊢ \frac{B - D}{M} \in ℤ [i] \to \overline{\frac{B - D}{M}} \in ℤ [i]$
282	10 281	syl	$⊢ φ \to \overline{\frac{B - D}{M}} \in ℤ [i]$
283		gzmulcl	$⊢ (B \in ℤ [i] \land \overline{\frac{B - D}{M}} \in ℤ [i]) \to B \overline{\frac{B - D}{M}} \in ℤ [i]$
284	3 282 283	syl2anc	$⊢ φ \to B \overline{\frac{B - D}{M}} \in ℤ [i]$
285		gzaddcl	$⊢ (\overline{A} (\frac{A - C}{M}) \in ℤ [i] \land B \overline{\frac{B - D}{M}} \in ℤ [i]) \to \overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}} \in ℤ [i]$
286	280 284 285	syl2anc	$⊢ φ \to \overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}} \in ℤ [i]$
287		gzsubcl	$⊢ (\frac{X}{M} \in ℤ [i] \land \overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}} \in ℤ [i]) \to (\frac{X}{M}) - (\overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}}) \in ℤ [i]$
288	276 286 287	syl2anc	$⊢ φ \to (\frac{X}{M}) - (\overline{A} (\frac{A - C}{M}) + B \overline{\frac{B - D}{M}}) \in ℤ [i]$
289	273 288	eqeltrd	$⊢ φ \to \frac{\overline{A} C + B \overline{D}}{M} \in ℤ [i]$
290	254	cjcld	$⊢ φ \to \overline{A - C} \in ℂ$
291	22 290	mulcld	$⊢ φ \to B \overline{A - C} \in ℂ$
292	31 256	mulcld	$⊢ φ \to \overline{A} (B - D) \in ℂ$
293	291 292 195 196	divsubdird	$⊢ φ \to \frac{B \overline{A - C} - \overline{A} (B - D)}{M} = (\frac{B \overline{A - C}}{M}) - (\frac{\overline{A} (B - D)}{M})$
294		cjsub	$⊢ (A \in ℂ \land C \in ℂ) \to \overline{A - C} = \overline{A} - \overline{C}$
295	13 15 294	syl2anc	$⊢ φ \to \overline{A - C} = \overline{A} - \overline{C}$
296	295	oveq2d	$⊢ φ \to B \overline{A - C} = B (\overline{A} - \overline{C})$
297	22 31 36	subdid	$⊢ φ \to B (\overline{A} - \overline{C}) = B \overline{A} - B \overline{C}$
298	296 297	eqtrd	$⊢ φ \to B \overline{A - C} = B \overline{A} - B \overline{C}$
299	31 22 24	subdid	$⊢ φ \to \overline{A} (B - D) = \overline{A} B - \overline{A} D$
300	31 22	mulcomd	$⊢ φ \to \overline{A} B = B \overline{A}$
301	300	oveq1d	$⊢ φ \to \overline{A} B - \overline{A} D = B \overline{A} - \overline{A} D$
302	299 301	eqtrd	$⊢ φ \to \overline{A} (B - D) = B \overline{A} - \overline{A} D$
303	298 302	oveq12d	$⊢ φ \to B \overline{A - C} - \overline{A} (B - D) = B \overline{A} - B \overline{C} - (B \overline{A} - \overline{A} D)$
304	22 31	mulcld	$⊢ φ \to B \overline{A} \in ℂ$
305	304 37 105	nnncan1d	$⊢ φ \to B \overline{A} - B \overline{C} - (B \overline{A} - \overline{A} D) = \overline{A} D - B \overline{C}$
306	303 305	eqtrd	$⊢ φ \to B \overline{A - C} - \overline{A} (B - D) = \overline{A} D - B \overline{C}$
307	306	oveq1d	$⊢ φ \to \frac{B \overline{A - C} - \overline{A} (B - D)}{M} = \frac{\overline{A} D - B \overline{C}}{M}$
308	293 307	eqtr3d	$⊢ φ \to (\frac{B \overline{A - C}}{M}) - (\frac{\overline{A} (B - D)}{M}) = \frac{\overline{A} D - B \overline{C}}{M}$
309	22 290 195 196	divassd	$⊢ φ \to \frac{B \overline{A - C}}{M} = B (\frac{\overline{A - C}}{M})$
310	254 195 196	cjdivd	$⊢ φ \to \overline{\frac{A - C}{M}} = \frac{\overline{A - C}}{\overline{M}}$
311	265	oveq2d	$⊢ φ \to \frac{\overline{A - C}}{\overline{M}} = \frac{\overline{A - C}}{M}$
312	310 311	eqtrd	$⊢ φ \to \overline{\frac{A - C}{M}} = \frac{\overline{A - C}}{M}$
313	312	oveq2d	$⊢ φ \to B \overline{\frac{A - C}{M}} = B (\frac{\overline{A - C}}{M})$
314	309 313	eqtr4d	$⊢ φ \to \frac{B \overline{A - C}}{M} = B \overline{\frac{A - C}{M}}$
315	31 256 195 196	divassd	$⊢ φ \to \frac{\overline{A} (B - D)}{M} = \overline{A} (\frac{B - D}{M})$
316	314 315	oveq12d	$⊢ φ \to (\frac{B \overline{A - C}}{M}) - (\frac{\overline{A} (B - D)}{M}) = B \overline{\frac{A - C}{M}} - \overline{A} (\frac{B - D}{M})$
317	308 316	eqtr3d	$⊢ φ \to \frac{\overline{A} D - B \overline{C}}{M} = B \overline{\frac{A - C}{M}} - \overline{A} (\frac{B - D}{M})$
318		gzcjcl	$⊢ \frac{A - C}{M} \in ℤ [i] \to \overline{\frac{A - C}{M}} \in ℤ [i]$
319	9 318	syl	$⊢ φ \to \overline{\frac{A - C}{M}} \in ℤ [i]$
320		gzmulcl	$⊢ (B \in ℤ [i] \land \overline{\frac{A - C}{M}} \in ℤ [i]) \to B \overline{\frac{A - C}{M}} \in ℤ [i]$
321	3 319 320	syl2anc	$⊢ φ \to B \overline{\frac{A - C}{M}} \in ℤ [i]$
322		gzmulcl	$⊢ (\overline{A} \in ℤ [i] \land \frac{B - D}{M} \in ℤ [i]) \to \overline{A} (\frac{B - D}{M}) \in ℤ [i]$
323	278 10 322	syl2anc	$⊢ φ \to \overline{A} (\frac{B - D}{M}) \in ℤ [i]$
324		gzsubcl	$⊢ (B \overline{\frac{A - C}{M}} \in ℤ [i] \land \overline{A} (\frac{B - D}{M}) \in ℤ [i]) \to B \overline{\frac{A - C}{M}} - \overline{A} (\frac{B - D}{M}) \in ℤ [i]$
325	321 323 324	syl2anc	$⊢ φ \to B \overline{\frac{A - C}{M}} - \overline{A} (\frac{B - D}{M}) \in ℤ [i]$
326	317 325	eqeltrd	$⊢ φ \to \frac{\overline{A} D - B \overline{C}}{M} \in ℤ [i]$
327	1	4sqlem4a	$⊢ (\frac{\overline{A} C + B \overline{D}}{M} \in ℤ [i] \land \frac{\overline{A} D - B \overline{C}}{M} \in ℤ [i]) \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} + {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} \in S$
328	289 326 327	syl2anc	$⊢ φ \to {\|\frac{\overline{A} C + B \overline{D}}{M}\|}^{2} + {\|\frac{\overline{A} D - B \overline{C}}{M}\|}^{2} \in S$
329	236 328	eqeltrrd	$⊢ φ \to (\frac{X}{M}) (\frac{Y}{M}) \in S$

Metamath Proof Explorer

Theorem mul4sqlem

Proof