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 35604

Description: Lemma for pellex 35605. 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 10627	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10627	. . . . . . . 8
5	2, 4	mulcld 9665	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10627	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10627	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10627	. . . . . . . . 9
12	9, 11	mulcld 9665	. . . . . . . 8
13	7, 12	mulcld 9665	. . . . . . 7
14	5, 13	subcld 9988	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 11043	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13510	. . . . 5
19	5, 13	negsubd 9994	. . . . . . . . . . 11
20	19	eqcomd 2431	. . . . . . . . . 10
21	20	oveq1d 6318	. . . . . . . . 9
22	1	nnred 10626	. . . . . . . . . . 11
23	3	nnred 10626	. . . . . . . . . . 11
24	22, 23	remulcld 9673	. . . . . . . . . 10
25	6	nnred 10626	. . . . . . . . . . 11
26	8	nnred 10626	. . . . . . . . . . . 12
27	10	nnred 10626	. . . . . . . . . . . 12
28	26, 27	remulcld 9673	. . . . . . . . . . 11
29	25, 28	remulcld 9673	. . . . . . . . . 10
30	29	renegcld 10048	. . . . . . . . . 10
31	16, 17	absrpcld 13503	. . . . . . . . . 10
32	3	nnzd 11041	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 12144	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1276	. . . . . . . . . . 11
36	4	sqcld 12415	. . . . . . . . . . . . . . 15
37	11	sqcld 12415	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9665	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9992	. . . . . . . . . . . . . 14
40	4	sqvald 12414	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2465	. . . . . . . . . . . . 13
42	41	oveq1d 6318	. . . . . . . . . . . 12
43	23	resqcld 12443	. . . . . . . . . . . . . 14
44	27	resqcld 12443	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9673	. . . . . . . . . . . . . 14
46	43, 45	resubcld 10049	. . . . . . . . . . . . 13
47		0red 9646	. . . . . . . . . . . . 13
48	16	abscld 13491	. . . . . . . . . . . . . . . . . . 19
49	48	recnd 9671	. . . . . . . . . . . . . . . . . 18
50	16, 17	absne0d 13502	. . . . . . . . . . . . . . . . . 18
51	49, 50	dividd 10383	. . . . . . . . . . . . . . . . 17
52		1zzd 10970	. . . . . . . . . . . . . . . . 17
53	51, 52	eqeltrd 2511	. . . . . . . . . . . . . . . 16
54		mod0 12104	. . . . . . . . . . . . . . . . 17 $/\$
55	48, 31, 54	syl2anc 666	. . . . . . . . . . . . . . . 16
56	53, 55	mpbird 236	. . . . . . . . . . . . . . 15
57	15	zred 11042	. . . . . . . . . . . . . . . 16
58		absmod0 13360	. . . . . . . . . . . . . . . 16 $/\$
59	57, 31, 58	syl2anc 666	. . . . . . . . . . . . . . 15
60	56, 59	mpbird 236	. . . . . . . . . . . . . 14
61		pellex.no2	. . . . . . . . . . . . . . 15
62	61	oveq1d 6318	. . . . . . . . . . . . . 14
63		0mod 12129	. . . . . . . . . . . . . . 15
64	31, 63	syl 17	. . . . . . . . . . . . . 14
65	60, 62, 64	3eqtr4d 2474	. . . . . . . . . . . . 13
66		modadd1 12135	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	46, 47, 45, 31, 65, 66	syl221anc 1276	. . . . . . . . . . . 12
68	38	addid2d 9836	. . . . . . . . . . . . . 14
69	11	sqvald 12414	. . . . . . . . . . . . . . 15
70	69	oveq2d 6319	. . . . . . . . . . . . . 14
71	7, 11, 11	mul12d 9844	. . . . . . . . . . . . . 14
72	68, 70, 71	3eqtrd 2468	. . . . . . . . . . . . 13
73	72	oveq1d 6318	. . . . . . . . . . . 12
74	42, 67, 73	3eqtrd 2468	. . . . . . . . . . 11
75	6	nnzd 11041	. . . . . . . . . . . . . 14
76	10	nnzd 11041	. . . . . . . . . . . . . 14
77	75, 76	zmulcld 11048	. . . . . . . . . . . . 13
78		pellex.ycg	. . . . . . . . . . . . . 14
79	78	eqcomd 2431	. . . . . . . . . . . . 13
80		modmul1 12144	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
81	27, 26, 77, 31, 79, 80	syl221anc 1276	. . . . . . . . . . . 12
82	9, 7, 11	mul12d 9844	. . . . . . . . . . . . 13
83	82	oveq1d 6318	. . . . . . . . . . . 12
84	81, 83	eqtrd 2464	. . . . . . . . . . 11
85	35, 74, 84	3eqtrd 2468	. . . . . . . . . 10
86		modadd1 12135	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
87	24, 29, 30, 31, 85, 86	syl221anc 1276	. . . . . . . . 9
88	13	negidd 9978	. . . . . . . . . 10
89	88	oveq1d 6318	. . . . . . . . 9
90	21, 87, 89	3eqtrd 2468	. . . . . . . 8
91	90, 64	eqtrd 2464	. . . . . . 7
92	24, 29	resubcld 10049	. . . . . . . 8
93		absmod0 13360	. . . . . . . 8 $/\$
94	92, 31, 93	syl2anc 666	. . . . . . 7
95	91, 94	mpbid 214	. . . . . 6
96	14	abscld 13491	. . . . . . 7
97		mod0 12104	. . . . . . 7 $/\$
98	96, 31, 97	syl2anc 666	. . . . . 6
99	95, 98	mpbid 214	. . . . 5
100	18, 99	eqeltrd 2511	. . . 4
101	92, 57, 17	redivcld 10437	. . . . 5
102		absz 13368	. . . . 5
103	101, 102	syl 17	. . . 4
104	100, 103	mpbird 236	. . 3
105		0lt1 10138	. . . . . . . 8
106		0re 9645	. . . . . . . . 9
107		1re 9644	. . . . . . . . 9
108	106, 107	ltnlei 9757	. . . . . . . 8
109	105, 108	mpbi 212	. . . . . . 7
110	9, 4	mulcld 9665	. . . . . . . . . . . . . 14
111	2, 11	mulcld 9665	. . . . . . . . . . . . . 14
112	110, 111	subcld 9988	. . . . . . . . . . . . 13
113	112, 16, 17	divcld 10385	. . . . . . . . . . . 12
114	113	abscld 13491	. . . . . . . . . . 11
115	114	resqcld 12443	. . . . . . . . . 10
116	6	nnnn0d 10927	. . . . . . . . . . 11
117	116	nn0ge0d 10930	. . . . . . . . . 10
118	114	sqge0d 12444	. . . . . . . . . 10
119	25, 115, 117, 118	mulge0d 10192	. . . . . . . . 9
120	25, 115	remulcld 9673	. . . . . . . . . 10
121	47, 120	suble0d 10206	. . . . . . . . 9
122	119, 121	mpbird 236	. . . . . . . 8
123		breq1 4424	. . . . . . . 8
124	122, 123	syl5ibrcom 226	. . . . . . 7
125	109, 124	mtoi 182	. . . . . 6
126		absresq 13359	. . . . . . . . . . . 12
127	101, 126	syl 17	. . . . . . . . . . 11
128	14, 16, 17	sqdivd 12430	. . . . . . . . . . 11
129	14	sqvald 12414	. . . . . . . . . . . 12
130	129	oveq1d 6318	. . . . . . . . . . 11
131	127, 128, 130	3eqtrd 2468	. . . . . . . . . 10
132	26, 23	remulcld 9673	. . . . . . . . . . . . . . . 16
133	22, 27	remulcld 9673	. . . . . . . . . . . . . . . 16
134	132, 133	resubcld 10049	. . . . . . . . . . . . . . 15
135	134, 57, 17	redivcld 10437	. . . . . . . . . . . . . 14
136		absresq 13359	. . . . . . . . . . . . . 14
137	135, 136	syl 17	. . . . . . . . . . . . 13
138	112, 16, 17	sqdivd 12430	. . . . . . . . . . . . 13
139	137, 138	eqtrd 2464	. . . . . . . . . . . 12
140	139	oveq2d 6319	. . . . . . . . . . 11
141	112	sqcld 12415	. . . . . . . . . . . 12
142	16	sqcld 12415	. . . . . . . . . . . 12
143		sqne0 12342	. . . . . . . . . . . . . 14
144	16, 143	syl 17	. . . . . . . . . . . . 13
145	17, 144	mpbird 236	. . . . . . . . . . . 12
146	7, 141, 142, 145	divassd 10420	. . . . . . . . . . 11
147	112	sqvald 12414	. . . . . . . . . . . . 13
148	147	oveq2d 6319	. . . . . . . . . . . 12
149	148	oveq1d 6318	. . . . . . . . . . 11
150	140, 146, 149	3eqtr2d 2470	. . . . . . . . . 10
151	131, 150	oveq12d 6321	. . . . . . . . 9
152	14, 14	mulcld 9665	. . . . . . . . . 10
153	112, 112	mulcld 9665	. . . . . . . . . . 11
154	7, 153	mulcld 9665	. . . . . . . . . 10
155	152, 154, 142, 145	divsubdird 10424	. . . . . . . . 9
156	5, 13, 5, 13	mulsubd 10079	. . . . . . . . . . . 12
157	110, 111, 110, 111	mulsubd 10079	. . . . . . . . . . . . . 14
158	157	oveq2d 6319	. . . . . . . . . . . . 13
159	110, 110	mulcld 9665	. . . . . . . . . . . . . . 15
160	111, 111	mulcld 9665	. . . . . . . . . . . . . . 15
161	159, 160	addcld 9664	. . . . . . . . . . . . . 14
162	110, 111	mulcld 9665	. . . . . . . . . . . . . . 15
163	162, 162	addcld 9664	. . . . . . . . . . . . . 14
164	7, 161, 163	subdid 10076	. . . . . . . . . . . . 13
165	7, 159, 160	adddid 9669	. . . . . . . . . . . . . 14
166	7, 162, 162	adddid 9669	. . . . . . . . . . . . . 14
167	165, 166	oveq12d 6321	. . . . . . . . . . . . 13
168	158, 164, 167	3eqtrd 2468	. . . . . . . . . . . 12
169	156, 168	oveq12d 6321	. . . . . . . . . . 11
170	169	oveq1d 6318	. . . . . . . . . 10
171	5, 13	mulcomd 9666	. . . . . . . . . . . . . . . 16
172	7, 12, 5	mulassd 9668	. . . . . . . . . . . . . . . 16
173	2, 4	mulcomd 9666	. . . . . . . . . . . . . . . . . . 19
174	173	oveq2d 6319	. . . . . . . . . . . . . . . . . 18
175	9, 11, 4, 2	mul4d 9847	. . . . . . . . . . . . . . . . . 18
176	11, 2	mulcomd 9666	. . . . . . . . . . . . . . . . . . 19
177	176	oveq2d 6319	. . . . . . . . . . . . . . . . . 18
178	174, 175, 177	3eqtrd 2468	. . . . . . . . . . . . . . . . 17
179	178	oveq2d 6319	. . . . . . . . . . . . . . . 16
180	171, 172, 179	3eqtrd 2468	. . . . . . . . . . . . . . 15
181	180, 180	oveq12d 6321	. . . . . . . . . . . . . 14
182	181	oveq2d 6319	. . . . . . . . . . . . 13
183	182	oveq1d 6318	. . . . . . . . . . . 12
184	5, 5	mulcld 9665	. . . . . . . . . . . . . 14
185	13, 13	mulcld 9665	. . . . . . . . . . . . . 14
186	184, 185	addcld 9664	. . . . . . . . . . . . 13
187	7, 159	mulcld 9665	. . . . . . . . . . . . . 14
188	7, 160	mulcld 9665	. . . . . . . . . . . . . 14
189	187, 188	addcld 9664	. . . . . . . . . . . . 13
190	7, 162	mulcld 9665	. . . . . . . . . . . . . 14
191	190, 190	addcld 9664	. . . . . . . . . . . . 13
192	186, 189, 191	nnncan2d 10023	. . . . . . . . . . . 12
193	184, 185, 187, 188	addsub4d 10035	. . . . . . . . . . . . 13
194	5	sqvald 12414	. . . . . . . . . . . . . . 15
195	110	sqvald 12414	. . . . . . . . . . . . . . . 16
196	195	oveq2d 6319	. . . . . . . . . . . . . . 15
197	194, 196	oveq12d 6321	. . . . . . . . . . . . . 14
198	13	sqvald 12414	. . . . . . . . . . . . . . 15
199	111	sqvald 12414	. . . . . . . . . . . . . . . 16
200	199	oveq2d 6319	. . . . . . . . . . . . . . 15
201	198, 200	oveq12d 6321	. . . . . . . . . . . . . 14
202	197, 201	oveq12d 6321	. . . . . . . . . . . . 13
203	2, 4	sqmuld 12429	. . . . . . . . . . . . . . . 16
204	9, 4	sqmuld 12429	. . . . . . . . . . . . . . . . . 18
205	204	oveq2d 6319	. . . . . . . . . . . . . . . . 17
206	9	sqcld 12415	. . . . . . . . . . . . . . . . . 18
207	7, 206, 36	mulassd 9668	. . . . . . . . . . . . . . . . 17
208	205, 207	eqtr4d 2467	. . . . . . . . . . . . . . . 16
209	203, 208	oveq12d 6321	. . . . . . . . . . . . . . 15
210	7	sqvald 12414	. . . . . . . . . . . . . . . . . 18
211	9, 11	sqmuld 12429	. . . . . . . . . . . . . . . . . 18
212	210, 211	oveq12d 6321	. . . . . . . . . . . . . . . . 17
213	7, 12	sqmuld 12429	. . . . . . . . . . . . . . . . 17
214	7, 7	mulcld 9665	. . . . . . . . . . . . . . . . . 18
215	214, 206, 37	mulassd 9668	. . . . . . . . . . . . . . . . 17
216	212, 213, 215	3eqtr4d 2474	. . . . . . . . . . . . . . . 16
217	2, 11	sqmuld 12429	. . . . . . . . . . . . . . . . . 18
218	217	oveq2d 6319	. . . . . . . . . . . . . . . . 17
219	2	sqcld 12415	. . . . . . . . . . . . . . . . . 18
220	7, 219, 37	mulassd 9668	. . . . . . . . . . . . . . . . 17
221	218, 220	eqtr4d 2467	. . . . . . . . . . . . . . . 16
222	216, 221	oveq12d 6321	. . . . . . . . . . . . . . 15
223	209, 222	oveq12d 6321	. . . . . . . . . . . . . 14
224	7, 206	mulcld 9665	. . . . . . . . . . . . . . . . 17
225	219, 224, 36	subdird 10077	. . . . . . . . . . . . . . . 16
226		pellex.no1	. . . . . . . . . . . . . . . . 17
227	226	oveq1d 6318	. . . . . . . . . . . . . . . 16
228	225, 227	eqtr3d 2466	. . . . . . . . . . . . . . 15
229	7, 7, 206	mulassd 9668	. . . . . . . . . . . . . . . . . 18
230	229	oveq1d 6318	. . . . . . . . . . . . . . . . 17
231	230	oveq1d 6318	. . . . . . . . . . . . . . . 16
232	214, 206	mulcld 9665	. . . . . . . . . . . . . . . . 17
233	7, 219	mulcld 9665	. . . . . . . . . . . . . . . . 17
234	232, 233, 37	subdird 10077	. . . . . . . . . . . . . . . 16
235		subdi 10054	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
236	235	eqcomd 2431	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
237	7, 224, 219, 236	syl3anc 1265	. . . . . . . . . . . . . . . . . 18
238		negsubdi2 9935	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
239	238	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . 21 $/\$
240	219, 224, 239	syl2anc 666	. . . . . . . . . . . . . . . . . . . 20
241	226	negeqd 9871	. . . . . . . . . . . . . . . . . . . 20
242	240, 241	eqtrd 2464	. . . . . . . . . . . . . . . . . . 19
243	242	oveq2d 6319	. . . . . . . . . . . . . . . . . 18
244	7, 16	mulneg2d 10074	. . . . . . . . . . . . . . . . . 18
245	237, 243, 244	3eqtrd 2468	. . . . . . . . . . . . . . . . 17
246	245	oveq1d 6318	. . . . . . . . . . . . . . . 16
247	231, 234, 246	3eqtr3d 2472	. . . . . . . . . . . . . . 15
248	228, 247	oveq12d 6321	. . . . . . . . . . . . . 14
249	7, 16	mulcld 9665	. . . . . . . . . . . . . . . . . 18
250	249, 37	mulneg1d 10073	. . . . . . . . . . . . . . . . 17
251	7, 16	mulcomd 9666	. . . . . . . . . . . . . . . . . . . 20
252	251	oveq1d 6318	. . . . . . . . . . . . . . . . . . 19
253	16, 7, 37	mulassd 9668	. . . . . . . . . . . . . . . . . . 19
254	252, 253	eqtrd 2464	. . . . . . . . . . . . . . . . . 18
255	254	negeqd 9871	. . . . . . . . . . . . . . . . 17
256	250, 255	eqtrd 2464	. . . . . . . . . . . . . . . 16
257	256	oveq2d 6319	. . . . . . . . . . . . . . 15
258	16, 36	mulcld 9665	. . . . . . . . . . . . . . . 16
259	16, 38	mulcld 9665	. . . . . . . . . . . . . . . 16
260	258, 259	negsubd 9994	. . . . . . . . . . . . . . 15
261	61	oveq2d 6319	. . . . . . . . . . . . . . . 16
262		subdi 10054	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
263	262	eqcomd 2431	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
264	16, 36, 38, 263	syl3anc 1265	. . . . . . . . . . . . . . . 16
265	16	sqvald 12414	. . . . . . . . . . . . . . . 16
266	261, 264, 265	3eqtr4d 2474	. . . . . . . . . . . . . . 15
267	257, 260, 266	3eqtrd 2468	. . . . . . . . . . . . . 14
268	223, 248, 267	3eqtrd 2468	. . . . . . . . . . . . 13
269	193, 202, 268	3eqtr2d 2470	. . . . . . . . . . . 12
270	183, 192, 269	3eqtrd 2468	. . . . . . . . . . 11
271	270	oveq1d 6318	. . . . . . . . . 10
272	142, 145	dividd 10383	. . . . . . . . . 10
273	170, 271, 272	3eqtrd 2468	. . . . . . . . 9
274	151, 155, 273	3eqtr2d 2470	. . . . . . . 8
275	274	adantr 467	. . . . . . 7 $/\$
276		simpr 463	. . . . . . . . . . . 12 $/\$
277	276	oveq1d 6318	. . . . . . . . . . 11 $/\$
278	277	fveq2d 5883	. . . . . . . . . 10 $/\$
279	16, 17	div0d 10384	. . . . . . . . . . . 12
280	279	abs00bd 13348	. . . . . . . . . . 11
281	280	adantr 467	. . . . . . . . . 10 $/\$
282	278, 281	eqtrd 2464	. . . . . . . . 9 $/\$
283	282	sq0id 12369	. . . . . . . 8 $/\$
284	283	oveq1d 6318	. . . . . . 7 $/\$
285	275, 284	eqtr3d 2466	. . . . . 6 $/\$
286	125, 285	mtand 664	. . . . 5
287	286	neqned 2628	. . . 4
288	14, 16, 287, 17	divne0d 10401	. . 3
289		nnabscl 13382	. . 3 $/\$
290	104, 288, 289	syl2anc 666	. 2
291	112, 16, 17	absdivd 13510	. . . . 5
292		negsub 9924	. . . . . . . . . . . 12 $/\$
293	292	eqcomd 2431	. . . . . . . . . . 11 $/\$
294	110, 111, 293	syl2anc 666	. . . . . . . . . 10
295	294	oveq1d 6318	. . . . . . . . 9
296	133	renegcld 10048	. . . . . . . . . 10
297	11, 4	mulcomd 9666	. . . . . . . . . . . 12
298	297	oveq1d 6318	. . . . . . . . . . 11
299		modmul1 12144	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
300	26, 27, 32, 31, 78, 299	syl221anc 1276	. . . . . . . . . . 11
301		modmul1 12144	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
302	22, 23, 76, 31, 33, 301	syl221anc 1276	. . . . . . . . . . 11
303	298, 300, 302	3eqtr4d 2474	. . . . . . . . . 10
304		modadd1 12135	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
305	132, 133, 296, 31, 303, 304	syl221anc 1276	. . . . . . . . 9
306	111	negidd 9978	. . . . . . . . . 10
307	306	oveq1d 6318	. . . . . . . . 9
308	295, 305, 307	3eqtrd 2468	. . . . . . . 8
309	308, 64	eqtrd 2464	. . . . . . 7
310		absmod0 13360	. . . . . . . 8 $/\$
311	134, 31, 310	syl2anc 666	. . . . . . 7
312	309, 311	mpbid 214	. . . . . 6
313	112	abscld 13491	. . . . . . 7
314		mod0 12104	. . . . . . 7 $/\$
315	313, 31, 314	syl2anc 666	. . . . . 6
316	312, 315	mpbid 214	. . . . 5
317	291, 316	eqeltrd 2511	. . . 4
318		absz 13368	. . . . 5
319	135, 318	syl 17	. . . 4
320	317, 319	mpbird 236	. . 3
321		pellex.neq	. . . . . . 7 $/\$
322	10	nnne0d 10656	. . . . . . . . 9
323	3	nnne0d 10656	. . . . . . . . 9
324	9, 11, 2, 4, 322, 323	divmuleqd 10431	. . . . . . . 8
325	61	adantr 467	. . . . . . . . . . . . . . 15 $/\$
326	325	eqcomd 2431	. . . . . . . . . . . . . 14 $/\$
327	326	oveq2d 6319	. . . . . . . . . . . . 13 $/\$
328	9, 11, 322	divcld 10385	. . . . . . . . . . . . . . . 16
329	328	sqcld 12415	. . . . . . . . . . . . . . 15
330	329	adantr 467	. . . . . . . . . . . . . 14 $/\$
331	36	adantr 467	. . . . . . . . . . . . . 14 $/\$
332	38	adantr 467	. . . . . . . . . . . . . 14 $/\$
333	330, 331, 332	subdid 10076	. . . . . . . . . . . . 13 $/\$
334		oveq1 6310	. . . . . . . . . . . . . . . . 17
335	334	oveq1d 6318	. . . . . . . . . . . . . . . 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 12430	. . . . . . . . . . . . . . . 16 $/\$
341	340	oveq1d 6318	. . . . . . . . . . . . . . 15 $/\$
342	219	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
343		sqne0 12342	. . . . . . . . . . . . . . . . . . 19
344	4, 343	syl 17	. . . . . . . . . . . . . . . . . 18
345	323, 344	mpbird 236	. . . . . . . . . . . . . . . . 17
346	345	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
347	342, 331, 346	divcan1d 10386	. . . . . . . . . . . . . . 15 $/\$
348	336, 341, 347	3eqtrd 2468	. . . . . . . . . . . . . 14 $/\$
349	7	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
350	37	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
351	330, 349, 350	mul12d 9844	. . . . . . . . . . . . . . 15 $/\$
352	9	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
353	11	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
354	322	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
355	352, 353, 354	sqdivd 12430	. . . . . . . . . . . . . . . . 17 $/\$
356	355	oveq1d 6318	. . . . . . . . . . . . . . . 16 $/\$
357	356	oveq2d 6319	. . . . . . . . . . . . . . 15 $/\$
358	206	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
359		sqne0 12342	. . . . . . . . . . . . . . . . . . . 20
360	11, 359	syl 17	. . . . . . . . . . . . . . . . . . 19
361	322, 360	mpbird 236	. . . . . . . . . . . . . . . . . 18
362	361	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
363	358, 350, 362	divcan1d 10386	. . . . . . . . . . . . . . . 16 $/\$