lgsquadlem1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lgsquadlem1		Unicode version

Theorem lgsquadlem1 15598

Description: Lemma for lgsquad 15601. Count the members of

with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)

**Hypotheses**
Ref	Expression
lgseisen.1	$\$
lgseisen.2	$\$
lgseisen.3
lgsquad.4
lgsquad.5
lgsquad.6	$/\$ $/\$

**Assertion**
Ref	Expression
lgsquadlem1	♯

Distinct variable groups:

Proof of Theorem lgsquadlem1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neg1cn 9148	. . . 4
2	1	a1i 9	. . 3
3		neg1ap0 9152	. . . 4 #
4	3	a1i 9	. . 3 #
5		lgseisen.1	. . . . . . . . . 10 $\$
6		lgsquad.4	. . . . . . . . . 10
7	5, 6	gausslemma2dlem0b 15571	. . . . . . . . 9
8	7	nnzd 9501	. . . . . . . 8
9		2nn 9205	. . . . . . . 8
10		znq 9752	. . . . . . . 8 $/\$
11	8, 9, 10	sylancl 413	. . . . . . 7
12	11	flqcld 10427	. . . . . 6
13	12	peano2zd 9505	. . . . 5
14	13, 8	fzfigd 10583	. . . 4
15		lgseisen.2	. . . . . . . . 9 $\$
16	15	gausslemma2dlem0a 15570	. . . . . . . 8
17	16	nnzd 9501	. . . . . . 7
18	5	gausslemma2dlem0a 15570	. . . . . . . 8
19	18	adantr 276	. . . . . . 7 $/\$
20		znq 9752	. . . . . . 7 $/\$
21	17, 19, 20	syl2an2r 595	. . . . . 6 $/\$
22		2z 9407	. . . . . . . 8
23		elfzelz 10154	. . . . . . . . 9
24	23	adantl 277	. . . . . . . 8 $/\$
25		zmulcl 9433	. . . . . . . 8 $/\$
26	22, 24, 25	sylancr 414	. . . . . . 7 $/\$
27		zq 9754	. . . . . . 7
28	26, 27	syl 14	. . . . . 6 $/\$
29		qmulcl 9765	. . . . . 6 $/\$
30	21, 28, 29	syl2anc 411	. . . . 5 $/\$
31	30	flqcld 10427	. . . 4 $/\$
32	14, 31	fsumzcl 11757	. . 3
33	2, 4, 32	expclzapd 10830	. 2
34		lgseisen.3	. . . . 5
35		lgsquad.5	. . . . 5
36		lgsquad.6	. . . . 5 $/\$ $/\$
37	5, 15, 34, 6, 35, 36	lgsquadlemofi 15597	. . . 4
38		hashcl 10933	. . . 4 ♯
39	37, 38	syl 14	. . 3 ♯
40		expcl 10709	. . 3 $/\$ ♯ ♯
41	1, 39, 40	sylancr 414	. 2 ♯
42	39	nn0zd 9500	. . 3 ♯
43	2, 4, 42	expap0d 10831	. 2 ♯ #
44	41, 43	recidapd 8863	. . . 4 ♯ ♯
45		1div1e1 8784	. . . . . . . . 9
46	45	negeqi 8273	. . . . . . . 8
47		ax-1cn 8025	. . . . . . . . 9
48		1ap0 8670	. . . . . . . . 9 #
49		divneg2ap 8816	. . . . . . . . 9 $/\$ $/\$ #
50	47, 47, 48, 49	mp3an 1350	. . . . . . . 8
51	46, 50	eqtr3i 2229	. . . . . . 7
52	51	oveq1i 5961	. . . . . 6 ♯ ♯
53	2, 4, 42	exprecapd 10833	. . . . . 6 ♯ ♯
54	52, 53	eqtrid 2251	. . . . 5 ♯ ♯
55	54	oveq2d 5967	. . . 4 ♯ ♯ ♯ ♯
56	5, 15, 34, 6, 35, 36	lgsquadlemsfi 15596	. . . . . . . . . . . . 13
57	56	adantr 276	. . . . . . . . . . . 12 $/\$
58		opabssxp 4753	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	36, 58	eqsstri 3226	. . . . . . . . . . . . . . . . 17
60	59	sseli 3190	. . . . . . . . . . . . . . . 16
61		xp1st 6258	. . . . . . . . . . . . . . . 16
62	60, 61	syl 14	. . . . . . . . . . . . . . 15
63	62	elfzelzd 10155	. . . . . . . . . . . . . 14
64	19	nnzd 9501	. . . . . . . . . . . . . . 15 $/\$
65	64, 26	zsubcld 9507	. . . . . . . . . . . . . 14 $/\$
66		zdceq 9455	. . . . . . . . . . . . . 14 $/\$ DECID
67	63, 65, 66	syl2anr 290	. . . . . . . . . . . . 13 $/\$ $/\$ DECID
68	67	ralrimiva 2580	. . . . . . . . . . . 12 $/\$ DECID
69	57, 68	ssfirab 7040	. . . . . . . . . . 11 $/\$
70		fveqeq2 5592	. . . . . . . . . . . . . . . . . . . 20
71	70	elrab 2930	. . . . . . . . . . . . . . . . . . 19 $/\$
72	71	simprbi 275	. . . . . . . . . . . . . . . . . 18
73	72	ad2antll 491	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	73	oveq2d 5967	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	19	nncnd 9057	. . . . . . . . . . . . . . . . . 18 $/\$
76	75	adantrr 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
77	26	zcnd 9503	. . . . . . . . . . . . . . . . . 18 $/\$
78	77	adantrr 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79	76, 78	nncand 8395	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80	74, 79	eqtrd 2239	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	80	oveq1d 5966	. . . . . . . . . . . . . 14 $/\$ $/\$
82	24	zcnd 9503	. . . . . . . . . . . . . . . 16 $/\$
83	82	adantrr 479	. . . . . . . . . . . . . . 15 $/\$ $/\$
84		2cnd 9116	. . . . . . . . . . . . . . 15 $/\$ $/\$
85		2ap0 9136	. . . . . . . . . . . . . . . 16 #
86	85	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
87	83, 84, 86	divcanap3d 8875	. . . . . . . . . . . . . 14 $/\$ $/\$
88	81, 87	eqtrd 2239	. . . . . . . . . . . . 13 $/\$ $/\$
89	88	ralrimivva 2589	. . . . . . . . . . . 12
90		invdisj 4040	. . . . . . . . . . . 12 Disj
91	89, 90	syl 14	. . . . . . . . . . 11 Disj
92	14, 69, 91	hashiun 11833	. . . . . . . . . 10 ♯ ♯
93		iunrab 3977	. . . . . . . . . . . 12
94		eldifsni 3764	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
95	5, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22
96	95	necomd 2463	. . . . . . . . . . . . . . . . . . . . 21
97	96	neneqd 2398	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		uzid 9669	. . . . . . . . . . . . . . . . . . . . 21
100	22, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
101	5	eldifad 3178	. . . . . . . . . . . . . . . . . . . . 21
102	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103		dvdsprm 12503	. . . . . . . . . . . . . . . . . . . 20 $/\$
104	100, 102, 103	sylancr 414	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
105	98, 104	mtbird 675	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
106	18	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	nncnd 9057	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	26	adantlr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
109	108	zcnd 9503	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
110	107, 109	npcand 8394	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
111	110	breq2d 4059	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	105, 111	mtbird 675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114		dvdsmul1 12168	. . . . . . . . . . . . . . . . . . 19 $/\$
115	22, 113, 114	sylancr 414	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
117	106	nnzd 9501	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118	117, 108	zsubcld 9507	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119		dvds2add 12180	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
120	116, 118, 108, 119	syl3anc 1250	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	115, 120	mpan2d 428	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
122	112, 121	mtod 665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
123		breq2 4051	. . . . . . . . . . . . . . . . 17
124	123	notbid 669	. . . . . . . . . . . . . . . 16
125	122, 124	syl5ibrcom 157	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	125	rexlimdva 2624	. . . . . . . . . . . . . 14 $/\$
127		simpr 110	. . . . . . . . . . . . . . . . . 18 $/\$
128	59, 127	sselid 3192	. . . . . . . . . . . . . . . . 17 $/\$
129	128, 61	syl 14	. . . . . . . . . . . . . . . 16 $/\$
130		elfzelz 10154	. . . . . . . . . . . . . . . 16
131		odd2np1 12228	. . . . . . . . . . . . . . . 16
132	129, 130, 131	3syl 17	. . . . . . . . . . . . . . 15 $/\$
133	11	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
134	133	flqcld 10427	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
135	134	peano2zd 9505	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
136	7	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	136	nnzd 9501	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138		simprl 529	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
139	137, 138	zsubcld 9507	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
140	134	zred 9502	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
141	7	nnred 9056	. . . . . . . . . . . . . . . . . . . . . 22
142	141	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
143	142	rehalfcld 9291	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
144	139	zred 9502	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
145		flqle 10428	. . . . . . . . . . . . . . . . . . . . 21
146	133, 145	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
147		zre 9383	. . . . . . . . . . . . . . . . . . . . . 22
148	147	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
149		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
150	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
151	149, 150	eqeltrd 2283	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
152		elfzle2 10157	. . . . . . . . . . . . . . . . . . . . . . . . 25
153	151, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154		zmulcl 9433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155	22, 138, 154	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156		zltp1le 9434	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
157	155, 137, 156	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
158	153, 157	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159		2re 9113	. . . . . . . . . . . . . . . . . . . . . . . . 25
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		2pos 9134	. . . . . . . . . . . . . . . . . . . . . . . . 25
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
163		ltmuldiv2 8955	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
164	148, 142, 160, 162, 163	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
165	158, 164	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
166	143	recnd 8108	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
167	7	nncnd 9057	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	167	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	168	2halvesd 9290	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170	166, 166, 169	mvlraddd 8443	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
171	165, 170	breqtrd 4073	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
172	148, 142, 143, 171	ltsub13d 8631	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	140, 143, 144, 146, 172	lelttrd 8204	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174		zltp1le 9434	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	134, 139, 174	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
176	173, 175	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
177		2t0e0 9203	. . . . . . . . . . . . . . . . . . . . 21
178		2cn 9114	. . . . . . . . . . . . . . . . . . . . . . . . 25
179		zcn 9384	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181		mulcl 8059	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
182	178, 180, 181	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
183		pncan 8285	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
184	182, 47, 183	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185		elfznn 10183	. . . . . . . . . . . . . . . . . . . . . . . 24
186		nnm1nn0 9343	. . . . . . . . . . . . . . . . . . . . . . . 24
187	151, 185, 186	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
188	184, 187	eqeltrrd 2284	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
189	188	nn0ge0d 9358	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
190	177, 189	eqbrtrid 4082	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
191		0red 8080	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
192		lemul2 8937	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
193	191, 148, 160, 162, 192	syl112anc 1254	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
194	190, 193	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	142, 148	subge02d 8617	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196	194, 195	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
197	135, 137, 139, 176, 196	elfzd 10145	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
198	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		prmnn 12476	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	200	nncnd 9057	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202		peano2cn 8214	. . . . . . . . . . . . . . . . . . . 20
203	182, 202	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
204	201, 203	nncand 8395	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		1cnd 8095	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	201, 182, 205	sub32d 8422	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	201, 182, 205	subsub4d 8421	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
208		2cnd 9116	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
209	208, 168, 180	subdid 8493	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
210	6	oveq2i 5962	. . . . . . . . . . . . . . . . . . . . . . 23
211	18	nnzd 9501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
212	211	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
213		peano2zm 9417	. . . . . . . . . . . . . . . . . . . . . . . . . 26
214	212, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
215	214	zcnd 9503	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
216	160, 162	gt0ap0d 8709	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ #
217	215, 208, 216	divcanap2d 8872	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
218	210, 217	eqtrid 2251	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
219	218	oveq1d 5966	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
220	209, 219	eqtr2d 2240	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
221	206, 207, 220	3eqtr3d 2247	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
222	221	oveq2d 5967	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
223	204, 222, 149	3eqtr3rd 2248	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
224		oveq2 5959	. . . . . . . . . . . . . . . . . . 19
225	224	oveq2d 5967	. . . . . . . . . . . . . . . . . 18
226	225	rspceeqv 2896	. . . . . . . . . . . . . . . . 17 $/\$
227	197, 223, 226	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
228	227	rexlimdvaa 2625	. . . . . . . . . . . . . . 15 $/\$
229	132, 228	sylbid 150	. . . . . . . . . . . . . 14 $/\$
230	126, 229	impbid 129	. . . . . . . . . . . . 13 $/\$
231	230	rabbidva 2761	. . . . . . . . . . . 12
232	93, 231	eqtrid 2251	. . . . . . . . . . 11
233	232	fveq2d 5587	. . . . . . . . . 10 ♯ ♯
234		ssrab2 3279	. . . . . . . . . . . . . . 15
235	36	relopabiv 4805	. . . . . . . . . . . . . . 15
236		relss 4766	. . . . . . . . . . . . . . 15
237	234, 235, 236	mp2 16	. . . . . . . . . . . . . 14
238		relxp 4788	. . . . . . . . . . . . . 14
239	36	eleq2i 2273	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
240		opabidw 4307	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
241	239, 240	bitri 184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
242		anass 401	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
243	31	peano2zd 9505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	243	zred 9502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
245	244	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
246	16	nnred 9056	. . . . . . . . . . . . . . . . . . . . . . . . . 26
247	246	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
248		nnre 9050	. . . . . . . . . . . . . . . . . . . . . . . . . 26
249	248	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
250		lesub 8521	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
251	245, 247, 249, 250	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
252	246	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
253	252	recnd 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
254	75, 253	mulcomd 8101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
255	77, 253	mulcomd 8101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
256	19	nnap0d 9089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ #
257	253, 75, 256	divcanap1d 8871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
258	257	oveq1d 5966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
259	246, 18	nndivred 9093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260	259	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
261	260	recnd 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
262	261, 75, 77	mul32d 8232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
263	255, 258, 262	3eqtr2d 2245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
264	254, 263	oveq12d 5969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
265	75, 77, 253	subdird 8494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	26	zred 9502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
267	260, 266	remulcld 8110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
268	267	recnd 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
269	253, 268, 75	subdird 8494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
270	264, 265, 269	3eqtr4d 2249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
271	270	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
272	271	breq2d 4059	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
273	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
274	247, 273	resubcld 8460	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
275	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
276	275	nnred 9056	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
277	275	nngt0d 9087	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
278		ltmul1 8672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
279	249, 274, 276, 277, 278	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
280		ltsub13 8523	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
281	249, 247, 273, 280	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
282	272, 279, 281	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
283	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
284	283	nnzd 9501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
285		nnz 9398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
286		zsubcl 9420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
287	284, 285, 286	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
288		flqlt 10433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
289	30, 287, 288	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
290		zltp1le 9434	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
291	31, 287, 290	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
292	282, 289, 291	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
293	35	oveq2i 5962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
294		peano2rem 8346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
295	252, 294	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
296	295	recnd 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
297		2cnd 9116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
298	85	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ #
299	296, 297, 298	divcanap2d 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
300	293, 299	eqtrid 2251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
301	300	oveq1d 5966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
302		1cnd 8095	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
303	31	zcnd 9503	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
304	253, 302, 303	sub32d 8422	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
305	253, 303, 302	subsub4d 8421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
306	301, 304, 305	3eqtrd 2243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	306	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
308	307	breq2d 4059	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
309	251, 292, 308	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310	309	anbi2d 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
311	15, 35	gausslemma2dlem0b 15571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
312		nnmulcl 9064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
313	9, 311, 312	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314	313	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
315	314	nnred 9056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
316	311	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
317	316	nnred 9056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
318	31	zred 9502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
319	311	nncnd 9057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
320	319	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
321	320	2timesd 9287	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
322	320, 320, 321	mvrladdd 8446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
323	252	rehalfcld 9291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
324	252	ltm1d 9012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
325	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
326	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
327		ltdiv1 8948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
328	295, 252, 325, 326, 327	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
329	324, 328	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
330	35, 329	eqbrtrid 4082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
331	317, 323, 330	ltled 8198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
332	253, 297, 75, 298	div32apd 8894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
333	141	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
334	333	rehalfcld 9291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
335	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
336	335	zred 9502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
337	24	zred 9502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
338	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
339		flqltp1 10429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
340	338, 339	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
341		elfzle1 10156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
342	341	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
343	334, 336, 337, 340, 342	ltletrd 8503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
344		ltdivmul 8956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
345	333, 337, 325, 326, 344	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
346	343, 345	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
347	6, 346	eqbrtrrid 4083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
348	19	nnred 9056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
349		peano2rem 8346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
350	348, 349	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
351		ltdivmul 8956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
352	350, 266, 325, 326, 351	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
353	347, 352	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
354		zmulcl 9433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
355	22, 26, 354	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
356		zlem1lt 9436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
357	211, 355, 356	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
358	353, 357	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
359		ledivmul 8957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
360	348, 266, 325, 326, 359	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
361	358, 360	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
362	348	rehalfcld 9291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
363	283	nngt0d 9087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
364		lemul2 8937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
365	362, 266, 252, 363, 364	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
366	361, 365	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
367	332, 366	eqbrtrd 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
368	252, 266	remulcld 8110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
369	19	nngt0d 9087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
370		lemuldiv 8961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
371	323, 368, 348, 369, 370	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
372	367, 371	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
373	253, 77, 75, 256	div23apd 8908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
374	372, 373	breqtrd 4073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
375	317, 323, 267, 331, 374	letrd 8203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
376	311	nnzd 9501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
377	376	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
378		flqge 10432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
379	30, 377, 378	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
380	375, 379	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
381	322, 380	eqbrtrd 4069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
382	315, 317, 318, 381	subled 8628	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
383	382	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
384	314	nnzd 9501	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
385	384, 31	zsubcld 9507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
386	385	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
387	386	zred 9502	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
388	311	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
389	388	nnred 9056	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
390		letr 8162	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
391	249, 387, 389, 390	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
392	383, 391	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
393	392	pm4.71rd 394	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
394	310, 393	bitr4d 191	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
395	394	pm5.32da 452	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
396	395	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
397	242, 396	bitrid 192	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
398		simpr 110	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
399	211	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
400	399, 26	zsubcld 9507	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
401		elfzle2 10157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402	401	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
403	402, 6	breqtrdi 4088	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
404		lemuldiv2 8962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
405	337, 350, 325, 326, 404	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
406	403, 405	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
407	348	ltm1d 9012	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
408	266, 350, 348, 406, 407	lelttrd 8204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
409	266, 348	posdifd 8612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
410	408, 409	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
411		elnnz 9389	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
412	400, 410, 411	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
413	75, 77, 302	sub32d 8422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
414	6, 6	oveq12i 5963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
415	64, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
416	415	zcnd 9503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
417	416	2halvesd 9290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
418	414, 417	eqtrid 2251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
419	418	oveq1d 5966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
420	167	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
421	420, 420	pncan2d 8392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
422	419, 421	eqtr3d 2241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
423	422, 346	eqbrtrd 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
424	350, 333, 266, 423	ltsub23d 8630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
425	413, 424	eqbrtrd 4069	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
426	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
427	426	nnzd 9501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
428		zlem1lt 9436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
429	400, 427, 428	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
430	425, 429	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
431		fznn 10218	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
432	427, 431	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
433	412, 430, 432	mpbir2and 947	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
434	433	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
435	398, 434	eqeltrd 2283	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
436	435	biantrurd 305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
437	376	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
438		fznn 10218	. . . . . . . . . . . . . . . . . . . . 21 $/\$
439	437, 438	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
440	436, 439	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
441	398	oveq1d 5966	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
442	441	breq2d 4059	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
443	440, 442	anbi12d 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
444	385	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
445		fznn 10218	. . . . . . . . . . . . . . . . . . 19 $/\$
446	444, 445	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
447	397, 443, 446	3bitr4d 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
448	241, 447	bitrid 192	. . . . . . . . . . . . . . . 16 $/\$ $/\$
449	448	pm5.32da 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
450		vex 2776	. . . . . . . . . . . . . . . . . . 19
451		vex 2776	. . . . . . . . . . . . . . . . . . 19
452	450, 451	op1std 6241	. . . . . . . . . . . . . . . . . 18
453	452	eqeq1d 2215	. . . . . . . . . . . . . . . . 17
454	453	elrab 2930	. . . . . . . . . . . . . . . 16 $/\$
455	454	biancomi 270	. . . . . . . . . . . . . . 15 $/\$
456		opelxp 4709	. . . . . . . . . . . . . . . 16 $/\$
457		velsn 3651	. . . . . . . . . . . . . . . . 17
458	457	anbi1i 458	. . . . . . . . . . . . . . . 16 $/\$ $/\$
459	456, 458	bitri 184	. . . . . . . . . . . . . . 15 $/\$
460	449, 455, 459	3bitr4g 223	. . . . . . . . . . . . . 14 $/\$
461	237, 238, 460	eqrelrdv 4775	. . . . . . . . . . . . 13 $/\$
462	461	fveq2d 5587	. . . . . . . . . . . 12 $/\$ ♯ ♯
463		1zzd 9406	. . . . . . . . . . . . . . 15 $/\$
464	463, 385	fzfigd 10583	. . . . . . . . . . . . . 14 $/\$
465		xpsnen2g 6931	. . . . . . . . . . . . . 14 $/\$
466	400, 464, 465	syl2anc 411	. . . . . . . . . . . . 13 $/\$
467	461, 69	eqeltrrd 2284	. . . . . . . . . . . . . 14 $/\$
468		hashen 10936	. . . . . . . . . . . . . 14 $/\$ ♯ ♯
469	467, 464, 468	syl2anc 411	. . . . . . . . . . . . 13 $/\$ ♯ ♯
470	466, 469	mpbird 167	. . . . . . . . . . . 12 $/\$ ♯ ♯
471		ltmul2 8936	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
472	266, 348, 252, 363, 471	syl112anc 1254	. . . . . . . . . . . . . . . . . . . 20 $/\$
473	408, 472	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$
474		ltdivmul2 8958	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
475	368, 252, 348, 369, 474	syl112anc 1254	. . . . . . . . . . . . . . . . . . 19 $/\$
476	473, 475	mpbird 167	. . . . . . . . . . . . . . . . . 18 $/\$
477	373, 476	eqbrtrrd 4071	. . . . . . . . . . . . . . . . 17 $/\$
478		flqlt 10433	. . . . . . . . . . . . . . . . . 18 $/\$
479	30, 284, 478	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$
480	477, 479	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$
481		zltlem1 9437	. . . . . . . . . . . . . . . . 17 $/\$
482	31, 284, 481	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$
483	480, 482	mpbid 147	. . . . . . . . . . . . . . 15 $/\$
484	483, 300	breqtrrd 4075	. . . . . . . . . . . . . 14 $/\$
485		eluz2 9661	. . . . . . . . . . . . . 14 $/\$ $/\$
486	31, 384, 484, 485	syl3anbrc 1184	. . . . . . . . . . . . 13 $/\$
487		uznn0sub 9687	. . . . . . . . . . . . 13
488		hashfz1 10935	. . . . . . . . . . . . 13 ♯
489	486, 487, 488	3syl 17	. . . . . . . . . . . 12 $/\$ ♯
490	462, 470, 489	3eqtrd 2243	. . . . . . . . . . 11 $/\$ ♯
491	490	sumeq2dv 11723	. . . . . . . . . 10 ♯
492	92, 233, 491	3eqtr3rd 2248	. . . . . . . . 9 ♯
493	313	nncnd 9057	. . . . . . . . . . 11
494	493	adantr 276	. . . . . . . . . 10 $/\$
495	14, 494, 303	fsumsub 11807	. . . . . . . . 9
496	492, 495	eqtr3d 2241	. . . . . . . 8 ♯
497	496	oveq2d 5967	. . . . . . 7 ♯
498	32	zcnd 9503	. . . . . . . 8
499	14, 384	fsumzcl 11757	. . . . . . . . 9
500	499	zcnd 9503	. . . . . . . 8
501	498, 500	pncan3d 8393	. . . . . . 7
502		fsumconst 11809	. . . . . . . . 9 $/\$ ♯
503	14, 493, 502	syl2anc 411	. . . . . . . 8 ♯
504		hashcl 10933	. . . . . . . . . . 11 ♯
505	14, 504	syl 14	. . . . . . . . . 10 ♯
506	505	nn0cnd 9357	. . . . . . . . 9 ♯
507		2cnd 9116	. . . . . . . . 9
508	506, 507, 319	mul12d 8231	. . . . . . . 8 ♯ ♯
509	503, 508	eqtrd 2239	. . . . . . 7 ♯
510	497, 501, 509	3eqtrd 2243	. . . . . 6 ♯ ♯
511	510	oveq2d 5967	. . . . 5 ♯ ♯
512	22	a1i 9	. . . . . 6
513	505	nn0zd 9500	. . . . . . 7 ♯
514	513, 376	zmulcld 9508	. . . . . 6 ♯
515		expmulzap 10737	. . . . . 6 $/\$ # $/\$ $/\$ ♯ ♯ ♯
516	2, 4, 512, 514, 515	syl22anc 1251	. . . . 5 ♯ ♯
517		neg1sqe1 10786	. . . . . . 7
518	517	oveq1i 5961	. . . . . 6 ♯ ♯
519		1exp 10720	. . . . . . 7 ♯ ♯
520	514, 519	syl 14	. . . . . 6 ♯
521	518, 520	eqtrid 2251	. . . . 5 ♯
522	511, 516, 521	3eqtrd 2243	. . . 4 ♯
523	44, 55, 522	3eqtr4d 2249	. . 3 ♯ ♯ ♯
524		expaddzap 10735	. . . 4 $/\$ # $/\$ $/\$ ♯ ♯ ♯
525	2, 4, 32, 42, 524	syl22anc 1251	. . 3 ♯ ♯
526	523, 525	eqtr2d 2240	. 2 ♯ ♯ ♯
527	33, 41, 41, 43, 526	mulcanap2ad 8744	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 DECID wdc 836

