Theorem 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=\left\{n|\exists x\in \mathbb{Z}\exists y\in \mathbb{Z}\exists z\in \mathbb{Z}\exists w\in \mathbb{Z}n=x^2+y^2+z^2+w^2\right\}$$
	mul4sq.1	$$⊢\phi \to A\in \mathbb{Z}\left[i\right]$$
	mul4sq.2	$$⊢\phi \to B\in \mathbb{Z}\left[i\right]$$
	mul4sq.3	$$⊢\phi \to C\in \mathbb{Z}\left[i\right]$$
	mul4sq.4	$$⊢\phi \to D\in \mathbb{Z}\left[i\right]$$
	mul4sq.5	$$⊢X={\left|A\right|}^2+{\left|B\right|}^2$$
	mul4sq.6	$$⊢Y={\left|C\right|}^2+{\left|D\right|}^2$$
	mul4sq.7	$$⊢\phi \to M\in \mathbb{N}$$
	mul4sq.8	$$⊢\phi \to \frac{A-C}{M}\in \mathbb{Z}\left[i\right]$$
	mul4sq.9	$$⊢\phi \to \frac{B-D}{M}\in \mathbb{Z}\left[i\right]$$
	mul4sq.10	$$⊢\phi \to \frac{X}{M}\in {\mathbb{N}}_0$$
Assertion	mul4sqlem	$$⊢\phi \to \left(\frac{X}{M}\right)\left(\frac{Y}{M}\right)\in S$$

Proof

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