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 30361

Description: Lemma for pellex 30362. 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 10541	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10541	. . . . . . . 8
5	2, 4	mulcld 9605	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10541	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10541	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10541	. . . . . . . . 9
12	9, 11	mulcld 9605	. . . . . . . 8
13	7, 12	mulcld 9605	. . . . . . 7
14	5, 13	subcld 9919	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10956	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13235	. . . . 5
19	5, 13	negsubd 9925	. . . . . . . . . . 11
20	19	eqcomd 2468	. . . . . . . . . 10
21	20	oveq1d 6290	. . . . . . . . 9
22	1	nnred 10540	. . . . . . . . . . 11
23	3	nnred 10540	. . . . . . . . . . 11
24	22, 23	remulcld 9613	. . . . . . . . . 10
25	6	nnred 10540	. . . . . . . . . . 11
26	8	nnred 10540	. . . . . . . . . . . 12
27	10	nnred 10540	. . . . . . . . . . . 12
28	26, 27	remulcld 9613	. . . . . . . . . . 11
29	25, 28	remulcld 9613	. . . . . . . . . 10
30	29	renegcld 9975	. . . . . . . . . 10
31	16, 17	absrpcld 13228	. . . . . . . . . 10
32	3	nnzd 10954	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 11996	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1234	. . . . . . . . . . 11
36	4	sqcld 12263	. . . . . . . . . . . . . . 15
37	11	sqcld 12263	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9605	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9923	. . . . . . . . . . . . . 14
40	4	sqvald 12262	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2502	. . . . . . . . . . . . 13
42	41	oveq1d 6290	. . . . . . . . . . . 12
43	23	resqcld 12291	. . . . . . . . . . . . . 14
44	27	resqcld 12291	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9613	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9976	. . . . . . . . . . . . 13
47		0re 9585	. . . . . . . . . . . . . 14
48	47	a1i 11	. . . . . . . . . . . . 13
49	16	abscld 13216	. . . . . . . . . . . . . . . . . . 19
50	49	recnd 9611	. . . . . . . . . . . . . . . . . 18
51	16, 17	absne0d 13227	. . . . . . . . . . . . . . . . . 18
52	50, 51	dividd 10307	. . . . . . . . . . . . . . . . 17
53		1z 10883	. . . . . . . . . . . . . . . . . 18
54	53	a1i 11	. . . . . . . . . . . . . . . . 17
55	52, 54	eqeltrd 2548	. . . . . . . . . . . . . . . 16
56		mod0 11959	. . . . . . . . . . . . . . . . 17 $/\$
57	49, 31, 56	syl2anc 661	. . . . . . . . . . . . . . . 16
58	55, 57	mpbird 232	. . . . . . . . . . . . . . 15
59	15	zred 10955	. . . . . . . . . . . . . . . 16
60		absmod0 13086	. . . . . . . . . . . . . . . 16 $/\$
61	59, 31, 60	syl2anc 661	. . . . . . . . . . . . . . 15
62	58, 61	mpbird 232	. . . . . . . . . . . . . 14
63		pellex.no2	. . . . . . . . . . . . . . 15
64	63	oveq1d 6290	. . . . . . . . . . . . . 14
65		0mod 11983	. . . . . . . . . . . . . . 15
66	31, 65	syl 16	. . . . . . . . . . . . . 14
67	62, 64, 66	3eqtr4d 2511	. . . . . . . . . . . . 13
68		modadd1 11989	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
69	46, 48, 45, 31, 67, 68	syl221anc 1234	. . . . . . . . . . . 12
70	38	addid2d 9769	. . . . . . . . . . . . . 14
71	11	sqvald 12262	. . . . . . . . . . . . . . 15
72	71	oveq2d 6291	. . . . . . . . . . . . . 14
73	7, 11, 11	mul12d 9777	. . . . . . . . . . . . . 14
74	70, 72, 73	3eqtrd 2505	. . . . . . . . . . . . 13
75	74	oveq1d 6290	. . . . . . . . . . . 12
76	42, 69, 75	3eqtrd 2505	. . . . . . . . . . 11
77	6	nnzd 10954	. . . . . . . . . . . . . 14
78	10	nnzd 10954	. . . . . . . . . . . . . 14
79	77, 78	zmulcld 10961	. . . . . . . . . . . . 13
80		pellex.ycg	. . . . . . . . . . . . . 14
81	80	eqcomd 2468	. . . . . . . . . . . . 13
82		modmul1 11996	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
83	27, 26, 79, 31, 81, 82	syl221anc 1234	. . . . . . . . . . . 12
84	9, 7, 11	mul12d 9777	. . . . . . . . . . . . 13
85	84	oveq1d 6290	. . . . . . . . . . . 12
86	83, 85	eqtrd 2501	. . . . . . . . . . 11
87	35, 76, 86	3eqtrd 2505	. . . . . . . . . 10
88		modadd1 11989	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
89	24, 29, 30, 31, 87, 88	syl221anc 1234	. . . . . . . . 9
90	13	negidd 9909	. . . . . . . . . 10
91	90	oveq1d 6290	. . . . . . . . 9
92	21, 89, 91	3eqtrd 2505	. . . . . . . 8
93	92, 66	eqtrd 2501	. . . . . . 7
94	24, 29	resubcld 9976	. . . . . . . 8
95		absmod0 13086	. . . . . . . 8 $/\$
96	94, 31, 95	syl2anc 661	. . . . . . 7
97	93, 96	mpbid 210	. . . . . 6
98	14	abscld 13216	. . . . . . 7
99		mod0 11959	. . . . . . 7 $/\$
100	98, 31, 99	syl2anc 661	. . . . . 6
101	97, 100	mpbid 210	. . . . 5
102	18, 101	eqeltrd 2548	. . . 4
103	94, 59, 17	redivcld 10361	. . . . 5
104		absz 13094	. . . . 5
105	103, 104	syl 16	. . . 4
106	102, 105	mpbird 232	. . 3
107		0lt1 10064	. . . . . . . 8
108		1re 9584	. . . . . . . . 9
109	47, 108	ltnlei 9694	. . . . . . . 8
110	107, 109	mpbi 208	. . . . . . 7
111	9, 4	mulcld 9605	. . . . . . . . . . . . . 14
112	2, 11	mulcld 9605	. . . . . . . . . . . . . 14
113	111, 112	subcld 9919	. . . . . . . . . . . . 13
114	113, 16, 17	divcld 10309	. . . . . . . . . . . 12
115	114	abscld 13216	. . . . . . . . . . 11
116	115	resqcld 12291	. . . . . . . . . 10
117	6	nnnn0d 10841	. . . . . . . . . . 11
118	117	nn0ge0d 10844	. . . . . . . . . 10
119	115	sqge0d 12292	. . . . . . . . . 10
120	25, 116, 118, 119	mulge0d 10118	. . . . . . . . 9
121	25, 116	remulcld 9613	. . . . . . . . . 10
122	48, 121	suble0d 10132	. . . . . . . . 9
123	120, 122	mpbird 232	. . . . . . . 8
124		breq1 4443	. . . . . . . 8
125	123, 124	syl5ibrcom 222	. . . . . . 7
126	110, 125	mtoi 178	. . . . . 6
127		absresq 13085	. . . . . . . . . . . 12
128	103, 127	syl 16	. . . . . . . . . . 11
129	14, 16, 17	sqdivd 12278	. . . . . . . . . . 11
130	14	sqvald 12262	. . . . . . . . . . . 12
131	130	oveq1d 6290	. . . . . . . . . . 11
132	128, 129, 131	3eqtrd 2505	. . . . . . . . . 10
133	26, 23	remulcld 9613	. . . . . . . . . . . . . . . 16
134	22, 27	remulcld 9613	. . . . . . . . . . . . . . . 16
135	133, 134	resubcld 9976	. . . . . . . . . . . . . . 15
136	135, 59, 17	redivcld 10361	. . . . . . . . . . . . . 14
137		absresq 13085	. . . . . . . . . . . . . 14
138	136, 137	syl 16	. . . . . . . . . . . . 13
139	113, 16, 17	sqdivd 12278	. . . . . . . . . . . . 13
140	138, 139	eqtrd 2501	. . . . . . . . . . . 12
141	140	oveq2d 6291	. . . . . . . . . . 11
142	113	sqcld 12263	. . . . . . . . . . . 12
143	16	sqcld 12263	. . . . . . . . . . . 12
144		sqne0 12189	. . . . . . . . . . . . . 14
145	16, 144	syl 16	. . . . . . . . . . . . 13
146	17, 145	mpbird 232	. . . . . . . . . . . 12
147	7, 142, 143, 146	divassd 10344	. . . . . . . . . . 11
148	113	sqvald 12262	. . . . . . . . . . . . 13
149	148	oveq2d 6291	. . . . . . . . . . . 12
150	149	oveq1d 6290	. . . . . . . . . . 11
151	141, 147, 150	3eqtr2d 2507	. . . . . . . . . 10
152	132, 151	oveq12d 6293	. . . . . . . . 9
153	14, 14	mulcld 9605	. . . . . . . . . 10
154	113, 113	mulcld 9605	. . . . . . . . . . 11
155	7, 154	mulcld 9605	. . . . . . . . . 10
156	153, 155, 143, 146	divsubdird 10348	. . . . . . . . 9
157	5, 13, 5, 13	mulsubd 10004	. . . . . . . . . . . 12
158	111, 112, 111, 112	mulsubd 10004	. . . . . . . . . . . . . 14
159	158	oveq2d 6291	. . . . . . . . . . . . 13
160	111, 111	mulcld 9605	. . . . . . . . . . . . . . 15
161	112, 112	mulcld 9605	. . . . . . . . . . . . . . 15
162	160, 161	addcld 9604	. . . . . . . . . . . . . 14
163	111, 112	mulcld 9605	. . . . . . . . . . . . . . 15
164	163, 163	addcld 9604	. . . . . . . . . . . . . 14
165	7, 162, 164	subdid 10001	. . . . . . . . . . . . 13
166	7, 160, 161	adddid 9609	. . . . . . . . . . . . . 14
167	7, 163, 163	adddid 9609	. . . . . . . . . . . . . 14
168	166, 167	oveq12d 6293	. . . . . . . . . . . . 13
169	159, 165, 168	3eqtrd 2505	. . . . . . . . . . . 12
170	157, 169	oveq12d 6293	. . . . . . . . . . 11
171	170	oveq1d 6290	. . . . . . . . . 10
172	5, 13	mulcomd 9606	. . . . . . . . . . . . . . . 16
173	7, 12, 5	mulassd 9608	. . . . . . . . . . . . . . . 16
174	2, 4	mulcomd 9606	. . . . . . . . . . . . . . . . . . 19
175	174	oveq2d 6291	. . . . . . . . . . . . . . . . . 18
176	9, 11, 4, 2	mul4d 9780	. . . . . . . . . . . . . . . . . 18
177	11, 2	mulcomd 9606	. . . . . . . . . . . . . . . . . . 19
178	177	oveq2d 6291	. . . . . . . . . . . . . . . . . 18
179	175, 176, 178	3eqtrd 2505	. . . . . . . . . . . . . . . . 17
180	179	oveq2d 6291	. . . . . . . . . . . . . . . 16
181	172, 173, 180	3eqtrd 2505	. . . . . . . . . . . . . . 15
182	181, 181	oveq12d 6293	. . . . . . . . . . . . . 14
183	182	oveq2d 6291	. . . . . . . . . . . . 13
184	183	oveq1d 6290	. . . . . . . . . . . 12
185	5, 5	mulcld 9605	. . . . . . . . . . . . . 14
186	13, 13	mulcld 9605	. . . . . . . . . . . . . 14
187	185, 186	addcld 9604	. . . . . . . . . . . . 13
188	7, 160	mulcld 9605	. . . . . . . . . . . . . 14
189	7, 161	mulcld 9605	. . . . . . . . . . . . . 14
190	188, 189	addcld 9604	. . . . . . . . . . . . 13
191	7, 163	mulcld 9605	. . . . . . . . . . . . . 14
192	191, 191	addcld 9604	. . . . . . . . . . . . 13
193	187, 190, 192	nnncan2d 9954	. . . . . . . . . . . 12
194	185, 186, 188, 189	addsub4d 9966	. . . . . . . . . . . . 13
195	5	sqvald 12262	. . . . . . . . . . . . . . 15
196	111	sqvald 12262	. . . . . . . . . . . . . . . 16
197	196	oveq2d 6291	. . . . . . . . . . . . . . 15
198	195, 197	oveq12d 6293	. . . . . . . . . . . . . 14
199	13	sqvald 12262	. . . . . . . . . . . . . . 15
200	112	sqvald 12262	. . . . . . . . . . . . . . . 16
201	200	oveq2d 6291	. . . . . . . . . . . . . . 15
202	199, 201	oveq12d 6293	. . . . . . . . . . . . . 14
203	198, 202	oveq12d 6293	. . . . . . . . . . . . 13
204	2, 4	sqmuld 12277	. . . . . . . . . . . . . . . 16
205	9, 4	sqmuld 12277	. . . . . . . . . . . . . . . . . 18
206	205	oveq2d 6291	. . . . . . . . . . . . . . . . 17
207	9	sqcld 12263	. . . . . . . . . . . . . . . . . 18
208	7, 207, 36	mulassd 9608	. . . . . . . . . . . . . . . . 17
209	206, 208	eqtr4d 2504	. . . . . . . . . . . . . . . 16
210	204, 209	oveq12d 6293	. . . . . . . . . . . . . . 15
211	7	sqvald 12262	. . . . . . . . . . . . . . . . . 18
212	9, 11	sqmuld 12277	. . . . . . . . . . . . . . . . . 18
213	211, 212	oveq12d 6293	. . . . . . . . . . . . . . . . 17
214	7, 12	sqmuld 12277	. . . . . . . . . . . . . . . . 17
215	7, 7	mulcld 9605	. . . . . . . . . . . . . . . . . 18
216	215, 207, 37	mulassd 9608	. . . . . . . . . . . . . . . . 17
217	213, 214, 216	3eqtr4d 2511	. . . . . . . . . . . . . . . 16
218	2, 11	sqmuld 12277	. . . . . . . . . . . . . . . . . 18
219	218	oveq2d 6291	. . . . . . . . . . . . . . . . 17
220	2	sqcld 12263	. . . . . . . . . . . . . . . . . 18
221	7, 220, 37	mulassd 9608	. . . . . . . . . . . . . . . . 17
222	219, 221	eqtr4d 2504	. . . . . . . . . . . . . . . 16
223	217, 222	oveq12d 6293	. . . . . . . . . . . . . . 15
224	210, 223	oveq12d 6293	. . . . . . . . . . . . . 14
225	7, 207	mulcld 9605	. . . . . . . . . . . . . . . . 17
226	220, 225, 36	subdird 10002	. . . . . . . . . . . . . . . 16
227		pellex.no1	. . . . . . . . . . . . . . . . 17
228	227	oveq1d 6290	. . . . . . . . . . . . . . . 16
229	226, 228	eqtr3d 2503	. . . . . . . . . . . . . . 15
230	7, 7, 207	mulassd 9608	. . . . . . . . . . . . . . . . . 18
231	230	oveq1d 6290	. . . . . . . . . . . . . . . . 17
232	231	oveq1d 6290	. . . . . . . . . . . . . . . 16
233	215, 207	mulcld 9605	. . . . . . . . . . . . . . . . 17
234	7, 220	mulcld 9605	. . . . . . . . . . . . . . . . 17
235	233, 234, 37	subdird 10002	. . . . . . . . . . . . . . . 16
236		subdi 9979	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	236	eqcomd 2468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
238	7, 225, 220, 237	syl3anc 1223	. . . . . . . . . . . . . . . . . 18
239		negsubdi2 9867	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
240	239	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . 21 $/\$
241	220, 225, 240	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
242	227	negeqd 9803	. . . . . . . . . . . . . . . . . . . 20
243	241, 242	eqtrd 2501	. . . . . . . . . . . . . . . . . . 19
244	243	oveq2d 6291	. . . . . . . . . . . . . . . . . 18
245	7, 16	mulneg2d 9999	. . . . . . . . . . . . . . . . . 18
246	238, 244, 245	3eqtrd 2505	. . . . . . . . . . . . . . . . 17
247	246	oveq1d 6290	. . . . . . . . . . . . . . . 16
248	232, 235, 247	3eqtr3d 2509	. . . . . . . . . . . . . . 15
249	229, 248	oveq12d 6293	. . . . . . . . . . . . . 14
250	7, 16	mulcld 9605	. . . . . . . . . . . . . . . . . 18
251	250, 37	mulneg1d 9998	. . . . . . . . . . . . . . . . 17
252	7, 16	mulcomd 9606	. . . . . . . . . . . . . . . . . . . 20
253	252	oveq1d 6290	. . . . . . . . . . . . . . . . . . 19
254	16, 7, 37	mulassd 9608	. . . . . . . . . . . . . . . . . . 19
255	253, 254	eqtrd 2501	. . . . . . . . . . . . . . . . . 18
256	255	negeqd 9803	. . . . . . . . . . . . . . . . 17
257	251, 256	eqtrd 2501	. . . . . . . . . . . . . . . 16
258	257	oveq2d 6291	. . . . . . . . . . . . . . 15
259	16, 36	mulcld 9605	. . . . . . . . . . . . . . . 16
260	16, 38	mulcld 9605	. . . . . . . . . . . . . . . 16
261	259, 260	negsubd 9925	. . . . . . . . . . . . . . 15
262	63	oveq2d 6291	. . . . . . . . . . . . . . . 16
263		subdi 9979	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
264	263	eqcomd 2468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
265	16, 36, 38, 264	syl3anc 1223	. . . . . . . . . . . . . . . 16
266	16	sqvald 12262	. . . . . . . . . . . . . . . 16
267	262, 265, 266	3eqtr4d 2511	. . . . . . . . . . . . . . 15
268	258, 261, 267	3eqtrd 2505	. . . . . . . . . . . . . 14
269	224, 249, 268	3eqtrd 2505	. . . . . . . . . . . . 13
270	194, 203, 269	3eqtr2d 2507	. . . . . . . . . . . 12
271	184, 193, 270	3eqtrd 2505	. . . . . . . . . . 11
272	271	oveq1d 6290	. . . . . . . . . 10
273	143, 146	dividd 10307	. . . . . . . . . 10
274	171, 272, 273	3eqtrd 2505	. . . . . . . . 9
275	152, 156, 274	3eqtr2d 2507	. . . . . . . 8
276	275	adantr 465	. . . . . . 7 $/\$
277		simpr 461	. . . . . . . . . . . 12 $/\$
278	277	oveq1d 6290	. . . . . . . . . . 11 $/\$
279	278	fveq2d 5861	. . . . . . . . . 10 $/\$
280	16, 17	div0d 10308	. . . . . . . . . . . 12
281	280	abs00bd 13074	. . . . . . . . . . 11
282	281	adantr 465	. . . . . . . . . 10 $/\$
283	279, 282	eqtrd 2501	. . . . . . . . 9 $/\$
284	283	sq0id 12216	. . . . . . . 8 $/\$
285	284	oveq1d 6290	. . . . . . 7 $/\$
286	276, 285	eqtr3d 2503	. . . . . 6 $/\$
287	126, 286	mtand 659	. . . . 5
288	287	neqned 2663	. . . 4
289	14, 16, 288, 17	divne0d 10325	. . 3
290		nnabscl 13107	. . 3 $/\$
291	106, 289, 290	syl2anc 661	. 2
292	113, 16, 17	absdivd 13235	. . . . 5
293		negsub 9856	. . . . . . . . . . . 12 $/\$
294	293	eqcomd 2468	. . . . . . . . . . 11 $/\$
295	111, 112, 294	syl2anc 661	. . . . . . . . . 10
296	295	oveq1d 6290	. . . . . . . . 9
297	134	renegcld 9975	. . . . . . . . . 10
298	11, 4	mulcomd 9606	. . . . . . . . . . . 12
299	298	oveq1d 6290	. . . . . . . . . . 11
300		modmul1 11996	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
301	26, 27, 32, 31, 80, 300	syl221anc 1234	. . . . . . . . . . 11
302		modmul1 11996	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
303	22, 23, 78, 31, 33, 302	syl221anc 1234	. . . . . . . . . . 11
304	299, 301, 303	3eqtr4d 2511	. . . . . . . . . 10
305		modadd1 11989	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
306	133, 134, 297, 31, 304, 305	syl221anc 1234	. . . . . . . . 9
307	112	negidd 9909	. . . . . . . . . 10
308	307	oveq1d 6290	. . . . . . . . 9
309	296, 306, 308	3eqtrd 2505	. . . . . . . 8
310	309, 66	eqtrd 2501	. . . . . . 7
311		absmod0 13086	. . . . . . . 8 $/\$
312	135, 31, 311	syl2anc 661	. . . . . . 7
313	310, 312	mpbid 210	. . . . . 6
314	113	abscld 13216	. . . . . . 7
315		mod0 11959	. . . . . . 7 $/\$
316	314, 31, 315	syl2anc 661	. . . . . 6
317	313, 316	mpbid 210	. . . . 5
318	292, 317	eqeltrd 2548	. . . 4
319		absz 13094	. . . . 5
320	136, 319	syl 16	. . . 4
321	318, 320	mpbird 232	. . 3
322		pellex.neq	. . . . . . 7 $/\$
323	10	nnne0d 10569	. . . . . . . . 9
324	3	nnne0d 10569	. . . . . . . . 9
325	9, 11, 2, 4, 323, 324	divmuleqd 10355	. . . . . . . 8
326	63	adantr 465	. . . . . . . . . . . . . . 15 $/\$
327	326	eqcomd 2468	. . . . . . . . . . . . . 14 $/\$
328	327	oveq2d 6291	. . . . . . . . . . . . 13 $/\$
329	9, 11, 323	divcld 10309	. . . . . . . . . . . . . . . 16
330	329	sqcld 12263	. . . . . . . . . . . . . . 15
331	330	adantr 465	. . . . . . . . . . . . . 14 $/\$
332	36	adantr 465	. . . . . . . . . . . . . 14 $/\$
333	38	adantr 465	. . . . . . . . . . . . . 14 $/\$
334	331, 332, 333	subdid 10001	. . . . . . . . . . . . 13 $/\$
335		oveq1 6282	. . . . . . . . . . . . . . . . 17
336	335	oveq1d 6290	. . . . . . . . . . . . . . . 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 12278	. . . . . . . . . . . . . . . 16 $/\$
342	341	oveq1d 6290	. . . . . . . . . . . . . . 15 $/\$
343	220	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
344		sqne0 12189	. . . . . . . . . . . . . . . . . . 19
345	4, 344	syl 16	. . . . . . . . . . . . . . . . . 18
346	324, 345	mpbird 232	. . . . . . . . . . . . . . . . 17
347	346	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
348	343, 332, 347	divcan1d 10310	. . . . . . . . . . . . . . 15 $/\$
349	337, 342, 348	3eqtrd 2505	. . . . . . . . . . . . . 14 $/\$
350	7	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
351	37	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
352	331, 350, 351	mul12d 9777	. . . . . . . . . . . . . . 15 $/\$
353	9	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
354	11	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
355	323	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
356	353, 354, 355	sqdivd 12278	. . . . . . . . . . . . . . . . 17 $/\$
357	356	oveq1d 6290	. . . . . . . . . . . . . . . 16 $/\$
358	357	oveq2d 6291	. . . . . . . . . . . . . . 15 $/\$
359	207	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
360		sqne0 12189	. . . . . . . . . . . . . . . . . . . 20
361	11, 360	syl 16	. . . . . . . . . . . . . . . . . . 19
362	323, 361	mpbird 232	. . . . . . . . . . . . . . . . . 18
363	362	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
364	359, 351, 363	divcan1d 10310	. . . . . . . . . . . . . . . 16 $/\$