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 29020

Description: Lemma for pellex 29021. 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 10326	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10326	. . . . . . . 8
5	2, 4	mulcld 9394	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10326	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10326	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10326	. . . . . . . . 9
12	9, 11	mulcld 9394	. . . . . . . 8
13	7, 12	mulcld 9394	. . . . . . 7
14	5, 13	subcld 9707	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10736	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 12925	. . . . 5
19	5, 13	negsubd 9713	. . . . . . . . . . 11
20	19	eqcomd 2438	. . . . . . . . . 10
21	20	oveq1d 6095	. . . . . . . . 9
22	1	nnred 10325	. . . . . . . . . . 11
23	3	nnred 10325	. . . . . . . . . . 11
24	22, 23	remulcld 9402	. . . . . . . . . 10
25	6	nnred 10325	. . . . . . . . . . 11
26	8	nnred 10325	. . . . . . . . . . . 12
27	10	nnred 10325	. . . . . . . . . . . 12
28	26, 27	remulcld 9402	. . . . . . . . . . 11
29	25, 28	remulcld 9402	. . . . . . . . . 10
30	29	renegcld 9763	. . . . . . . . . 10
31	16, 17	absrpcld 12918	. . . . . . . . . 10
32	3	nnzd 10734	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 11736	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1222	. . . . . . . . . . 11
36	4	sqcld 11990	. . . . . . . . . . . . . . 15
37	11	sqcld 11990	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9394	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9711	. . . . . . . . . . . . . 14
40	4	sqvald 11989	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2466	. . . . . . . . . . . . 13
42	41	oveq1d 6095	. . . . . . . . . . . 12
43	23	resqcld 12018	. . . . . . . . . . . . . 14
44	27	resqcld 12018	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9402	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9764	. . . . . . . . . . . . 13
47		0re 9374	. . . . . . . . . . . . . 14
48	47	a1i 11	. . . . . . . . . . . . 13
49	16	abscld 12906	. . . . . . . . . . . . . . . . . . 19
50	49	recnd 9400	. . . . . . . . . . . . . . . . . 18
51	16, 17	absne0d 12917	. . . . . . . . . . . . . . . . . 18
52	50, 51	dividd 10093	. . . . . . . . . . . . . . . . 17
53		1z 10664	. . . . . . . . . . . . . . . . . 18
54	53	a1i 11	. . . . . . . . . . . . . . . . 17
55	52, 54	eqeltrd 2507	. . . . . . . . . . . . . . . 16
56		mod0 11699	. . . . . . . . . . . . . . . . 17 $/\$
57	49, 31, 56	syl2anc 654	. . . . . . . . . . . . . . . 16
58	55, 57	mpbird 232	. . . . . . . . . . . . . . 15
59	15	zred 10735	. . . . . . . . . . . . . . . 16
60		absmod0 12776	. . . . . . . . . . . . . . . 16 $/\$
61	59, 31, 60	syl2anc 654	. . . . . . . . . . . . . . 15
62	58, 61	mpbird 232	. . . . . . . . . . . . . 14
63		pellex.no2	. . . . . . . . . . . . . . 15
64	63	oveq1d 6095	. . . . . . . . . . . . . 14
65		0mod 11723	. . . . . . . . . . . . . . 15
66	31, 65	syl 16	. . . . . . . . . . . . . 14
67	62, 64, 66	3eqtr4d 2475	. . . . . . . . . . . . 13
68		modadd1 11729	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
69	46, 48, 45, 31, 67, 68	syl221anc 1222	. . . . . . . . . . . 12
70	38	addid2d 9558	. . . . . . . . . . . . . 14
71	11	sqvald 11989	. . . . . . . . . . . . . . 15
72	71	oveq2d 6096	. . . . . . . . . . . . . 14
73	7, 11, 11	mul12d 9566	. . . . . . . . . . . . . 14
74	70, 72, 73	3eqtrd 2469	. . . . . . . . . . . . 13
75	74	oveq1d 6095	. . . . . . . . . . . 12
76	42, 69, 75	3eqtrd 2469	. . . . . . . . . . 11
77	6	nnzd 10734	. . . . . . . . . . . . . 14
78	10	nnzd 10734	. . . . . . . . . . . . . 14
79	77, 78	zmulcld 10741	. . . . . . . . . . . . 13
80		pellex.ycg	. . . . . . . . . . . . . 14
81	80	eqcomd 2438	. . . . . . . . . . . . 13
82		modmul1 11736	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
83	27, 26, 79, 31, 81, 82	syl221anc 1222	. . . . . . . . . . . 12
84	9, 7, 11	mul12d 9566	. . . . . . . . . . . . 13
85	84	oveq1d 6095	. . . . . . . . . . . 12
86	83, 85	eqtrd 2465	. . . . . . . . . . 11
87	35, 76, 86	3eqtrd 2469	. . . . . . . . . 10
88		modadd1 11729	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
89	24, 29, 30, 31, 87, 88	syl221anc 1222	. . . . . . . . 9
90	13	negidd 9697	. . . . . . . . . 10
91	90	oveq1d 6095	. . . . . . . . 9
92	21, 89, 91	3eqtrd 2469	. . . . . . . 8
93	92, 66	eqtrd 2465	. . . . . . 7
94	24, 29	resubcld 9764	. . . . . . . 8
95		absmod0 12776	. . . . . . . 8 $/\$
96	94, 31, 95	syl2anc 654	. . . . . . 7
97	93, 96	mpbid 210	. . . . . 6
98	14	abscld 12906	. . . . . . 7
99		mod0 11699	. . . . . . 7 $/\$
100	98, 31, 99	syl2anc 654	. . . . . 6
101	97, 100	mpbid 210	. . . . 5
102	18, 101	eqeltrd 2507	. . . 4
103	94, 59, 17	redivcld 10147	. . . . 5
104		absz 12784	. . . . 5
105	103, 104	syl 16	. . . 4
106	102, 105	mpbird 232	. . 3
107		0lt1 9850	. . . . . . . 8
108		1re 9373	. . . . . . . . 9
109	47, 108	ltnlei 9483	. . . . . . . 8
110	107, 109	mpbi 208	. . . . . . 7
111	9, 4	mulcld 9394	. . . . . . . . . . . . . 14
112	2, 11	mulcld 9394	. . . . . . . . . . . . . 14
113	111, 112	subcld 9707	. . . . . . . . . . . . 13
114	113, 16, 17	divcld 10095	. . . . . . . . . . . 12
115	114	abscld 12906	. . . . . . . . . . 11
116	115	resqcld 12018	. . . . . . . . . 10
117	6	nnnn0d 10624	. . . . . . . . . . 11
118	117	nn0ge0d 10627	. . . . . . . . . 10
119	115	sqge0d 12019	. . . . . . . . . 10
120	25, 116, 118, 119	mulge0d 9904	. . . . . . . . 9
121	25, 116	remulcld 9402	. . . . . . . . . 10
122	48, 121	suble0d 9918	. . . . . . . . 9
123	120, 122	mpbird 232	. . . . . . . 8
124		breq1 4283	. . . . . . . 8
125	123, 124	syl5ibrcom 222	. . . . . . 7
126	110, 125	mtoi 178	. . . . . 6
127		absresq 12775	. . . . . . . . . . . 12
128	103, 127	syl 16	. . . . . . . . . . 11
129	14, 16, 17	sqdivd 12005	. . . . . . . . . . 11
130	14	sqvald 11989	. . . . . . . . . . . 12
131	130	oveq1d 6095	. . . . . . . . . . 11
132	128, 129, 131	3eqtrd 2469	. . . . . . . . . 10
133	26, 23	remulcld 9402	. . . . . . . . . . . . . . . 16
134	22, 27	remulcld 9402	. . . . . . . . . . . . . . . 16
135	133, 134	resubcld 9764	. . . . . . . . . . . . . . 15
136	135, 59, 17	redivcld 10147	. . . . . . . . . . . . . 14
137		absresq 12775	. . . . . . . . . . . . . 14
138	136, 137	syl 16	. . . . . . . . . . . . 13
139	113, 16, 17	sqdivd 12005	. . . . . . . . . . . . 13
140	138, 139	eqtrd 2465	. . . . . . . . . . . 12
141	140	oveq2d 6096	. . . . . . . . . . 11
142	113	sqcld 11990	. . . . . . . . . . . 12
143	16	sqcld 11990	. . . . . . . . . . . 12
144		sqne0 11916	. . . . . . . . . . . . . 14
145	16, 144	syl 16	. . . . . . . . . . . . 13
146	17, 145	mpbird 232	. . . . . . . . . . . 12
147	7, 142, 143, 146	divassd 10130	. . . . . . . . . . 11
148	113	sqvald 11989	. . . . . . . . . . . . 13
149	148	oveq2d 6096	. . . . . . . . . . . 12
150	149	oveq1d 6095	. . . . . . . . . . 11
151	141, 147, 150	3eqtr2d 2471	. . . . . . . . . 10
152	132, 151	oveq12d 6098	. . . . . . . . 9
153	14, 14	mulcld 9394	. . . . . . . . . 10
154	113, 113	mulcld 9394	. . . . . . . . . . 11
155	7, 154	mulcld 9394	. . . . . . . . . 10
156	153, 155, 143, 146	divsubdird 10134	. . . . . . . . 9
157	5, 13, 5, 13	mulsubd 9791	. . . . . . . . . . . 12
158	111, 112, 111, 112	mulsubd 9791	. . . . . . . . . . . . . 14
159	158	oveq2d 6096	. . . . . . . . . . . . 13
160	111, 111	mulcld 9394	. . . . . . . . . . . . . . 15
161	112, 112	mulcld 9394	. . . . . . . . . . . . . . 15
162	160, 161	addcld 9393	. . . . . . . . . . . . . 14
163	111, 112	mulcld 9394	. . . . . . . . . . . . . . 15
164	163, 163	addcld 9393	. . . . . . . . . . . . . 14
165	7, 162, 164	subdid 9788	. . . . . . . . . . . . 13
166	7, 160, 161	adddid 9398	. . . . . . . . . . . . . 14
167	7, 163, 163	adddid 9398	. . . . . . . . . . . . . 14
168	166, 167	oveq12d 6098	. . . . . . . . . . . . 13
169	159, 165, 168	3eqtrd 2469	. . . . . . . . . . . 12
170	157, 169	oveq12d 6098	. . . . . . . . . . 11
171	170	oveq1d 6095	. . . . . . . . . 10
172	5, 13	mulcomd 9395	. . . . . . . . . . . . . . . 16
173	7, 12, 5	mulassd 9397	. . . . . . . . . . . . . . . 16
174	2, 4	mulcomd 9395	. . . . . . . . . . . . . . . . . . 19
175	174	oveq2d 6096	. . . . . . . . . . . . . . . . . 18
176	9, 11, 4, 2	mul4d 9569	. . . . . . . . . . . . . . . . . 18
177	11, 2	mulcomd 9395	. . . . . . . . . . . . . . . . . . 19
178	177	oveq2d 6096	. . . . . . . . . . . . . . . . . 18
179	175, 176, 178	3eqtrd 2469	. . . . . . . . . . . . . . . . 17
180	179	oveq2d 6096	. . . . . . . . . . . . . . . 16
181	172, 173, 180	3eqtrd 2469	. . . . . . . . . . . . . . 15
182	181, 181	oveq12d 6098	. . . . . . . . . . . . . 14
183	182	oveq2d 6096	. . . . . . . . . . . . 13
184	183	oveq1d 6095	. . . . . . . . . . . 12
185	5, 5	mulcld 9394	. . . . . . . . . . . . . 14
186	13, 13	mulcld 9394	. . . . . . . . . . . . . 14
187	185, 186	addcld 9393	. . . . . . . . . . . . 13
188	7, 160	mulcld 9394	. . . . . . . . . . . . . 14
189	7, 161	mulcld 9394	. . . . . . . . . . . . . 14
190	188, 189	addcld 9393	. . . . . . . . . . . . 13
191	7, 163	mulcld 9394	. . . . . . . . . . . . . 14
192	191, 191	addcld 9393	. . . . . . . . . . . . 13
193	187, 190, 192	nnncan2d 9742	. . . . . . . . . . . 12
194	185, 186, 188, 189	addsub4d 9754	. . . . . . . . . . . . 13
195	5	sqvald 11989	. . . . . . . . . . . . . . 15
196	111	sqvald 11989	. . . . . . . . . . . . . . . 16
197	196	oveq2d 6096	. . . . . . . . . . . . . . 15
198	195, 197	oveq12d 6098	. . . . . . . . . . . . . 14
199	13	sqvald 11989	. . . . . . . . . . . . . . 15
200	112	sqvald 11989	. . . . . . . . . . . . . . . 16
201	200	oveq2d 6096	. . . . . . . . . . . . . . 15
202	199, 201	oveq12d 6098	. . . . . . . . . . . . . 14
203	198, 202	oveq12d 6098	. . . . . . . . . . . . 13
204	2, 4	sqmuld 12004	. . . . . . . . . . . . . . . 16
205	9, 4	sqmuld 12004	. . . . . . . . . . . . . . . . . 18
206	205	oveq2d 6096	. . . . . . . . . . . . . . . . 17
207	9	sqcld 11990	. . . . . . . . . . . . . . . . . 18
208	7, 207, 36	mulassd 9397	. . . . . . . . . . . . . . . . 17
209	206, 208	eqtr4d 2468	. . . . . . . . . . . . . . . 16
210	204, 209	oveq12d 6098	. . . . . . . . . . . . . . 15
211	7	sqvald 11989	. . . . . . . . . . . . . . . . . 18
212	9, 11	sqmuld 12004	. . . . . . . . . . . . . . . . . 18
213	211, 212	oveq12d 6098	. . . . . . . . . . . . . . . . 17
214	7, 12	sqmuld 12004	. . . . . . . . . . . . . . . . 17
215	7, 7	mulcld 9394	. . . . . . . . . . . . . . . . . 18
216	215, 207, 37	mulassd 9397	. . . . . . . . . . . . . . . . 17
217	213, 214, 216	3eqtr4d 2475	. . . . . . . . . . . . . . . 16
218	2, 11	sqmuld 12004	. . . . . . . . . . . . . . . . . 18
219	218	oveq2d 6096	. . . . . . . . . . . . . . . . 17
220	2	sqcld 11990	. . . . . . . . . . . . . . . . . 18
221	7, 220, 37	mulassd 9397	. . . . . . . . . . . . . . . . 17
222	219, 221	eqtr4d 2468	. . . . . . . . . . . . . . . 16
223	217, 222	oveq12d 6098	. . . . . . . . . . . . . . 15
224	210, 223	oveq12d 6098	. . . . . . . . . . . . . 14
225	7, 207	mulcld 9394	. . . . . . . . . . . . . . . . 17
226	220, 225, 36	subdird 9789	. . . . . . . . . . . . . . . 16
227		pellex.no1	. . . . . . . . . . . . . . . . 17
228	227	oveq1d 6095	. . . . . . . . . . . . . . . 16
229	226, 228	eqtr3d 2467	. . . . . . . . . . . . . . 15
230	7, 7, 207	mulassd 9397	. . . . . . . . . . . . . . . . . 18
231	230	oveq1d 6095	. . . . . . . . . . . . . . . . 17
232	231	oveq1d 6095	. . . . . . . . . . . . . . . 16
233	215, 207	mulcld 9394	. . . . . . . . . . . . . . . . 17
234	7, 220	mulcld 9394	. . . . . . . . . . . . . . . . 17
235	233, 234, 37	subdird 9789	. . . . . . . . . . . . . . . 16
236		subdi 9766	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	236	eqcomd 2438	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
238	7, 225, 220, 237	syl3anc 1211	. . . . . . . . . . . . . . . . . 18
239		negsubdi2 9656	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
240	239	eqcomd 2438	. . . . . . . . . . . . . . . . . . . . 21 $/\$
241	220, 225, 240	syl2anc 654	. . . . . . . . . . . . . . . . . . . 20
242	227	negeqd 9592	. . . . . . . . . . . . . . . . . . . 20
243	241, 242	eqtrd 2465	. . . . . . . . . . . . . . . . . . 19
244	243	oveq2d 6096	. . . . . . . . . . . . . . . . . 18
245	7, 16	mulneg2d 9786	. . . . . . . . . . . . . . . . . 18
246	238, 244, 245	3eqtrd 2469	. . . . . . . . . . . . . . . . 17
247	246	oveq1d 6095	. . . . . . . . . . . . . . . 16
248	232, 235, 247	3eqtr3d 2473	. . . . . . . . . . . . . . 15
249	229, 248	oveq12d 6098	. . . . . . . . . . . . . 14
250	7, 16	mulcld 9394	. . . . . . . . . . . . . . . . . 18
251	250, 37	mulneg1d 9785	. . . . . . . . . . . . . . . . 17
252	7, 16	mulcomd 9395	. . . . . . . . . . . . . . . . . . . 20
253	252	oveq1d 6095	. . . . . . . . . . . . . . . . . . 19
254	16, 7, 37	mulassd 9397	. . . . . . . . . . . . . . . . . . 19
255	253, 254	eqtrd 2465	. . . . . . . . . . . . . . . . . 18
256	255	negeqd 9592	. . . . . . . . . . . . . . . . 17
257	251, 256	eqtrd 2465	. . . . . . . . . . . . . . . 16
258	257	oveq2d 6096	. . . . . . . . . . . . . . 15
259	16, 36	mulcld 9394	. . . . . . . . . . . . . . . 16
260	16, 38	mulcld 9394	. . . . . . . . . . . . . . . 16
261	259, 260	negsubd 9713	. . . . . . . . . . . . . . 15
262	63	oveq2d 6096	. . . . . . . . . . . . . . . 16
263		subdi 9766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
264	263	eqcomd 2438	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
265	16, 36, 38, 264	syl3anc 1211	. . . . . . . . . . . . . . . 16
266	16	sqvald 11989	. . . . . . . . . . . . . . . 16
267	262, 265, 266	3eqtr4d 2475	. . . . . . . . . . . . . . 15
268	258, 261, 267	3eqtrd 2469	. . . . . . . . . . . . . 14
269	224, 249, 268	3eqtrd 2469	. . . . . . . . . . . . 13
270	194, 203, 269	3eqtr2d 2471	. . . . . . . . . . . 12
271	184, 193, 270	3eqtrd 2469	. . . . . . . . . . 11
272	271	oveq1d 6095	. . . . . . . . . 10
273	143, 146	dividd 10093	. . . . . . . . . 10
274	171, 272, 273	3eqtrd 2469	. . . . . . . . 9
275	152, 156, 274	3eqtr2d 2471	. . . . . . . 8
276	275	adantr 462	. . . . . . 7 $/\$
277		simpr 458	. . . . . . . . . . . 12 $/\$
278	277	oveq1d 6095	. . . . . . . . . . 11 $/\$
279	278	fveq2d 5683	. . . . . . . . . 10 $/\$
280	16, 17	div0d 10094	. . . . . . . . . . . 12
281	280	abs00bd 12764	. . . . . . . . . . 11
282	281	adantr 462	. . . . . . . . . 10 $/\$
283	279, 282	eqtrd 2465	. . . . . . . . 9 $/\$
284	283	sq0id 11943	. . . . . . . 8 $/\$
285	284	oveq1d 6095	. . . . . . 7 $/\$
286	276, 285	eqtr3d 2467	. . . . . 6 $/\$
287	126, 286	mtand 652	. . . . 5
288	287	neneqad 2671	. . . 4
289	14, 16, 288, 17	divne0d 10111	. . 3
290		nnabscl 12797	. . 3 $/\$
291	106, 289, 290	syl2anc 654	. 2
292	113, 16, 17	absdivd 12925	. . . . 5
293		negsub 9645	. . . . . . . . . . . 12 $/\$
294	293	eqcomd 2438	. . . . . . . . . . 11 $/\$
295	111, 112, 294	syl2anc 654	. . . . . . . . . 10
296	295	oveq1d 6095	. . . . . . . . 9
297	134	renegcld 9763	. . . . . . . . . 10
298	11, 4	mulcomd 9395	. . . . . . . . . . . 12
299	298	oveq1d 6095	. . . . . . . . . . 11
300		modmul1 11736	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
301	26, 27, 32, 31, 80, 300	syl221anc 1222	. . . . . . . . . . 11
302		modmul1 11736	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
303	22, 23, 78, 31, 33, 302	syl221anc 1222	. . . . . . . . . . 11
304	299, 301, 303	3eqtr4d 2475	. . . . . . . . . 10
305		modadd1 11729	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
306	133, 134, 297, 31, 304, 305	syl221anc 1222	. . . . . . . . 9
307	112	negidd 9697	. . . . . . . . . 10
308	307	oveq1d 6095	. . . . . . . . 9
309	296, 306, 308	3eqtrd 2469	. . . . . . . 8
310	309, 66	eqtrd 2465	. . . . . . 7
311		absmod0 12776	. . . . . . . 8 $/\$
312	135, 31, 311	syl2anc 654	. . . . . . 7
313	310, 312	mpbid 210	. . . . . 6
314	113	abscld 12906	. . . . . . 7
315		mod0 11699	. . . . . . 7 $/\$
316	314, 31, 315	syl2anc 654	. . . . . 6
317	313, 316	mpbid 210	. . . . 5
318	292, 317	eqeltrd 2507	. . . 4
319		absz 12784	. . . . 5
320	136, 319	syl 16	. . . 4
321	318, 320	mpbird 232	. . 3
322		pellex.neq	. . . . . . 7 $/\$
323	10	nnne0d 10354	. . . . . . . . 9
324	3	nnne0d 10354	. . . . . . . . 9
325	9, 11, 2, 4, 323, 324	divmuleqd 10141	. . . . . . . 8
326	63	adantr 462	. . . . . . . . . . . . . . 15 $/\$
327	326	eqcomd 2438	. . . . . . . . . . . . . 14 $/\$
328	327	oveq2d 6096	. . . . . . . . . . . . 13 $/\$
329	9, 11, 323	divcld 10095	. . . . . . . . . . . . . . . 16
330	329	sqcld 11990	. . . . . . . . . . . . . . 15
331	330	adantr 462	. . . . . . . . . . . . . 14 $/\$
332	36	adantr 462	. . . . . . . . . . . . . 14 $/\$
333	38	adantr 462	. . . . . . . . . . . . . 14 $/\$
334	331, 332, 333	subdid 9788	. . . . . . . . . . . . 13 $/\$
335		oveq1 6087	. . . . . . . . . . . . . . . . 17
336	335	oveq1d 6095	. . . . . . . . . . . . . . . 16
337	336	adantl 463	. . . . . . . . . . . . . . 15 $/\$
338	2	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
339	4	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
340	324	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
341	338, 339, 340	sqdivd 12005	. . . . . . . . . . . . . . . 16 $/\$
342	341	oveq1d 6095	. . . . . . . . . . . . . . 15 $/\$
343	220	adantr 462	. . . . . . . . . . . . . . . 16 $/\$
344		sqne0 11916	. . . . . . . . . . . . . . . . . . 19
345	4, 344	syl 16	. . . . . . . . . . . . . . . . . 18
346	324, 345	mpbird 232	. . . . . . . . . . . . . . . . 17
347	346	adantr 462	. . . . . . . . . . . . . . . 16 $/\$
348	343, 332, 347	divcan1d 10096	. . . . . . . . . . . . . . 15 $/\$
349	337, 342, 348	3eqtrd 2469	. . . . . . . . . . . . . 14 $/\$
350	7	adantr 462	. . . . . . . . . . . . . . . 16 $/\$
351	37	adantr 462	. . . . . . . . . . . . . . . 16 $/\$
352	331, 350, 351	mul12d 9566	. . . . . . . . . . . . . . 15 $/\$
353	9	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$
354	11	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$
355	323	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$
356	353, 354, 355	sqdivd 12005	. . . . . . . . . . . . . . . . 17 $/\$
357	356	oveq1d 6095	. . . . . . . . . . . . . . . 16 $/\$
358	357	oveq2d 6096	. . . . . . . . . . . . . . 15 $/\$
359	207	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
360		sqne0 11916	. . . . . . . . . . . . . . . . . . . 20
361	11, 360	syl 16	. . . . . . . . . . . . . . . . . . 19
362	323, 361	mpbird 232	. . . . . . . . . . . . . . . . . 18
363	362	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$
364	359, 351, 363	divcan1d 10096	. . . . . . . . . . . . . . . 16 $/\$