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 30745

Description: Lemma for pellex 30746. 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 10559	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10559	. . . . . . . 8
5	2, 4	mulcld 9619	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10559	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10559	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10559	. . . . . . . . 9
12	9, 11	mulcld 9619	. . . . . . . 8
13	7, 12	mulcld 9619	. . . . . . 7
14	5, 13	subcld 9936	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10976	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13267	. . . . 5
19	5, 13	negsubd 9942	. . . . . . . . . . 11
20	19	eqcomd 2451	. . . . . . . . . 10
21	20	oveq1d 6296	. . . . . . . . 9
22	1	nnred 10558	. . . . . . . . . . 11
23	3	nnred 10558	. . . . . . . . . . 11
24	22, 23	remulcld 9627	. . . . . . . . . 10
25	6	nnred 10558	. . . . . . . . . . 11
26	8	nnred 10558	. . . . . . . . . . . 12
27	10	nnred 10558	. . . . . . . . . . . 12
28	26, 27	remulcld 9627	. . . . . . . . . . 11
29	25, 28	remulcld 9627	. . . . . . . . . 10
30	29	renegcld 9993	. . . . . . . . . 10
31	16, 17	absrpcld 13260	. . . . . . . . . 10
32	3	nnzd 10974	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 12021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1240	. . . . . . . . . . 11
36	4	sqcld 12289	. . . . . . . . . . . . . . 15
37	11	sqcld 12289	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9619	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9940	. . . . . . . . . . . . . 14
40	4	sqvald 12288	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2485	. . . . . . . . . . . . 13
42	41	oveq1d 6296	. . . . . . . . . . . 12
43	23	resqcld 12317	. . . . . . . . . . . . . 14
44	27	resqcld 12317	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9627	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9994	. . . . . . . . . . . . 13
47		0red 9600	. . . . . . . . . . . . 13
48	16	abscld 13248	. . . . . . . . . . . . . . . . . . 19
49	48	recnd 9625	. . . . . . . . . . . . . . . . . 18
50	16, 17	absne0d 13259	. . . . . . . . . . . . . . . . . 18
51	49, 50	dividd 10325	. . . . . . . . . . . . . . . . 17
52		1zzd 10902	. . . . . . . . . . . . . . . . 17
53	51, 52	eqeltrd 2531	. . . . . . . . . . . . . . . 16
54		mod0 11984	. . . . . . . . . . . . . . . . 17 $/\$
55	48, 31, 54	syl2anc 661	. . . . . . . . . . . . . . . 16
56	53, 55	mpbird 232	. . . . . . . . . . . . . . 15
57	15	zred 10975	. . . . . . . . . . . . . . . 16
58		absmod0 13117	. . . . . . . . . . . . . . . 16 $/\$
59	57, 31, 58	syl2anc 661	. . . . . . . . . . . . . . 15
60	56, 59	mpbird 232	. . . . . . . . . . . . . 14
61		pellex.no2	. . . . . . . . . . . . . . 15
62	61	oveq1d 6296	. . . . . . . . . . . . . 14
63		0mod 12008	. . . . . . . . . . . . . . 15
64	31, 63	syl 16	. . . . . . . . . . . . . 14
65	60, 62, 64	3eqtr4d 2494	. . . . . . . . . . . . 13
66		modadd1 12014	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	46, 47, 45, 31, 65, 66	syl221anc 1240	. . . . . . . . . . . 12
68	38	addid2d 9784	. . . . . . . . . . . . . 14
69	11	sqvald 12288	. . . . . . . . . . . . . . 15
70	69	oveq2d 6297	. . . . . . . . . . . . . 14
71	7, 11, 11	mul12d 9792	. . . . . . . . . . . . . 14
72	68, 70, 71	3eqtrd 2488	. . . . . . . . . . . . 13
73	72	oveq1d 6296	. . . . . . . . . . . 12
74	42, 67, 73	3eqtrd 2488	. . . . . . . . . . 11
75	6	nnzd 10974	. . . . . . . . . . . . . 14
76	10	nnzd 10974	. . . . . . . . . . . . . 14
77	75, 76	zmulcld 10981	. . . . . . . . . . . . 13
78		pellex.ycg	. . . . . . . . . . . . . 14
79	78	eqcomd 2451	. . . . . . . . . . . . 13
80		modmul1 12021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
81	27, 26, 77, 31, 79, 80	syl221anc 1240	. . . . . . . . . . . 12
82	9, 7, 11	mul12d 9792	. . . . . . . . . . . . 13
83	82	oveq1d 6296	. . . . . . . . . . . 12
84	81, 83	eqtrd 2484	. . . . . . . . . . 11
85	35, 74, 84	3eqtrd 2488	. . . . . . . . . 10
86		modadd1 12014	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
87	24, 29, 30, 31, 85, 86	syl221anc 1240	. . . . . . . . 9
88	13	negidd 9926	. . . . . . . . . 10
89	88	oveq1d 6296	. . . . . . . . 9
90	21, 87, 89	3eqtrd 2488	. . . . . . . 8
91	90, 64	eqtrd 2484	. . . . . . 7
92	24, 29	resubcld 9994	. . . . . . . 8
93		absmod0 13117	. . . . . . . 8 $/\$
94	92, 31, 93	syl2anc 661	. . . . . . 7
95	91, 94	mpbid 210	. . . . . 6
96	14	abscld 13248	. . . . . . 7
97		mod0 11984	. . . . . . 7 $/\$
98	96, 31, 97	syl2anc 661	. . . . . 6
99	95, 98	mpbid 210	. . . . 5
100	18, 99	eqeltrd 2531	. . . 4
101	92, 57, 17	redivcld 10379	. . . . 5
102		absz 13125	. . . . 5
103	101, 102	syl 16	. . . 4
104	100, 103	mpbird 232	. . 3
105		0lt1 10082	. . . . . . . 8
106		0re 9599	. . . . . . . . 9
107		1re 9598	. . . . . . . . 9
108	106, 107	ltnlei 9708	. . . . . . . 8
109	105, 108	mpbi 208	. . . . . . 7
110	9, 4	mulcld 9619	. . . . . . . . . . . . . 14
111	2, 11	mulcld 9619	. . . . . . . . . . . . . 14
112	110, 111	subcld 9936	. . . . . . . . . . . . 13
113	112, 16, 17	divcld 10327	. . . . . . . . . . . 12
114	113	abscld 13248	. . . . . . . . . . 11
115	114	resqcld 12317	. . . . . . . . . 10
116	6	nnnn0d 10859	. . . . . . . . . . 11
117	116	nn0ge0d 10862	. . . . . . . . . 10
118	114	sqge0d 12318	. . . . . . . . . 10
119	25, 115, 117, 118	mulge0d 10136	. . . . . . . . 9
120	25, 115	remulcld 9627	. . . . . . . . . 10
121	47, 120	suble0d 10150	. . . . . . . . 9
122	119, 121	mpbird 232	. . . . . . . 8
123		breq1 4440	. . . . . . . 8
124	122, 123	syl5ibrcom 222	. . . . . . 7
125	109, 124	mtoi 178	. . . . . 6
126		absresq 13116	. . . . . . . . . . . 12
127	101, 126	syl 16	. . . . . . . . . . 11
128	14, 16, 17	sqdivd 12304	. . . . . . . . . . 11
129	14	sqvald 12288	. . . . . . . . . . . 12
130	129	oveq1d 6296	. . . . . . . . . . 11
131	127, 128, 130	3eqtrd 2488	. . . . . . . . . 10
132	26, 23	remulcld 9627	. . . . . . . . . . . . . . . 16
133	22, 27	remulcld 9627	. . . . . . . . . . . . . . . 16
134	132, 133	resubcld 9994	. . . . . . . . . . . . . . 15
135	134, 57, 17	redivcld 10379	. . . . . . . . . . . . . 14
136		absresq 13116	. . . . . . . . . . . . . 14
137	135, 136	syl 16	. . . . . . . . . . . . 13
138	112, 16, 17	sqdivd 12304	. . . . . . . . . . . . 13
139	137, 138	eqtrd 2484	. . . . . . . . . . . 12
140	139	oveq2d 6297	. . . . . . . . . . 11
141	112	sqcld 12289	. . . . . . . . . . . 12
142	16	sqcld 12289	. . . . . . . . . . . 12
143		sqne0 12215	. . . . . . . . . . . . . 14
144	16, 143	syl 16	. . . . . . . . . . . . 13
145	17, 144	mpbird 232	. . . . . . . . . . . 12
146	7, 141, 142, 145	divassd 10362	. . . . . . . . . . 11
147	112	sqvald 12288	. . . . . . . . . . . . 13
148	147	oveq2d 6297	. . . . . . . . . . . 12
149	148	oveq1d 6296	. . . . . . . . . . 11
150	140, 146, 149	3eqtr2d 2490	. . . . . . . . . 10
151	131, 150	oveq12d 6299	. . . . . . . . 9
152	14, 14	mulcld 9619	. . . . . . . . . 10
153	112, 112	mulcld 9619	. . . . . . . . . . 11
154	7, 153	mulcld 9619	. . . . . . . . . 10
155	152, 154, 142, 145	divsubdird 10366	. . . . . . . . 9
156	5, 13, 5, 13	mulsubd 10022	. . . . . . . . . . . 12
157	110, 111, 110, 111	mulsubd 10022	. . . . . . . . . . . . . 14
158	157	oveq2d 6297	. . . . . . . . . . . . 13
159	110, 110	mulcld 9619	. . . . . . . . . . . . . . 15
160	111, 111	mulcld 9619	. . . . . . . . . . . . . . 15
161	159, 160	addcld 9618	. . . . . . . . . . . . . 14
162	110, 111	mulcld 9619	. . . . . . . . . . . . . . 15
163	162, 162	addcld 9618	. . . . . . . . . . . . . 14
164	7, 161, 163	subdid 10019	. . . . . . . . . . . . 13
165	7, 159, 160	adddid 9623	. . . . . . . . . . . . . 14
166	7, 162, 162	adddid 9623	. . . . . . . . . . . . . 14
167	165, 166	oveq12d 6299	. . . . . . . . . . . . 13
168	158, 164, 167	3eqtrd 2488	. . . . . . . . . . . 12
169	156, 168	oveq12d 6299	. . . . . . . . . . 11
170	169	oveq1d 6296	. . . . . . . . . 10
171	5, 13	mulcomd 9620	. . . . . . . . . . . . . . . 16
172	7, 12, 5	mulassd 9622	. . . . . . . . . . . . . . . 16
173	2, 4	mulcomd 9620	. . . . . . . . . . . . . . . . . . 19
174	173	oveq2d 6297	. . . . . . . . . . . . . . . . . 18
175	9, 11, 4, 2	mul4d 9795	. . . . . . . . . . . . . . . . . 18
176	11, 2	mulcomd 9620	. . . . . . . . . . . . . . . . . . 19
177	176	oveq2d 6297	. . . . . . . . . . . . . . . . . 18
178	174, 175, 177	3eqtrd 2488	. . . . . . . . . . . . . . . . 17
179	178	oveq2d 6297	. . . . . . . . . . . . . . . 16
180	171, 172, 179	3eqtrd 2488	. . . . . . . . . . . . . . 15
181	180, 180	oveq12d 6299	. . . . . . . . . . . . . 14
182	181	oveq2d 6297	. . . . . . . . . . . . 13
183	182	oveq1d 6296	. . . . . . . . . . . 12
184	5, 5	mulcld 9619	. . . . . . . . . . . . . 14
185	13, 13	mulcld 9619	. . . . . . . . . . . . . 14
186	184, 185	addcld 9618	. . . . . . . . . . . . 13
187	7, 159	mulcld 9619	. . . . . . . . . . . . . 14
188	7, 160	mulcld 9619	. . . . . . . . . . . . . 14
189	187, 188	addcld 9618	. . . . . . . . . . . . 13
190	7, 162	mulcld 9619	. . . . . . . . . . . . . 14
191	190, 190	addcld 9618	. . . . . . . . . . . . 13
192	186, 189, 191	nnncan2d 9971	. . . . . . . . . . . 12
193	184, 185, 187, 188	addsub4d 9983	. . . . . . . . . . . . 13
194	5	sqvald 12288	. . . . . . . . . . . . . . 15
195	110	sqvald 12288	. . . . . . . . . . . . . . . 16
196	195	oveq2d 6297	. . . . . . . . . . . . . . 15
197	194, 196	oveq12d 6299	. . . . . . . . . . . . . 14
198	13	sqvald 12288	. . . . . . . . . . . . . . 15
199	111	sqvald 12288	. . . . . . . . . . . . . . . 16
200	199	oveq2d 6297	. . . . . . . . . . . . . . 15
201	198, 200	oveq12d 6299	. . . . . . . . . . . . . 14
202	197, 201	oveq12d 6299	. . . . . . . . . . . . 13
203	2, 4	sqmuld 12303	. . . . . . . . . . . . . . . 16
204	9, 4	sqmuld 12303	. . . . . . . . . . . . . . . . . 18
205	204	oveq2d 6297	. . . . . . . . . . . . . . . . 17
206	9	sqcld 12289	. . . . . . . . . . . . . . . . . 18
207	7, 206, 36	mulassd 9622	. . . . . . . . . . . . . . . . 17
208	205, 207	eqtr4d 2487	. . . . . . . . . . . . . . . 16
209	203, 208	oveq12d 6299	. . . . . . . . . . . . . . 15
210	7	sqvald 12288	. . . . . . . . . . . . . . . . . 18
211	9, 11	sqmuld 12303	. . . . . . . . . . . . . . . . . 18
212	210, 211	oveq12d 6299	. . . . . . . . . . . . . . . . 17
213	7, 12	sqmuld 12303	. . . . . . . . . . . . . . . . 17
214	7, 7	mulcld 9619	. . . . . . . . . . . . . . . . . 18
215	214, 206, 37	mulassd 9622	. . . . . . . . . . . . . . . . 17
216	212, 213, 215	3eqtr4d 2494	. . . . . . . . . . . . . . . 16
217	2, 11	sqmuld 12303	. . . . . . . . . . . . . . . . . 18
218	217	oveq2d 6297	. . . . . . . . . . . . . . . . 17
219	2	sqcld 12289	. . . . . . . . . . . . . . . . . 18
220	7, 219, 37	mulassd 9622	. . . . . . . . . . . . . . . . 17
221	218, 220	eqtr4d 2487	. . . . . . . . . . . . . . . 16
222	216, 221	oveq12d 6299	. . . . . . . . . . . . . . 15
223	209, 222	oveq12d 6299	. . . . . . . . . . . . . 14
224	7, 206	mulcld 9619	. . . . . . . . . . . . . . . . 17
225	219, 224, 36	subdird 10020	. . . . . . . . . . . . . . . 16
226		pellex.no1	. . . . . . . . . . . . . . . . 17
227	226	oveq1d 6296	. . . . . . . . . . . . . . . 16
228	225, 227	eqtr3d 2486	. . . . . . . . . . . . . . 15
229	7, 7, 206	mulassd 9622	. . . . . . . . . . . . . . . . . 18
230	229	oveq1d 6296	. . . . . . . . . . . . . . . . 17
231	230	oveq1d 6296	. . . . . . . . . . . . . . . 16
232	214, 206	mulcld 9619	. . . . . . . . . . . . . . . . 17
233	7, 219	mulcld 9619	. . . . . . . . . . . . . . . . 17
234	232, 233, 37	subdird 10020	. . . . . . . . . . . . . . . 16
235		subdi 9997	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
236	235	eqcomd 2451	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
237	7, 224, 219, 236	syl3anc 1229	. . . . . . . . . . . . . . . . . 18
238		negsubdi2 9883	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
239	238	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . 21 $/\$
240	219, 224, 239	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
241	226	negeqd 9819	. . . . . . . . . . . . . . . . . . . 20
242	240, 241	eqtrd 2484	. . . . . . . . . . . . . . . . . . 19
243	242	oveq2d 6297	. . . . . . . . . . . . . . . . . 18
244	7, 16	mulneg2d 10017	. . . . . . . . . . . . . . . . . 18
245	237, 243, 244	3eqtrd 2488	. . . . . . . . . . . . . . . . 17
246	245	oveq1d 6296	. . . . . . . . . . . . . . . 16
247	231, 234, 246	3eqtr3d 2492	. . . . . . . . . . . . . . 15
248	228, 247	oveq12d 6299	. . . . . . . . . . . . . 14
249	7, 16	mulcld 9619	. . . . . . . . . . . . . . . . . 18
250	249, 37	mulneg1d 10016	. . . . . . . . . . . . . . . . 17
251	7, 16	mulcomd 9620	. . . . . . . . . . . . . . . . . . . 20
252	251	oveq1d 6296	. . . . . . . . . . . . . . . . . . 19
253	16, 7, 37	mulassd 9622	. . . . . . . . . . . . . . . . . . 19
254	252, 253	eqtrd 2484	. . . . . . . . . . . . . . . . . 18
255	254	negeqd 9819	. . . . . . . . . . . . . . . . 17
256	250, 255	eqtrd 2484	. . . . . . . . . . . . . . . 16
257	256	oveq2d 6297	. . . . . . . . . . . . . . 15
258	16, 36	mulcld 9619	. . . . . . . . . . . . . . . 16
259	16, 38	mulcld 9619	. . . . . . . . . . . . . . . 16
260	258, 259	negsubd 9942	. . . . . . . . . . . . . . 15
261	61	oveq2d 6297	. . . . . . . . . . . . . . . 16
262		subdi 9997	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
263	262	eqcomd 2451	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
264	16, 36, 38, 263	syl3anc 1229	. . . . . . . . . . . . . . . 16
265	16	sqvald 12288	. . . . . . . . . . . . . . . 16
266	261, 264, 265	3eqtr4d 2494	. . . . . . . . . . . . . . 15
267	257, 260, 266	3eqtrd 2488	. . . . . . . . . . . . . 14
268	223, 248, 267	3eqtrd 2488	. . . . . . . . . . . . 13
269	193, 202, 268	3eqtr2d 2490	. . . . . . . . . . . 12
270	183, 192, 269	3eqtrd 2488	. . . . . . . . . . 11
271	270	oveq1d 6296	. . . . . . . . . 10
272	142, 145	dividd 10325	. . . . . . . . . 10
273	170, 271, 272	3eqtrd 2488	. . . . . . . . 9
274	151, 155, 273	3eqtr2d 2490	. . . . . . . 8
275	274	adantr 465	. . . . . . 7 $/\$
276		simpr 461	. . . . . . . . . . . 12 $/\$
277	276	oveq1d 6296	. . . . . . . . . . 11 $/\$
278	277	fveq2d 5860	. . . . . . . . . 10 $/\$
279	16, 17	div0d 10326	. . . . . . . . . . . 12
280	279	abs00bd 13105	. . . . . . . . . . 11
281	280	adantr 465	. . . . . . . . . 10 $/\$
282	278, 281	eqtrd 2484	. . . . . . . . 9 $/\$
283	282	sq0id 12242	. . . . . . . 8 $/\$
284	283	oveq1d 6296	. . . . . . 7 $/\$
285	275, 284	eqtr3d 2486	. . . . . 6 $/\$
286	125, 285	mtand 659	. . . . 5
287	286	neqned 2646	. . . 4
288	14, 16, 287, 17	divne0d 10343	. . 3
289		nnabscl 13139	. . 3 $/\$
290	104, 288, 289	syl2anc 661	. 2
291	112, 16, 17	absdivd 13267	. . . . 5
292		negsub 9872	. . . . . . . . . . . 12 $/\$
293	292	eqcomd 2451	. . . . . . . . . . 11 $/\$
294	110, 111, 293	syl2anc 661	. . . . . . . . . 10
295	294	oveq1d 6296	. . . . . . . . 9
296	133	renegcld 9993	. . . . . . . . . 10
297	11, 4	mulcomd 9620	. . . . . . . . . . . 12
298	297	oveq1d 6296	. . . . . . . . . . 11
299		modmul1 12021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
300	26, 27, 32, 31, 78, 299	syl221anc 1240	. . . . . . . . . . 11
301		modmul1 12021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
302	22, 23, 76, 31, 33, 301	syl221anc 1240	. . . . . . . . . . 11
303	298, 300, 302	3eqtr4d 2494	. . . . . . . . . 10
304		modadd1 12014	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
305	132, 133, 296, 31, 303, 304	syl221anc 1240	. . . . . . . . 9
306	111	negidd 9926	. . . . . . . . . 10
307	306	oveq1d 6296	. . . . . . . . 9
308	295, 305, 307	3eqtrd 2488	. . . . . . . 8
309	308, 64	eqtrd 2484	. . . . . . 7
310		absmod0 13117	. . . . . . . 8 $/\$
311	134, 31, 310	syl2anc 661	. . . . . . 7
312	309, 311	mpbid 210	. . . . . 6
313	112	abscld 13248	. . . . . . 7
314		mod0 11984	. . . . . . 7 $/\$
315	313, 31, 314	syl2anc 661	. . . . . 6
316	312, 315	mpbid 210	. . . . 5
317	291, 316	eqeltrd 2531	. . . 4
318		absz 13125	. . . . 5
319	135, 318	syl 16	. . . 4
320	317, 319	mpbird 232	. . 3
321		pellex.neq	. . . . . . 7 $/\$
322	10	nnne0d 10587	. . . . . . . . 9
323	3	nnne0d 10587	. . . . . . . . 9
324	9, 11, 2, 4, 322, 323	divmuleqd 10373	. . . . . . . 8
325	61	adantr 465	. . . . . . . . . . . . . . 15 $/\$
326	325	eqcomd 2451	. . . . . . . . . . . . . 14 $/\$
327	326	oveq2d 6297	. . . . . . . . . . . . 13 $/\$
328	9, 11, 322	divcld 10327	. . . . . . . . . . . . . . . 16
329	328	sqcld 12289	. . . . . . . . . . . . . . 15
330	329	adantr 465	. . . . . . . . . . . . . 14 $/\$
331	36	adantr 465	. . . . . . . . . . . . . 14 $/\$
332	38	adantr 465	. . . . . . . . . . . . . 14 $/\$
333	330, 331, 332	subdid 10019	. . . . . . . . . . . . 13 $/\$
334		oveq1 6288	. . . . . . . . . . . . . . . . 17
335	334	oveq1d 6296	. . . . . . . . . . . . . . . 16
336	335	adantl 466	. . . . . . . . . . . . . . 15 $/\$
337	2	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
338	4	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
339	323	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
340	337, 338, 339	sqdivd 12304	. . . . . . . . . . . . . . . 16 $/\$
341	340	oveq1d 6296	. . . . . . . . . . . . . . 15 $/\$
342	219	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
343		sqne0 12215	. . . . . . . . . . . . . . . . . . 19
344	4, 343	syl 16	. . . . . . . . . . . . . . . . . 18
345	323, 344	mpbird 232	. . . . . . . . . . . . . . . . 17
346	345	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
347	342, 331, 346	divcan1d 10328	. . . . . . . . . . . . . . 15 $/\$
348	336, 341, 347	3eqtrd 2488	. . . . . . . . . . . . . 14 $/\$
349	7	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
350	37	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
351	330, 349, 350	mul12d 9792	. . . . . . . . . . . . . . 15 $/\$
352	9	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
353	11	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
354	322	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
355	352, 353, 354	sqdivd 12304	. . . . . . . . . . . . . . . . 17 $/\$
356	355	oveq1d 6296	. . . . . . . . . . . . . . . 16 $/\$
357	356	oveq2d 6297	. . . . . . . . . . . . . . 15 $/\$
358	206	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
359		sqne0 12215	. . . . . . . . . . . . . . . . . . . 20
360	11, 359	syl 16	. . . . . . . . . . . . . . . . . . 19
361	322, 360	mpbird 232	. . . . . . . . . . . . . . . . . 18
362	361	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
363	358, 350, 362	divcan1d 10328	. . . . . . . . . . . . . . . 16 $/\$