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 35095

Description: Lemma for pellex 35096. 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 10510	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10510	. . . . . . . 8
5	2, 4	mulcld 9564	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10510	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10510	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10510	. . . . . . . . 9
12	9, 11	mulcld 9564	. . . . . . . 8
13	7, 12	mulcld 9564	. . . . . . 7
14	5, 13	subcld 9885	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10927	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13340	. . . . 5
19	5, 13	negsubd 9891	. . . . . . . . . . 11
20	19	eqcomd 2408	. . . . . . . . . 10
21	20	oveq1d 6247	. . . . . . . . 9
22	1	nnred 10509	. . . . . . . . . . 11
23	3	nnred 10509	. . . . . . . . . . 11
24	22, 23	remulcld 9572	. . . . . . . . . 10
25	6	nnred 10509	. . . . . . . . . . 11
26	8	nnred 10509	. . . . . . . . . . . 12
27	10	nnred 10509	. . . . . . . . . . . 12
28	26, 27	remulcld 9572	. . . . . . . . . . 11
29	25, 28	remulcld 9572	. . . . . . . . . 10
30	29	renegcld 9945	. . . . . . . . . 10
31	16, 17	absrpcld 13333	. . . . . . . . . 10
32	3	nnzd 10925	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 11992	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1239	. . . . . . . . . . 11
36	4	sqcld 12260	. . . . . . . . . . . . . . 15
37	11	sqcld 12260	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9564	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9889	. . . . . . . . . . . . . 14
40	4	sqvald 12259	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2442	. . . . . . . . . . . . 13
42	41	oveq1d 6247	. . . . . . . . . . . 12
43	23	resqcld 12288	. . . . . . . . . . . . . 14
44	27	resqcld 12288	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9572	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9946	. . . . . . . . . . . . 13
47		0red 9545	. . . . . . . . . . . . 13
48	16	abscld 13321	. . . . . . . . . . . . . . . . . . 19
49	48	recnd 9570	. . . . . . . . . . . . . . . . . 18
50	16, 17	absne0d 13332	. . . . . . . . . . . . . . . . . 18
51	49, 50	dividd 10277	. . . . . . . . . . . . . . . . 17
52		1zzd 10854	. . . . . . . . . . . . . . . . 17
53	51, 52	eqeltrd 2488	. . . . . . . . . . . . . . . 16
54		mod0 11952	. . . . . . . . . . . . . . . . 17 $/\$
55	48, 31, 54	syl2anc 659	. . . . . . . . . . . . . . . 16
56	53, 55	mpbird 232	. . . . . . . . . . . . . . 15
57	15	zred 10926	. . . . . . . . . . . . . . . 16
58		absmod0 13190	. . . . . . . . . . . . . . . 16 $/\$
59	57, 31, 58	syl2anc 659	. . . . . . . . . . . . . . 15
60	56, 59	mpbird 232	. . . . . . . . . . . . . 14
61		pellex.no2	. . . . . . . . . . . . . . 15
62	61	oveq1d 6247	. . . . . . . . . . . . . 14
63		0mod 11977	. . . . . . . . . . . . . . 15
64	31, 63	syl 17	. . . . . . . . . . . . . 14
65	60, 62, 64	3eqtr4d 2451	. . . . . . . . . . . . 13
66		modadd1 11983	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	46, 47, 45, 31, 65, 66	syl221anc 1239	. . . . . . . . . . . 12
68	38	addid2d 9733	. . . . . . . . . . . . . 14
69	11	sqvald 12259	. . . . . . . . . . . . . . 15
70	69	oveq2d 6248	. . . . . . . . . . . . . 14
71	7, 11, 11	mul12d 9741	. . . . . . . . . . . . . 14
72	68, 70, 71	3eqtrd 2445	. . . . . . . . . . . . 13
73	72	oveq1d 6247	. . . . . . . . . . . 12
74	42, 67, 73	3eqtrd 2445	. . . . . . . . . . 11
75	6	nnzd 10925	. . . . . . . . . . . . . 14
76	10	nnzd 10925	. . . . . . . . . . . . . 14
77	75, 76	zmulcld 10932	. . . . . . . . . . . . 13
78		pellex.ycg	. . . . . . . . . . . . . 14
79	78	eqcomd 2408	. . . . . . . . . . . . 13
80		modmul1 11992	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
81	27, 26, 77, 31, 79, 80	syl221anc 1239	. . . . . . . . . . . 12
82	9, 7, 11	mul12d 9741	. . . . . . . . . . . . 13
83	82	oveq1d 6247	. . . . . . . . . . . 12
84	81, 83	eqtrd 2441	. . . . . . . . . . 11
85	35, 74, 84	3eqtrd 2445	. . . . . . . . . 10
86		modadd1 11983	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
87	24, 29, 30, 31, 85, 86	syl221anc 1239	. . . . . . . . 9
88	13	negidd 9875	. . . . . . . . . 10
89	88	oveq1d 6247	. . . . . . . . 9
90	21, 87, 89	3eqtrd 2445	. . . . . . . 8
91	90, 64	eqtrd 2441	. . . . . . 7
92	24, 29	resubcld 9946	. . . . . . . 8
93		absmod0 13190	. . . . . . . 8 $/\$
94	92, 31, 93	syl2anc 659	. . . . . . 7
95	91, 94	mpbid 210	. . . . . 6
96	14	abscld 13321	. . . . . . 7
97		mod0 11952	. . . . . . 7 $/\$
98	96, 31, 97	syl2anc 659	. . . . . 6
99	95, 98	mpbid 210	. . . . 5
100	18, 99	eqeltrd 2488	. . . 4
101	92, 57, 17	redivcld 10331	. . . . 5
102		absz 13198	. . . . 5
103	101, 102	syl 17	. . . 4
104	100, 103	mpbird 232	. . 3
105		0lt1 10033	. . . . . . . 8
106		0re 9544	. . . . . . . . 9
107		1re 9543	. . . . . . . . 9
108	106, 107	ltnlei 9655	. . . . . . . 8
109	105, 108	mpbi 208	. . . . . . 7
110	9, 4	mulcld 9564	. . . . . . . . . . . . . 14
111	2, 11	mulcld 9564	. . . . . . . . . . . . . 14
112	110, 111	subcld 9885	. . . . . . . . . . . . 13
113	112, 16, 17	divcld 10279	. . . . . . . . . . . 12
114	113	abscld 13321	. . . . . . . . . . 11
115	114	resqcld 12288	. . . . . . . . . 10
116	6	nnnn0d 10811	. . . . . . . . . . 11
117	116	nn0ge0d 10814	. . . . . . . . . 10
118	114	sqge0d 12289	. . . . . . . . . 10
119	25, 115, 117, 118	mulge0d 10087	. . . . . . . . 9
120	25, 115	remulcld 9572	. . . . . . . . . 10
121	47, 120	suble0d 10101	. . . . . . . . 9
122	119, 121	mpbird 232	. . . . . . . 8
123		breq1 4395	. . . . . . . 8
124	122, 123	syl5ibrcom 222	. . . . . . 7
125	109, 124	mtoi 178	. . . . . 6
126		absresq 13189	. . . . . . . . . . . 12
127	101, 126	syl 17	. . . . . . . . . . 11
128	14, 16, 17	sqdivd 12275	. . . . . . . . . . 11
129	14	sqvald 12259	. . . . . . . . . . . 12
130	129	oveq1d 6247	. . . . . . . . . . 11
131	127, 128, 130	3eqtrd 2445	. . . . . . . . . 10
132	26, 23	remulcld 9572	. . . . . . . . . . . . . . . 16
133	22, 27	remulcld 9572	. . . . . . . . . . . . . . . 16
134	132, 133	resubcld 9946	. . . . . . . . . . . . . . 15
135	134, 57, 17	redivcld 10331	. . . . . . . . . . . . . 14
136		absresq 13189	. . . . . . . . . . . . . 14
137	135, 136	syl 17	. . . . . . . . . . . . 13
138	112, 16, 17	sqdivd 12275	. . . . . . . . . . . . 13
139	137, 138	eqtrd 2441	. . . . . . . . . . . 12
140	139	oveq2d 6248	. . . . . . . . . . 11
141	112	sqcld 12260	. . . . . . . . . . . 12
142	16	sqcld 12260	. . . . . . . . . . . 12
143		sqne0 12187	. . . . . . . . . . . . . 14
144	16, 143	syl 17	. . . . . . . . . . . . 13
145	17, 144	mpbird 232	. . . . . . . . . . . 12
146	7, 141, 142, 145	divassd 10314	. . . . . . . . . . 11
147	112	sqvald 12259	. . . . . . . . . . . . 13
148	147	oveq2d 6248	. . . . . . . . . . . 12
149	148	oveq1d 6247	. . . . . . . . . . 11
150	140, 146, 149	3eqtr2d 2447	. . . . . . . . . 10
151	131, 150	oveq12d 6250	. . . . . . . . 9
152	14, 14	mulcld 9564	. . . . . . . . . 10
153	112, 112	mulcld 9564	. . . . . . . . . . 11
154	7, 153	mulcld 9564	. . . . . . . . . 10
155	152, 154, 142, 145	divsubdird 10318	. . . . . . . . 9
156	5, 13, 5, 13	mulsubd 9974	. . . . . . . . . . . 12
157	110, 111, 110, 111	mulsubd 9974	. . . . . . . . . . . . . 14
158	157	oveq2d 6248	. . . . . . . . . . . . 13
159	110, 110	mulcld 9564	. . . . . . . . . . . . . . 15
160	111, 111	mulcld 9564	. . . . . . . . . . . . . . 15
161	159, 160	addcld 9563	. . . . . . . . . . . . . 14
162	110, 111	mulcld 9564	. . . . . . . . . . . . . . 15
163	162, 162	addcld 9563	. . . . . . . . . . . . . 14
164	7, 161, 163	subdid 9971	. . . . . . . . . . . . 13
165	7, 159, 160	adddid 9568	. . . . . . . . . . . . . 14
166	7, 162, 162	adddid 9568	. . . . . . . . . . . . . 14
167	165, 166	oveq12d 6250	. . . . . . . . . . . . 13
168	158, 164, 167	3eqtrd 2445	. . . . . . . . . . . 12
169	156, 168	oveq12d 6250	. . . . . . . . . . 11
170	169	oveq1d 6247	. . . . . . . . . 10
171	5, 13	mulcomd 9565	. . . . . . . . . . . . . . . 16
172	7, 12, 5	mulassd 9567	. . . . . . . . . . . . . . . 16
173	2, 4	mulcomd 9565	. . . . . . . . . . . . . . . . . . 19
174	173	oveq2d 6248	. . . . . . . . . . . . . . . . . 18
175	9, 11, 4, 2	mul4d 9744	. . . . . . . . . . . . . . . . . 18
176	11, 2	mulcomd 9565	. . . . . . . . . . . . . . . . . . 19
177	176	oveq2d 6248	. . . . . . . . . . . . . . . . . 18
178	174, 175, 177	3eqtrd 2445	. . . . . . . . . . . . . . . . 17
179	178	oveq2d 6248	. . . . . . . . . . . . . . . 16
180	171, 172, 179	3eqtrd 2445	. . . . . . . . . . . . . . 15
181	180, 180	oveq12d 6250	. . . . . . . . . . . . . 14
182	181	oveq2d 6248	. . . . . . . . . . . . 13
183	182	oveq1d 6247	. . . . . . . . . . . 12
184	5, 5	mulcld 9564	. . . . . . . . . . . . . 14
185	13, 13	mulcld 9564	. . . . . . . . . . . . . 14
186	184, 185	addcld 9563	. . . . . . . . . . . . 13
187	7, 159	mulcld 9564	. . . . . . . . . . . . . 14
188	7, 160	mulcld 9564	. . . . . . . . . . . . . 14
189	187, 188	addcld 9563	. . . . . . . . . . . . 13
190	7, 162	mulcld 9564	. . . . . . . . . . . . . 14
191	190, 190	addcld 9563	. . . . . . . . . . . . 13
192	186, 189, 191	nnncan2d 9920	. . . . . . . . . . . 12
193	184, 185, 187, 188	addsub4d 9932	. . . . . . . . . . . . 13
194	5	sqvald 12259	. . . . . . . . . . . . . . 15
195	110	sqvald 12259	. . . . . . . . . . . . . . . 16
196	195	oveq2d 6248	. . . . . . . . . . . . . . 15
197	194, 196	oveq12d 6250	. . . . . . . . . . . . . 14
198	13	sqvald 12259	. . . . . . . . . . . . . . 15
199	111	sqvald 12259	. . . . . . . . . . . . . . . 16
200	199	oveq2d 6248	. . . . . . . . . . . . . . 15
201	198, 200	oveq12d 6250	. . . . . . . . . . . . . 14
202	197, 201	oveq12d 6250	. . . . . . . . . . . . 13
203	2, 4	sqmuld 12274	. . . . . . . . . . . . . . . 16
204	9, 4	sqmuld 12274	. . . . . . . . . . . . . . . . . 18
205	204	oveq2d 6248	. . . . . . . . . . . . . . . . 17
206	9	sqcld 12260	. . . . . . . . . . . . . . . . . 18
207	7, 206, 36	mulassd 9567	. . . . . . . . . . . . . . . . 17
208	205, 207	eqtr4d 2444	. . . . . . . . . . . . . . . 16
209	203, 208	oveq12d 6250	. . . . . . . . . . . . . . 15
210	7	sqvald 12259	. . . . . . . . . . . . . . . . . 18
211	9, 11	sqmuld 12274	. . . . . . . . . . . . . . . . . 18
212	210, 211	oveq12d 6250	. . . . . . . . . . . . . . . . 17
213	7, 12	sqmuld 12274	. . . . . . . . . . . . . . . . 17
214	7, 7	mulcld 9564	. . . . . . . . . . . . . . . . . 18
215	214, 206, 37	mulassd 9567	. . . . . . . . . . . . . . . . 17
216	212, 213, 215	3eqtr4d 2451	. . . . . . . . . . . . . . . 16
217	2, 11	sqmuld 12274	. . . . . . . . . . . . . . . . . 18
218	217	oveq2d 6248	. . . . . . . . . . . . . . . . 17
219	2	sqcld 12260	. . . . . . . . . . . . . . . . . 18
220	7, 219, 37	mulassd 9567	. . . . . . . . . . . . . . . . 17
221	218, 220	eqtr4d 2444	. . . . . . . . . . . . . . . 16
222	216, 221	oveq12d 6250	. . . . . . . . . . . . . . 15
223	209, 222	oveq12d 6250	. . . . . . . . . . . . . 14
224	7, 206	mulcld 9564	. . . . . . . . . . . . . . . . 17
225	219, 224, 36	subdird 9972	. . . . . . . . . . . . . . . 16
226		pellex.no1	. . . . . . . . . . . . . . . . 17
227	226	oveq1d 6247	. . . . . . . . . . . . . . . 16
228	225, 227	eqtr3d 2443	. . . . . . . . . . . . . . 15
229	7, 7, 206	mulassd 9567	. . . . . . . . . . . . . . . . . 18
230	229	oveq1d 6247	. . . . . . . . . . . . . . . . 17
231	230	oveq1d 6247	. . . . . . . . . . . . . . . 16
232	214, 206	mulcld 9564	. . . . . . . . . . . . . . . . 17
233	7, 219	mulcld 9564	. . . . . . . . . . . . . . . . 17
234	232, 233, 37	subdird 9972	. . . . . . . . . . . . . . . 16
235		subdi 9949	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
236	235	eqcomd 2408	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
237	7, 224, 219, 236	syl3anc 1228	. . . . . . . . . . . . . . . . . 18
238		negsubdi2 9832	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
239	238	eqcomd 2408	. . . . . . . . . . . . . . . . . . . . 21 $/\$
240	219, 224, 239	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20
241	226	negeqd 9768	. . . . . . . . . . . . . . . . . . . 20
242	240, 241	eqtrd 2441	. . . . . . . . . . . . . . . . . . 19
243	242	oveq2d 6248	. . . . . . . . . . . . . . . . . 18
244	7, 16	mulneg2d 9969	. . . . . . . . . . . . . . . . . 18
245	237, 243, 244	3eqtrd 2445	. . . . . . . . . . . . . . . . 17
246	245	oveq1d 6247	. . . . . . . . . . . . . . . 16
247	231, 234, 246	3eqtr3d 2449	. . . . . . . . . . . . . . 15
248	228, 247	oveq12d 6250	. . . . . . . . . . . . . 14
249	7, 16	mulcld 9564	. . . . . . . . . . . . . . . . . 18
250	249, 37	mulneg1d 9968	. . . . . . . . . . . . . . . . 17
251	7, 16	mulcomd 9565	. . . . . . . . . . . . . . . . . . . 20
252	251	oveq1d 6247	. . . . . . . . . . . . . . . . . . 19
253	16, 7, 37	mulassd 9567	. . . . . . . . . . . . . . . . . . 19
254	252, 253	eqtrd 2441	. . . . . . . . . . . . . . . . . 18
255	254	negeqd 9768	. . . . . . . . . . . . . . . . 17
256	250, 255	eqtrd 2441	. . . . . . . . . . . . . . . 16
257	256	oveq2d 6248	. . . . . . . . . . . . . . 15
258	16, 36	mulcld 9564	. . . . . . . . . . . . . . . 16
259	16, 38	mulcld 9564	. . . . . . . . . . . . . . . 16
260	258, 259	negsubd 9891	. . . . . . . . . . . . . . 15
261	61	oveq2d 6248	. . . . . . . . . . . . . . . 16
262		subdi 9949	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
263	262	eqcomd 2408	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
264	16, 36, 38, 263	syl3anc 1228	. . . . . . . . . . . . . . . 16
265	16	sqvald 12259	. . . . . . . . . . . . . . . 16
266	261, 264, 265	3eqtr4d 2451	. . . . . . . . . . . . . . 15
267	257, 260, 266	3eqtrd 2445	. . . . . . . . . . . . . 14
268	223, 248, 267	3eqtrd 2445	. . . . . . . . . . . . 13
269	193, 202, 268	3eqtr2d 2447	. . . . . . . . . . . 12
270	183, 192, 269	3eqtrd 2445	. . . . . . . . . . 11
271	270	oveq1d 6247	. . . . . . . . . 10
272	142, 145	dividd 10277	. . . . . . . . . 10
273	170, 271, 272	3eqtrd 2445	. . . . . . . . 9
274	151, 155, 273	3eqtr2d 2447	. . . . . . . 8
275	274	adantr 463	. . . . . . 7 $/\$
276		simpr 459	. . . . . . . . . . . 12 $/\$
277	276	oveq1d 6247	. . . . . . . . . . 11 $/\$
278	277	fveq2d 5807	. . . . . . . . . 10 $/\$
279	16, 17	div0d 10278	. . . . . . . . . . . 12
280	279	abs00bd 13178	. . . . . . . . . . 11
281	280	adantr 463	. . . . . . . . . 10 $/\$
282	278, 281	eqtrd 2441	. . . . . . . . 9 $/\$
283	282	sq0id 12214	. . . . . . . 8 $/\$
284	283	oveq1d 6247	. . . . . . 7 $/\$
285	275, 284	eqtr3d 2443	. . . . . 6 $/\$
286	125, 285	mtand 657	. . . . 5
287	286	neqned 2604	. . . 4
288	14, 16, 287, 17	divne0d 10295	. . 3
289		nnabscl 13212	. . 3 $/\$
290	104, 288, 289	syl2anc 659	. 2
291	112, 16, 17	absdivd 13340	. . . . 5
292		negsub 9821	. . . . . . . . . . . 12 $/\$
293	292	eqcomd 2408	. . . . . . . . . . 11 $/\$
294	110, 111, 293	syl2anc 659	. . . . . . . . . 10
295	294	oveq1d 6247	. . . . . . . . 9
296	133	renegcld 9945	. . . . . . . . . 10
297	11, 4	mulcomd 9565	. . . . . . . . . . . 12
298	297	oveq1d 6247	. . . . . . . . . . 11
299		modmul1 11992	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
300	26, 27, 32, 31, 78, 299	syl221anc 1239	. . . . . . . . . . 11
301		modmul1 11992	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
302	22, 23, 76, 31, 33, 301	syl221anc 1239	. . . . . . . . . . 11
303	298, 300, 302	3eqtr4d 2451	. . . . . . . . . 10
304		modadd1 11983	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
305	132, 133, 296, 31, 303, 304	syl221anc 1239	. . . . . . . . 9
306	111	negidd 9875	. . . . . . . . . 10
307	306	oveq1d 6247	. . . . . . . . 9
308	295, 305, 307	3eqtrd 2445	. . . . . . . 8
309	308, 64	eqtrd 2441	. . . . . . 7
310		absmod0 13190	. . . . . . . 8 $/\$
311	134, 31, 310	syl2anc 659	. . . . . . 7
312	309, 311	mpbid 210	. . . . . 6
313	112	abscld 13321	. . . . . . 7
314		mod0 11952	. . . . . . 7 $/\$
315	313, 31, 314	syl2anc 659	. . . . . 6
316	312, 315	mpbid 210	. . . . 5
317	291, 316	eqeltrd 2488	. . . 4
318		absz 13198	. . . . 5
319	135, 318	syl 17	. . . 4
320	317, 319	mpbird 232	. . 3
321		pellex.neq	. . . . . . 7 $/\$
322	10	nnne0d 10539	. . . . . . . . 9
323	3	nnne0d 10539	. . . . . . . . 9
324	9, 11, 2, 4, 322, 323	divmuleqd 10325	. . . . . . . 8
325	61	adantr 463	. . . . . . . . . . . . . . 15 $/\$
326	325	eqcomd 2408	. . . . . . . . . . . . . 14 $/\$
327	326	oveq2d 6248	. . . . . . . . . . . . 13 $/\$
328	9, 11, 322	divcld 10279	. . . . . . . . . . . . . . . 16
329	328	sqcld 12260	. . . . . . . . . . . . . . 15
330	329	adantr 463	. . . . . . . . . . . . . 14 $/\$
331	36	adantr 463	. . . . . . . . . . . . . 14 $/\$
332	38	adantr 463	. . . . . . . . . . . . . 14 $/\$
333	330, 331, 332	subdid 9971	. . . . . . . . . . . . 13 $/\$
334		oveq1 6239	. . . . . . . . . . . . . . . . 17
335	334	oveq1d 6247	. . . . . . . . . . . . . . . 16
336	335	adantl 464	. . . . . . . . . . . . . . 15 $/\$
337	2	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
338	4	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
339	323	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
340	337, 338, 339	sqdivd 12275	. . . . . . . . . . . . . . . 16 $/\$
341	340	oveq1d 6247	. . . . . . . . . . . . . . 15 $/\$
342	219	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
343		sqne0 12187	. . . . . . . . . . . . . . . . . . 19
344	4, 343	syl 17	. . . . . . . . . . . . . . . . . 18
345	323, 344	mpbird 232	. . . . . . . . . . . . . . . . 17
346	345	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
347	342, 331, 346	divcan1d 10280	. . . . . . . . . . . . . . 15 $/\$
348	336, 341, 347	3eqtrd 2445	. . . . . . . . . . . . . 14 $/\$
349	7	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
350	37	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
351	330, 349, 350	mul12d 9741	. . . . . . . . . . . . . . 15 $/\$
352	9	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
353	11	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
354	322	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$
355	352, 353, 354	sqdivd 12275	. . . . . . . . . . . . . . . . 17 $/\$
356	355	oveq1d 6247	. . . . . . . . . . . . . . . 16 $/\$
357	356	oveq2d 6248	. . . . . . . . . . . . . . 15 $/\$
358	206	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
359		sqne0 12187	. . . . . . . . . . . . . . . . . . . 20
360	11, 359	syl 17	. . . . . . . . . . . . . . . . . . 19
361	322, 360	mpbird 232	. . . . . . . . . . . . . . . . . 18
362	361	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$
363	358, 350, 362	divcan1d 10280	. . . . . . . . . . . . . . . 16 $/\$