lgsquadlem1 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem1 15318

Description: Lemma for lgsquad 15321. 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 9095	. . . 4
2	1	a1i 9	. . 3
3		neg1ap0 9099	. . . 4 #
4	3	a1i 9	. . 3 #
5		lgseisen.1	. . . . . . . . . 10 $\$
6		lgsquad.4	. . . . . . . . . 10
7	5, 6	gausslemma2dlem0b 15291	. . . . . . . . 9
8	7	nnzd 9447	. . . . . . . 8
9		2nn 9152	. . . . . . . 8
10		znq 9698	. . . . . . . 8 $/\$
11	8, 9, 10	sylancl 413	. . . . . . 7
12	11	flqcld 10367	. . . . . 6
13	12	peano2zd 9451	. . . . 5
14	13, 8	fzfigd 10523	. . . 4
15		lgseisen.2	. . . . . . . . 9 $\$
16	15	gausslemma2dlem0a 15290	. . . . . . . 8
17	16	nnzd 9447	. . . . . . 7
18	5	gausslemma2dlem0a 15290	. . . . . . . 8
19	18	adantr 276	. . . . . . 7 $/\$
20		znq 9698	. . . . . . 7 $/\$
21	17, 19, 20	syl2an2r 595	. . . . . 6 $/\$
22		2z 9354	. . . . . . . 8
23		elfzelz 10100	. . . . . . . . 9
24	23	adantl 277	. . . . . . . 8 $/\$
25		zmulcl 9379	. . . . . . . 8 $/\$
26	22, 24, 25	sylancr 414	. . . . . . 7 $/\$
27		zq 9700	. . . . . . 7
28	26, 27	syl 14	. . . . . 6 $/\$
29		qmulcl 9711	. . . . . 6 $/\$
30	21, 28, 29	syl2anc 411	. . . . 5 $/\$
31	30	flqcld 10367	. . . 4 $/\$
32	14, 31	fsumzcl 11567	. . 3
33	2, 4, 32	expclzapd 10770	. 2
34		lgseisen.3	. . . . 5
35		lgsquad.5	. . . . 5
36		lgsquad.6	. . . . 5 $/\$ $/\$
37	5, 15, 34, 6, 35, 36	lgsquadlemofi 15317	. . . 4
38		hashcl 10873	. . . 4 ♯
39	37, 38	syl 14	. . 3 ♯
40		expcl 10649	. . 3 $/\$ ♯ ♯
41	1, 39, 40	sylancr 414	. 2 ♯
42	39	nn0zd 9446	. . 3 ♯
43	2, 4, 42	expap0d 10771	. 2 ♯ #
44	41, 43	recidapd 8810	. . . 4 ♯ ♯
45		1div1e1 8731	. . . . . . . . 9
46	45	negeqi 8220	. . . . . . . 8
47		ax-1cn 7972	. . . . . . . . 9
48		1ap0 8617	. . . . . . . . 9 #
49		divneg2ap 8763	. . . . . . . . 9 $/\$ $/\$ #
50	47, 47, 48, 49	mp3an 1348	. . . . . . . 8
51	46, 50	eqtr3i 2219	. . . . . . 7
52	51	oveq1i 5932	. . . . . 6 ♯ ♯
53	2, 4, 42	exprecapd 10773	. . . . . 6 ♯ ♯
54	52, 53	eqtrid 2241	. . . . 5 ♯ ♯
55	54	oveq2d 5938	. . . 4 ♯ ♯ ♯ ♯
56	5, 15, 34, 6, 35, 36	lgsquadlemsfi 15316	. . . . . . . . . . . . 13
57	56	adantr 276	. . . . . . . . . . . 12 $/\$
58		opabssxp 4737	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	36, 58	eqsstri 3215	. . . . . . . . . . . . . . . . 17
60	59	sseli 3179	. . . . . . . . . . . . . . . 16
61		xp1st 6223	. . . . . . . . . . . . . . . 16
62	60, 61	syl 14	. . . . . . . . . . . . . . 15
63	62	elfzelzd 10101	. . . . . . . . . . . . . 14
64	19	nnzd 9447	. . . . . . . . . . . . . . 15 $/\$
65	64, 26	zsubcld 9453	. . . . . . . . . . . . . 14 $/\$
66		zdceq 9401	. . . . . . . . . . . . . 14 $/\$ DECID
67	63, 65, 66	syl2anr 290	. . . . . . . . . . . . 13 $/\$ $/\$ DECID
68	67	ralrimiva 2570	. . . . . . . . . . . 12 $/\$ DECID
69	57, 68	ssfirab 6997	. . . . . . . . . . 11 $/\$
70		fveqeq2 5567	. . . . . . . . . . . . . . . . . . . 20
71	70	elrab 2920	. . . . . . . . . . . . . . . . . . 19 $/\$
72	71	simprbi 275	. . . . . . . . . . . . . . . . . 18
73	72	ad2antll 491	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	73	oveq2d 5938	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	19	nncnd 9004	. . . . . . . . . . . . . . . . . 18 $/\$
76	75	adantrr 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
77	26	zcnd 9449	. . . . . . . . . . . . . . . . . 18 $/\$
78	77	adantrr 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79	76, 78	nncand 8342	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80	74, 79	eqtrd 2229	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	80	oveq1d 5937	. . . . . . . . . . . . . 14 $/\$ $/\$
82	24	zcnd 9449	. . . . . . . . . . . . . . . 16 $/\$
83	82	adantrr 479	. . . . . . . . . . . . . . 15 $/\$ $/\$
84		2cnd 9063	. . . . . . . . . . . . . . 15 $/\$ $/\$
85		2ap0 9083	. . . . . . . . . . . . . . . 16 #
86	85	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
87	83, 84, 86	divcanap3d 8822	. . . . . . . . . . . . . 14 $/\$ $/\$
88	81, 87	eqtrd 2229	. . . . . . . . . . . . 13 $/\$ $/\$
89	88	ralrimivva 2579	. . . . . . . . . . . 12
90		invdisj 4027	. . . . . . . . . . . 12 Disj
91	89, 90	syl 14	. . . . . . . . . . 11 Disj
92	14, 69, 91	hashiun 11643	. . . . . . . . . 10 ♯ ♯
93		iunrab 3964	. . . . . . . . . . . 12
94		eldifsni 3751	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
95	5, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22
96	95	necomd 2453	. . . . . . . . . . . . . . . . . . . . 21
97	96	neneqd 2388	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		uzid 9615	. . . . . . . . . . . . . . . . . . . . 21
100	22, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
101	5	eldifad 3168	. . . . . . . . . . . . . . . . . . . . 21
102	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103		dvdsprm 12305	. . . . . . . . . . . . . . . . . . . 20 $/\$
104	100, 102, 103	sylancr 414	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
105	98, 104	mtbird 674	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
106	18	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	nncnd 9004	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	26	adantlr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
109	108	zcnd 9449	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
110	107, 109	npcand 8341	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
111	110	breq2d 4045	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	105, 111	mtbird 674	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114		dvdsmul1 11978	. . . . . . . . . . . . . . . . . . 19 $/\$
115	22, 113, 114	sylancr 414	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
117	106	nnzd 9447	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118	117, 108	zsubcld 9453	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119		dvds2add 11990	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
120	116, 118, 108, 119	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	115, 120	mpan2d 428	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
122	112, 121	mtod 664	. . . . . . . . . . . . . . . 16 $/\$ $/\$
123		breq2 4037	. . . . . . . . . . . . . . . . 17
124	123	notbid 668	. . . . . . . . . . . . . . . 16
125	122, 124	syl5ibrcom 157	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	125	rexlimdva 2614	. . . . . . . . . . . . . 14 $/\$
127		simpr 110	. . . . . . . . . . . . . . . . . 18 $/\$
128	59, 127	sselid 3181	. . . . . . . . . . . . . . . . 17 $/\$
129	128, 61	syl 14	. . . . . . . . . . . . . . . 16 $/\$
130		elfzelz 10100	. . . . . . . . . . . . . . . 16
131		odd2np1 12038	. . . . . . . . . . . . . . . 16
132	129, 130, 131	3syl 17	. . . . . . . . . . . . . . 15 $/\$
133	11	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
134	133	flqcld 10367	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
135	134	peano2zd 9451	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
136	7	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	136	nnzd 9447	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138		simprl 529	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
139	137, 138	zsubcld 9453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
140	134	zred 9448	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
141	7	nnred 9003	. . . . . . . . . . . . . . . . . . . . . 22
142	141	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
143	142	rehalfcld 9238	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
144	139	zred 9448	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
145		flqle 10368	. . . . . . . . . . . . . . . . . . . . 21
146	133, 145	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
147		zre 9330	. . . . . . . . . . . . . . . . . . . . . 22
148	147	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
149		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
150	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
151	149, 150	eqeltrd 2273	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
152		elfzle2 10103	. . . . . . . . . . . . . . . . . . . . . . . . 25
153	151, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154		zmulcl 9379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155	22, 138, 154	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156		zltp1le 9380	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
157	155, 137, 156	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
158	153, 157	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159		2re 9060	. . . . . . . . . . . . . . . . . . . . . . . . 25
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		2pos 9081	. . . . . . . . . . . . . . . . . . . . . . . . 25
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
163		ltmuldiv2 8902	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
164	148, 142, 160, 162, 163	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
165	158, 164	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
166	143	recnd 8055	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
167	7	nncnd 9004	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	167	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	168	2halvesd 9237	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170	166, 166, 169	mvlraddd 8390	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
171	165, 170	breqtrd 4059	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
172	148, 142, 143, 171	ltsub13d 8578	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	140, 143, 144, 146, 172	lelttrd 8151	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174		zltp1le 9380	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	134, 139, 174	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
176	173, 175	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
177		2t0e0 9150	. . . . . . . . . . . . . . . . . . . . 21
178		2cn 9061	. . . . . . . . . . . . . . . . . . . . . . . . 25
179		zcn 9331	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181		mulcl 8006	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
182	178, 180, 181	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
183		pncan 8232	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
184	182, 47, 183	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185		elfznn 10129	. . . . . . . . . . . . . . . . . . . . . . . 24
186		nnm1nn0 9290	. . . . . . . . . . . . . . . . . . . . . . . 24
187	151, 185, 186	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
188	184, 187	eqeltrrd 2274	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
189	188	nn0ge0d 9305	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
190	177, 189	eqbrtrid 4068	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
191		0red 8027	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
192		lemul2 8884	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
193	191, 148, 160, 162, 192	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
194	190, 193	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	142, 148	subge02d 8564	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196	194, 195	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
197	135, 137, 139, 176, 196	elfzd 10091	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
198	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		prmnn 12278	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	200	nncnd 9004	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202		peano2cn 8161	. . . . . . . . . . . . . . . . . . . 20
203	182, 202	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
204	201, 203	nncand 8342	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		1cnd 8042	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	201, 182, 205	sub32d 8369	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	201, 182, 205	subsub4d 8368	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
208		2cnd 9063	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
209	208, 168, 180	subdid 8440	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
210	6	oveq2i 5933	. . . . . . . . . . . . . . . . . . . . . . 23
211	18	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
212	211	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
213		peano2zm 9364	. . . . . . . . . . . . . . . . . . . . . . . . . 26
214	212, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
215	214	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
216	160, 162	gt0ap0d 8656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ #
217	215, 208, 216	divcanap2d 8819	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
218	210, 217	eqtrid 2241	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
219	218	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
220	209, 219	eqtr2d 2230	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
221	206, 207, 220	3eqtr3d 2237	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
222	221	oveq2d 5938	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
223	204, 222, 149	3eqtr3rd 2238	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
224		oveq2 5930	. . . . . . . . . . . . . . . . . . 19
225	224	oveq2d 5938	. . . . . . . . . . . . . . . . . 18
226	225	rspceeqv 2886	. . . . . . . . . . . . . . . . 17 $/\$
227	197, 223, 226	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
228	227	rexlimdvaa 2615	. . . . . . . . . . . . . . 15 $/\$
229	132, 228	sylbid 150	. . . . . . . . . . . . . 14 $/\$
230	126, 229	impbid 129	. . . . . . . . . . . . 13 $/\$
231	230	rabbidva 2751	. . . . . . . . . . . 12
232	93, 231	eqtrid 2241	. . . . . . . . . . 11
233	232	fveq2d 5562	. . . . . . . . . 10 ♯ ♯
234		ssrab2 3268	. . . . . . . . . . . . . . 15
235	36	relopabiv 4789	. . . . . . . . . . . . . . 15
236		relss 4750	. . . . . . . . . . . . . . 15
237	234, 235, 236	mp2 16	. . . . . . . . . . . . . 14
238		relxp 4772	. . . . . . . . . . . . . 14
239	36	eleq2i 2263	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
240		opabidw 4291	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
241	239, 240	bitri 184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
242		anass 401	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
243	31	peano2zd 9451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	243	zred 9448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
245	244	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
246	16	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . . . 26
247	246	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
248		nnre 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26
249	248	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
250		lesub 8468	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
251	245, 247, 249, 250	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
252	246	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
253	252	recnd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
254	75, 253	mulcomd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
255	77, 253	mulcomd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
256	19	nnap0d 9036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ #
257	253, 75, 256	divcanap1d 8818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
258	257	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
259	246, 18	nndivred 9040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260	259	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
261	260	recnd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
262	261, 75, 77	mul32d 8179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
263	255, 258, 262	3eqtr2d 2235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
264	254, 263	oveq12d 5940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
265	75, 77, 253	subdird 8441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	26	zred 9448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
267	260, 266	remulcld 8057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
268	267	recnd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
269	253, 268, 75	subdird 8441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
270	264, 265, 269	3eqtr4d 2239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
271	270	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
272	271	breq2d 4045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
273	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
274	247, 273	resubcld 8407	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
275	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
276	275	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
277	275	nngt0d 9034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
278		ltmul1 8619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
279	249, 274, 276, 277, 278	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
280		ltsub13 8470	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
281	249, 247, 273, 280	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
282	272, 279, 281	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
283	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
284	283	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
285		nnz 9345	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
286		zsubcl 9367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
287	284, 285, 286	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
288		flqlt 10373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
289	30, 287, 288	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
290		zltp1le 9380	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
291	31, 287, 290	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
292	282, 289, 291	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
293	35	oveq2i 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
294		peano2rem 8293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
295	252, 294	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
296	295	recnd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
297		2cnd 9063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
298	85	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ #
299	296, 297, 298	divcanap2d 8819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
300	293, 299	eqtrid 2241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
301	300	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
302		1cnd 8042	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
303	31	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
304	253, 302, 303	sub32d 8369	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
305	253, 303, 302	subsub4d 8368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
306	301, 304, 305	3eqtrd 2233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	306	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
308	307	breq2d 4045	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
309	251, 292, 308	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310	309	anbi2d 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
311	15, 35	gausslemma2dlem0b 15291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
312		nnmulcl 9011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
313	9, 311, 312	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314	313	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
315	314	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
316	311	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
317	316	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
318	31	zred 9448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
319	311	nncnd 9004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
320	319	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
321	320	2timesd 9234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
322	320, 320, 321	mvrladdd 8393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
323	252	rehalfcld 9238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
324	252	ltm1d 8959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
325	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
326	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
327		ltdiv1 8895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
328	295, 252, 325, 326, 327	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
329	324, 328	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
330	35, 329	eqbrtrid 4068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
331	317, 323, 330	ltled 8145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
332	253, 297, 75, 298	div32apd 8841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
333	141	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
334	333	rehalfcld 9238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
335	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
336	335	zred 9448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
337	24	zred 9448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
338	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
339		flqltp1 10369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
340	338, 339	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
341		elfzle1 10102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
342	341	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
343	334, 336, 337, 340, 342	ltletrd 8450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
344		ltdivmul 8903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
345	333, 337, 325, 326, 344	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
346	343, 345	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
347	6, 346	eqbrtrrid 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
348	19	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
349		peano2rem 8293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
350	348, 349	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
351		ltdivmul 8903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
352	350, 266, 325, 326, 351	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
353	347, 352	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
354		zmulcl 9379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
355	22, 26, 354	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
356		zlem1lt 9382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
357	211, 355, 356	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
358	353, 357	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
359		ledivmul 8904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
360	348, 266, 325, 326, 359	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
361	358, 360	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
362	348	rehalfcld 9238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
363	283	nngt0d 9034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
364		lemul2 8884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
365	362, 266, 252, 363, 364	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
366	361, 365	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
367	332, 366	eqbrtrd 4055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
368	252, 266	remulcld 8057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
369	19	nngt0d 9034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
370		lemuldiv 8908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
371	323, 368, 348, 369, 370	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
372	367, 371	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
373	253, 77, 75, 256	div23apd 8855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
374	372, 373	breqtrd 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
375	317, 323, 267, 331, 374	letrd 8150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
376	311	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
377	376	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
378		flqge 10372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
379	30, 377, 378	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
380	375, 379	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
381	322, 380	eqbrtrd 4055	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
382	315, 317, 318, 381	subled 8575	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
383	382	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
384	314	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
385	384, 31	zsubcld 9453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
386	385	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
387	386	zred 9448	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
388	311	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
389	388	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
390		letr 8109	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
391	249, 387, 389, 390	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 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 9453	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
401		elfzle2 10103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402	401	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
403	402, 6	breqtrdi 4074	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
404		lemuldiv2 8909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
405	337, 350, 325, 326, 404	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
406	403, 405	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
407	348	ltm1d 8959	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
408	266, 350, 348, 406, 407	lelttrd 8151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
409	266, 348	posdifd 8559	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
410	408, 409	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
411		elnnz 9336	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
412	400, 410, 411	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
413	75, 77, 302	sub32d 8369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
414	6, 6	oveq12i 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
415	64, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
416	415	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
417	416	2halvesd 9237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
418	414, 417	eqtrid 2241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
419	418	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
420	167	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
421	420, 420	pncan2d 8339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
422	419, 421	eqtr3d 2231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
423	422, 346	eqbrtrd 4055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
424	350, 333, 266, 423	ltsub23d 8577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
425	413, 424	eqbrtrd 4055	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
426	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
427	426	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
428		zlem1lt 9382	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
429	400, 427, 428	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
430	425, 429	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
431		fznn 10164	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
432	427, 431	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
433	412, 430, 432	mpbir2and 946	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
434	433	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
435	398, 434	eqeltrd 2273	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
436	435	biantrurd 305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
437	376	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
438		fznn 10164	. . . . . . . . . . . . . . . . . . . . 21 $/\$
439	437, 438	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
440	436, 439	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
441	398	oveq1d 5937	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
442	441	breq2d 4045	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
443	440, 442	anbi12d 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
444	385	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
445		fznn 10164	. . . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . . . . 19
451		vex 2766	. . . . . . . . . . . . . . . . . . 19
452	450, 451	op1std 6206	. . . . . . . . . . . . . . . . . 18
453	452	eqeq1d 2205	. . . . . . . . . . . . . . . . 17
454	453	elrab 2920	. . . . . . . . . . . . . . . 16 $/\$
455	454	biancomi 270	. . . . . . . . . . . . . . 15 $/\$
456		opelxp 4693	. . . . . . . . . . . . . . . 16 $/\$
457		velsn 3639	. . . . . . . . . . . . . . . . 17
458	457	anbi1i 458	. . . . . . . . . . . . . . . 16 $/\$ $/\$
459	456, 458	bitri 184	. . . . . . . . . . . . . . 15 $/\$
460	449, 455, 459	3bitr4g 223	. . . . . . . . . . . . . 14 $/\$
461	237, 238, 460	eqrelrdv 4759	. . . . . . . . . . . . 13 $/\$
462	461	fveq2d 5562	. . . . . . . . . . . 12 $/\$ ♯ ♯
463		1zzd 9353	. . . . . . . . . . . . . . 15 $/\$
464	463, 385	fzfigd 10523	. . . . . . . . . . . . . 14 $/\$
465		xpsnen2g 6888	. . . . . . . . . . . . . 14 $/\$
466	400, 464, 465	syl2anc 411	. . . . . . . . . . . . 13 $/\$
467	461, 69	eqeltrrd 2274	. . . . . . . . . . . . . 14 $/\$
468		hashen 10876	. . . . . . . . . . . . . 14 $/\$ ♯ ♯
469	467, 464, 468	syl2anc 411	. . . . . . . . . . . . 13 $/\$ ♯ ♯
470	466, 469	mpbird 167	. . . . . . . . . . . 12 $/\$ ♯ ♯
471		ltmul2 8883	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
472	266, 348, 252, 363, 471	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$
473	408, 472	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$
474		ltdivmul2 8905	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
475	368, 252, 348, 369, 474	syl112anc 1253	. . . . . . . . . . . . . . . . . . 19 $/\$
476	473, 475	mpbird 167	. . . . . . . . . . . . . . . . . 18 $/\$
477	373, 476	eqbrtrrd 4057	. . . . . . . . . . . . . . . . 17 $/\$
478		flqlt 10373	. . . . . . . . . . . . . . . . . 18 $/\$
479	30, 284, 478	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$
480	477, 479	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$
481		zltlem1 9383	. . . . . . . . . . . . . . . . 17 $/\$
482	31, 284, 481	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$
483	480, 482	mpbid 147	. . . . . . . . . . . . . . 15 $/\$
484	483, 300	breqtrrd 4061	. . . . . . . . . . . . . 14 $/\$
485		eluz2 9607	. . . . . . . . . . . . . 14 $/\$ $/\$
486	31, 384, 484, 485	syl3anbrc 1183	. . . . . . . . . . . . 13 $/\$
487		uznn0sub 9633	. . . . . . . . . . . . 13
488		hashfz1 10875	. . . . . . . . . . . . 13 ♯
489	486, 487, 488	3syl 17	. . . . . . . . . . . 12 $/\$ ♯
490	462, 470, 489	3eqtrd 2233	. . . . . . . . . . 11 $/\$ ♯
491	490	sumeq2dv 11533	. . . . . . . . . 10 ♯
492	92, 233, 491	3eqtr3rd 2238	. . . . . . . . 9 ♯
493	313	nncnd 9004	. . . . . . . . . . 11
494	493	adantr 276	. . . . . . . . . 10 $/\$
495	14, 494, 303	fsumsub 11617	. . . . . . . . 9
496	492, 495	eqtr3d 2231	. . . . . . . 8 ♯
497	496	oveq2d 5938	. . . . . . 7 ♯
498	32	zcnd 9449	. . . . . . . 8
499	14, 384	fsumzcl 11567	. . . . . . . . 9
500	499	zcnd 9449	. . . . . . . 8
501	498, 500	pncan3d 8340	. . . . . . 7
502		fsumconst 11619	. . . . . . . . 9 $/\$ ♯
503	14, 493, 502	syl2anc 411	. . . . . . . 8 ♯
504		hashcl 10873	. . . . . . . . . . 11 ♯
505	14, 504	syl 14	. . . . . . . . . 10 ♯
506	505	nn0cnd 9304	. . . . . . . . 9 ♯
507		2cnd 9063	. . . . . . . . 9
508	506, 507, 319	mul12d 8178	. . . . . . . 8 ♯ ♯
509	503, 508	eqtrd 2229	. . . . . . 7 ♯
510	497, 501, 509	3eqtrd 2233	. . . . . 6 ♯ ♯
511	510	oveq2d 5938	. . . . 5 ♯ ♯
512	22	a1i 9	. . . . . 6
513	505	nn0zd 9446	. . . . . . 7 ♯
514	513, 376	zmulcld 9454	. . . . . 6 ♯
515		expmulzap 10677	. . . . . 6 $/\$ # $/\$ $/\$ ♯ ♯ ♯
516	2, 4, 512, 514, 515	syl22anc 1250	. . . . 5 ♯ ♯
517		neg1sqe1 10726	. . . . . . 7
518	517	oveq1i 5932	. . . . . 6 ♯ ♯
519		1exp 10660	. . . . . . 7 ♯ ♯
520	514, 519	syl 14	. . . . . 6 ♯
521	518, 520	eqtrid 2241	. . . . 5 ♯
522	511, 516, 521	3eqtrd 2233	. . . 4 ♯
523	44, 55, 522	3eqtr4d 2239	. . 3 ♯ ♯ ♯
524		expaddzap 10675	. . . 4 $/\$ # $/\$ $/\$ ♯ ♯ ♯
525	2, 4, 32, 42, 524	syl22anc 1250	. . 3 ♯ ♯
526	523, 525	eqtr2d 2230	. 2 ♯ ♯ ♯
527	33, 41, 41, 43, 526	mulcanap2ad 8691	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 DECID wdc 835

wceq 1364

wcel 2167

wne 2367

wral 2475

wrex 2476

crab 2479 $\$ cdif 3154

wss 3157

csn 3622

cop 3625

ciun 3916 Disj wdisj 4010 class class class wbr 4033

copab 4093

cxp 4661

wrel 4668

cfv 5258 (class class class)co 5922

c1st 6196

cen 6797

cfn 6799

cc 7877

cr 7878

cc0 7879

c1 7880

caddc 7882

cmul 7884

clt 8061

cle 8062

cmin 8197

cneg 8198 # cap 8608

cdiv 8699

cn 8990

c2 9041

cn0 9249

cz 9326

cuz 9601

cq 9693

cfz 10083

cfl 10358

cexp 10630 ♯chash 10867

csu 11518

cdvds 11952

cprime 12275

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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-disj 4011 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-irdg 6428 df-frec 6449 df-1o 6474 df-2o 6475 df-oadd 6478 df-er 6592 df-en 6800 df-dom 6801 df-fin 6802 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-ihash 10868 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-clim 11444 df-sumdc 11519 df-dvds 11953 df-prm 12276

This theorem is referenced by: lgsquadlem2 15319

W3C validator