wceq 1373

wcel 2177

wne 2377

wral 2485

wrex 2486

crab 2489 $\$ cdif 3164

wss 3167

csn 3634

cop 3637

ciun 3929 Disj wdisj 4023 class class class wbr 4047

copab 4108

cxp 4677

wrel 4684

cfv 5276 (class class class)co 5951

c1st 6231

cen 6832

cfn 6834

cc 7930

cr 7931

cc0 7932

c1 7933

caddc 7935

cmul 7937

clt 8114

cle 8115

cmin 8250

cneg 8251 # cap 8661

cdiv 8752

cn 9043

c2 9094

cn0 9302

cz 9379

cuz 9655

cq 9747

cfz 10137

cfl 10418

cexp 10690 ♯chash 10927

csu 11708

cdvds 12142

cprime 12473

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4163 ax-sep 4166 ax-nul 4174 ax-pow 4222 ax-pr 4257 ax-un 4484 ax-setind 4589 ax-iinf 4640 ax-cnex 8023 ax-resscn 8024 ax-1cn 8025 ax-1re 8026 ax-icn 8027 ax-addcl 8028 ax-addrcl 8029 ax-mulcl 8030 ax-mulrcl 8031 ax-addcom 8032 ax-mulcom 8033 ax-addass 8034 ax-mulass 8035 ax-distr 8036 ax-i2m1 8037 ax-0lt1 8038 ax-1rid 8039 ax-0id 8040 ax-rnegex 8041 ax-precex 8042 ax-cnre 8043 ax-pre-ltirr 8044 ax-pre-ltwlin 8045 ax-pre-lttrn 8046 ax-pre-apti 8047 ax-pre-ltadd 8048 ax-pre-mulgt0 8049 ax-pre-mulext 8050 ax-arch 8051 ax-caucvg 8052

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-xor 1396 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3000 df-csb 3095 df-dif 3169 df-un 3171 df-in 3173 df-ss 3180 df-nul 3462 df-if 3573 df-pw 3619 df-sn 3640 df-pr 3641 df-op 3643 df-uni 3853 df-int 3888 df-iun 3931 df-disj 4024 df-br 4048 df-opab 4110 df-mpt 4111 df-tr 4147 df-id 4344 df-po 4347 df-iso 4348 df-iord 4417 df-on 4419 df-ilim 4420 df-suc 4422 df-iom 4643 df-xp 4685 df-rel 4686 df-cnv 4687 df-co 4688 df-dm 4689 df-rn 4690 df-res 4691 df-ima 4692 df-iota 5237 df-fun 5278 df-fn 5279 df-f 5280 df-f1 5281 df-fo 5282 df-f1o 5283 df-fv 5284 df-isom 5285 df-riota 5906 df-ov 5954 df-oprab 5955 df-mpo 5956 df-1st 6233 df-2nd 6234 df-recs 6398 df-irdg 6463 df-frec 6484 df-1o 6509 df-2o 6510 df-oadd 6513 df-er 6627 df-en 6835 df-dom 6836 df-fin 6837 df-pnf 8116 df-mnf 8117 df-xr 8118 df-ltxr 8119 df-le 8120 df-sub 8252 df-neg 8253 df-reap 8655 df-ap 8662 df-div 8753 df-inn 9044 df-2 9102 df-3 9103 df-4 9104 df-n0 9303 df-z 9380 df-uz 9656 df-q 9748 df-rp 9783 df-fz 10138 df-fzo 10272 df-fl 10420 df-mod 10475 df-seqfrec 10600 df-exp 10691 df-ihash 10928 df-cj 11197 df-re 11198 df-im 11199 df-rsqrt 11353 df-abs 11354 df-clim 11634 df-sumdc 11709 df-dvds 12143 df-prm 12474

This theorem is referenced by: lgsquadlem2 15599

W3C validator