pellexlem6 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pellexlem6		Unicode version

Theorem pellexlem6 26787

Description: Lemma for pellex 26788. 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 9972	. . . . . . . 8
3		pellex.enn	. . . . . . . . 9
4	3	nncnd 9972	. . . . . . . 8
5	2, 4	mulcld 9064	. . . . . . 7
6		pellex.dnn	. . . . . . . . 9
7	6	nncnd 9972	. . . . . . . 8
8		pellex.bnn	. . . . . . . . . 10
9	8	nncnd 9972	. . . . . . . . 9
10		pellex.fnn	. . . . . . . . . 10
11	10	nncnd 9972	. . . . . . . . 9
12	9, 11	mulcld 9064	. . . . . . . 8
13	7, 12	mulcld 9064	. . . . . . 7
14	5, 13	subcld 9367	. . . . . 6
15		pellex.cz	. . . . . . 7
16	15	zcnd 10332	. . . . . 6
17		pellex.cn0	. . . . . 6
18	14, 16, 17	absdivd 12212	. . . . 5
19	5, 13	negsubd 9373	. . . . . . . . . . 11
20	19	eqcomd 2409	. . . . . . . . . 10
21	20	oveq1d 6055	. . . . . . . . 9
22	1	nnred 9971	. . . . . . . . . . 11
23	3	nnred 9971	. . . . . . . . . . 11
24	22, 23	remulcld 9072	. . . . . . . . . 10
25	6	nnred 9971	. . . . . . . . . . 11
26	8	nnred 9971	. . . . . . . . . . . 12
27	10	nnred 9971	. . . . . . . . . . . 12
28	26, 27	remulcld 9072	. . . . . . . . . . 11
29	25, 28	remulcld 9072	. . . . . . . . . 10
30	29	renegcld 9420	. . . . . . . . . 10
31	16, 17	absrpcld 12205	. . . . . . . . . 10
32	3	nnzd 10330	. . . . . . . . . . . 12
33		pellex.xcg	. . . . . . . . . . . 12
34		modmul1 11234	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
35	22, 23, 32, 31, 33, 34	syl221anc 1195	. . . . . . . . . . 11
36	4	sqcld 11476	. . . . . . . . . . . . . . 15
37	11	sqcld 11476	. . . . . . . . . . . . . . . 16
38	7, 37	mulcld 9064	. . . . . . . . . . . . . . 15
39	36, 38	npcand 9371	. . . . . . . . . . . . . 14
40	4	sqvald 11475	. . . . . . . . . . . . . 14
41	39, 40	eqtr2d 2437	. . . . . . . . . . . . 13
42	41	oveq1d 6055	. . . . . . . . . . . 12
43	23	resqcld 11504	. . . . . . . . . . . . . 14
44	27	resqcld 11504	. . . . . . . . . . . . . . 15
45	25, 44	remulcld 9072	. . . . . . . . . . . . . 14
46	43, 45	resubcld 9421	. . . . . . . . . . . . 13
47		0re 9047	. . . . . . . . . . . . . 14
48	47	a1i 11	. . . . . . . . . . . . 13
49	16	abscld 12193	. . . . . . . . . . . . . . . . . . 19
50	49	recnd 9070	. . . . . . . . . . . . . . . . . 18
51	16, 17	absne0d 12204	. . . . . . . . . . . . . . . . . 18
52	50, 51	dividd 9744	. . . . . . . . . . . . . . . . 17
53		1z 10267	. . . . . . . . . . . . . . . . . 18
54	53	a1i 11	. . . . . . . . . . . . . . . . 17
55	52, 54	eqeltrd 2478	. . . . . . . . . . . . . . . 16
56		mod0 11210	. . . . . . . . . . . . . . . . 17 $/\$
57	49, 31, 56	syl2anc 643	. . . . . . . . . . . . . . . 16
58	55, 57	mpbird 224	. . . . . . . . . . . . . . 15
59	15	zred 10331	. . . . . . . . . . . . . . . 16
60		absmod0 12063	. . . . . . . . . . . . . . . 16 $/\$
61	59, 31, 60	syl2anc 643	. . . . . . . . . . . . . . 15
62	58, 61	mpbird 224	. . . . . . . . . . . . . 14
63		pellex.no2	. . . . . . . . . . . . . . 15
64	63	oveq1d 6055	. . . . . . . . . . . . . 14
65		0mod 11227	. . . . . . . . . . . . . . 15
66	31, 65	syl 16	. . . . . . . . . . . . . 14
67	62, 64, 66	3eqtr4d 2446	. . . . . . . . . . . . 13
68		modadd1 11233	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
69	46, 48, 45, 31, 67, 68	syl221anc 1195	. . . . . . . . . . . 12
70	38	addid2d 9223	. . . . . . . . . . . . . 14
71	11	sqvald 11475	. . . . . . . . . . . . . . 15
72	71	oveq2d 6056	. . . . . . . . . . . . . 14
73	7, 11, 11	mul12d 9231	. . . . . . . . . . . . . 14
74	70, 72, 73	3eqtrd 2440	. . . . . . . . . . . . 13
75	74	oveq1d 6055	. . . . . . . . . . . 12
76	42, 69, 75	3eqtrd 2440	. . . . . . . . . . 11
77	6	nnzd 10330	. . . . . . . . . . . . . 14
78	10	nnzd 10330	. . . . . . . . . . . . . 14
79	77, 78	zmulcld 10337	. . . . . . . . . . . . 13
80		pellex.ycg	. . . . . . . . . . . . . 14
81	80	eqcomd 2409	. . . . . . . . . . . . 13
82		modmul1 11234	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
83	27, 26, 79, 31, 81, 82	syl221anc 1195	. . . . . . . . . . . 12
84	9, 7, 11	mul12d 9231	. . . . . . . . . . . . 13
85	84	oveq1d 6055	. . . . . . . . . . . 12
86	83, 85	eqtrd 2436	. . . . . . . . . . 11
87	35, 76, 86	3eqtrd 2440	. . . . . . . . . 10
88		modadd1 11233	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
89	24, 29, 30, 31, 87, 88	syl221anc 1195	. . . . . . . . 9
90	13	negidd 9357	. . . . . . . . . 10
91	90	oveq1d 6055	. . . . . . . . 9
92	21, 89, 91	3eqtrd 2440	. . . . . . . 8
93	92, 66	eqtrd 2436	. . . . . . 7
94	24, 29	resubcld 9421	. . . . . . . 8
95		absmod0 12063	. . . . . . . 8 $/\$
96	94, 31, 95	syl2anc 643	. . . . . . 7
97	93, 96	mpbid 202	. . . . . 6
98	14	abscld 12193	. . . . . . 7
99		mod0 11210	. . . . . . 7 $/\$
100	98, 31, 99	syl2anc 643	. . . . . 6
101	97, 100	mpbid 202	. . . . 5
102	18, 101	eqeltrd 2478	. . . 4
103	94, 59, 17	redivcld 9798	. . . . 5
104		absz 12071	. . . . 5
105	103, 104	syl 16	. . . 4
106	102, 105	mpbird 224	. . 3
107		0lt1 9506	. . . . . . . 8
108		1re 9046	. . . . . . . . 9
109	47, 108	ltnlei 9150	. . . . . . . 8
110	107, 109	mpbi 200	. . . . . . 7
111	9, 4	mulcld 9064	. . . . . . . . . . . . . 14
112	2, 11	mulcld 9064	. . . . . . . . . . . . . 14
113	111, 112	subcld 9367	. . . . . . . . . . . . 13
114	113, 16, 17	divcld 9746	. . . . . . . . . . . 12
115	114	abscld 12193	. . . . . . . . . . 11
116	115	resqcld 11504	. . . . . . . . . 10
117	6	nnnn0d 10230	. . . . . . . . . . 11
118	117	nn0ge0d 10233	. . . . . . . . . 10
119	115	sqge0d 11505	. . . . . . . . . 10
120	25, 116, 118, 119	mulge0d 9559	. . . . . . . . 9
121	25, 116	remulcld 9072	. . . . . . . . . 10
122	48, 121	suble0d 9573	. . . . . . . . 9
123	120, 122	mpbird 224	. . . . . . . 8
124		breq1 4175	. . . . . . . 8
125	123, 124	syl5ibrcom 214	. . . . . . 7
126	110, 125	mtoi 171	. . . . . 6
127		absresq 12062	. . . . . . . . . . . 12
128	103, 127	syl 16	. . . . . . . . . . 11
129	14, 16, 17	sqdivd 11491	. . . . . . . . . . 11
130	14	sqvald 11475	. . . . . . . . . . . 12
131	130	oveq1d 6055	. . . . . . . . . . 11
132	128, 129, 131	3eqtrd 2440	. . . . . . . . . 10
133	26, 23	remulcld 9072	. . . . . . . . . . . . . . . 16
134	22, 27	remulcld 9072	. . . . . . . . . . . . . . . 16
135	133, 134	resubcld 9421	. . . . . . . . . . . . . . 15
136	135, 59, 17	redivcld 9798	. . . . . . . . . . . . . 14
137		absresq 12062	. . . . . . . . . . . . . 14
138	136, 137	syl 16	. . . . . . . . . . . . 13
139	113, 16, 17	sqdivd 11491	. . . . . . . . . . . . 13
140	138, 139	eqtrd 2436	. . . . . . . . . . . 12
141	140	oveq2d 6056	. . . . . . . . . . 11
142	113	sqcld 11476	. . . . . . . . . . . 12
143	16	sqcld 11476	. . . . . . . . . . . 12
144		sqne0 11403	. . . . . . . . . . . . . 14
145	16, 144	syl 16	. . . . . . . . . . . . 13
146	17, 145	mpbird 224	. . . . . . . . . . . 12
147	7, 142, 143, 146	divassd 9781	. . . . . . . . . . 11
148	113	sqvald 11475	. . . . . . . . . . . . 13
149	148	oveq2d 6056	. . . . . . . . . . . 12
150	149	oveq1d 6055	. . . . . . . . . . 11
151	141, 147, 150	3eqtr2d 2442	. . . . . . . . . 10
152	132, 151	oveq12d 6058	. . . . . . . . 9
153	14, 14	mulcld 9064	. . . . . . . . . 10
154	113, 113	mulcld 9064	. . . . . . . . . . 11
155	7, 154	mulcld 9064	. . . . . . . . . 10
156	153, 155, 143, 146	divsubdird 9785	. . . . . . . . 9
157	5, 13, 5, 13	mulsubd 9448	. . . . . . . . . . . 12
158	111, 112, 111, 112	mulsubd 9448	. . . . . . . . . . . . . 14
159	158	oveq2d 6056	. . . . . . . . . . . . 13
160	111, 111	mulcld 9064	. . . . . . . . . . . . . . 15
161	112, 112	mulcld 9064	. . . . . . . . . . . . . . 15
162	160, 161	addcld 9063	. . . . . . . . . . . . . 14
163	111, 112	mulcld 9064	. . . . . . . . . . . . . . 15
164	163, 163	addcld 9063	. . . . . . . . . . . . . 14
165	7, 162, 164	subdid 9445	. . . . . . . . . . . . 13
166	7, 160, 161	adddid 9068	. . . . . . . . . . . . . 14
167	7, 163, 163	adddid 9068	. . . . . . . . . . . . . 14
168	166, 167	oveq12d 6058	. . . . . . . . . . . . 13
169	159, 165, 168	3eqtrd 2440	. . . . . . . . . . . 12
170	157, 169	oveq12d 6058	. . . . . . . . . . 11
171	170	oveq1d 6055	. . . . . . . . . 10
172	5, 13	mulcomd 9065	. . . . . . . . . . . . . . . 16
173	7, 12, 5	mulassd 9067	. . . . . . . . . . . . . . . 16
174	2, 4	mulcomd 9065	. . . . . . . . . . . . . . . . . . 19
175	174	oveq2d 6056	. . . . . . . . . . . . . . . . . 18
176	9, 11, 4, 2	mul4d 9234	. . . . . . . . . . . . . . . . . 18
177	11, 2	mulcomd 9065	. . . . . . . . . . . . . . . . . . 19
178	177	oveq2d 6056	. . . . . . . . . . . . . . . . . 18
179	175, 176, 178	3eqtrd 2440	. . . . . . . . . . . . . . . . 17
180	179	oveq2d 6056	. . . . . . . . . . . . . . . 16
181	172, 173, 180	3eqtrd 2440	. . . . . . . . . . . . . . 15
182	181, 181	oveq12d 6058	. . . . . . . . . . . . . 14
183	182	oveq2d 6056	. . . . . . . . . . . . 13
184	183	oveq1d 6055	. . . . . . . . . . . 12
185	5, 5	mulcld 9064	. . . . . . . . . . . . . 14
186	13, 13	mulcld 9064	. . . . . . . . . . . . . 14
187	185, 186	addcld 9063	. . . . . . . . . . . . 13
188	7, 160	mulcld 9064	. . . . . . . . . . . . . 14
189	7, 161	mulcld 9064	. . . . . . . . . . . . . 14
190	188, 189	addcld 9063	. . . . . . . . . . . . 13
191	7, 163	mulcld 9064	. . . . . . . . . . . . . 14
192	191, 191	addcld 9063	. . . . . . . . . . . . 13
193	187, 190, 192	nnncan2d 9402	. . . . . . . . . . . 12
194	185, 186, 188, 189	addsub4d 9414	. . . . . . . . . . . . 13
195	5	sqvald 11475	. . . . . . . . . . . . . . 15
196	111	sqvald 11475	. . . . . . . . . . . . . . . 16
197	196	oveq2d 6056	. . . . . . . . . . . . . . 15
198	195, 197	oveq12d 6058	. . . . . . . . . . . . . 14
199	13	sqvald 11475	. . . . . . . . . . . . . . 15
200	112	sqvald 11475	. . . . . . . . . . . . . . . 16
201	200	oveq2d 6056	. . . . . . . . . . . . . . 15
202	199, 201	oveq12d 6058	. . . . . . . . . . . . . 14
203	198, 202	oveq12d 6058	. . . . . . . . . . . . 13
204	2, 4	sqmuld 11490	. . . . . . . . . . . . . . . 16
205	9, 4	sqmuld 11490	. . . . . . . . . . . . . . . . . 18
206	205	oveq2d 6056	. . . . . . . . . . . . . . . . 17
207	9	sqcld 11476	. . . . . . . . . . . . . . . . . 18
208	7, 207, 36	mulassd 9067	. . . . . . . . . . . . . . . . 17
209	206, 208	eqtr4d 2439	. . . . . . . . . . . . . . . 16
210	204, 209	oveq12d 6058	. . . . . . . . . . . . . . 15
211	7	sqvald 11475	. . . . . . . . . . . . . . . . . 18
212	9, 11	sqmuld 11490	. . . . . . . . . . . . . . . . . 18
213	211, 212	oveq12d 6058	. . . . . . . . . . . . . . . . 17
214	7, 12	sqmuld 11490	. . . . . . . . . . . . . . . . 17
215	7, 7	mulcld 9064	. . . . . . . . . . . . . . . . . 18
216	215, 207, 37	mulassd 9067	. . . . . . . . . . . . . . . . 17
217	213, 214, 216	3eqtr4d 2446	. . . . . . . . . . . . . . . 16
218	2, 11	sqmuld 11490	. . . . . . . . . . . . . . . . . 18
219	218	oveq2d 6056	. . . . . . . . . . . . . . . . 17
220	2	sqcld 11476	. . . . . . . . . . . . . . . . . 18
221	7, 220, 37	mulassd 9067	. . . . . . . . . . . . . . . . 17
222	219, 221	eqtr4d 2439	. . . . . . . . . . . . . . . 16
223	217, 222	oveq12d 6058	. . . . . . . . . . . . . . 15
224	210, 223	oveq12d 6058	. . . . . . . . . . . . . 14
225	7, 207	mulcld 9064	. . . . . . . . . . . . . . . . 17
226	220, 225, 36	subdird 9446	. . . . . . . . . . . . . . . 16
227		pellex.no1	. . . . . . . . . . . . . . . . 17
228	227	oveq1d 6055	. . . . . . . . . . . . . . . 16
229	226, 228	eqtr3d 2438	. . . . . . . . . . . . . . 15
230	7, 7, 207	mulassd 9067	. . . . . . . . . . . . . . . . . 18
231	230	oveq1d 6055	. . . . . . . . . . . . . . . . 17
232	231	oveq1d 6055	. . . . . . . . . . . . . . . 16
233	215, 207	mulcld 9064	. . . . . . . . . . . . . . . . 17
234	7, 220	mulcld 9064	. . . . . . . . . . . . . . . . 17
235	233, 234, 37	subdird 9446	. . . . . . . . . . . . . . . 16
236		subdi 9423	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	236	eqcomd 2409	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
238	7, 225, 220, 237	syl3anc 1184	. . . . . . . . . . . . . . . . . 18
239		negsubdi2 9316	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
240	239	eqcomd 2409	. . . . . . . . . . . . . . . . . . . . 21 $/\$
241	220, 225, 240	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20
242	227	negeqd 9256	. . . . . . . . . . . . . . . . . . . 20
243	241, 242	eqtrd 2436	. . . . . . . . . . . . . . . . . . 19
244	243	oveq2d 6056	. . . . . . . . . . . . . . . . . 18
245	7, 16	mulneg2d 9443	. . . . . . . . . . . . . . . . . 18
246	238, 244, 245	3eqtrd 2440	. . . . . . . . . . . . . . . . 17
247	246	oveq1d 6055	. . . . . . . . . . . . . . . 16
248	232, 235, 247	3eqtr3d 2444	. . . . . . . . . . . . . . 15
249	229, 248	oveq12d 6058	. . . . . . . . . . . . . 14
250	7, 16	mulcld 9064	. . . . . . . . . . . . . . . . . 18
251	250, 37	mulneg1d 9442	. . . . . . . . . . . . . . . . 17
252	7, 16	mulcomd 9065	. . . . . . . . . . . . . . . . . . . 20
253	252	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19
254	16, 7, 37	mulassd 9067	. . . . . . . . . . . . . . . . . . 19
255	253, 254	eqtrd 2436	. . . . . . . . . . . . . . . . . 18
256	255	negeqd 9256	. . . . . . . . . . . . . . . . 17
257	251, 256	eqtrd 2436	. . . . . . . . . . . . . . . 16
258	257	oveq2d 6056	. . . . . . . . . . . . . . 15
259	16, 36	mulcld 9064	. . . . . . . . . . . . . . . 16
260	16, 38	mulcld 9064	. . . . . . . . . . . . . . . 16
261	259, 260	negsubd 9373	. . . . . . . . . . . . . . 15
262	63	oveq2d 6056	. . . . . . . . . . . . . . . 16
263		subdi 9423	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
264	263	eqcomd 2409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
265	16, 36, 38, 264	syl3anc 1184	. . . . . . . . . . . . . . . 16
266	16	sqvald 11475	. . . . . . . . . . . . . . . 16
267	262, 265, 266	3eqtr4d 2446	. . . . . . . . . . . . . . 15
268	258, 261, 267	3eqtrd 2440	. . . . . . . . . . . . . 14
269	224, 249, 268	3eqtrd 2440	. . . . . . . . . . . . 13
270	194, 203, 269	3eqtr2d 2442	. . . . . . . . . . . 12
271	184, 193, 270	3eqtrd 2440	. . . . . . . . . . 11
272	271	oveq1d 6055	. . . . . . . . . 10
273	143, 146	dividd 9744	. . . . . . . . . 10
274	171, 272, 273	3eqtrd 2440	. . . . . . . . 9
275	152, 156, 274	3eqtr2d 2442	. . . . . . . 8
276	275	adantr 452	. . . . . . 7 $/\$
277		simpr 448	. . . . . . . . . . . 12 $/\$
278	277	oveq1d 6055	. . . . . . . . . . 11 $/\$
279	278	fveq2d 5691	. . . . . . . . . 10 $/\$
280	16, 17	div0d 9745	. . . . . . . . . . . 12
281	280	abs00bd 12051	. . . . . . . . . . 11
282	281	adantr 452	. . . . . . . . . 10 $/\$
283	279, 282	eqtrd 2436	. . . . . . . . 9 $/\$
284	283	sq0id 11430	. . . . . . . 8 $/\$
285	284	oveq1d 6055	. . . . . . 7 $/\$
286	276, 285	eqtr3d 2438	. . . . . 6 $/\$
287	126, 286	mtand 641	. . . . 5
288	287	neneqad 2637	. . . 4
289	14, 16, 288, 17	divne0d 9762	. . 3
290		nnabscl 12084	. . 3 $/\$
291	106, 289, 290	syl2anc 643	. 2
292	113, 16, 17	absdivd 12212	. . . . 5
293		negsub 9305	. . . . . . . . . . . 12 $/\$
294	293	eqcomd 2409	. . . . . . . . . . 11 $/\$
295	111, 112, 294	syl2anc 643	. . . . . . . . . 10
296	295	oveq1d 6055	. . . . . . . . 9
297	134	renegcld 9420	. . . . . . . . . 10
298	11, 4	mulcomd 9065	. . . . . . . . . . . 12
299	298	oveq1d 6055	. . . . . . . . . . 11
300		modmul1 11234	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
301	26, 27, 32, 31, 80, 300	syl221anc 1195	. . . . . . . . . . 11
302		modmul1 11234	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
303	22, 23, 78, 31, 33, 302	syl221anc 1195	. . . . . . . . . . 11
304	299, 301, 303	3eqtr4d 2446	. . . . . . . . . 10
305		modadd1 11233	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
306	133, 134, 297, 31, 304, 305	syl221anc 1195	. . . . . . . . 9
307	112	negidd 9357	. . . . . . . . . 10
308	307	oveq1d 6055	. . . . . . . . 9
309	296, 306, 308	3eqtrd 2440	. . . . . . . 8
310	309, 66	eqtrd 2436	. . . . . . 7
311		absmod0 12063	. . . . . . . 8 $/\$
312	135, 31, 311	syl2anc 643	. . . . . . 7
313	310, 312	mpbid 202	. . . . . 6
314	113	abscld 12193	. . . . . . 7
315		mod0 11210	. . . . . . 7 $/\$
316	314, 31, 315	syl2anc 643	. . . . . 6
317	313, 316	mpbid 202	. . . . 5
318	292, 317	eqeltrd 2478	. . . 4
319		absz 12071	. . . . 5
320	136, 319	syl 16	. . . 4
321	318, 320	mpbird 224	. . 3
322		pellex.neq	. . . . . . 7 $/\$
323	10	nnne0d 10000	. . . . . . . . 9
324	3	nnne0d 10000	. . . . . . . . 9
325	9, 11, 2, 4, 323, 324	divmuleqd 9792	. . . . . . . 8
326	63	adantr 452	. . . . . . . . . . . . . . 15 $/\$
327	326	eqcomd 2409	. . . . . . . . . . . . . 14 $/\$
328	327	oveq2d 6056	. . . . . . . . . . . . 13 $/\$
329	9, 11, 323	divcld 9746	. . . . . . . . . . . . . . . 16
330	329	sqcld 11476	. . . . . . . . . . . . . . 15
331	330	adantr 452	. . . . . . . . . . . . . 14 $/\$
332	36	adantr 452	. . . . . . . . . . . . . 14 $/\$
333	38	adantr 452	. . . . . . . . . . . . . 14 $/\$
334	331, 332, 333	subdid 9445	. . . . . . . . . . . . 13 $/\$
335		oveq1 6047	. . . . . . . . . . . . . . . . 17
336	335	oveq1d 6055	. . . . . . . . . . . . . . . 16
337	336	adantl 453	. . . . . . . . . . . . . . 15 $/\$
338	2	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
339	4	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
340	324	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
341	338, 339, 340	sqdivd 11491	. . . . . . . . . . . . . . . 16 $/\$
342	341	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$
343	220	adantr 452	. . . . . . . . . . . . . . . 16 $/\$
344		sqne0 11403	. . . . . . . . . . . . . . . . . . 19
345	4, 344	syl 16	. . . . . . . . . . . . . . . . . 18
346	324, 345	mpbird 224	. . . . . . . . . . . . . . . . 17
347	346	adantr 452	. . . . . . . . . . . . . . . 16 $/\$
348	343, 332, 347	divcan1d 9747	. . . . . . . . . . . . . . 15 $/\$
349	337, 342, 348	3eqtrd 2440	. . . . . . . . . . . . . 14 $/\$
350	7	adantr 452	. . . . . . . . . . . . . . . 16 $/\$
351	37	adantr 452	. . . . . . . . . . . . . . . 16 $/\$
352	331, 350, 351	mul12d 9231	. . . . . . . . . . . . . . 15 $/\$
353	9	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$
354	11	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$
355	323	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$
356	353, 354, 355	sqdivd 11491	. . . . . . . . . . . . . . . . 17 $/\$
357	356	oveq1d 6055	. . . . . . . . . . . . . . . 16 $/\$
358	357	oveq2d 6056	. . . . . . . . . . . . . . 15 $/\$
359	207	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
360		sqne0 11403	. . . . . . . . . . . . . . . . . . . 20
361	11, 360	syl 16	. . . . . . . . . . . . . . . . . . 19
362	323, 361	mpbird 224	. . . . . . . . . . . . . . . . . 18
363	362	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$
364	359, 351, 363	divcan1d 9747	. . . . . . . . . . . . . . . 16 $/\$