lgsquadlem1 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem1 16208

Description: Lemma for lgsquad 16211. 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 9410	. . . 4
2	1	a1i 9	. . 3
3		neg1ap0 9414	. . . 4 #
4	3	a1i 9	. . 3 #
5		lgseisen.1	. . . . . . . . . 10 $\$
6		lgsquad.4	. . . . . . . . . 10
7	5, 6	gausslemma2dlem0b 16181	. . . . . . . . 9
8	7	nnzd 9769	. . . . . . . 8
9		2nn 9468	. . . . . . . 8
10		znq 10026	. . . . . . . 8 $/\$
11	8, 9, 10	sylancl 417	. . . . . . 7
12	11	flqcld 10714	. . . . . 6
13	12	peano2zd 9773	. . . . 5
14	13, 8	fzfigd 10870	. . . 4
15		lgseisen.2	. . . . . . . . 9 $\$
16	15	gausslemma2dlem0a 16180	. . . . . . . 8
17	16	nnzd 9769	. . . . . . 7
18	5	gausslemma2dlem0a 16180	. . . . . . . 8
19	18	adantr 276	. . . . . . 7 $/\$
20		znq 10026	. . . . . . 7 $/\$
21	17, 19, 20	syl2an2r 603	. . . . . 6 $/\$
22		2z 9674	. . . . . . . 8
23		elfzelz 10430	. . . . . . . . 9
24	23	adantl 277	. . . . . . . 8 $/\$
25		zmulcl 9700	. . . . . . . 8 $/\$
26	22, 24, 25	sylancr 418	. . . . . . 7 $/\$
27		zq 10028	. . . . . . 7
28	26, 27	syl 14	. . . . . 6 $/\$
29		qmulcl 10039	. . . . . 6 $/\$
30	21, 28, 29	syl2anc 415	. . . . 5 $/\$
31	30	flqcld 10714	. . . 4 $/\$
32	14, 31	fsumzcl 12171	. . 3
33	2, 4, 32	expclzapd 11118	. 2
34		lgseisen.3	. . . . 5
35		lgsquad.5	. . . . 5
36		lgsquad.6	. . . . 5 $/\$ $/\$
37	5, 15, 34, 6, 35, 36	lgsquadlemofi 16207	. . . 4
38		hashcl 11222	. . . 4 ♯
39	37, 38	syl 14	. . 3 ♯
40		expcl 10996	. . 3 $/\$ ♯ ♯
41	1, 39, 40	sylancr 418	. 2 ♯
42	39	nn0zd 9768	. . 3 ♯
43	2, 4, 42	expap0d 11119	. 2 ♯ #
44	41, 43	recidapd 9114	. . . 4 ♯ ♯
45		1div1e1 9035	. . . . . . . . 9
46	45	negeqi 8520	. . . . . . . 8
47		ax-1cn 8272	. . . . . . . . 9
48		1ap0 8919	. . . . . . . . 9 #
49		divneg2ap 9067	. . . . . . . . 9 $/\$ $/\$ #
50	47, 47, 48, 49	mp3an 1378	. . . . . . . 8
51	46, 50	eqtr3i 2261	. . . . . . 7
52	51	oveq1i 6095	. . . . . 6 ♯ ♯
53	2, 4, 42	exprecapd 11121	. . . . . 6 ♯ ♯
54	52, 53	eqtrid 2283	. . . . 5 ♯ ♯
55	54	oveq2d 6101	. . . 4 ♯ ♯ ♯ ♯
56	5, 15, 34, 6, 35, 36	lgsquadlemsfi 16206	. . . . . . . . . . . . 13
57	56	adantr 276	. . . . . . . . . . . 12 $/\$
58		opabssxp 4849	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	36, 58	eqsstri 3280	. . . . . . . . . . . . . . . . 17
60	59	sseli 3244	. . . . . . . . . . . . . . . 16
61		xp1st 6399	. . . . . . . . . . . . . . . 16
62	60, 61	syl 14	. . . . . . . . . . . . . . 15
63	62	elfzelzd 10431	. . . . . . . . . . . . . 14
64	19	nnzd 9769	. . . . . . . . . . . . . . 15 $/\$
65	64, 26	zsubcld 9775	. . . . . . . . . . . . . 14 $/\$
66		zdceq 9722	. . . . . . . . . . . . . 14 $/\$ DECID
67	63, 65, 66	syl2anr 290	. . . . . . . . . . . . 13 $/\$ $/\$ DECID
68	67	ralrimiva 2623	. . . . . . . . . . . 12 $/\$ DECID
69	57, 68	ssfirab 7244	. . . . . . . . . . 11 $/\$
70		fveqeq2 5704	. . . . . . . . . . . . . . . . . . . 20
71	70	elrab 2982	. . . . . . . . . . . . . . . . . . 19 $/\$
72	71	simprbi 275	. . . . . . . . . . . . . . . . . 18
73	72	ad2antll 495	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	73	oveq2d 6101	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	19	nncnd 9319	. . . . . . . . . . . . . . . . . 18 $/\$
76	75	adantrr 483	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
77	26	zcnd 9771	. . . . . . . . . . . . . . . . . 18 $/\$
78	77	adantrr 483	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79	76, 78	nncand 8642	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80	74, 79	eqtrd 2271	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	80	oveq1d 6100	. . . . . . . . . . . . . 14 $/\$ $/\$
82	24	zcnd 9771	. . . . . . . . . . . . . . . 16 $/\$
83	82	adantrr 483	. . . . . . . . . . . . . . 15 $/\$ $/\$
84		2cnd 9378	. . . . . . . . . . . . . . 15 $/\$ $/\$
85		2ap0 9398	. . . . . . . . . . . . . . . 16 #
86	85	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
87	83, 84, 86	divcanap3d 9126	. . . . . . . . . . . . . 14 $/\$ $/\$
88	81, 87	eqtrd 2271	. . . . . . . . . . . . 13 $/\$ $/\$
89	88	ralrimivva 2632	. . . . . . . . . . . 12
90		invdisj 4123	. . . . . . . . . . . 12 Disj
91	89, 90	syl 14	. . . . . . . . . . 11 Disj
92	14, 69, 91	hashiun 12247	. . . . . . . . . 10 ♯ ♯
93		iunrab 4060	. . . . . . . . . . . 12
94		eldifsni 3843	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
95	5, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22
96	95	necomd 2506	. . . . . . . . . . . . . . . . . . . . 21
97	96	neneqd 2441	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		uzid 9938	. . . . . . . . . . . . . . . . . . . . 21
100	22, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
101	5	eldifad 3231	. . . . . . . . . . . . . . . . . . . . 21
102	101	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103		dvdsprm 12917	. . . . . . . . . . . . . . . . . . . 20 $/\$
104	100, 102, 103	sylancr 418	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
105	98, 104	mtbird 684	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
106	18	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	nncnd 9319	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	26	adantlr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
109	108	zcnd 9771	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
110	107, 109	npcand 8641	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
111	110	breq2d 4142	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	105, 111	mtbird 684	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114		dvdsmul1 12582	. . . . . . . . . . . . . . . . . . 19 $/\$
115	22, 113, 114	sylancr 418	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
117	106	nnzd 9769	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118	117, 108	zsubcld 9775	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119		dvds2add 12594	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
120	116, 118, 108, 119	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	115, 120	mpan2d 432	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
122	112, 121	mtod 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$
123		breq2 4134	. . . . . . . . . . . . . . . . 17
124	123	notbid 677	. . . . . . . . . . . . . . . 16
125	122, 124	syl5ibrcom 157	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	125	rexlimdva 2668	. . . . . . . . . . . . . 14 $/\$
127		simpr 110	. . . . . . . . . . . . . . . . . 18 $/\$
128	59, 127	sselid 3246	. . . . . . . . . . . . . . . . 17 $/\$
129	128, 61	syl 14	. . . . . . . . . . . . . . . 16 $/\$
130		elfzelz 10430	. . . . . . . . . . . . . . . 16
131		odd2np1 12642	. . . . . . . . . . . . . . . 16
132	129, 130, 131	3syl 17	. . . . . . . . . . . . . . 15 $/\$
133	11	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
134	133	flqcld 10714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
135	134	peano2zd 9773	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
136	7	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	136	nnzd 9769	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138		simprl 535	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
139	137, 138	zsubcld 9775	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
140	134	zred 9770	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
141	7	nnred 9318	. . . . . . . . . . . . . . . . . . . . . 22
142	141	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
143	142	rehalfcld 9554	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
144	139	zred 9770	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
145		flqle 10715	. . . . . . . . . . . . . . . . . . . . 21
146	133, 145	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
147		zre 9650	. . . . . . . . . . . . . . . . . . . . . 22
148	147	ad2antrl 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
149		simprr 537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
150	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
151	149, 150	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
152		elfzle2 10434	. . . . . . . . . . . . . . . . . . . . . . . . 25
153	151, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154		zmulcl 9700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155	22, 138, 154	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156		zltp1le 9701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
157	155, 137, 156	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
158	153, 157	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159		2re 9375	. . . . . . . . . . . . . . . . . . . . . . . . 25
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		2pos 9396	. . . . . . . . . . . . . . . . . . . . . . . . 25
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
163		ltmuldiv2 9206	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
164	148, 142, 160, 162, 163	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
165	158, 164	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
166	143	recnd 8354	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
167	7	nncnd 9319	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	167	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	168	2halvesd 9553	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170	166, 166, 169	mvlraddd 8690	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
171	165, 170	breqtrd 4156	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
172	148, 142, 143, 171	ltsub13d 8879	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	140, 143, 144, 146, 172	lelttrd 8451	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174		zltp1le 9701	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	134, 139, 174	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
176	173, 175	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
177		2t0e0 9466	. . . . . . . . . . . . . . . . . . . . 21
178		2cn 9376	. . . . . . . . . . . . . . . . . . . . . . . . 25
179		zcn 9651	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	ad2antrl 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181		mulcl 8306	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
182	178, 180, 181	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
183		pncan 8532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
184	182, 47, 183	sylancl 417	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185		elfznn 10462	. . . . . . . . . . . . . . . . . . . . . . . 24
186		nnm1nn0 9606	. . . . . . . . . . . . . . . . . . . . . . . 24
187	151, 185, 186	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
188	184, 187	eqeltrrd 2316	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
189	188	nn0ge0d 9625	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
190	177, 189	eqbrtrid 4165	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
191		0red 8327	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
192		lemul2 9188	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
193	191, 148, 160, 162, 192	syl112anc 1282	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
194	190, 193	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	142, 148	subge02d 8865	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196	194, 195	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
197	135, 137, 139, 176, 196	elfzd 10421	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
198	101	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		prmnn 12890	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	200	nncnd 9319	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202		peano2cn 8461	. . . . . . . . . . . . . . . . . . . 20
203	182, 202	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
204	201, 203	nncand 8642	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		1cnd 8342	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	201, 182, 205	sub32d 8669	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	201, 182, 205	subsub4d 8668	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
208		2cnd 9378	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
209	208, 168, 180	subdid 8741	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
210	6	oveq2i 6096	. . . . . . . . . . . . . . . . . . . . . . 23
211	18	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
212	211	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
213		peano2zm 9684	. . . . . . . . . . . . . . . . . . . . . . . . . 26
214	212, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
215	214	zcnd 9771	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
216	160, 162	gt0ap0d 8958	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ #
217	215, 208, 216	divcanap2d 9123	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
218	210, 217	eqtrid 2283	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
219	218	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
220	209, 219	eqtr2d 2272	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
221	206, 207, 220	3eqtr3d 2279	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
222	221	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
223	204, 222, 149	3eqtr3rd 2280	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
224		oveq2 6093	. . . . . . . . . . . . . . . . . . 19
225	224	oveq2d 6101	. . . . . . . . . . . . . . . . . 18
226	225	rspceeqv 2948	. . . . . . . . . . . . . . . . 17 $/\$
227	197, 223, 226	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
228	227	rexlimdvaa 2669	. . . . . . . . . . . . . . 15 $/\$
229	132, 228	sylbid 150	. . . . . . . . . . . . . 14 $/\$
230	126, 229	impbid 129	. . . . . . . . . . . . 13 $/\$
231	230	rabbidva 2809	. . . . . . . . . . . 12
232	93, 231	eqtrid 2283	. . . . . . . . . . 11
233	232	fveq2d 5699	. . . . . . . . . 10 ♯ ♯
234		ssrab2 3333	. . . . . . . . . . . . . . 15
235	36	relopabiv 4903	. . . . . . . . . . . . . . 15
236		relss 4862	. . . . . . . . . . . . . . 15
237	234, 235, 236	mp2 16	. . . . . . . . . . . . . 14
238		relxp 4884	. . . . . . . . . . . . . 14
239	36	eleq2i 2305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
240		opabidw 4399	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
241	239, 240	bitri 184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
242		anass 405	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
243	31	peano2zd 9773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	243	zred 9770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
245	244	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
246	16	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . 26
247	246	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
248		nnre 9312	. . . . . . . . . . . . . . . . . . . . . . . . . 26
249	248	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
250		lesub 8769	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
251	245, 247, 249, 250	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
252	246	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
253	252	recnd 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
254	75, 253	mulcomd 8347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
255	77, 253	mulcomd 8347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
256	19	nnap0d 9351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ #
257	253, 75, 256	divcanap1d 9122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
258	257	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
259	246, 18	nndivred 9355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260	259	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
261	260	recnd 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
262	261, 75, 77	mul32d 8479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
263	255, 258, 262	3eqtr2d 2277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
264	254, 263	oveq12d 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
265	75, 77, 253	subdird 8742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	26	zred 9770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
267	260, 266	remulcld 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
268	267	recnd 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
269	253, 268, 75	subdird 8742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
270	264, 265, 269	3eqtr4d 2281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
271	270	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
272	271	breq2d 4142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
273	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
274	247, 273	resubcld 8708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
275	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
276	275	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
277	275	nngt0d 9349	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
278		ltmul1 8921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
279	249, 274, 276, 277, 278	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
280		ltsub13 8771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
281	249, 247, 273, 280	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
282	272, 279, 281	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
283	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
284	283	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
285		nnz 9665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
286		zsubcl 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
287	284, 285, 286	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
288		flqlt 10720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
289	30, 287, 288	syl2an2r 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
290		zltp1le 9701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
291	31, 287, 290	syl2an2r 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
292	282, 289, 291	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
293	35	oveq2i 6096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
294		peano2rem 8593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
295	252, 294	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
296	295	recnd 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
297		2cnd 9378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
298	85	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ #
299	296, 297, 298	divcanap2d 9123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
300	293, 299	eqtrid 2283	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
301	300	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
302		1cnd 8342	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
303	31	zcnd 9771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
304	253, 302, 303	sub32d 8669	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
305	253, 303, 302	subsub4d 8668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
306	301, 304, 305	3eqtrd 2275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	306	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
308	307	breq2d 4142	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
309	251, 292, 308	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310	309	anbi2d 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
311	15, 35	gausslemma2dlem0b 16181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
312		nnmulcl 9326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
313	9, 311, 312	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314	313	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
315	314	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
316	311	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
317	316	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
318	31	zred 9770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
319	311	nncnd 9319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
320	319	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
321	320	2timesd 9550	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
322	320, 320, 321	mvrladdd 8693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
323	252	rehalfcld 9554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
324	252	ltm1d 9263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
325	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
326	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
327		ltdiv1 9199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
328	295, 252, 325, 326, 327	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
329	324, 328	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
330	35, 329	eqbrtrid 4165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
331	317, 323, 330	ltled 8445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
332	253, 297, 75, 298	div32apd 9145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
333	141	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
334	333	rehalfcld 9554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
335	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
336	335	zred 9770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
337	24	zred 9770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
338	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
339		flqltp1 10716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
340	338, 339	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
341		elfzle1 10433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
342	341	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
343	334, 336, 337, 340, 342	ltletrd 8751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
344		ltdivmul 9207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
345	333, 337, 325, 326, 344	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
346	343, 345	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
347	6, 346	eqbrtrrid 4166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
348	19	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
349		peano2rem 8593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
350	348, 349	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
351		ltdivmul 9207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
352	350, 266, 325, 326, 351	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
353	347, 352	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
354		zmulcl 9700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
355	22, 26, 354	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
356		zlem1lt 9703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
357	211, 355, 356	syl2an2r 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
358	353, 357	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
359		ledivmul 9208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
360	348, 266, 325, 326, 359	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
361	358, 360	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
362	348	rehalfcld 9554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
363	283	nngt0d 9349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
364		lemul2 9188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
365	362, 266, 252, 363, 364	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
366	361, 365	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
367	332, 366	eqbrtrd 4152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
368	252, 266	remulcld 8356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
369	19	nngt0d 9349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
370		lemuldiv 9212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
371	323, 368, 348, 369, 370	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
372	367, 371	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
373	253, 77, 75, 256	div23apd 9159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
374	372, 373	breqtrd 4156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
375	317, 323, 267, 331, 374	letrd 8450	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
376	311	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
377	376	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
378		flqge 10719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
379	30, 377, 378	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
380	375, 379	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
381	322, 380	eqbrtrd 4152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
382	315, 317, 318, 381	subled 8876	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
383	382	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
384	314	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
385	384, 31	zsubcld 9775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
386	385	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
387	386	zred 9770	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
388	311	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
389	388	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
390		letr 8408	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
391	249, 387, 389, 390	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
392	383, 391	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
393	392	pm4.71rd 398	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
394	310, 393	bitr4d 191	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
395	394	pm5.32da 456	. . . . . . . . . . . . . . . . . . . 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 9775	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
401		elfzle2 10434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402	401	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
403	402, 6	breqtrdi 4171	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
404		lemuldiv2 9213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
405	337, 350, 325, 326, 404	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
406	403, 405	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
407	348	ltm1d 9263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
408	266, 350, 348, 406, 407	lelttrd 8451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
409	266, 348	posdifd 8860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
410	408, 409	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
411		elnnz 9656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
412	400, 410, 411	sylanbrc 421	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
413	75, 77, 302	sub32d 8669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
414	6, 6	oveq12i 6097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
415	64, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
416	415	zcnd 9771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
417	416	2halvesd 9553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
418	414, 417	eqtrid 2283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
419	418	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
420	167	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
421	420, 420	pncan2d 8639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
422	419, 421	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
423	422, 346	eqbrtrd 4152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
424	350, 333, 266, 423	ltsub23d 8878	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
425	413, 424	eqbrtrd 4152	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
426	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
427	426	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
428		zlem1lt 9703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
429	400, 427, 428	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
430	425, 429	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
431		fznn 10498	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
432	427, 431	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
433	412, 430, 432	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
434	433	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
435	398, 434	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
436	435	biantrurd 305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
437	376	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
438		fznn 10498	. . . . . . . . . . . . . . . . . . . . 21 $/\$
439	437, 438	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
440	436, 439	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
441	398	oveq1d 6100	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
442	441	breq2d 4142	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
443	440, 442	anbi12d 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
444	385	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
445		fznn 10498	. . . . . . . . . . . . . . . . . . 19 $/\$
446	444, 445	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
447	397, 443, 446	3bitr4d 220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
448	241, 447	bitrid 192	. . . . . . . . . . . . . . . 16 $/\$ $/\$
449	448	pm5.32da 456	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
450		vex 2824	. . . . . . . . . . . . . . . . . . 19
451		vex 2824	. . . . . . . . . . . . . . . . . . 19
452	450, 451	op1std 6382	. . . . . . . . . . . . . . . . . 18
453	452	eqeq1d 2247	. . . . . . . . . . . . . . . . 17
454	453	elrab 2982	. . . . . . . . . . . . . . . 16 $/\$
455	454	biancomi 270	. . . . . . . . . . . . . . 15 $/\$
456		opelxp 4804	. . . . . . . . . . . . . . . 16 $/\$
457		velsn 3726	. . . . . . . . . . . . . . . . 17
458	457	anbi1i 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$
459	456, 458	bitri 184	. . . . . . . . . . . . . . 15 $/\$
460	449, 455, 459	3bitr4g 223	. . . . . . . . . . . . . 14 $/\$
461	237, 238, 460	eqrelrdv 4871	. . . . . . . . . . . . 13 $/\$
462	461	fveq2d 5699	. . . . . . . . . . . 12 $/\$ ♯ ♯
463		1zzd 9673	. . . . . . . . . . . . . . 15 $/\$
464	463, 385	fzfigd 10870	. . . . . . . . . . . . . 14 $/\$
465		xpsnen2g 7127	. . . . . . . . . . . . . 14 $/\$
466	400, 464, 465	syl2anc 415	. . . . . . . . . . . . 13 $/\$
467	461, 69	eqeltrrd 2316	. . . . . . . . . . . . . 14 $/\$
468		hashen 11225	. . . . . . . . . . . . . 14 $/\$ ♯ ♯
469	467, 464, 468	syl2anc 415	. . . . . . . . . . . . 13 $/\$ ♯ ♯
470	466, 469	mpbird 167	. . . . . . . . . . . 12 $/\$ ♯ ♯
471		ltmul2 9187	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
472	266, 348, 252, 363, 471	syl112anc 1282	. . . . . . . . . . . . . . . . . . . 20 $/\$
473	408, 472	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$
474		ltdivmul2 9209	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
475	368, 252, 348, 369, 474	syl112anc 1282	. . . . . . . . . . . . . . . . . . 19 $/\$
476	473, 475	mpbird 167	. . . . . . . . . . . . . . . . . 18 $/\$
477	373, 476	eqbrtrrd 4154	. . . . . . . . . . . . . . . . 17 $/\$
478		flqlt 10720	. . . . . . . . . . . . . . . . . 18 $/\$
479	30, 284, 478	syl2anc 415	. . . . . . . . . . . . . . . . 17 $/\$
480	477, 479	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$
481		zltlem1 9704	. . . . . . . . . . . . . . . . 17 $/\$
482	31, 284, 481	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$
483	480, 482	mpbid 147	. . . . . . . . . . . . . . 15 $/\$
484	483, 300	breqtrrd 4158	. . . . . . . . . . . . . 14 $/\$
485		eluz2 9929	. . . . . . . . . . . . . 14 $/\$ $/\$
486	31, 384, 484, 485	syl3anbrc 1212	. . . . . . . . . . . . 13 $/\$
487		uznn0sub 9956	. . . . . . . . . . . . 13
488		hashfz1 11224	. . . . . . . . . . . . 13 ♯
489	486, 487, 488	3syl 17	. . . . . . . . . . . 12 $/\$ ♯
490	462, 470, 489	3eqtrd 2275	. . . . . . . . . . 11 $/\$ ♯
491	490	sumeq2dv 12136	. . . . . . . . . 10 ♯
492	92, 233, 491	3eqtr3rd 2280	. . . . . . . . 9 ♯
493	313	nncnd 9319	. . . . . . . . . . 11
494	493	adantr 276	. . . . . . . . . 10 $/\$
495	14, 494, 303	fsumsub 12221	. . . . . . . . 9
496	492, 495	eqtr3d 2273	. . . . . . . 8 ♯
497	496	oveq2d 6101	. . . . . . 7 ♯
498	32	zcnd 9771	. . . . . . . 8
499	14, 384	fsumzcl 12171	. . . . . . . . 9
500	499	zcnd 9771	. . . . . . . 8
501	498, 500	pncan3d 8640	. . . . . . 7
502		fsumconst 12223	. . . . . . . . 9 $/\$ ♯
503	14, 493, 502	syl2anc 415	. . . . . . . 8 ♯
504		hashcl 11222	. . . . . . . . . . 11 ♯
505	14, 504	syl 14	. . . . . . . . . 10 ♯
506	505	nn0cnd 9624	. . . . . . . . 9 ♯
507		2cnd 9378	. . . . . . . . 9
508	506, 507, 319	mul12d 8478	. . . . . . . 8 ♯ ♯
509	503, 508	eqtrd 2271	. . . . . . 7 ♯
510	497, 501, 509	3eqtrd 2275	. . . . . 6 ♯ ♯
511	510	oveq2d 6101	. . . . 5 ♯ ♯
512	22	a1i 9	. . . . . 6
513	505	nn0zd 9768	. . . . . . 7 ♯
514	513, 376	zmulcld 9776	. . . . . 6 ♯
515		expmulzap 11024	. . . . . 6 $/\$ # $/\$ $/\$ ♯ ♯ ♯
516	2, 4, 512, 514, 515	syl22anc 1279	. . . . 5 ♯ ♯
517		neg1sqe1 11073	. . . . . . 7
518	517	oveq1i 6095	. . . . . 6 ♯ ♯
519		1exp 11007	. . . . . . 7 ♯ ♯
520	514, 519	syl 14	. . . . . 6 ♯
521	518, 520	eqtrid 2283	. . . . 5 ♯
522	511, 516, 521	3eqtrd 2275	. . . 4 ♯
523	44, 55, 522	3eqtr4d 2281	. . 3 ♯ ♯ ♯
524		expaddzap 11022	. . . 4 $/\$ # $/\$ $/\$ ♯ ♯ ♯
525	2, 4, 32, 42, 524	syl22anc 1279	. . 3 ♯ ♯
526	523, 525	eqtr2d 2272	. 2 ♯ ♯ ♯
527	33, 41, 41, 43, 526	mulcanap2ad 8993	1 ♯

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104

