pellexlem6 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pellexlem6		Structured version Unicode version

Theorem pellexlem6 29128

Description: Lemma for pellex 29129. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)

**Hypotheses**
Ref	Expression
pellex.ann
pellex.bnn
pellex.cz
pellex.dnn
pellex.irr
pellex.enn
pellex.fnn
pellex.neq	$/\$
pellex.cn0
pellex.no1
pellex.no2
pellex.xcg
pellex.ycg

**Assertion**
Ref	Expression
pellexlem6

Distinct variable groups:

**Proof of Theorem pellexlem6**
Step	Hyp	Ref	Expression
1		pellex.ann	. . . . . . . . 9
2	1	nncnd 10330	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10330	. . . . . . . 8
5	2, 4	mulcld 9398	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10330	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10330	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10330	. . . . . . . . 9
12	9, 11	mulcld 9398	. . . . . . . 8
13	7, 12	mulcld 9398	. . . . . . 7
14	5, 13	subcld 9711	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10740	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 12933	. . . . 5
19	5, 13	negsubd 9717	. . . . . . . . . . 11
20	19	eqcomd 2443	. . . . . . . . . 10
21	20	oveq1d 6101	. . . . . . . . 9
22	1	nnred 10329	. . . . . . . . . . 11
23	3	nnred 10329	. . . . . . . . . . 11
24	22, 23	remulcld 9406	. . . . . . . . . 10
25	6	nnred 10329	. . . . . . . . . . 11
26	8	nnred 10329	. . . . . . . . . . . 12
27	10	nnred 10329	. . . . . . . . . . . 12
28	26, 27	remulcld 9406	. . . . . . . . . . 11
29	25, 28	remulcld 9406	. . . . . . . . . 10
30	29	renegcld 9767	. . . . . . . . . 10
31	16, 17	absrpcld 12926	. . . . . . . . . 10
32	3	nnzd 10738	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 11744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1229	. . . . . . . . . . 11
36	4	sqcld 11998	. . . . . . . . . . . . . . 15
37	11	sqcld 11998	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9398	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9715	. . . . . . . . . . . . . 14
40	4	sqvald 11997	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2471	. . . . . . . . . . . . 13
42	41	oveq1d 6101	. . . . . . . . . . . 12
43	23	resqcld 12026	. . . . . . . . . . . . . 14
44	27	resqcld 12026	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9406	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9768	. . . . . . . . . . . . 13
47		0re 9378	. . . . . . . . . . . . . 14
48	47	a1i 11	. . . . . . . . . . . . 13
49	16	abscld 12914	. . . . . . . . . . . . . . . . . . 19
50	49	recnd 9404	. . . . . . . . . . . . . . . . . 18
51	16, 17	absne0d 12925	. . . . . . . . . . . . . . . . . 18
52	50, 51	dividd 10097	. . . . . . . . . . . . . . . . 17
53		1z 10668	. . . . . . . . . . . . . . . . . 18
54	53	a1i 11	. . . . . . . . . . . . . . . . 17
55	52, 54	eqeltrd 2512	. . . . . . . . . . . . . . . 16
56		mod0 11707	. . . . . . . . . . . . . . . . 17 $/\$
57	49, 31, 56	syl2anc 661	. . . . . . . . . . . . . . . 16
58	55, 57	mpbird 232	. . . . . . . . . . . . . . 15
59	15	zred 10739	. . . . . . . . . . . . . . . 16
60		absmod0 12784	. . . . . . . . . . . . . . . 16 $/\$
61	59, 31, 60	syl2anc 661	. . . . . . . . . . . . . . 15
62	58, 61	mpbird 232	. . . . . . . . . . . . . 14
63		pellex.no2	. . . . . . . . . . . . . . 15
64	63	oveq1d 6101	. . . . . . . . . . . . . 14
65		0mod 11731	. . . . . . . . . . . . . . 15
66	31, 65	syl 16	. . . . . . . . . . . . . 14
67	62, 64, 66	3eqtr4d 2480	. . . . . . . . . . . . 13
68		modadd1 11737	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
69	46, 48, 45, 31, 67, 68	syl221anc 1229	. . . . . . . . . . . 12
70	38	addid2d 9562	. . . . . . . . . . . . . 14
71	11	sqvald 11997	. . . . . . . . . . . . . . 15
72	71	oveq2d 6102	. . . . . . . . . . . . . 14
73	7, 11, 11	mul12d 9570	. . . . . . . . . . . . . 14
74	70, 72, 73	3eqtrd 2474	. . . . . . . . . . . . 13
75	74	oveq1d 6101	. . . . . . . . . . . 12
76	42, 69, 75	3eqtrd 2474	. . . . . . . . . . 11
77	6	nnzd 10738	. . . . . . . . . . . . . 14
78	10	nnzd 10738	. . . . . . . . . . . . . 14
79	77, 78	zmulcld 10745	. . . . . . . . . . . . 13
80		pellex.ycg	. . . . . . . . . . . . . 14
81	80	eqcomd 2443	. . . . . . . . . . . . 13
82		modmul1 11744	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
83	27, 26, 79, 31, 81, 82	syl221anc 1229	. . . . . . . . . . . 12
84	9, 7, 11	mul12d 9570	. . . . . . . . . . . . 13
85	84	oveq1d 6101	. . . . . . . . . . . 12
86	83, 85	eqtrd 2470	. . . . . . . . . . 11
87	35, 76, 86	3eqtrd 2474	. . . . . . . . . 10
88		modadd1 11737	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
89	24, 29, 30, 31, 87, 88	syl221anc 1229	. . . . . . . . 9
90	13	negidd 9701	. . . . . . . . . 10
91	90	oveq1d 6101	. . . . . . . . 9
92	21, 89, 91	3eqtrd 2474	. . . . . . . 8
93	92, 66	eqtrd 2470	. . . . . . 7
94	24, 29	resubcld 9768	. . . . . . . 8
95		absmod0 12784	. . . . . . . 8 $/\$
96	94, 31, 95	syl2anc 661	. . . . . . 7
97	93, 96	mpbid 210	. . . . . 6
98	14	abscld 12914	. . . . . . 7
99		mod0 11707	. . . . . . 7 $/\$
100	98, 31, 99	syl2anc 661	. . . . . 6
101	97, 100	mpbid 210	. . . . 5
102	18, 101	eqeltrd 2512	. . . 4
103	94, 59, 17	redivcld 10151	. . . . 5
104		absz 12792	. . . . 5
105	103, 104	syl 16	. . . 4
106	102, 105	mpbird 232	. . 3
107		0lt1 9854	. . . . . . . 8
108		1re 9377	. . . . . . . . 9
109	47, 108	ltnlei 9487	. . . . . . . 8
110	107, 109	mpbi 208	. . . . . . 7
111	9, 4	mulcld 9398	. . . . . . . . . . . . . 14
112	2, 11	mulcld 9398	. . . . . . . . . . . . . 14
113	111, 112	subcld 9711	. . . . . . . . . . . . 13
114	113, 16, 17	divcld 10099	. . . . . . . . . . . 12
115	114	abscld 12914	. . . . . . . . . . 11
116	115	resqcld 12026	. . . . . . . . . 10
117	6	nnnn0d 10628	. . . . . . . . . . 11
118	117	nn0ge0d 10631	. . . . . . . . . 10
119	115	sqge0d 12027	. . . . . . . . . 10
120	25, 116, 118, 119	mulge0d 9908	. . . . . . . . 9
121	25, 116	remulcld 9406	. . . . . . . . . 10
122	48, 121	suble0d 9922	. . . . . . . . 9
123	120, 122	mpbird 232	. . . . . . . 8
124		breq1 4290	. . . . . . . 8
125	123, 124	syl5ibrcom 222	. . . . . . 7
126	110, 125	mtoi 178	. . . . . 6
127		absresq 12783	. . . . . . . . . . . 12
128	103, 127	syl 16	. . . . . . . . . . 11
129	14, 16, 17	sqdivd 12013	. . . . . . . . . . 11
130	14	sqvald 11997	. . . . . . . . . . . 12
131	130	oveq1d 6101	. . . . . . . . . . 11
132	128, 129, 131	3eqtrd 2474	. . . . . . . . . 10
133	26, 23	remulcld 9406	. . . . . . . . . . . . . . . 16
134	22, 27	remulcld 9406	. . . . . . . . . . . . . . . 16
135	133, 134	resubcld 9768	. . . . . . . . . . . . . . 15
136	135, 59, 17	redivcld 10151	. . . . . . . . . . . . . 14
137		absresq 12783	. . . . . . . . . . . . . 14
138	136, 137	syl 16	. . . . . . . . . . . . 13
139	113, 16, 17	sqdivd 12013	. . . . . . . . . . . . 13
140	138, 139	eqtrd 2470	. . . . . . . . . . . 12
141	140	oveq2d 6102	. . . . . . . . . . 11
142	113	sqcld 11998	. . . . . . . . . . . 12
143	16	sqcld 11998	. . . . . . . . . . . 12
144		sqne0 11924	. . . . . . . . . . . . . 14
145	16, 144	syl 16	. . . . . . . . . . . . 13
146	17, 145	mpbird 232	. . . . . . . . . . . 12
147	7, 142, 143, 146	divassd 10134	. . . . . . . . . . 11
148	113	sqvald 11997	. . . . . . . . . . . . 13
149	148	oveq2d 6102	. . . . . . . . . . . 12
150	149	oveq1d 6101	. . . . . . . . . . 11
151	141, 147, 150	3eqtr2d 2476	. . . . . . . . . 10
152	132, 151	oveq12d 6104	. . . . . . . . 9
153	14, 14	mulcld 9398	. . . . . . . . . 10
154	113, 113	mulcld 9398	. . . . . . . . . . 11
155	7, 154	mulcld 9398	. . . . . . . . . 10
156	153, 155, 143, 146	divsubdird 10138	. . . . . . . . 9
157	5, 13, 5, 13	mulsubd 9795	. . . . . . . . . . . 12
158	111, 112, 111, 112	mulsubd 9795	. . . . . . . . . . . . . 14
159	158	oveq2d 6102	. . . . . . . . . . . . 13
160	111, 111	mulcld 9398	. . . . . . . . . . . . . . 15
161	112, 112	mulcld 9398	. . . . . . . . . . . . . . 15
162	160, 161	addcld 9397	. . . . . . . . . . . . . 14
163	111, 112	mulcld 9398	. . . . . . . . . . . . . . 15
164	163, 163	addcld 9397	. . . . . . . . . . . . . 14
165	7, 162, 164	subdid 9792	. . . . . . . . . . . . 13
166	7, 160, 161	adddid 9402	. . . . . . . . . . . . . 14
167	7, 163, 163	adddid 9402	. . . . . . . . . . . . . 14
168	166, 167	oveq12d 6104	. . . . . . . . . . . . 13
169	159, 165, 168	3eqtrd 2474	. . . . . . . . . . . 12
170	157, 169	oveq12d 6104	. . . . . . . . . . 11
171	170	oveq1d 6101	. . . . . . . . . 10
172	5, 13	mulcomd 9399	. . . . . . . . . . . . . . . 16
173	7, 12, 5	mulassd 9401	. . . . . . . . . . . . . . . 16
174	2, 4	mulcomd 9399	. . . . . . . . . . . . . . . . . . 19
175	174	oveq2d 6102	. . . . . . . . . . . . . . . . . 18
176	9, 11, 4, 2	mul4d 9573	. . . . . . . . . . . . . . . . . 18
177	11, 2	mulcomd 9399	. . . . . . . . . . . . . . . . . . 19
178	177	oveq2d 6102	. . . . . . . . . . . . . . . . . 18
179	175, 176, 178	3eqtrd 2474	. . . . . . . . . . . . . . . . 17
180	179	oveq2d 6102	. . . . . . . . . . . . . . . 16
181	172, 173, 180	3eqtrd 2474	. . . . . . . . . . . . . . 15
182	181, 181	oveq12d 6104	. . . . . . . . . . . . . 14
183	182	oveq2d 6102	. . . . . . . . . . . . 13
184	183	oveq1d 6101	. . . . . . . . . . . 12
185	5, 5	mulcld 9398	. . . . . . . . . . . . . 14
186	13, 13	mulcld 9398	. . . . . . . . . . . . . 14
187	185, 186	addcld 9397	. . . . . . . . . . . . 13
188	7, 160	mulcld 9398	. . . . . . . . . . . . . 14
189	7, 161	mulcld 9398	. . . . . . . . . . . . . 14
190	188, 189	addcld 9397	. . . . . . . . . . . . 13
191	7, 163	mulcld 9398	. . . . . . . . . . . . . 14
192	191, 191	addcld 9397	. . . . . . . . . . . . 13
193	187, 190, 192	nnncan2d 9746	. . . . . . . . . . . 12
194	185, 186, 188, 189	addsub4d 9758	. . . . . . . . . . . . 13
195	5	sqvald 11997	. . . . . . . . . . . . . . 15
196	111	sqvald 11997	. . . . . . . . . . . . . . . 16
197	196	oveq2d 6102	. . . . . . . . . . . . . . 15
198	195, 197	oveq12d 6104	. . . . . . . . . . . . . 14
199	13	sqvald 11997	. . . . . . . . . . . . . . 15
200	112	sqvald 11997	. . . . . . . . . . . . . . . 16
201	200	oveq2d 6102	. . . . . . . . . . . . . . 15
202	199, 201	oveq12d 6104	. . . . . . . . . . . . . 14
203	198, 202	oveq12d 6104	. . . . . . . . . . . . 13
204	2, 4	sqmuld 12012	. . . . . . . . . . . . . . . 16
205	9, 4	sqmuld 12012	. . . . . . . . . . . . . . . . . 18
206	205	oveq2d 6102	. . . . . . . . . . . . . . . . 17
207	9	sqcld 11998	. . . . . . . . . . . . . . . . . 18
208	7, 207, 36	mulassd 9401	. . . . . . . . . . . . . . . . 17
209	206, 208	eqtr4d 2473	. . . . . . . . . . . . . . . 16
210	204, 209	oveq12d 6104	. . . . . . . . . . . . . . 15
211	7	sqvald 11997	. . . . . . . . . . . . . . . . . 18
212	9, 11	sqmuld 12012	. . . . . . . . . . . . . . . . . 18
213	211, 212	oveq12d 6104	. . . . . . . . . . . . . . . . 17
214	7, 12	sqmuld 12012	. . . . . . . . . . . . . . . . 17
215	7, 7	mulcld 9398	. . . . . . . . . . . . . . . . . 18
216	215, 207, 37	mulassd 9401	. . . . . . . . . . . . . . . . 17
217	213, 214, 216	3eqtr4d 2480	. . . . . . . . . . . . . . . 16
218	2, 11	sqmuld 12012	. . . . . . . . . . . . . . . . . 18
219	218	oveq2d 6102	. . . . . . . . . . . . . . . . 17
220	2	sqcld 11998	. . . . . . . . . . . . . . . . . 18
221	7, 220, 37	mulassd 9401	. . . . . . . . . . . . . . . . 17
222	219, 221	eqtr4d 2473	. . . . . . . . . . . . . . . 16
223	217, 222	oveq12d 6104	. . . . . . . . . . . . . . 15
224	210, 223	oveq12d 6104	. . . . . . . . . . . . . 14
225	7, 207	mulcld 9398	. . . . . . . . . . . . . . . . 17
226	220, 225, 36	subdird 9793	. . . . . . . . . . . . . . . 16
227		pellex.no1	. . . . . . . . . . . . . . . . 17
228	227	oveq1d 6101	. . . . . . . . . . . . . . . 16
229	226, 228	eqtr3d 2472	. . . . . . . . . . . . . . 15
230	7, 7, 207	mulassd 9401	. . . . . . . . . . . . . . . . . 18
231	230	oveq1d 6101	. . . . . . . . . . . . . . . . 17
232	231	oveq1d 6101	. . . . . . . . . . . . . . . 16
233	215, 207	mulcld 9398	. . . . . . . . . . . . . . . . 17
234	7, 220	mulcld 9398	. . . . . . . . . . . . . . . . 17
235	233, 234, 37	subdird 9793	. . . . . . . . . . . . . . . 16
236		subdi 9770	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	236	eqcomd 2443	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
238	7, 225, 220, 237	syl3anc 1218	. . . . . . . . . . . . . . . . . 18
239		negsubdi2 9660	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
240	239	eqcomd 2443	. . . . . . . . . . . . . . . . . . . . 21 $/\$
241	220, 225, 240	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
242	227	negeqd 9596	. . . . . . . . . . . . . . . . . . . 20
243	241, 242	eqtrd 2470	. . . . . . . . . . . . . . . . . . 19
244	243	oveq2d 6102	. . . . . . . . . . . . . . . . . 18
245	7, 16	mulneg2d 9790	. . . . . . . . . . . . . . . . . 18
246	238, 244, 245	3eqtrd 2474	. . . . . . . . . . . . . . . . 17
247	246	oveq1d 6101	. . . . . . . . . . . . . . . 16
248	232, 235, 247	3eqtr3d 2478	. . . . . . . . . . . . . . 15
249	229, 248	oveq12d 6104	. . . . . . . . . . . . . 14
250	7, 16	mulcld 9398	. . . . . . . . . . . . . . . . . 18
251	250, 37	mulneg1d 9789	. . . . . . . . . . . . . . . . 17
252	7, 16	mulcomd 9399	. . . . . . . . . . . . . . . . . . . 20
253	252	oveq1d 6101	. . . . . . . . . . . . . . . . . . 19
254	16, 7, 37	mulassd 9401	. . . . . . . . . . . . . . . . . . 19
255	253, 254	eqtrd 2470	. . . . . . . . . . . . . . . . . 18
256	255	negeqd 9596	. . . . . . . . . . . . . . . . 17
257	251, 256	eqtrd 2470	. . . . . . . . . . . . . . . 16
258	257	oveq2d 6102	. . . . . . . . . . . . . . 15
259	16, 36	mulcld 9398	. . . . . . . . . . . . . . . 16
260	16, 38	mulcld 9398	. . . . . . . . . . . . . . . 16
261	259, 260	negsubd 9717	. . . . . . . . . . . . . . 15
262	63	oveq2d 6102	. . . . . . . . . . . . . . . 16
263		subdi 9770	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
264	263	eqcomd 2443	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
265	16, 36, 38, 264	syl3anc 1218	. . . . . . . . . . . . . . . 16
266	16	sqvald 11997	. . . . . . . . . . . . . . . 16
267	262, 265, 266	3eqtr4d 2480	. . . . . . . . . . . . . . 15
268	258, 261, 267	3eqtrd 2474	. . . . . . . . . . . . . 14
269	224, 249, 268	3eqtrd 2474	. . . . . . . . . . . . 13
270	194, 203, 269	3eqtr2d 2476	. . . . . . . . . . . 12
271	184, 193, 270	3eqtrd 2474	. . . . . . . . . . 11
272	271	oveq1d 6101	. . . . . . . . . 10
273	143, 146	dividd 10097	. . . . . . . . . 10
274	171, 272, 273	3eqtrd 2474	. . . . . . . . 9
275	152, 156, 274	3eqtr2d 2476	. . . . . . . 8
276	275	adantr 465	. . . . . . 7 $/\$
277		simpr 461	. . . . . . . . . . . 12 $/\$
278	277	oveq1d 6101	. . . . . . . . . . 11 $/\$
279	278	fveq2d 5690	. . . . . . . . . 10 $/\$
280	16, 17	div0d 10098	. . . . . . . . . . . 12
281	280	abs00bd 12772	. . . . . . . . . . 11
282	281	adantr 465	. . . . . . . . . 10 $/\$
283	279, 282	eqtrd 2470	. . . . . . . . 9 $/\$
284	283	sq0id 11951	. . . . . . . 8 $/\$
285	284	oveq1d 6101	. . . . . . 7 $/\$
286	276, 285	eqtr3d 2472	. . . . . 6 $/\$
287	126, 286	mtand 659	. . . . 5
288	287	neneqad 2676	. . . 4
289	14, 16, 288, 17	divne0d 10115	. . 3
290		nnabscl 12805	. . 3 $/\$
291	106, 289, 290	syl2anc 661	. 2
292	113, 16, 17	absdivd 12933	. . . . 5
293		negsub 9649	. . . . . . . . . . . 12 $/\$
294	293	eqcomd 2443	. . . . . . . . . . 11 $/\$
295	111, 112, 294	syl2anc 661	. . . . . . . . . 10
296	295	oveq1d 6101	. . . . . . . . 9
297	134	renegcld 9767	. . . . . . . . . 10
298	11, 4	mulcomd 9399	. . . . . . . . . . . 12
299	298	oveq1d 6101	. . . . . . . . . . 11
300		modmul1 11744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
301	26, 27, 32, 31, 80, 300	syl221anc 1229	. . . . . . . . . . 11
302		modmul1 11744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
303	22, 23, 78, 31, 33, 302	syl221anc 1229	. . . . . . . . . . 11
304	299, 301, 303	3eqtr4d 2480	. . . . . . . . . 10
305		modadd1 11737	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
306	133, 134, 297, 31, 304, 305	syl221anc 1229	. . . . . . . . 9
307	112	negidd 9701	. . . . . . . . . 10
308	307	oveq1d 6101	. . . . . . . . 9
309	296, 306, 308	3eqtrd 2474	. . . . . . . 8
310	309, 66	eqtrd 2470	. . . . . . 7
311		absmod0 12784	. . . . . . . 8 $/\$
312	135, 31, 311	syl2anc 661	. . . . . . 7
313	310, 312	mpbid 210	. . . . . 6
314	113	abscld 12914	. . . . . . 7
315		mod0 11707	. . . . . . 7 $/\$
316	314, 31, 315	syl2anc 661	. . . . . 6
317	313, 316	mpbid 210	. . . . 5
318	292, 317	eqeltrd 2512	. . . 4
319		absz 12792	. . . . 5
320	136, 319	syl 16	. . . 4
321	318, 320	mpbird 232	. . 3
322		pellex.neq	. . . . . . 7 $/\$
323	10	nnne0d 10358	. . . . . . . . 9
324	3	nnne0d 10358	. . . . . . . . 9
325	9, 11, 2, 4, 323, 324	divmuleqd 10145	. . . . . . . 8
326	63	adantr 465	. . . . . . . . . . . . . . 15 $/\$
327	326	eqcomd 2443	. . . . . . . . . . . . . 14 $/\$
328	327	oveq2d 6102	. . . . . . . . . . . . 13 $/\$
329	9, 11, 323	divcld 10099	. . . . . . . . . . . . . . . 16
330	329	sqcld 11998	. . . . . . . . . . . . . . 15
331	330	adantr 465	. . . . . . . . . . . . . 14 $/\$
332	36	adantr 465	. . . . . . . . . . . . . 14 $/\$
333	38	adantr 465	. . . . . . . . . . . . . 14 $/\$
334	331, 332, 333	subdid 9792	. . . . . . . . . . . . 13 $/\$
335		oveq1 6093	. . . . . . . . . . . . . . . . 17
336	335	oveq1d 6101	. . . . . . . . . . . . . . . 16
337	336	adantl 466	. . . . . . . . . . . . . . 15 $/\$
338	2	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
339	4	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
340	324	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
341	338, 339, 340	sqdivd 12013	. . . . . . . . . . . . . . . 16 $/\$
342	341	oveq1d 6101	. . . . . . . . . . . . . . 15 $/\$
343	220	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
344		sqne0 11924	. . . . . . . . . . . . . . . . . . 19
345	4, 344	syl 16	. . . . . . . . . . . . . . . . . 18
346	324, 345	mpbird 232	. . . . . . . . . . . . . . . . 17
347	346	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
348	343, 332, 347	divcan1d 10100	. . . . . . . . . . . . . . 15 $/\$
349	337, 342, 348	3eqtrd 2474	. . . . . . . . . . . . . 14 $/\$
350	7	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
351	37	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
352	331, 350, 351	mul12d 9570	. . . . . . . . . . . . . . 15 $/\$
353	9	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
354	11	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
355	323	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
356	353, 354, 355	sqdivd 12013	. . . . . . . . . . . . . . . . 17 $/\$
357	356	oveq1d 6101	. . . . . . . . . . . . . . . 16 $/\$
358	357	oveq2d 6102	. . . . . . . . . . . . . . 15 $/\$
359	207	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
360		sqne0 11924	. . . . . . . . . . . . . . . . . . . 20
361	11, 360	syl 16	. . . . . . . . . . . . . . . . . . 19
362	323, 361	mpbird 232	. . . . . . . . . . . . . . . . . 18
363	362	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
364	359, 351, 363	divcan1d 10100	. . . . . . . . . . . . . . . 16 $/\$