lgsquadlem1 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem1 16179

Description: Lemma for lgsquad 16182. 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 9392	. . . 4
2	1	a1i 9	. . 3
3		neg1ap0 9396	. . . 4 #
4	3	a1i 9	. . 3 #
5		lgseisen.1	. . . . . . . . . 10 $\$
6		lgsquad.4	. . . . . . . . . 10
7	5, 6	gausslemma2dlem0b 16152	. . . . . . . . 9
8	7	nnzd 9750	. . . . . . . 8
9		2nn 9449	. . . . . . . 8
10		znq 10007	. . . . . . . 8 $/\$
11	8, 9, 10	sylancl 417	. . . . . . 7
12	11	flqcld 10695	. . . . . 6
13	12	peano2zd 9754	. . . . 5
14	13, 8	fzfigd 10851	. . . 4
15		lgseisen.2	. . . . . . . . 9 $\$
16	15	gausslemma2dlem0a 16151	. . . . . . . 8
17	16	nnzd 9750	. . . . . . 7
18	5	gausslemma2dlem0a 16151	. . . . . . . 8
19	18	adantr 276	. . . . . . 7 $/\$
20		znq 10007	. . . . . . 7 $/\$
21	17, 19, 20	syl2an2r 603	. . . . . 6 $/\$
22		2z 9655	. . . . . . . 8
23		elfzelz 10411	. . . . . . . . 9
24	23	adantl 277	. . . . . . . 8 $/\$
25		zmulcl 9681	. . . . . . . 8 $/\$
26	22, 24, 25	sylancr 418	. . . . . . 7 $/\$
27		zq 10009	. . . . . . 7
28	26, 27	syl 14	. . . . . 6 $/\$
29		qmulcl 10020	. . . . . 6 $/\$
30	21, 28, 29	syl2anc 415	. . . . 5 $/\$
31	30	flqcld 10695	. . . 4 $/\$
32	14, 31	fsumzcl 12152	. . 3
33	2, 4, 32	expclzapd 11099	. 2
34		lgseisen.3	. . . . 5
35		lgsquad.5	. . . . 5
36		lgsquad.6	. . . . 5 $/\$ $/\$
37	5, 15, 34, 6, 35, 36	lgsquadlemofi 16178	. . . 4
38		hashcl 11203	. . . 4 ♯
39	37, 38	syl 14	. . 3 ♯
40		expcl 10977	. . 3 $/\$ ♯ ♯
41	1, 39, 40	sylancr 418	. 2 ♯
42	39	nn0zd 9749	. . 3 ♯
43	2, 4, 42	expap0d 11100	. 2 ♯ #
44	41, 43	recidapd 9107	. . . 4 ♯ ♯
45		1div1e1 9028	. . . . . . . . 9
46	45	negeqi 8514	. . . . . . . 8
47		ax-1cn 8266	. . . . . . . . 9
48		1ap0 8912	. . . . . . . . 9 #
49		divneg2ap 9060	. . . . . . . . 9 $/\$ $/\$ #
50	47, 47, 48, 49	mp3an 1378	. . . . . . . 8
51	46, 50	eqtr3i 2261	. . . . . . 7
52	51	oveq1i 6089	. . . . . 6 ♯ ♯
53	2, 4, 42	exprecapd 11102	. . . . . 6 ♯ ♯
54	52, 53	eqtrid 2283	. . . . 5 ♯ ♯
55	54	oveq2d 6095	. . . 4 ♯ ♯ ♯ ♯
56	5, 15, 34, 6, 35, 36	lgsquadlemsfi 16177	. . . . . . . . . . . . 13
57	56	adantr 276	. . . . . . . . . . . 12 $/\$
58		opabssxp 4847	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	36, 58	eqsstri 3280	. . . . . . . . . . . . . . . . 17
60	59	sseli 3244	. . . . . . . . . . . . . . . 16
61		xp1st 6393	. . . . . . . . . . . . . . . 16
62	60, 61	syl 14	. . . . . . . . . . . . . . 15
63	62	elfzelzd 10412	. . . . . . . . . . . . . 14
64	19	nnzd 9750	. . . . . . . . . . . . . . 15 $/\$
65	64, 26	zsubcld 9756	. . . . . . . . . . . . . 14 $/\$
66		zdceq 9703	. . . . . . . . . . . . . 14 $/\$ DECID
67	63, 65, 66	syl2anr 290	. . . . . . . . . . . . 13 $/\$ $/\$ DECID
68	67	ralrimiva 2623	. . . . . . . . . . . 12 $/\$ DECID
69	57, 68	ssfirab 7238	. . . . . . . . . . 11 $/\$
70		fveqeq2 5702	. . . . . . . . . . . . . . . . . . . 20
71	70	elrab 2982	. . . . . . . . . . . . . . . . . . 19 $/\$
72	71	simprbi 275	. . . . . . . . . . . . . . . . . 18
73	72	ad2antll 495	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	73	oveq2d 6095	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	19	nncnd 9301	. . . . . . . . . . . . . . . . . 18 $/\$
76	75	adantrr 483	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
77	26	zcnd 9752	. . . . . . . . . . . . . . . . . 18 $/\$
78	77	adantrr 483	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79	76, 78	nncand 8636	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80	74, 79	eqtrd 2271	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	80	oveq1d 6094	. . . . . . . . . . . . . 14 $/\$ $/\$
82	24	zcnd 9752	. . . . . . . . . . . . . . . 16 $/\$
83	82	adantrr 483	. . . . . . . . . . . . . . 15 $/\$ $/\$
84		2cnd 9360	. . . . . . . . . . . . . . 15 $/\$ $/\$
85		2ap0 9380	. . . . . . . . . . . . . . . 16 #
86	85	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
87	83, 84, 86	divcanap3d 9119	. . . . . . . . . . . . . 14 $/\$ $/\$
88	81, 87	eqtrd 2271	. . . . . . . . . . . . 13 $/\$ $/\$
89	88	ralrimivva 2632	. . . . . . . . . . . 12
90		invdisj 4121	. . . . . . . . . . . 12 Disj
91	89, 90	syl 14	. . . . . . . . . . 11 Disj
92	14, 69, 91	hashiun 12228	. . . . . . . . . 10 ♯ ♯
93		iunrab 4058	. . . . . . . . . . . 12
94		eldifsni 3841	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
95	5, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22
96	95	necomd 2506	. . . . . . . . . . . . . . . . . . . . 21
97	96	neneqd 2441	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		uzid 9919	. . . . . . . . . . . . . . . . . . . . 21
100	22, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
101	5	eldifad 3231	. . . . . . . . . . . . . . . . . . . . 21
102	101	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103		dvdsprm 12898	. . . . . . . . . . . . . . . . . . . 20 $/\$
104	100, 102, 103	sylancr 418	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
105	98, 104	mtbird 684	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
106	18	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	nncnd 9301	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	26	adantlr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
109	108	zcnd 9752	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
110	107, 109	npcand 8635	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
111	110	breq2d 4140	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	105, 111	mtbird 684	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114		dvdsmul1 12563	. . . . . . . . . . . . . . . . . . 19 $/\$
115	22, 113, 114	sylancr 418	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
117	106	nnzd 9750	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118	117, 108	zsubcld 9756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119		dvds2add 12575	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
120	116, 118, 108, 119	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	115, 120	mpan2d 432	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
122	112, 121	mtod 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$
123		breq2 4132	. . . . . . . . . . . . . . . . 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 10411	. . . . . . . . . . . . . . . 16
131		odd2np1 12623	. . . . . . . . . . . . . . . 16
132	129, 130, 131	3syl 17	. . . . . . . . . . . . . . 15 $/\$
133	11	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
134	133	flqcld 10695	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
135	134	peano2zd 9754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
136	7	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	136	nnzd 9750	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138		simprl 535	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
139	137, 138	zsubcld 9756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
140	134	zred 9751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
141	7	nnred 9300	. . . . . . . . . . . . . . . . . . . . . 22
142	141	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
143	142	rehalfcld 9535	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
144	139	zred 9751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
145		flqle 10696	. . . . . . . . . . . . . . . . . . . . 21
146	133, 145	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
147		zre 9631	. . . . . . . . . . . . . . . . . . . . . 22
148	147	ad2antrl 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
149		simprr 537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
150	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
151	149, 150	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
152		elfzle2 10415	. . . . . . . . . . . . . . . . . . . . . . . . 25
153	151, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154		zmulcl 9681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155	22, 138, 154	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156		zltp1le 9682	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
157	155, 137, 156	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
158	153, 157	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159		2re 9357	. . . . . . . . . . . . . . . . . . . . . . . . 25
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		2pos 9378	. . . . . . . . . . . . . . . . . . . . . . . . 25
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
163		ltmuldiv2 9199	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
164	148, 142, 160, 162, 163	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
165	158, 164	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
166	143	recnd 8348	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
167	7	nncnd 9301	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	167	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	168	2halvesd 9534	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170	166, 166, 169	mvlraddd 8684	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
171	165, 170	breqtrd 4154	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
172	148, 142, 143, 171	ltsub13d 8873	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	140, 143, 144, 146, 172	lelttrd 8445	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174		zltp1le 9682	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	134, 139, 174	syl2anc 415	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
176	173, 175	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
177		2t0e0 9447	. . . . . . . . . . . . . . . . . . . . 21
178		2cn 9358	. . . . . . . . . . . . . . . . . . . . . . . . 25
179		zcn 9632	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	ad2antrl 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181		mulcl 8300	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
182	178, 180, 181	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
183		pncan 8526	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
184	182, 47, 183	sylancl 417	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185		elfznn 10443	. . . . . . . . . . . . . . . . . . . . . . . 24
186		nnm1nn0 9587	. . . . . . . . . . . . . . . . . . . . . . . 24
187	151, 185, 186	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
188	184, 187	eqeltrrd 2316	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
189	188	nn0ge0d 9606	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
190	177, 189	eqbrtrid 4163	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
191		0red 8321	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
192		lemul2 9181	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
193	191, 148, 160, 162, 192	syl112anc 1282	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
194	190, 193	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	142, 148	subge02d 8859	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196	194, 195	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
197	135, 137, 139, 176, 196	elfzd 10402	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
198	101	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		prmnn 12871	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	200	nncnd 9301	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202		peano2cn 8455	. . . . . . . . . . . . . . . . . . . 20
203	182, 202	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
204	201, 203	nncand 8636	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		1cnd 8336	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	201, 182, 205	sub32d 8663	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	201, 182, 205	subsub4d 8662	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
208		2cnd 9360	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
209	208, 168, 180	subdid 8735	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
210	6	oveq2i 6090	. . . . . . . . . . . . . . . . . . . . . . 23
211	18	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
212	211	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
213		peano2zm 9665	. . . . . . . . . . . . . . . . . . . . . . . . . 26
214	212, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
215	214	zcnd 9752	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
216	160, 162	gt0ap0d 8951	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ #
217	215, 208, 216	divcanap2d 9116	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
218	210, 217	eqtrid 2283	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
219	218	oveq1d 6094	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
220	209, 219	eqtr2d 2272	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
221	206, 207, 220	3eqtr3d 2279	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
222	221	oveq2d 6095	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
223	204, 222, 149	3eqtr3rd 2280	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
224		oveq2 6087	. . . . . . . . . . . . . . . . . . 19
225	224	oveq2d 6095	. . . . . . . . . . . . . . . . . 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 5697	. . . . . . . . . 10 ♯ ♯
234		ssrab2 3333	. . . . . . . . . . . . . . 15
235	36	relopabiv 4901	. . . . . . . . . . . . . . 15
236		relss 4860	. . . . . . . . . . . . . . 15
237	234, 235, 236	mp2 16	. . . . . . . . . . . . . 14
238		relxp 4882	. . . . . . . . . . . . . 14
239	36	eleq2i 2305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
240		opabidw 4397	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
241	239, 240	bitri 184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
242		anass 405	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
243	31	peano2zd 9754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	243	zred 9751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
245	244	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
246	16	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . 26
247	246	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
248		nnre 9294	. . . . . . . . . . . . . . . . . . . . . . . . . 26
249	248	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
250		lesub 8763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
251	245, 247, 249, 250	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
252	246	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
253	252	recnd 8348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
254	75, 253	mulcomd 8341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
255	77, 253	mulcomd 8341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
256	19	nnap0d 9333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ #
257	253, 75, 256	divcanap1d 9115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
258	257	oveq1d 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
259	246, 18	nndivred 9337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260	259	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
261	260	recnd 8348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
262	261, 75, 77	mul32d 8473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
263	255, 258, 262	3eqtr2d 2277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
264	254, 263	oveq12d 6097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
265	75, 77, 253	subdird 8736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	26	zred 9751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
267	260, 266	remulcld 8350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
268	267	recnd 8348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
269	253, 268, 75	subdird 8736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
270	264, 265, 269	3eqtr4d 2281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
271	270	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
272	271	breq2d 4140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
273	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
274	247, 273	resubcld 8702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
275	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
276	275	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
277	275	nngt0d 9331	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
278		ltmul1 8914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
279	249, 274, 276, 277, 278	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
280		ltsub13 8765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
281	249, 247, 273, 280	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
282	272, 279, 281	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
283	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
284	283	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
285		nnz 9646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
286		zsubcl 9668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
287	284, 285, 286	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
288		flqlt 10701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
289	30, 287, 288	syl2an2r 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
290		zltp1le 9682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
291	31, 287, 290	syl2an2r 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
292	282, 289, 291	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
293	35	oveq2i 6090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
294		peano2rem 8587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
295	252, 294	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
296	295	recnd 8348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
297		2cnd 9360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
298	85	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ #
299	296, 297, 298	divcanap2d 9116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
300	293, 299	eqtrid 2283	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
301	300	oveq1d 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
302		1cnd 8336	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
303	31	zcnd 9752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
304	253, 302, 303	sub32d 8663	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
305	253, 303, 302	subsub4d 8662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
306	301, 304, 305	3eqtrd 2275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	306	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
308	307	breq2d 4140	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
309	251, 292, 308	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310	309	anbi2d 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
311	15, 35	gausslemma2dlem0b 16152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
312		nnmulcl 9308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
313	9, 311, 312	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314	313	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
315	314	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
316	311	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
317	316	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
318	31	zred 9751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
319	311	nncnd 9301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
320	319	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
321	320	2timesd 9531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
322	320, 320, 321	mvrladdd 8687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
323	252	rehalfcld 9535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
324	252	ltm1d 9256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
325	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
326	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
327		ltdiv1 9192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
328	295, 252, 325, 326, 327	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
329	324, 328	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
330	35, 329	eqbrtrid 4163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
331	317, 323, 330	ltled 8439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
332	253, 297, 75, 298	div32apd 9138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
333	141	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
334	333	rehalfcld 9535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
335	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
336	335	zred 9751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
337	24	zred 9751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
338	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
339		flqltp1 10697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
340	338, 339	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
341		elfzle1 10414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
342	341	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
343	334, 336, 337, 340, 342	ltletrd 8745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
344		ltdivmul 9200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
345	333, 337, 325, 326, 344	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
346	343, 345	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
347	6, 346	eqbrtrrid 4164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
348	19	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
349		peano2rem 8587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
350	348, 349	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
351		ltdivmul 9200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
352	350, 266, 325, 326, 351	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
353	347, 352	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
354		zmulcl 9681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
355	22, 26, 354	sylancr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
356		zlem1lt 9684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
357	211, 355, 356	syl2an2r 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
358	353, 357	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
359		ledivmul 9201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
360	348, 266, 325, 326, 359	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
361	358, 360	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
362	348	rehalfcld 9535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
363	283	nngt0d 9331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
364		lemul2 9181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
365	362, 266, 252, 363, 364	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
366	361, 365	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
367	332, 366	eqbrtrd 4150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
368	252, 266	remulcld 8350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
369	19	nngt0d 9331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
370		lemuldiv 9205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
371	323, 368, 348, 369, 370	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
372	367, 371	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
373	253, 77, 75, 256	div23apd 9152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
374	372, 373	breqtrd 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
375	317, 323, 267, 331, 374	letrd 8444	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
376	311	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
377	376	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
378		flqge 10700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
379	30, 377, 378	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
380	375, 379	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
381	322, 380	eqbrtrd 4150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
382	315, 317, 318, 381	subled 8870	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
383	382	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
384	314	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
385	384, 31	zsubcld 9756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
386	385	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
387	386	zred 9751	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
388	311	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
389	388	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
390		letr 8402	. . . . . . . . . . . . . . . . . . . . . . . . 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 9756	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
401		elfzle2 10415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402	401	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
403	402, 6	breqtrdi 4169	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
404		lemuldiv2 9206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
405	337, 350, 325, 326, 404	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
406	403, 405	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
407	348	ltm1d 9256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
408	266, 350, 348, 406, 407	lelttrd 8445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
409	266, 348	posdifd 8854	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
410	408, 409	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
411		elnnz 9637	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
412	400, 410, 411	sylanbrc 421	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
413	75, 77, 302	sub32d 8663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
414	6, 6	oveq12i 6091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
415	64, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
416	415	zcnd 9752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
417	416	2halvesd 9534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
418	414, 417	eqtrid 2283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
419	418	oveq1d 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
420	167	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
421	420, 420	pncan2d 8633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
422	419, 421	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
423	422, 346	eqbrtrd 4150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
424	350, 333, 266, 423	ltsub23d 8872	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
425	413, 424	eqbrtrd 4150	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
426	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
427	426	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
428		zlem1lt 9684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
429	400, 427, 428	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
430	425, 429	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
431		fznn 10479	. . . . . . . . . . . . . . . . . . . . . . . . 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 10479	. . . . . . . . . . . . . . . . . . . . 21 $/\$
439	437, 438	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
440	436, 439	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
441	398	oveq1d 6094	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
442	441	breq2d 4140	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
443	440, 442	anbi12d 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
444	385	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
445		fznn 10479	. . . . . . . . . . . . . . . . . . 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 6376	. . . . . . . . . . . . . . . . . 18
453	452	eqeq1d 2247	. . . . . . . . . . . . . . . . 17
454	453	elrab 2982	. . . . . . . . . . . . . . . 16 $/\$
455	454	biancomi 270	. . . . . . . . . . . . . . 15 $/\$
456		opelxp 4802	. . . . . . . . . . . . . . . 16 $/\$
457		velsn 3725	. . . . . . . . . . . . . . . . 17
458	457	anbi1i 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$
459	456, 458	bitri 184	. . . . . . . . . . . . . . 15 $/\$
460	449, 455, 459	3bitr4g 223	. . . . . . . . . . . . . 14 $/\$
461	237, 238, 460	eqrelrdv 4869	. . . . . . . . . . . . 13 $/\$
462	461	fveq2d 5697	. . . . . . . . . . . 12 $/\$ ♯ ♯
463		1zzd 9654	. . . . . . . . . . . . . . 15 $/\$
464	463, 385	fzfigd 10851	. . . . . . . . . . . . . 14 $/\$
465		xpsnen2g 7121	. . . . . . . . . . . . . 14 $/\$
466	400, 464, 465	syl2anc 415	. . . . . . . . . . . . 13 $/\$
467	461, 69	eqeltrrd 2316	. . . . . . . . . . . . . 14 $/\$
468		hashen 11206	. . . . . . . . . . . . . 14 $/\$ ♯ ♯
469	467, 464, 468	syl2anc 415	. . . . . . . . . . . . 13 $/\$ ♯ ♯
470	466, 469	mpbird 167	. . . . . . . . . . . 12 $/\$ ♯ ♯
471		ltmul2 9180	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
472	266, 348, 252, 363, 471	syl112anc 1282	. . . . . . . . . . . . . . . . . . . 20 $/\$
473	408, 472	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$
474		ltdivmul2 9202	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
475	368, 252, 348, 369, 474	syl112anc 1282	. . . . . . . . . . . . . . . . . . 19 $/\$
476	473, 475	mpbird 167	. . . . . . . . . . . . . . . . . 18 $/\$
477	373, 476	eqbrtrrd 4152	. . . . . . . . . . . . . . . . 17 $/\$
478		flqlt 10701	. . . . . . . . . . . . . . . . . 18 $/\$
479	30, 284, 478	syl2anc 415	. . . . . . . . . . . . . . . . 17 $/\$
480	477, 479	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$
481		zltlem1 9685	. . . . . . . . . . . . . . . . 17 $/\$
482	31, 284, 481	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$
483	480, 482	mpbid 147	. . . . . . . . . . . . . . 15 $/\$
484	483, 300	breqtrrd 4156	. . . . . . . . . . . . . 14 $/\$
485		eluz2 9910	. . . . . . . . . . . . . 14 $/\$ $/\$
486	31, 384, 484, 485	syl3anbrc 1212	. . . . . . . . . . . . 13 $/\$
487		uznn0sub 9937	. . . . . . . . . . . . 13
488		hashfz1 11205	. . . . . . . . . . . . 13 ♯
489	486, 487, 488	3syl 17	. . . . . . . . . . . 12 $/\$ ♯
490	462, 470, 489	3eqtrd 2275	. . . . . . . . . . 11 $/\$ ♯
491	490	sumeq2dv 12117	. . . . . . . . . 10 ♯
492	92, 233, 491	3eqtr3rd 2280	. . . . . . . . 9 ♯
493	313	nncnd 9301	. . . . . . . . . . 11
494	493	adantr 276	. . . . . . . . . 10 $/\$
495	14, 494, 303	fsumsub 12202	. . . . . . . . 9
496	492, 495	eqtr3d 2273	. . . . . . . 8 ♯
497	496	oveq2d 6095	. . . . . . 7 ♯
498	32	zcnd 9752	. . . . . . . 8
499	14, 384	fsumzcl 12152	. . . . . . . . 9
500	499	zcnd 9752	. . . . . . . 8
501	498, 500	pncan3d 8634	. . . . . . 7
502		fsumconst 12204	. . . . . . . . 9 $/\$ ♯
503	14, 493, 502	syl2anc 415	. . . . . . . 8 ♯
504		hashcl 11203	. . . . . . . . . . 11 ♯
505	14, 504	syl 14	. . . . . . . . . 10 ♯
506	505	nn0cnd 9605	. . . . . . . . 9 ♯
507		2cnd 9360	. . . . . . . . 9
508	506, 507, 319	mul12d 8472	. . . . . . . 8 ♯ ♯
509	503, 508	eqtrd 2271	. . . . . . 7 ♯
510	497, 501, 509	3eqtrd 2275	. . . . . 6 ♯ ♯
511	510	oveq2d 6095	. . . . 5 ♯ ♯
512	22	a1i 9	. . . . . 6
513	505	nn0zd 9749	. . . . . . 7 ♯
514	513, 376	zmulcld 9757	. . . . . 6 ♯
515		expmulzap 11005	. . . . . 6 $/\$ # $/\$ $/\$ ♯ ♯ ♯
516	2, 4, 512, 514, 515	syl22anc 1279	. . . . 5 ♯ ♯
517		neg1sqe1 11054	. . . . . . 7
518	517	oveq1i 6089	. . . . . 6 ♯ ♯
519		1exp 10988	. . . . . . 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 11003	. . . 4 $/\$ # $/\$ $/\$ ♯ ♯ ♯
525	2, 4, 32, 42, 524	syl22anc 1279	. . 3 ♯ ♯
526	523, 525	eqtr2d 2272	. 2 ♯ ♯ ♯
527	33, 41, 41, 43, 526	mulcanap2ad 8986	1 ♯