wb 105 DECID wdc 846

wceq 1402

wcel 2209

wne 2420

wral 2528

wrex 2529

crab 2532 $\$ cdif 3217

wss 3220

csn 3709

cop 3712

ciun 4012 Disj wdisj 4106 class class class wbr 4130

copab 4191

cxp 4772

wrel 4779

cfv 5377 (class class class)co 6085

c1st 6372

cen 7020

cfn 7022

cc 8177

cr 8178

cc0 8179

c1 8180

caddc 8182

cmul 8184

clt 8360

cle 8361

cmin 8497

cneg 8498 # cap 8910

cdiv 9003

cn 9305

c2 9356

cn0 9565

cz 9646

cuz 9923

cq 10021

cfz 10413

cfl 10705

cexp 10977 ♯chash 11216

csu 12121

cdvds 12556

cprime 12887

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-xor 1425 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8904 df-ap 8911 df-div 9004 df-inn 9306 df-2 9364 df-3 9365 df-4 9366 df-n0 9566 df-z 9647 df-uz 9924 df-q 10022 df-rp 10057 df-fz 10414 df-fzo 10552 df-fl 10707 df-mod 10762 df-seqfrec 10887 df-exp 10978 df-ihash 11217 df-cj 11609 df-re 11610 df-im 11611 df-rsqrt 11766 df-abs 11767 df-clim 12047 df-sumdc 12122 df-dvds 12557 df-prm 12888

This theorem is used by: lgsquadlem2 16209

W3C validator