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 Visualization version Unicode version

Theorem pellexlem6 35749

Description: Lemma for pellex 35750. 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 10647	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 10647	. . . . . . . 8
5	2, 4	mulcld 9681	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 10647	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 10647	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 10647	. . . . . . . . 9
12	9, 11	mulcld 9681	. . . . . . . 8
13	7, 12	mulcld 9681	. . . . . . 7
14	5, 13	subcld 10005	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 11064	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 13594	. . . . 5
19	5, 13	negsubd 10011	. . . . . . . . . . 11
20	19	eqcomd 2477	. . . . . . . . . 10
21	20	oveq1d 6323	. . . . . . . . 9
22	1	nnred 10646	. . . . . . . . . . 11
23	3	nnred 10646	. . . . . . . . . . 11
24	22, 23	remulcld 9689	. . . . . . . . . 10
25	6	nnred 10646	. . . . . . . . . . 11
26	8	nnred 10646	. . . . . . . . . . . 12
27	10	nnred 10646	. . . . . . . . . . . 12
28	26, 27	remulcld 9689	. . . . . . . . . . 11
29	25, 28	remulcld 9689	. . . . . . . . . 10
30	29	renegcld 10067	. . . . . . . . . 10
31	16, 17	absrpcld 13587	. . . . . . . . . 10
32	3	nnzd 11062	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 12177	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1303	. . . . . . . . . . 11
36	4	sqcld 12452	. . . . . . . . . . . . . . 15
37	11	sqcld 12452	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9681	. . . . . . . . . . . . . . 15
39	36, 38	npcand 10009	. . . . . . . . . . . . . 14
40	4	sqvald 12451	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2506	. . . . . . . . . . . . 13
42	41	oveq1d 6323	. . . . . . . . . . . 12
43	23	resqcld 12480	. . . . . . . . . . . . . 14
44	27	resqcld 12480	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9689	. . . . . . . . . . . . . 14
46	43, 45	resubcld 10068	. . . . . . . . . . . . 13
47		0red 9662	. . . . . . . . . . . . 13
48	16	abscld 13575	. . . . . . . . . . . . . . . . . . 19
49	48	recnd 9687	. . . . . . . . . . . . . . . . . 18
50	16, 17	absne0d 13586	. . . . . . . . . . . . . . . . . 18
51	49, 50	dividd 10403	. . . . . . . . . . . . . . . . 17
52		1zzd 10992	. . . . . . . . . . . . . . . . 17
53	51, 52	eqeltrd 2549	. . . . . . . . . . . . . . . 16
54		mod0 12136	. . . . . . . . . . . . . . . . 17 $/\$
55	48, 31, 54	syl2anc 673	. . . . . . . . . . . . . . . 16
56	53, 55	mpbird 240	. . . . . . . . . . . . . . 15
57	15	zred 11063	. . . . . . . . . . . . . . . 16
58		absmod0 13443	. . . . . . . . . . . . . . . 16 $/\$
59	57, 31, 58	syl2anc 673	. . . . . . . . . . . . . . 15
60	56, 59	mpbird 240	. . . . . . . . . . . . . 14
61		pellex.no2	. . . . . . . . . . . . . . 15
62	61	oveq1d 6323	. . . . . . . . . . . . . 14
63		0mod 12161	. . . . . . . . . . . . . . 15
64	31, 63	syl 17	. . . . . . . . . . . . . 14
65	60, 62, 64	3eqtr4d 2515	. . . . . . . . . . . . 13
66		modadd1 12167	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	46, 47, 45, 31, 65, 66	syl221anc 1303	. . . . . . . . . . . 12
68	38	addid2d 9852	. . . . . . . . . . . . . 14
69	11	sqvald 12451	. . . . . . . . . . . . . . 15
70	69	oveq2d 6324	. . . . . . . . . . . . . 14
71	7, 11, 11	mul12d 9860	. . . . . . . . . . . . . 14
72	68, 70, 71	3eqtrd 2509	. . . . . . . . . . . . 13
73	72	oveq1d 6323	. . . . . . . . . . . 12
74	42, 67, 73	3eqtrd 2509	. . . . . . . . . . 11
75	6	nnzd 11062	. . . . . . . . . . . . . 14
76	10	nnzd 11062	. . . . . . . . . . . . . 14
77	75, 76	zmulcld 11069	. . . . . . . . . . . . 13
78		pellex.ycg	. . . . . . . . . . . . . 14
79	78	eqcomd 2477	. . . . . . . . . . . . 13
80		modmul1 12177	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
81	27, 26, 77, 31, 79, 80	syl221anc 1303	. . . . . . . . . . . 12
82	9, 7, 11	mul12d 9860	. . . . . . . . . . . . 13
83	82	oveq1d 6323	. . . . . . . . . . . 12
84	81, 83	eqtrd 2505	. . . . . . . . . . 11
85	35, 74, 84	3eqtrd 2509	. . . . . . . . . 10
86		modadd1 12167	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
87	24, 29, 30, 31, 85, 86	syl221anc 1303	. . . . . . . . 9
88	13	negidd 9995	. . . . . . . . . 10
89	88	oveq1d 6323	. . . . . . . . 9
90	21, 87, 89	3eqtrd 2509	. . . . . . . 8
91	90, 64	eqtrd 2505	. . . . . . 7
92	24, 29	resubcld 10068	. . . . . . . 8
93		absmod0 13443	. . . . . . . 8 $/\$
94	92, 31, 93	syl2anc 673	. . . . . . 7
95	91, 94	mpbid 215	. . . . . 6
96	14	abscld 13575	. . . . . . 7
97		mod0 12136	. . . . . . 7 $/\$
98	96, 31, 97	syl2anc 673	. . . . . 6
99	95, 98	mpbid 215	. . . . 5
100	18, 99	eqeltrd 2549	. . . 4
101	92, 57, 17	redivcld 10457	. . . . 5
102		absz 13451	. . . . 5
103	101, 102	syl 17	. . . 4
104	100, 103	mpbird 240	. . 3
105		0lt1 10157	. . . . . . . 8
106		0re 9661	. . . . . . . . 9
107		1re 9660	. . . . . . . . 9
108	106, 107	ltnlei 9773	. . . . . . . 8
109	105, 108	mpbi 213	. . . . . . 7
110	9, 4	mulcld 9681	. . . . . . . . . . . . . 14
111	2, 11	mulcld 9681	. . . . . . . . . . . . . 14
112	110, 111	subcld 10005	. . . . . . . . . . . . 13
113	112, 16, 17	divcld 10405	. . . . . . . . . . . 12
114	113	abscld 13575	. . . . . . . . . . 11
115	114	resqcld 12480	. . . . . . . . . 10
116	6	nnnn0d 10949	. . . . . . . . . . 11
117	116	nn0ge0d 10952	. . . . . . . . . 10
118	114	sqge0d 12481	. . . . . . . . . 10
119	25, 115, 117, 118	mulge0d 10211	. . . . . . . . 9
120	25, 115	remulcld 9689	. . . . . . . . . 10
121	47, 120	suble0d 10225	. . . . . . . . 9
122	119, 121	mpbird 240	. . . . . . . 8
123		breq1 4398	. . . . . . . 8
124	122, 123	syl5ibrcom 230	. . . . . . 7
125	109, 124	mtoi 183	. . . . . 6
126		absresq 13442	. . . . . . . . . . . 12
127	101, 126	syl 17	. . . . . . . . . . 11
128	14, 16, 17	sqdivd 12467	. . . . . . . . . . 11
129	14	sqvald 12451	. . . . . . . . . . . 12
130	129	oveq1d 6323	. . . . . . . . . . 11
131	127, 128, 130	3eqtrd 2509	. . . . . . . . . 10
132	26, 23	remulcld 9689	. . . . . . . . . . . . . . . 16
133	22, 27	remulcld 9689	. . . . . . . . . . . . . . . 16
134	132, 133	resubcld 10068	. . . . . . . . . . . . . . 15
135	134, 57, 17	redivcld 10457	. . . . . . . . . . . . . 14
136		absresq 13442	. . . . . . . . . . . . . 14
137	135, 136	syl 17	. . . . . . . . . . . . 13
138	112, 16, 17	sqdivd 12467	. . . . . . . . . . . . 13
139	137, 138	eqtrd 2505	. . . . . . . . . . . 12
140	139	oveq2d 6324	. . . . . . . . . . 11
141	112	sqcld 12452	. . . . . . . . . . . 12
142	16	sqcld 12452	. . . . . . . . . . . 12
143		sqne0 12379	. . . . . . . . . . . . . 14
144	16, 143	syl 17	. . . . . . . . . . . . 13
145	17, 144	mpbird 240	. . . . . . . . . . . 12
146	7, 141, 142, 145	divassd 10440	. . . . . . . . . . 11
147	112	sqvald 12451	. . . . . . . . . . . . 13
148	147	oveq2d 6324	. . . . . . . . . . . 12
149	148	oveq1d 6323	. . . . . . . . . . 11
150	140, 146, 149	3eqtr2d 2511	. . . . . . . . . 10
151	131, 150	oveq12d 6326	. . . . . . . . 9
152	14, 14	mulcld 9681	. . . . . . . . . 10
153	112, 112	mulcld 9681	. . . . . . . . . . 11
154	7, 153	mulcld 9681	. . . . . . . . . 10
155	152, 154, 142, 145	divsubdird 10444	. . . . . . . . 9
156	5, 13, 5, 13	mulsubd 10098	. . . . . . . . . . . 12
157	110, 111, 110, 111	mulsubd 10098	. . . . . . . . . . . . . 14
158	157	oveq2d 6324	. . . . . . . . . . . . 13
159	110, 110	mulcld 9681	. . . . . . . . . . . . . . 15
160	111, 111	mulcld 9681	. . . . . . . . . . . . . . 15
161	159, 160	addcld 9680	. . . . . . . . . . . . . 14
162	110, 111	mulcld 9681	. . . . . . . . . . . . . . 15
163	162, 162	addcld 9680	. . . . . . . . . . . . . 14
164	7, 161, 163	subdid 10095	. . . . . . . . . . . . 13
165	7, 159, 160	adddid 9685	. . . . . . . . . . . . . 14
166	7, 162, 162	adddid 9685	. . . . . . . . . . . . . 14
167	165, 166	oveq12d 6326	. . . . . . . . . . . . 13
168	158, 164, 167	3eqtrd 2509	. . . . . . . . . . . 12
169	156, 168	oveq12d 6326	. . . . . . . . . . 11
170	169	oveq1d 6323	. . . . . . . . . 10
171	5, 13	mulcomd 9682	. . . . . . . . . . . . . . . 16
172	7, 12, 5	mulassd 9684	. . . . . . . . . . . . . . . 16
173	2, 4	mulcomd 9682	. . . . . . . . . . . . . . . . . . 19
174	173	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
175	9, 11, 4, 2	mul4d 9863	. . . . . . . . . . . . . . . . . 18
176	11, 2	mulcomd 9682	. . . . . . . . . . . . . . . . . . 19
177	176	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
178	174, 175, 177	3eqtrd 2509	. . . . . . . . . . . . . . . . 17
179	178	oveq2d 6324	. . . . . . . . . . . . . . . 16
180	171, 172, 179	3eqtrd 2509	. . . . . . . . . . . . . . 15
181	180, 180	oveq12d 6326	. . . . . . . . . . . . . 14
182	181	oveq2d 6324	. . . . . . . . . . . . 13
183	182	oveq1d 6323	. . . . . . . . . . . 12
184	5, 5	mulcld 9681	. . . . . . . . . . . . . 14
185	13, 13	mulcld 9681	. . . . . . . . . . . . . 14
186	184, 185	addcld 9680	. . . . . . . . . . . . 13
187	7, 159	mulcld 9681	. . . . . . . . . . . . . 14
188	7, 160	mulcld 9681	. . . . . . . . . . . . . 14
189	187, 188	addcld 9680	. . . . . . . . . . . . 13
190	7, 162	mulcld 9681	. . . . . . . . . . . . . 14
191	190, 190	addcld 9680	. . . . . . . . . . . . 13
192	186, 189, 191	nnncan2d 10040	. . . . . . . . . . . 12
193	184, 185, 187, 188	addsub4d 10052	. . . . . . . . . . . . 13
194	5	sqvald 12451	. . . . . . . . . . . . . . 15
195	110	sqvald 12451	. . . . . . . . . . . . . . . 16
196	195	oveq2d 6324	. . . . . . . . . . . . . . 15
197	194, 196	oveq12d 6326	. . . . . . . . . . . . . 14
198	13	sqvald 12451	. . . . . . . . . . . . . . 15
199	111	sqvald 12451	. . . . . . . . . . . . . . . 16
200	199	oveq2d 6324	. . . . . . . . . . . . . . 15
201	198, 200	oveq12d 6326	. . . . . . . . . . . . . 14
202	197, 201	oveq12d 6326	. . . . . . . . . . . . 13
203	2, 4	sqmuld 12466	. . . . . . . . . . . . . . . 16
204	9, 4	sqmuld 12466	. . . . . . . . . . . . . . . . . 18
205	204	oveq2d 6324	. . . . . . . . . . . . . . . . 17
206	9	sqcld 12452	. . . . . . . . . . . . . . . . . 18
207	7, 206, 36	mulassd 9684	. . . . . . . . . . . . . . . . 17
208	205, 207	eqtr4d 2508	. . . . . . . . . . . . . . . 16
209	203, 208	oveq12d 6326	. . . . . . . . . . . . . . 15
210	7	sqvald 12451	. . . . . . . . . . . . . . . . . 18
211	9, 11	sqmuld 12466	. . . . . . . . . . . . . . . . . 18
212	210, 211	oveq12d 6326	. . . . . . . . . . . . . . . . 17
213	7, 12	sqmuld 12466	. . . . . . . . . . . . . . . . 17
214	7, 7	mulcld 9681	. . . . . . . . . . . . . . . . . 18
215	214, 206, 37	mulassd 9684	. . . . . . . . . . . . . . . . 17
216	212, 213, 215	3eqtr4d 2515	. . . . . . . . . . . . . . . 16
217	2, 11	sqmuld 12466	. . . . . . . . . . . . . . . . . 18
218	217	oveq2d 6324	. . . . . . . . . . . . . . . . 17
219	2	sqcld 12452	. . . . . . . . . . . . . . . . . 18
220	7, 219, 37	mulassd 9684	. . . . . . . . . . . . . . . . 17
221	218, 220	eqtr4d 2508	. . . . . . . . . . . . . . . 16
222	216, 221	oveq12d 6326	. . . . . . . . . . . . . . 15
223	209, 222	oveq12d 6326	. . . . . . . . . . . . . 14
224	7, 206	mulcld 9681	. . . . . . . . . . . . . . . . 17
225	219, 224, 36	subdird 10096	. . . . . . . . . . . . . . . 16
226		pellex.no1	. . . . . . . . . . . . . . . . 17
227	226	oveq1d 6323	. . . . . . . . . . . . . . . 16
228	225, 227	eqtr3d 2507	. . . . . . . . . . . . . . 15
229	7, 7, 206	mulassd 9684	. . . . . . . . . . . . . . . . . 18
230	229	oveq1d 6323	. . . . . . . . . . . . . . . . 17
231	230	oveq1d 6323	. . . . . . . . . . . . . . . 16
232	214, 206	mulcld 9681	. . . . . . . . . . . . . . . . 17
233	7, 219	mulcld 9681	. . . . . . . . . . . . . . . . 17
234	232, 233, 37	subdird 10096	. . . . . . . . . . . . . . . 16
235		subdi 10073	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
236	235	eqcomd 2477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
237	7, 224, 219, 236	syl3anc 1292	. . . . . . . . . . . . . . . . . 18
238		negsubdi2 9953	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
239	238	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
240	219, 224, 239	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20
241	226	negeqd 9889	. . . . . . . . . . . . . . . . . . . 20
242	240, 241	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19
243	242	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
244	7, 16	mulneg2d 10093	. . . . . . . . . . . . . . . . . 18
245	237, 243, 244	3eqtrd 2509	. . . . . . . . . . . . . . . . 17
246	245	oveq1d 6323	. . . . . . . . . . . . . . . 16
247	231, 234, 246	3eqtr3d 2513	. . . . . . . . . . . . . . 15
248	228, 247	oveq12d 6326	. . . . . . . . . . . . . 14
249	7, 16	mulcld 9681	. . . . . . . . . . . . . . . . . 18
250	249, 37	mulneg1d 10092	. . . . . . . . . . . . . . . . 17
251	7, 16	mulcomd 9682	. . . . . . . . . . . . . . . . . . . 20
252	251	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
253	16, 7, 37	mulassd 9684	. . . . . . . . . . . . . . . . . . 19
254	252, 253	eqtrd 2505	. . . . . . . . . . . . . . . . . 18
255	254	negeqd 9889	. . . . . . . . . . . . . . . . 17
256	250, 255	eqtrd 2505	. . . . . . . . . . . . . . . 16
257	256	oveq2d 6324	. . . . . . . . . . . . . . 15
258	16, 36	mulcld 9681	. . . . . . . . . . . . . . . 16
259	16, 38	mulcld 9681	. . . . . . . . . . . . . . . 16
260	258, 259	negsubd 10011	. . . . . . . . . . . . . . 15
261	61	oveq2d 6324	. . . . . . . . . . . . . . . 16
262		subdi 10073	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
263	262	eqcomd 2477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
264	16, 36, 38, 263	syl3anc 1292	. . . . . . . . . . . . . . . 16
265	16	sqvald 12451	. . . . . . . . . . . . . . . 16
266	261, 264, 265	3eqtr4d 2515	. . . . . . . . . . . . . . 15
267	257, 260, 266	3eqtrd 2509	. . . . . . . . . . . . . 14
268	223, 248, 267	3eqtrd 2509	. . . . . . . . . . . . 13
269	193, 202, 268	3eqtr2d 2511	. . . . . . . . . . . 12
270	183, 192, 269	3eqtrd 2509	. . . . . . . . . . 11
271	270	oveq1d 6323	. . . . . . . . . 10
272	142, 145	dividd 10403	. . . . . . . . . 10
273	170, 271, 272	3eqtrd 2509	. . . . . . . . 9
274	151, 155, 273	3eqtr2d 2511	. . . . . . . 8
275	274	adantr 472	. . . . . . 7 $/\$
276		simpr 468	. . . . . . . . . . . 12 $/\$
277	276	oveq1d 6323	. . . . . . . . . . 11 $/\$
278	277	fveq2d 5883	. . . . . . . . . 10 $/\$
279	16, 17	div0d 10404	. . . . . . . . . . . 12
280	279	abs00bd 13431	. . . . . . . . . . 11
281	280	adantr 472	. . . . . . . . . 10 $/\$
282	278, 281	eqtrd 2505	. . . . . . . . 9 $/\$
283	282	sq0id 12406	. . . . . . . 8 $/\$
284	283	oveq1d 6323	. . . . . . 7 $/\$
285	275, 284	eqtr3d 2507	. . . . . 6 $/\$
286	125, 285	mtand 671	. . . . 5
287	286	neqned 2650	. . . 4
288	14, 16, 287, 17	divne0d 10421	. . 3
289		nnabscl 13465	. . 3 $/\$
290	104, 288, 289	syl2anc 673	. 2
291	112, 16, 17	absdivd 13594	. . . . 5
292		negsub 9942	. . . . . . . . . . . 12 $/\$
293	292	eqcomd 2477	. . . . . . . . . . 11 $/\$
294	110, 111, 293	syl2anc 673	. . . . . . . . . 10
295	294	oveq1d 6323	. . . . . . . . 9
296	133	renegcld 10067	. . . . . . . . . 10
297	11, 4	mulcomd 9682	. . . . . . . . . . . 12
298	297	oveq1d 6323	. . . . . . . . . . 11
299		modmul1 12177	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
300	26, 27, 32, 31, 78, 299	syl221anc 1303	. . . . . . . . . . 11
301		modmul1 12177	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
302	22, 23, 76, 31, 33, 301	syl221anc 1303	. . . . . . . . . . 11
303	298, 300, 302	3eqtr4d 2515	. . . . . . . . . 10
304		modadd1 12167	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
305	132, 133, 296, 31, 303, 304	syl221anc 1303	. . . . . . . . 9
306	111	negidd 9995	. . . . . . . . . 10
307	306	oveq1d 6323	. . . . . . . . 9
308	295, 305, 307	3eqtrd 2509	. . . . . . . 8
309	308, 64	eqtrd 2505	. . . . . . 7
310		absmod0 13443	. . . . . . . 8 $/\$
311	134, 31, 310	syl2anc 673	. . . . . . 7
312	309, 311	mpbid 215	. . . . . 6
313	112	abscld 13575	. . . . . . 7
314		mod0 12136	. . . . . . 7 $/\$
315	313, 31, 314	syl2anc 673	. . . . . 6
316	312, 315	mpbid 215	. . . . 5
317	291, 316	eqeltrd 2549	. . . 4
318		absz 13451	. . . . 5
319	135, 318	syl 17	. . . 4
320	317, 319	mpbird 240	. . 3
321		pellex.neq	. . . . . . 7 $/\$
322	10	nnne0d 10676	. . . . . . . . 9
323	3	nnne0d 10676	. . . . . . . . 9
324	9, 11, 2, 4, 322, 323	divmuleqd 10451	. . . . . . . 8
325	61	adantr 472	. . . . . . . . . . . . . . 15 $/\$
326	325	eqcomd 2477	. . . . . . . . . . . . . 14 $/\$
327	326	oveq2d 6324	. . . . . . . . . . . . 13 $/\$
328	9, 11, 322	divcld 10405	. . . . . . . . . . . . . . . 16
329	328	sqcld 12452	. . . . . . . . . . . . . . 15
330	329	adantr 472	. . . . . . . . . . . . . 14 $/\$
331	36	adantr 472	. . . . . . . . . . . . . 14 $/\$
332	38	adantr 472	. . . . . . . . . . . . . 14 $/\$
333	330, 331, 332	subdid 10095	. . . . . . . . . . . . 13 $/\$
334		oveq1 6315	. . . . . . . . . . . . . . . . 17
335	334	oveq1d 6323	. . . . . . . . . . . . . . . 16
336	335	adantl 473	. . . . . . . . . . . . . . 15 $/\$
337	2	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
338	4	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
339	323	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
340	337, 338, 339	sqdivd 12467	. . . . . . . . . . . . . . . 16 $/\$
341	340	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$
342	219	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
343		sqne0 12379	. . . . . . . . . . . . . . . . . . 19
344	4, 343	syl 17	. . . . . . . . . . . . . . . . . 18
345	323, 344	mpbird 240	. . . . . . . . . . . . . . . . 17
346	345	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
347	342, 331, 346	divcan1d 10406	. . . . . . . . . . . . . . 15 $/\$
348	336, 341, 347	3eqtrd 2509	. . . . . . . . . . . . . 14 $/\$
349	7	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
350	37	adantr 472	. . . . . . . . . . . . . . . 16 $/\$
351	330, 349, 350	mul12d 9860	. . . . . . . . . . . . . . 15 $/\$
352	9	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
353	11	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
354	322	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
355	352, 353, 354	sqdivd 12467	. . . . . . . . . . . . . . . . 17 $/\$
356	355	oveq1d 6323	. . . . . . . . . . . . . . . 16 $/\$
357	356	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$
358	206	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
359		sqne0 12379	. . . . . . . . . . . . . . . . . . . 20
360	11, 359	syl 17	. . . . . . . . . . . . . . . . . . 19
361	322, 360	mpbird 240	. . . . . . . . . . . . . . . . . 18
362	361	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
363	358, 350, 362	divcan1d 10406	. . . . . . . . . . . . . . . 16 $/\$