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 Visualization version Unicode version

Theorem pellexlem6 35678

Description: Lemma for pellex 35679. 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 10625	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10625	. . . . . . . 8
5	2, 4	mulcld 9663	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10625	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10625	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10625	. . . . . . . . 9
12	9, 11	mulcld 9663	. . . . . . . 8
13	7, 12	mulcld 9663	. . . . . . 7
14	5, 13	subcld 9986	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 11041	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13517	. . . . 5
19	5, 13	negsubd 9992	. . . . . . . . . . 11
20	19	eqcomd 2457	. . . . . . . . . 10
21	20	oveq1d 6305	. . . . . . . . 9
22	1	nnred 10624	. . . . . . . . . . 11
23	3	nnred 10624	. . . . . . . . . . 11
24	22, 23	remulcld 9671	. . . . . . . . . 10
25	6	nnred 10624	. . . . . . . . . . 11
26	8	nnred 10624	. . . . . . . . . . . 12
27	10	nnred 10624	. . . . . . . . . . . 12
28	26, 27	remulcld 9671	. . . . . . . . . . 11
29	25, 28	remulcld 9671	. . . . . . . . . 10
30	29	renegcld 10046	. . . . . . . . . 10
31	16, 17	absrpcld 13510	. . . . . . . . . 10
32	3	nnzd 11039	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 12143	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1279	. . . . . . . . . . 11
36	4	sqcld 12414	. . . . . . . . . . . . . . 15
37	11	sqcld 12414	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9663	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9990	. . . . . . . . . . . . . 14
40	4	sqvald 12413	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2486	. . . . . . . . . . . . 13
42	41	oveq1d 6305	. . . . . . . . . . . 12
43	23	resqcld 12442	. . . . . . . . . . . . . 14
44	27	resqcld 12442	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9671	. . . . . . . . . . . . . 14
46	43, 45	resubcld 10047	. . . . . . . . . . . . 13
47		0red 9644	. . . . . . . . . . . . 13
48	16	abscld 13498	. . . . . . . . . . . . . . . . . . 19
49	48	recnd 9669	. . . . . . . . . . . . . . . . . 18
50	16, 17	absne0d 13509	. . . . . . . . . . . . . . . . . 18
51	49, 50	dividd 10381	. . . . . . . . . . . . . . . . 17
52		1zzd 10968	. . . . . . . . . . . . . . . . 17
53	51, 52	eqeltrd 2529	. . . . . . . . . . . . . . . 16
54		mod0 12103	. . . . . . . . . . . . . . . . 17 $/\$
55	48, 31, 54	syl2anc 667	. . . . . . . . . . . . . . . 16
56	53, 55	mpbird 236	. . . . . . . . . . . . . . 15
57	15	zred 11040	. . . . . . . . . . . . . . . 16
58		absmod0 13366	. . . . . . . . . . . . . . . 16 $/\$
59	57, 31, 58	syl2anc 667	. . . . . . . . . . . . . . 15
60	56, 59	mpbird 236	. . . . . . . . . . . . . 14
61		pellex.no2	. . . . . . . . . . . . . . 15
62	61	oveq1d 6305	. . . . . . . . . . . . . 14
63		0mod 12128	. . . . . . . . . . . . . . 15
64	31, 63	syl 17	. . . . . . . . . . . . . 14
65	60, 62, 64	3eqtr4d 2495	. . . . . . . . . . . . 13
66		modadd1 12134	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	46, 47, 45, 31, 65, 66	syl221anc 1279	. . . . . . . . . . . 12
68	38	addid2d 9834	. . . . . . . . . . . . . 14
69	11	sqvald 12413	. . . . . . . . . . . . . . 15
70	69	oveq2d 6306	. . . . . . . . . . . . . 14
71	7, 11, 11	mul12d 9842	. . . . . . . . . . . . . 14
72	68, 70, 71	3eqtrd 2489	. . . . . . . . . . . . 13
73	72	oveq1d 6305	. . . . . . . . . . . 12
74	42, 67, 73	3eqtrd 2489	. . . . . . . . . . 11
75	6	nnzd 11039	. . . . . . . . . . . . . 14
76	10	nnzd 11039	. . . . . . . . . . . . . 14
77	75, 76	zmulcld 11046	. . . . . . . . . . . . 13
78		pellex.ycg	. . . . . . . . . . . . . 14
79	78	eqcomd 2457	. . . . . . . . . . . . 13
80		modmul1 12143	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
81	27, 26, 77, 31, 79, 80	syl221anc 1279	. . . . . . . . . . . 12
82	9, 7, 11	mul12d 9842	. . . . . . . . . . . . 13
83	82	oveq1d 6305	. . . . . . . . . . . 12
84	81, 83	eqtrd 2485	. . . . . . . . . . 11
85	35, 74, 84	3eqtrd 2489	. . . . . . . . . 10
86		modadd1 12134	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
87	24, 29, 30, 31, 85, 86	syl221anc 1279	. . . . . . . . 9
88	13	negidd 9976	. . . . . . . . . 10
89	88	oveq1d 6305	. . . . . . . . 9
90	21, 87, 89	3eqtrd 2489	. . . . . . . 8
91	90, 64	eqtrd 2485	. . . . . . 7
92	24, 29	resubcld 10047	. . . . . . . 8
93		absmod0 13366	. . . . . . . 8 $/\$
94	92, 31, 93	syl2anc 667	. . . . . . 7
95	91, 94	mpbid 214	. . . . . 6
96	14	abscld 13498	. . . . . . 7
97		mod0 12103	. . . . . . 7 $/\$
98	96, 31, 97	syl2anc 667	. . . . . 6
99	95, 98	mpbid 214	. . . . 5
100	18, 99	eqeltrd 2529	. . . 4
101	92, 57, 17	redivcld 10435	. . . . 5
102		absz 13374	. . . . 5
103	101, 102	syl 17	. . . 4
104	100, 103	mpbird 236	. . 3
105		0lt1 10136	. . . . . . . 8
106		0re 9643	. . . . . . . . 9
107		1re 9642	. . . . . . . . 9
108	106, 107	ltnlei 9755	. . . . . . . 8
109	105, 108	mpbi 212	. . . . . . 7
110	9, 4	mulcld 9663	. . . . . . . . . . . . . 14
111	2, 11	mulcld 9663	. . . . . . . . . . . . . 14
112	110, 111	subcld 9986	. . . . . . . . . . . . 13
113	112, 16, 17	divcld 10383	. . . . . . . . . . . 12
114	113	abscld 13498	. . . . . . . . . . 11
115	114	resqcld 12442	. . . . . . . . . 10
116	6	nnnn0d 10925	. . . . . . . . . . 11
117	116	nn0ge0d 10928	. . . . . . . . . 10
118	114	sqge0d 12443	. . . . . . . . . 10
119	25, 115, 117, 118	mulge0d 10190	. . . . . . . . 9
120	25, 115	remulcld 9671	. . . . . . . . . 10
121	47, 120	suble0d 10204	. . . . . . . . 9
122	119, 121	mpbird 236	. . . . . . . 8
123		breq1 4405	. . . . . . . 8
124	122, 123	syl5ibrcom 226	. . . . . . 7
125	109, 124	mtoi 182	. . . . . 6
126		absresq 13365	. . . . . . . . . . . 12
127	101, 126	syl 17	. . . . . . . . . . 11
128	14, 16, 17	sqdivd 12429	. . . . . . . . . . 11
129	14	sqvald 12413	. . . . . . . . . . . 12
130	129	oveq1d 6305	. . . . . . . . . . 11
131	127, 128, 130	3eqtrd 2489	. . . . . . . . . 10
132	26, 23	remulcld 9671	. . . . . . . . . . . . . . . 16
133	22, 27	remulcld 9671	. . . . . . . . . . . . . . . 16
134	132, 133	resubcld 10047	. . . . . . . . . . . . . . 15
135	134, 57, 17	redivcld 10435	. . . . . . . . . . . . . 14
136		absresq 13365	. . . . . . . . . . . . . 14
137	135, 136	syl 17	. . . . . . . . . . . . 13
138	112, 16, 17	sqdivd 12429	. . . . . . . . . . . . 13
139	137, 138	eqtrd 2485	. . . . . . . . . . . 12
140	139	oveq2d 6306	. . . . . . . . . . 11
141	112	sqcld 12414	. . . . . . . . . . . 12
142	16	sqcld 12414	. . . . . . . . . . . 12
143		sqne0 12341	. . . . . . . . . . . . . 14
144	16, 143	syl 17	. . . . . . . . . . . . 13
145	17, 144	mpbird 236	. . . . . . . . . . . 12
146	7, 141, 142, 145	divassd 10418	. . . . . . . . . . 11
147	112	sqvald 12413	. . . . . . . . . . . . 13
148	147	oveq2d 6306	. . . . . . . . . . . 12
149	148	oveq1d 6305	. . . . . . . . . . 11
150	140, 146, 149	3eqtr2d 2491	. . . . . . . . . 10
151	131, 150	oveq12d 6308	. . . . . . . . 9
152	14, 14	mulcld 9663	. . . . . . . . . 10
153	112, 112	mulcld 9663	. . . . . . . . . . 11
154	7, 153	mulcld 9663	. . . . . . . . . 10
155	152, 154, 142, 145	divsubdird 10422	. . . . . . . . 9
156	5, 13, 5, 13	mulsubd 10077	. . . . . . . . . . . 12
157	110, 111, 110, 111	mulsubd 10077	. . . . . . . . . . . . . 14
158	157	oveq2d 6306	. . . . . . . . . . . . 13
159	110, 110	mulcld 9663	. . . . . . . . . . . . . . 15
160	111, 111	mulcld 9663	. . . . . . . . . . . . . . 15
161	159, 160	addcld 9662	. . . . . . . . . . . . . 14
162	110, 111	mulcld 9663	. . . . . . . . . . . . . . 15
163	162, 162	addcld 9662	. . . . . . . . . . . . . 14
164	7, 161, 163	subdid 10074	. . . . . . . . . . . . 13
165	7, 159, 160	adddid 9667	. . . . . . . . . . . . . 14
166	7, 162, 162	adddid 9667	. . . . . . . . . . . . . 14
167	165, 166	oveq12d 6308	. . . . . . . . . . . . 13
168	158, 164, 167	3eqtrd 2489	. . . . . . . . . . . 12
169	156, 168	oveq12d 6308	. . . . . . . . . . 11
170	169	oveq1d 6305	. . . . . . . . . 10
171	5, 13	mulcomd 9664	. . . . . . . . . . . . . . . 16
172	7, 12, 5	mulassd 9666	. . . . . . . . . . . . . . . 16
173	2, 4	mulcomd 9664	. . . . . . . . . . . . . . . . . . 19
174	173	oveq2d 6306	. . . . . . . . . . . . . . . . . 18
175	9, 11, 4, 2	mul4d 9845	. . . . . . . . . . . . . . . . . 18
176	11, 2	mulcomd 9664	. . . . . . . . . . . . . . . . . . 19
177	176	oveq2d 6306	. . . . . . . . . . . . . . . . . 18
178	174, 175, 177	3eqtrd 2489	. . . . . . . . . . . . . . . . 17
179	178	oveq2d 6306	. . . . . . . . . . . . . . . 16
180	171, 172, 179	3eqtrd 2489	. . . . . . . . . . . . . . 15
181	180, 180	oveq12d 6308	. . . . . . . . . . . . . 14
182	181	oveq2d 6306	. . . . . . . . . . . . 13
183	182	oveq1d 6305	. . . . . . . . . . . 12
184	5, 5	mulcld 9663	. . . . . . . . . . . . . 14
185	13, 13	mulcld 9663	. . . . . . . . . . . . . 14
186	184, 185	addcld 9662	. . . . . . . . . . . . 13
187	7, 159	mulcld 9663	. . . . . . . . . . . . . 14
188	7, 160	mulcld 9663	. . . . . . . . . . . . . 14
189	187, 188	addcld 9662	. . . . . . . . . . . . 13
190	7, 162	mulcld 9663	. . . . . . . . . . . . . 14
191	190, 190	addcld 9662	. . . . . . . . . . . . 13
192	186, 189, 191	nnncan2d 10021	. . . . . . . . . . . 12
193	184, 185, 187, 188	addsub4d 10033	. . . . . . . . . . . . 13
194	5	sqvald 12413	. . . . . . . . . . . . . . 15
195	110	sqvald 12413	. . . . . . . . . . . . . . . 16
196	195	oveq2d 6306	. . . . . . . . . . . . . . 15
197	194, 196	oveq12d 6308	. . . . . . . . . . . . . 14
198	13	sqvald 12413	. . . . . . . . . . . . . . 15
199	111	sqvald 12413	. . . . . . . . . . . . . . . 16
200	199	oveq2d 6306	. . . . . . . . . . . . . . 15
201	198, 200	oveq12d 6308	. . . . . . . . . . . . . 14
202	197, 201	oveq12d 6308	. . . . . . . . . . . . 13
203	2, 4	sqmuld 12428	. . . . . . . . . . . . . . . 16
204	9, 4	sqmuld 12428	. . . . . . . . . . . . . . . . . 18
205	204	oveq2d 6306	. . . . . . . . . . . . . . . . 17
206	9	sqcld 12414	. . . . . . . . . . . . . . . . . 18
207	7, 206, 36	mulassd 9666	. . . . . . . . . . . . . . . . 17
208	205, 207	eqtr4d 2488	. . . . . . . . . . . . . . . 16
209	203, 208	oveq12d 6308	. . . . . . . . . . . . . . 15
210	7	sqvald 12413	. . . . . . . . . . . . . . . . . 18
211	9, 11	sqmuld 12428	. . . . . . . . . . . . . . . . . 18
212	210, 211	oveq12d 6308	. . . . . . . . . . . . . . . . 17
213	7, 12	sqmuld 12428	. . . . . . . . . . . . . . . . 17
214	7, 7	mulcld 9663	. . . . . . . . . . . . . . . . . 18
215	214, 206, 37	mulassd 9666	. . . . . . . . . . . . . . . . 17
216	212, 213, 215	3eqtr4d 2495	. . . . . . . . . . . . . . . 16
217	2, 11	sqmuld 12428	. . . . . . . . . . . . . . . . . 18
218	217	oveq2d 6306	. . . . . . . . . . . . . . . . 17
219	2	sqcld 12414	. . . . . . . . . . . . . . . . . 18
220	7, 219, 37	mulassd 9666	. . . . . . . . . . . . . . . . 17
221	218, 220	eqtr4d 2488	. . . . . . . . . . . . . . . 16
222	216, 221	oveq12d 6308	. . . . . . . . . . . . . . 15
223	209, 222	oveq12d 6308	. . . . . . . . . . . . . 14
224	7, 206	mulcld 9663	. . . . . . . . . . . . . . . . 17
225	219, 224, 36	subdird 10075	. . . . . . . . . . . . . . . 16
226		pellex.no1	. . . . . . . . . . . . . . . . 17
227	226	oveq1d 6305	. . . . . . . . . . . . . . . 16
228	225, 227	eqtr3d 2487	. . . . . . . . . . . . . . 15
229	7, 7, 206	mulassd 9666	. . . . . . . . . . . . . . . . . 18
230	229	oveq1d 6305	. . . . . . . . . . . . . . . . 17
231	230	oveq1d 6305	. . . . . . . . . . . . . . . 16
232	214, 206	mulcld 9663	. . . . . . . . . . . . . . . . 17
233	7, 219	mulcld 9663	. . . . . . . . . . . . . . . . 17
234	232, 233, 37	subdird 10075	. . . . . . . . . . . . . . . 16
235		subdi 10052	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
236	235	eqcomd 2457	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
237	7, 224, 219, 236	syl3anc 1268	. . . . . . . . . . . . . . . . . 18
238		negsubdi2 9933	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
239	238	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
240	219, 224, 239	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20
241	226	negeqd 9869	. . . . . . . . . . . . . . . . . . . 20
242	240, 241	eqtrd 2485	. . . . . . . . . . . . . . . . . . 19
243	242	oveq2d 6306	. . . . . . . . . . . . . . . . . 18
244	7, 16	mulneg2d 10072	. . . . . . . . . . . . . . . . . 18
245	237, 243, 244	3eqtrd 2489	. . . . . . . . . . . . . . . . 17
246	245	oveq1d 6305	. . . . . . . . . . . . . . . 16
247	231, 234, 246	3eqtr3d 2493	. . . . . . . . . . . . . . 15
248	228, 247	oveq12d 6308	. . . . . . . . . . . . . 14
249	7, 16	mulcld 9663	. . . . . . . . . . . . . . . . . 18
250	249, 37	mulneg1d 10071	. . . . . . . . . . . . . . . . 17
251	7, 16	mulcomd 9664	. . . . . . . . . . . . . . . . . . . 20
252	251	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19
253	16, 7, 37	mulassd 9666	. . . . . . . . . . . . . . . . . . 19
254	252, 253	eqtrd 2485	. . . . . . . . . . . . . . . . . 18
255	254	negeqd 9869	. . . . . . . . . . . . . . . . 17
256	250, 255	eqtrd 2485	. . . . . . . . . . . . . . . 16
257	256	oveq2d 6306	. . . . . . . . . . . . . . 15
258	16, 36	mulcld 9663	. . . . . . . . . . . . . . . 16
259	16, 38	mulcld 9663	. . . . . . . . . . . . . . . 16
260	258, 259	negsubd 9992	. . . . . . . . . . . . . . 15
261	61	oveq2d 6306	. . . . . . . . . . . . . . . 16
262		subdi 10052	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
263	262	eqcomd 2457	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
264	16, 36, 38, 263	syl3anc 1268	. . . . . . . . . . . . . . . 16
265	16	sqvald 12413	. . . . . . . . . . . . . . . 16
266	261, 264, 265	3eqtr4d 2495	. . . . . . . . . . . . . . 15
267	257, 260, 266	3eqtrd 2489	. . . . . . . . . . . . . 14
268	223, 248, 267	3eqtrd 2489	. . . . . . . . . . . . 13
269	193, 202, 268	3eqtr2d 2491	. . . . . . . . . . . 12
270	183, 192, 269	3eqtrd 2489	. . . . . . . . . . 11
271	270	oveq1d 6305	. . . . . . . . . 10
272	142, 145	dividd 10381	. . . . . . . . . 10
273	170, 271, 272	3eqtrd 2489	. . . . . . . . 9
274	151, 155, 273	3eqtr2d 2491	. . . . . . . 8
275	274	adantr 467	. . . . . . 7 $/\$
276		simpr 463	. . . . . . . . . . . 12 $/\$
277	276	oveq1d 6305	. . . . . . . . . . 11 $/\$
278	277	fveq2d 5869	. . . . . . . . . 10 $/\$
279	16, 17	div0d 10382	. . . . . . . . . . . 12
280	279	abs00bd 13354	. . . . . . . . . . 11
281	280	adantr 467	. . . . . . . . . 10 $/\$
282	278, 281	eqtrd 2485	. . . . . . . . 9 $/\$
283	282	sq0id 12368	. . . . . . . 8 $/\$
284	283	oveq1d 6305	. . . . . . 7 $/\$
285	275, 284	eqtr3d 2487	. . . . . 6 $/\$
286	125, 285	mtand 665	. . . . 5
287	286	neqned 2631	. . . 4
288	14, 16, 287, 17	divne0d 10399	. . 3
289		nnabscl 13388	. . 3 $/\$
290	104, 288, 289	syl2anc 667	. 2
291	112, 16, 17	absdivd 13517	. . . . 5
292		negsub 9922	. . . . . . . . . . . 12 $/\$
293	292	eqcomd 2457	. . . . . . . . . . 11 $/\$
294	110, 111, 293	syl2anc 667	. . . . . . . . . 10
295	294	oveq1d 6305	. . . . . . . . 9
296	133	renegcld 10046	. . . . . . . . . 10
297	11, 4	mulcomd 9664	. . . . . . . . . . . 12
298	297	oveq1d 6305	. . . . . . . . . . 11
299		modmul1 12143	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
300	26, 27, 32, 31, 78, 299	syl221anc 1279	. . . . . . . . . . 11
301		modmul1 12143	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
302	22, 23, 76, 31, 33, 301	syl221anc 1279	. . . . . . . . . . 11
303	298, 300, 302	3eqtr4d 2495	. . . . . . . . . 10
304		modadd1 12134	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
305	132, 133, 296, 31, 303, 304	syl221anc 1279	. . . . . . . . 9
306	111	negidd 9976	. . . . . . . . . 10
307	306	oveq1d 6305	. . . . . . . . 9
308	295, 305, 307	3eqtrd 2489	. . . . . . . 8
309	308, 64	eqtrd 2485	. . . . . . 7
310		absmod0 13366	. . . . . . . 8 $/\$
311	134, 31, 310	syl2anc 667	. . . . . . 7
312	309, 311	mpbid 214	. . . . . 6
313	112	abscld 13498	. . . . . . 7
314		mod0 12103	. . . . . . 7 $/\$
315	313, 31, 314	syl2anc 667	. . . . . 6
316	312, 315	mpbid 214	. . . . 5
317	291, 316	eqeltrd 2529	. . . 4
318		absz 13374	. . . . 5
319	135, 318	syl 17	. . . 4
320	317, 319	mpbird 236	. . 3
321		pellex.neq	. . . . . . 7 $/\$
322	10	nnne0d 10654	. . . . . . . . 9
323	3	nnne0d 10654	. . . . . . . . 9
324	9, 11, 2, 4, 322, 323	divmuleqd 10429	. . . . . . . 8
325	61	adantr 467	. . . . . . . . . . . . . . 15 $/\$
326	325	eqcomd 2457	. . . . . . . . . . . . . 14 $/\$
327	326	oveq2d 6306	. . . . . . . . . . . . 13 $/\$
328	9, 11, 322	divcld 10383	. . . . . . . . . . . . . . . 16
329	328	sqcld 12414	. . . . . . . . . . . . . . 15
330	329	adantr 467	. . . . . . . . . . . . . 14 $/\$
331	36	adantr 467	. . . . . . . . . . . . . 14 $/\$
332	38	adantr 467	. . . . . . . . . . . . . 14 $/\$
333	330, 331, 332	subdid 10074	. . . . . . . . . . . . 13 $/\$
334		oveq1 6297	. . . . . . . . . . . . . . . . 17
335	334	oveq1d 6305	. . . . . . . . . . . . . . . 16
336	335	adantl 468	. . . . . . . . . . . . . . 15 $/\$
337	2	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
338	4	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
339	323	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
340	337, 338, 339	sqdivd 12429	. . . . . . . . . . . . . . . 16 $/\$
341	340	oveq1d 6305	. . . . . . . . . . . . . . 15 $/\$
342	219	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
343		sqne0 12341	. . . . . . . . . . . . . . . . . . 19
344	4, 343	syl 17	. . . . . . . . . . . . . . . . . 18
345	323, 344	mpbird 236	. . . . . . . . . . . . . . . . 17
346	345	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
347	342, 331, 346	divcan1d 10384	. . . . . . . . . . . . . . 15 $/\$
348	336, 341, 347	3eqtrd 2489	. . . . . . . . . . . . . 14 $/\$
349	7	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
350	37	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
351	330, 349, 350	mul12d 9842	. . . . . . . . . . . . . . 15 $/\$
352	9	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
353	11	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
354	322	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
355	352, 353, 354	sqdivd 12429	. . . . . . . . . . . . . . . . 17 $/\$
356	355	oveq1d 6305	. . . . . . . . . . . . . . . 16 $/\$
357	356	oveq2d 6306	. . . . . . . . . . . . . . 15 $/\$
358	206	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
359		sqne0 12341	. . . . . . . . . . . . . . . . . . . 20
360	11, 359	syl 17	. . . . . . . . . . . . . . . . . . 19
361	322, 360	mpbird 236	. . . . . . . . . . . . . . . . . 18
362	361	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
363	358, 350, 362	divcan1d 10384	. . . . . . . . . . . . . . . 16 $/\$