Colors of variables: wff set class

Syntax hints:

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 3708

cop 3711

ciun 4010 Disj wdisj 4104 class class class wbr 4128

copab 4189

cxp 4770

wrel 4777

cfv 5375 (class class class)co 6079

c1st 6366

cen 7014

cfn 7016

cc 8171

cr 8172

cc0 8173

c1 8174

caddc 8176

cmul 8178

clt 8354

cle 8355

cmin 8491

cneg 8492 # cap 8903

cdiv 8996

cn 9287

c2 9338

cn0 9546

cz 9627

cuz 9904

cq 10002

cfz 10394

cfl 10686

cexp 10958 ♯chash 11197

csu 12102

cdvds 12537

cprime 12868

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 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 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293

This theorem 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 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-disj 4105 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-isom 5384 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-1st 6368 df-2nd 6369 df-recs 6570 df-irdg 6635 df-frec 6656 df-1o 6681 df-2o 6682 df-oadd 6685 df-er 6801 df-en 7017 df-dom 7018 df-fin 7019 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-n0 9547 df-z 9628 df-uz 9905 df-q 10003 df-rp 10038 df-fz 10395 df-fzo 10533 df-fl 10688 df-mod 10743 df-seqfrec 10868 df-exp 10959 df-ihash 11198 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-clim 12028 df-sumdc 12103 df-dvds 12538 df-prm 12869

This theorem is referenced by: lgsquadlem2 16180

W3C validator