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 29324

Description: Lemma for pellex 29325. 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 10450	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10450	. . . . . . . 8
5	2, 4	mulcld 9518	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10450	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10450	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10450	. . . . . . . . 9
12	9, 11	mulcld 9518	. . . . . . . 8
13	7, 12	mulcld 9518	. . . . . . 7
14	5, 13	subcld 9831	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10860	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13060	. . . . 5
19	5, 13	negsubd 9837	. . . . . . . . . . 11
20	19	eqcomd 2462	. . . . . . . . . 10
21	20	oveq1d 6216	. . . . . . . . 9
22	1	nnred 10449	. . . . . . . . . . 11
23	3	nnred 10449	. . . . . . . . . . 11
24	22, 23	remulcld 9526	. . . . . . . . . 10
25	6	nnred 10449	. . . . . . . . . . 11
26	8	nnred 10449	. . . . . . . . . . . 12
27	10	nnred 10449	. . . . . . . . . . . 12
28	26, 27	remulcld 9526	. . . . . . . . . . 11
29	25, 28	remulcld 9526	. . . . . . . . . 10
30	29	renegcld 9887	. . . . . . . . . 10
31	16, 17	absrpcld 13053	. . . . . . . . . 10
32	3	nnzd 10858	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 11870	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1230	. . . . . . . . . . 11
36	4	sqcld 12124	. . . . . . . . . . . . . . 15
37	11	sqcld 12124	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9518	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9835	. . . . . . . . . . . . . 14
40	4	sqvald 12123	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2496	. . . . . . . . . . . . 13
42	41	oveq1d 6216	. . . . . . . . . . . 12
43	23	resqcld 12152	. . . . . . . . . . . . . 14
44	27	resqcld 12152	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9526	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9888	. . . . . . . . . . . . 13
47		0re 9498	. . . . . . . . . . . . . 14
48	47	a1i 11	. . . . . . . . . . . . 13
49	16	abscld 13041	. . . . . . . . . . . . . . . . . . 19
50	49	recnd 9524	. . . . . . . . . . . . . . . . . 18
51	16, 17	absne0d 13052	. . . . . . . . . . . . . . . . . 18
52	50, 51	dividd 10217	. . . . . . . . . . . . . . . . 17
53		1z 10788	. . . . . . . . . . . . . . . . . 18
54	53	a1i 11	. . . . . . . . . . . . . . . . 17
55	52, 54	eqeltrd 2542	. . . . . . . . . . . . . . . 16
56		mod0 11833	. . . . . . . . . . . . . . . . 17 $/\$
57	49, 31, 56	syl2anc 661	. . . . . . . . . . . . . . . 16
58	55, 57	mpbird 232	. . . . . . . . . . . . . . 15
59	15	zred 10859	. . . . . . . . . . . . . . . 16
60		absmod0 12911	. . . . . . . . . . . . . . . 16 $/\$
61	59, 31, 60	syl2anc 661	. . . . . . . . . . . . . . 15
62	58, 61	mpbird 232	. . . . . . . . . . . . . 14
63		pellex.no2	. . . . . . . . . . . . . . 15
64	63	oveq1d 6216	. . . . . . . . . . . . . 14
65		0mod 11857	. . . . . . . . . . . . . . 15
66	31, 65	syl 16	. . . . . . . . . . . . . 14
67	62, 64, 66	3eqtr4d 2505	. . . . . . . . . . . . 13
68		modadd1 11863	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
69	46, 48, 45, 31, 67, 68	syl221anc 1230	. . . . . . . . . . . 12
70	38	addid2d 9682	. . . . . . . . . . . . . 14
71	11	sqvald 12123	. . . . . . . . . . . . . . 15
72	71	oveq2d 6217	. . . . . . . . . . . . . 14
73	7, 11, 11	mul12d 9690	. . . . . . . . . . . . . 14
74	70, 72, 73	3eqtrd 2499	. . . . . . . . . . . . 13
75	74	oveq1d 6216	. . . . . . . . . . . 12
76	42, 69, 75	3eqtrd 2499	. . . . . . . . . . 11
77	6	nnzd 10858	. . . . . . . . . . . . . 14
78	10	nnzd 10858	. . . . . . . . . . . . . 14
79	77, 78	zmulcld 10865	. . . . . . . . . . . . 13
80		pellex.ycg	. . . . . . . . . . . . . 14
81	80	eqcomd 2462	. . . . . . . . . . . . 13
82		modmul1 11870	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
83	27, 26, 79, 31, 81, 82	syl221anc 1230	. . . . . . . . . . . 12
84	9, 7, 11	mul12d 9690	. . . . . . . . . . . . 13
85	84	oveq1d 6216	. . . . . . . . . . . 12
86	83, 85	eqtrd 2495	. . . . . . . . . . 11
87	35, 76, 86	3eqtrd 2499	. . . . . . . . . 10
88		modadd1 11863	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
89	24, 29, 30, 31, 87, 88	syl221anc 1230	. . . . . . . . 9
90	13	negidd 9821	. . . . . . . . . 10
91	90	oveq1d 6216	. . . . . . . . 9
92	21, 89, 91	3eqtrd 2499	. . . . . . . 8
93	92, 66	eqtrd 2495	. . . . . . 7
94	24, 29	resubcld 9888	. . . . . . . 8
95		absmod0 12911	. . . . . . . 8 $/\$
96	94, 31, 95	syl2anc 661	. . . . . . 7
97	93, 96	mpbid 210	. . . . . 6
98	14	abscld 13041	. . . . . . 7
99		mod0 11833	. . . . . . 7 $/\$
100	98, 31, 99	syl2anc 661	. . . . . 6
101	97, 100	mpbid 210	. . . . 5
102	18, 101	eqeltrd 2542	. . . 4
103	94, 59, 17	redivcld 10271	. . . . 5
104		absz 12919	. . . . 5
105	103, 104	syl 16	. . . 4
106	102, 105	mpbird 232	. . 3
107		0lt1 9974	. . . . . . . 8
108		1re 9497	. . . . . . . . 9
109	47, 108	ltnlei 9607	. . . . . . . 8
110	107, 109	mpbi 208	. . . . . . 7
111	9, 4	mulcld 9518	. . . . . . . . . . . . . 14
112	2, 11	mulcld 9518	. . . . . . . . . . . . . 14
113	111, 112	subcld 9831	. . . . . . . . . . . . 13
114	113, 16, 17	divcld 10219	. . . . . . . . . . . 12
115	114	abscld 13041	. . . . . . . . . . 11
116	115	resqcld 12152	. . . . . . . . . 10
117	6	nnnn0d 10748	. . . . . . . . . . 11
118	117	nn0ge0d 10751	. . . . . . . . . 10
119	115	sqge0d 12153	. . . . . . . . . 10
120	25, 116, 118, 119	mulge0d 10028	. . . . . . . . 9
121	25, 116	remulcld 9526	. . . . . . . . . 10
122	48, 121	suble0d 10042	. . . . . . . . 9
123	120, 122	mpbird 232	. . . . . . . 8
124		breq1 4404	. . . . . . . 8
125	123, 124	syl5ibrcom 222	. . . . . . 7
126	110, 125	mtoi 178	. . . . . 6
127		absresq 12910	. . . . . . . . . . . 12
128	103, 127	syl 16	. . . . . . . . . . 11
129	14, 16, 17	sqdivd 12139	. . . . . . . . . . 11
130	14	sqvald 12123	. . . . . . . . . . . 12
131	130	oveq1d 6216	. . . . . . . . . . 11
132	128, 129, 131	3eqtrd 2499	. . . . . . . . . 10
133	26, 23	remulcld 9526	. . . . . . . . . . . . . . . 16
134	22, 27	remulcld 9526	. . . . . . . . . . . . . . . 16
135	133, 134	resubcld 9888	. . . . . . . . . . . . . . 15
136	135, 59, 17	redivcld 10271	. . . . . . . . . . . . . 14
137		absresq 12910	. . . . . . . . . . . . . 14
138	136, 137	syl 16	. . . . . . . . . . . . 13
139	113, 16, 17	sqdivd 12139	. . . . . . . . . . . . 13
140	138, 139	eqtrd 2495	. . . . . . . . . . . 12
141	140	oveq2d 6217	. . . . . . . . . . 11
142	113	sqcld 12124	. . . . . . . . . . . 12
143	16	sqcld 12124	. . . . . . . . . . . 12
144		sqne0 12050	. . . . . . . . . . . . . 14
145	16, 144	syl 16	. . . . . . . . . . . . 13
146	17, 145	mpbird 232	. . . . . . . . . . . 12
147	7, 142, 143, 146	divassd 10254	. . . . . . . . . . 11
148	113	sqvald 12123	. . . . . . . . . . . . 13
149	148	oveq2d 6217	. . . . . . . . . . . 12
150	149	oveq1d 6216	. . . . . . . . . . 11
151	141, 147, 150	3eqtr2d 2501	. . . . . . . . . 10
152	132, 151	oveq12d 6219	. . . . . . . . 9
153	14, 14	mulcld 9518	. . . . . . . . . 10
154	113, 113	mulcld 9518	. . . . . . . . . . 11
155	7, 154	mulcld 9518	. . . . . . . . . 10
156	153, 155, 143, 146	divsubdird 10258	. . . . . . . . 9
157	5, 13, 5, 13	mulsubd 9915	. . . . . . . . . . . 12
158	111, 112, 111, 112	mulsubd 9915	. . . . . . . . . . . . . 14
159	158	oveq2d 6217	. . . . . . . . . . . . 13
160	111, 111	mulcld 9518	. . . . . . . . . . . . . . 15
161	112, 112	mulcld 9518	. . . . . . . . . . . . . . 15
162	160, 161	addcld 9517	. . . . . . . . . . . . . 14
163	111, 112	mulcld 9518	. . . . . . . . . . . . . . 15
164	163, 163	addcld 9517	. . . . . . . . . . . . . 14
165	7, 162, 164	subdid 9912	. . . . . . . . . . . . 13
166	7, 160, 161	adddid 9522	. . . . . . . . . . . . . 14
167	7, 163, 163	adddid 9522	. . . . . . . . . . . . . 14
168	166, 167	oveq12d 6219	. . . . . . . . . . . . 13
169	159, 165, 168	3eqtrd 2499	. . . . . . . . . . . 12
170	157, 169	oveq12d 6219	. . . . . . . . . . 11
171	170	oveq1d 6216	. . . . . . . . . 10
172	5, 13	mulcomd 9519	. . . . . . . . . . . . . . . 16
173	7, 12, 5	mulassd 9521	. . . . . . . . . . . . . . . 16
174	2, 4	mulcomd 9519	. . . . . . . . . . . . . . . . . . 19
175	174	oveq2d 6217	. . . . . . . . . . . . . . . . . 18
176	9, 11, 4, 2	mul4d 9693	. . . . . . . . . . . . . . . . . 18
177	11, 2	mulcomd 9519	. . . . . . . . . . . . . . . . . . 19
178	177	oveq2d 6217	. . . . . . . . . . . . . . . . . 18
179	175, 176, 178	3eqtrd 2499	. . . . . . . . . . . . . . . . 17
180	179	oveq2d 6217	. . . . . . . . . . . . . . . 16
181	172, 173, 180	3eqtrd 2499	. . . . . . . . . . . . . . 15
182	181, 181	oveq12d 6219	. . . . . . . . . . . . . 14
183	182	oveq2d 6217	. . . . . . . . . . . . 13
184	183	oveq1d 6216	. . . . . . . . . . . 12
185	5, 5	mulcld 9518	. . . . . . . . . . . . . 14
186	13, 13	mulcld 9518	. . . . . . . . . . . . . 14
187	185, 186	addcld 9517	. . . . . . . . . . . . 13
188	7, 160	mulcld 9518	. . . . . . . . . . . . . 14
189	7, 161	mulcld 9518	. . . . . . . . . . . . . 14
190	188, 189	addcld 9517	. . . . . . . . . . . . 13
191	7, 163	mulcld 9518	. . . . . . . . . . . . . 14
192	191, 191	addcld 9517	. . . . . . . . . . . . 13
193	187, 190, 192	nnncan2d 9866	. . . . . . . . . . . 12
194	185, 186, 188, 189	addsub4d 9878	. . . . . . . . . . . . 13
195	5	sqvald 12123	. . . . . . . . . . . . . . 15
196	111	sqvald 12123	. . . . . . . . . . . . . . . 16
197	196	oveq2d 6217	. . . . . . . . . . . . . . 15
198	195, 197	oveq12d 6219	. . . . . . . . . . . . . 14
199	13	sqvald 12123	. . . . . . . . . . . . . . 15
200	112	sqvald 12123	. . . . . . . . . . . . . . . 16
201	200	oveq2d 6217	. . . . . . . . . . . . . . 15
202	199, 201	oveq12d 6219	. . . . . . . . . . . . . 14
203	198, 202	oveq12d 6219	. . . . . . . . . . . . 13
204	2, 4	sqmuld 12138	. . . . . . . . . . . . . . . 16
205	9, 4	sqmuld 12138	. . . . . . . . . . . . . . . . . 18
206	205	oveq2d 6217	. . . . . . . . . . . . . . . . 17
207	9	sqcld 12124	. . . . . . . . . . . . . . . . . 18
208	7, 207, 36	mulassd 9521	. . . . . . . . . . . . . . . . 17
209	206, 208	eqtr4d 2498	. . . . . . . . . . . . . . . 16
210	204, 209	oveq12d 6219	. . . . . . . . . . . . . . 15
211	7	sqvald 12123	. . . . . . . . . . . . . . . . . 18
212	9, 11	sqmuld 12138	. . . . . . . . . . . . . . . . . 18
213	211, 212	oveq12d 6219	. . . . . . . . . . . . . . . . 17
214	7, 12	sqmuld 12138	. . . . . . . . . . . . . . . . 17
215	7, 7	mulcld 9518	. . . . . . . . . . . . . . . . . 18
216	215, 207, 37	mulassd 9521	. . . . . . . . . . . . . . . . 17
217	213, 214, 216	3eqtr4d 2505	. . . . . . . . . . . . . . . 16
218	2, 11	sqmuld 12138	. . . . . . . . . . . . . . . . . 18
219	218	oveq2d 6217	. . . . . . . . . . . . . . . . 17
220	2	sqcld 12124	. . . . . . . . . . . . . . . . . 18
221	7, 220, 37	mulassd 9521	. . . . . . . . . . . . . . . . 17
222	219, 221	eqtr4d 2498	. . . . . . . . . . . . . . . 16
223	217, 222	oveq12d 6219	. . . . . . . . . . . . . . 15
224	210, 223	oveq12d 6219	. . . . . . . . . . . . . 14
225	7, 207	mulcld 9518	. . . . . . . . . . . . . . . . 17
226	220, 225, 36	subdird 9913	. . . . . . . . . . . . . . . 16
227		pellex.no1	. . . . . . . . . . . . . . . . 17
228	227	oveq1d 6216	. . . . . . . . . . . . . . . 16
229	226, 228	eqtr3d 2497	. . . . . . . . . . . . . . 15
230	7, 7, 207	mulassd 9521	. . . . . . . . . . . . . . . . . 18
231	230	oveq1d 6216	. . . . . . . . . . . . . . . . 17
232	231	oveq1d 6216	. . . . . . . . . . . . . . . 16
233	215, 207	mulcld 9518	. . . . . . . . . . . . . . . . 17
234	7, 220	mulcld 9518	. . . . . . . . . . . . . . . . 17
235	233, 234, 37	subdird 9913	. . . . . . . . . . . . . . . 16
236		subdi 9890	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	236	eqcomd 2462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
238	7, 225, 220, 237	syl3anc 1219	. . . . . . . . . . . . . . . . . 18
239		negsubdi2 9780	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
240	239	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . 21 $/\$
241	220, 225, 240	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
242	227	negeqd 9716	. . . . . . . . . . . . . . . . . . . 20
243	241, 242	eqtrd 2495	. . . . . . . . . . . . . . . . . . 19
244	243	oveq2d 6217	. . . . . . . . . . . . . . . . . 18
245	7, 16	mulneg2d 9910	. . . . . . . . . . . . . . . . . 18
246	238, 244, 245	3eqtrd 2499	. . . . . . . . . . . . . . . . 17
247	246	oveq1d 6216	. . . . . . . . . . . . . . . 16
248	232, 235, 247	3eqtr3d 2503	. . . . . . . . . . . . . . 15
249	229, 248	oveq12d 6219	. . . . . . . . . . . . . 14
250	7, 16	mulcld 9518	. . . . . . . . . . . . . . . . . 18
251	250, 37	mulneg1d 9909	. . . . . . . . . . . . . . . . 17
252	7, 16	mulcomd 9519	. . . . . . . . . . . . . . . . . . . 20
253	252	oveq1d 6216	. . . . . . . . . . . . . . . . . . 19
254	16, 7, 37	mulassd 9521	. . . . . . . . . . . . . . . . . . 19
255	253, 254	eqtrd 2495	. . . . . . . . . . . . . . . . . 18
256	255	negeqd 9716	. . . . . . . . . . . . . . . . 17
257	251, 256	eqtrd 2495	. . . . . . . . . . . . . . . 16
258	257	oveq2d 6217	. . . . . . . . . . . . . . 15
259	16, 36	mulcld 9518	. . . . . . . . . . . . . . . 16
260	16, 38	mulcld 9518	. . . . . . . . . . . . . . . 16
261	259, 260	negsubd 9837	. . . . . . . . . . . . . . 15
262	63	oveq2d 6217	. . . . . . . . . . . . . . . 16
263		subdi 9890	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
264	263	eqcomd 2462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
265	16, 36, 38, 264	syl3anc 1219	. . . . . . . . . . . . . . . 16
266	16	sqvald 12123	. . . . . . . . . . . . . . . 16
267	262, 265, 266	3eqtr4d 2505	. . . . . . . . . . . . . . 15
268	258, 261, 267	3eqtrd 2499	. . . . . . . . . . . . . 14
269	224, 249, 268	3eqtrd 2499	. . . . . . . . . . . . 13
270	194, 203, 269	3eqtr2d 2501	. . . . . . . . . . . 12
271	184, 193, 270	3eqtrd 2499	. . . . . . . . . . 11
272	271	oveq1d 6216	. . . . . . . . . 10
273	143, 146	dividd 10217	. . . . . . . . . 10
274	171, 272, 273	3eqtrd 2499	. . . . . . . . 9
275	152, 156, 274	3eqtr2d 2501	. . . . . . . 8
276	275	adantr 465	. . . . . . 7 $/\$
277		simpr 461	. . . . . . . . . . . 12 $/\$
278	277	oveq1d 6216	. . . . . . . . . . 11 $/\$
279	278	fveq2d 5804	. . . . . . . . . 10 $/\$
280	16, 17	div0d 10218	. . . . . . . . . . . 12
281	280	abs00bd 12899	. . . . . . . . . . 11
282	281	adantr 465	. . . . . . . . . 10 $/\$
283	279, 282	eqtrd 2495	. . . . . . . . 9 $/\$
284	283	sq0id 12077	. . . . . . . 8 $/\$
285	284	oveq1d 6216	. . . . . . 7 $/\$
286	276, 285	eqtr3d 2497	. . . . . 6 $/\$
287	126, 286	mtand 659	. . . . 5
288	287	neneqad 2656	. . . 4
289	14, 16, 288, 17	divne0d 10235	. . 3
290		nnabscl 12932	. . 3 $/\$
291	106, 289, 290	syl2anc 661	. 2
292	113, 16, 17	absdivd 13060	. . . . 5
293		negsub 9769	. . . . . . . . . . . 12 $/\$
294	293	eqcomd 2462	. . . . . . . . . . 11 $/\$
295	111, 112, 294	syl2anc 661	. . . . . . . . . 10
296	295	oveq1d 6216	. . . . . . . . 9
297	134	renegcld 9887	. . . . . . . . . 10
298	11, 4	mulcomd 9519	. . . . . . . . . . . 12
299	298	oveq1d 6216	. . . . . . . . . . 11
300		modmul1 11870	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
301	26, 27, 32, 31, 80, 300	syl221anc 1230	. . . . . . . . . . 11
302		modmul1 11870	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
303	22, 23, 78, 31, 33, 302	syl221anc 1230	. . . . . . . . . . 11
304	299, 301, 303	3eqtr4d 2505	. . . . . . . . . 10
305		modadd1 11863	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
306	133, 134, 297, 31, 304, 305	syl221anc 1230	. . . . . . . . 9
307	112	negidd 9821	. . . . . . . . . 10
308	307	oveq1d 6216	. . . . . . . . 9
309	296, 306, 308	3eqtrd 2499	. . . . . . . 8
310	309, 66	eqtrd 2495	. . . . . . 7
311		absmod0 12911	. . . . . . . 8 $/\$
312	135, 31, 311	syl2anc 661	. . . . . . 7
313	310, 312	mpbid 210	. . . . . 6
314	113	abscld 13041	. . . . . . 7
315		mod0 11833	. . . . . . 7 $/\$
316	314, 31, 315	syl2anc 661	. . . . . 6
317	313, 316	mpbid 210	. . . . 5
318	292, 317	eqeltrd 2542	. . . 4
319		absz 12919	. . . . 5
320	136, 319	syl 16	. . . 4
321	318, 320	mpbird 232	. . 3
322		pellex.neq	. . . . . . 7 $/\$
323	10	nnne0d 10478	. . . . . . . . 9
324	3	nnne0d 10478	. . . . . . . . 9
325	9, 11, 2, 4, 323, 324	divmuleqd 10265	. . . . . . . 8
326	63	adantr 465	. . . . . . . . . . . . . . 15 $/\$
327	326	eqcomd 2462	. . . . . . . . . . . . . 14 $/\$
328	327	oveq2d 6217	. . . . . . . . . . . . 13 $/\$
329	9, 11, 323	divcld 10219	. . . . . . . . . . . . . . . 16
330	329	sqcld 12124	. . . . . . . . . . . . . . 15
331	330	adantr 465	. . . . . . . . . . . . . 14 $/\$
332	36	adantr 465	. . . . . . . . . . . . . 14 $/\$
333	38	adantr 465	. . . . . . . . . . . . . 14 $/\$
334	331, 332, 333	subdid 9912	. . . . . . . . . . . . 13 $/\$
335		oveq1 6208	. . . . . . . . . . . . . . . . 17
336	335	oveq1d 6216	. . . . . . . . . . . . . . . 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 12139	. . . . . . . . . . . . . . . 16 $/\$
342	341	oveq1d 6216	. . . . . . . . . . . . . . 15 $/\$
343	220	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
344		sqne0 12050	. . . . . . . . . . . . . . . . . . 19
345	4, 344	syl 16	. . . . . . . . . . . . . . . . . 18
346	324, 345	mpbird 232	. . . . . . . . . . . . . . . . 17
347	346	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
348	343, 332, 347	divcan1d 10220	. . . . . . . . . . . . . . 15 $/\$
349	337, 342, 348	3eqtrd 2499	. . . . . . . . . . . . . 14 $/\$
350	7	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
351	37	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
352	331, 350, 351	mul12d 9690	. . . . . . . . . . . . . . 15 $/\$
353	9	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
354	11	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
355	323	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
356	353, 354, 355	sqdivd 12139	. . . . . . . . . . . . . . . . 17 $/\$
357	356	oveq1d 6216	. . . . . . . . . . . . . . . 16 $/\$
358	357	oveq2d 6217	. . . . . . . . . . . . . . 15 $/\$
359	207	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
360		sqne0 12050	. . . . . . . . . . . . . . . . . . . 20
361	11, 360	syl 16	. . . . . . . . . . . . . . . . . . 19
362	323, 361	mpbird 232	. . . . . . . . . . . . . . . . . 18
363	362	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
364	359, 351, 363	divcan1d 10220	. . . . . . . . . . . . . . . 16 $/\$