lgsquadlem1 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem1 15234

Description: Lemma for lgsquad 15237. 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 9089	. . . 4
2	1	a1i 9	. . 3
3		neg1ap0 9093	. . . 4 #
4	3	a1i 9	. . 3 #
5		lgseisen.1	. . . . . . . . . 10 $\$
6		lgsquad.4	. . . . . . . . . 10
7	5, 6	gausslemma2dlem0b 15207	. . . . . . . . 9
8	7	nnzd 9441	. . . . . . . 8
9		2nn 9146	. . . . . . . 8
10		znq 9692	. . . . . . . 8 $/\$
11	8, 9, 10	sylancl 413	. . . . . . 7
12	11	flqcld 10349	. . . . . 6
13	12	peano2zd 9445	. . . . 5
14	13, 8	fzfigd 10505	. . . 4
15		lgseisen.2	. . . . . . . . 9 $\$
16	15	gausslemma2dlem0a 15206	. . . . . . . 8
17	16	nnzd 9441	. . . . . . 7
18	5	gausslemma2dlem0a 15206	. . . . . . . 8
19	18	adantr 276	. . . . . . 7 $/\$
20		znq 9692	. . . . . . 7 $/\$
21	17, 19, 20	syl2an2r 595	. . . . . 6 $/\$
22		2z 9348	. . . . . . . 8
23		elfzelz 10094	. . . . . . . . 9
24	23	adantl 277	. . . . . . . 8 $/\$
25		zmulcl 9373	. . . . . . . 8 $/\$
26	22, 24, 25	sylancr 414	. . . . . . 7 $/\$
27		zq 9694	. . . . . . 7
28	26, 27	syl 14	. . . . . 6 $/\$
29		qmulcl 9705	. . . . . 6 $/\$
30	21, 28, 29	syl2anc 411	. . . . 5 $/\$
31	30	flqcld 10349	. . . 4 $/\$
32	14, 31	fsumzcl 11548	. . 3
33	2, 4, 32	expclzapd 10752	. 2
34		lgseisen.3	. . . . 5
35		lgsquad.5	. . . . 5
36		lgsquad.6	. . . . 5 $/\$ $/\$
37	5, 15, 34, 6, 35, 36	lgsquadlemofi 15233	. . . 4
38		hashcl 10855	. . . 4 ♯
39	37, 38	syl 14	. . 3 ♯
40		expcl 10631	. . 3 $/\$ ♯ ♯
41	1, 39, 40	sylancr 414	. 2 ♯
42	39	nn0zd 9440	. . 3 ♯
43	2, 4, 42	expap0d 10753	. 2 ♯ #
44	41, 43	recidapd 8804	. . . 4 ♯ ♯
45		1div1e1 8725	. . . . . . . . 9
46	45	negeqi 8215	. . . . . . . 8
47		ax-1cn 7967	. . . . . . . . 9
48		1ap0 8611	. . . . . . . . 9 #
49		divneg2ap 8757	. . . . . . . . 9 $/\$ $/\$ #
50	47, 47, 48, 49	mp3an 1348	. . . . . . . 8
51	46, 50	eqtr3i 2216	. . . . . . 7
52	51	oveq1i 5929	. . . . . 6 ♯ ♯
53	2, 4, 42	exprecapd 10755	. . . . . 6 ♯ ♯
54	52, 53	eqtrid 2238	. . . . 5 ♯ ♯
55	54	oveq2d 5935	. . . 4 ♯ ♯ ♯ ♯
56	5, 15, 34, 6, 35, 36	lgsquadlemsfi 15232	. . . . . . . . . . . . 13
57	56	adantr 276	. . . . . . . . . . . 12 $/\$
58		opabssxp 4734	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	36, 58	eqsstri 3212	. . . . . . . . . . . . . . . . 17
60	59	sseli 3176	. . . . . . . . . . . . . . . 16
61		xp1st 6220	. . . . . . . . . . . . . . . 16
62	60, 61	syl 14	. . . . . . . . . . . . . . 15
63	62	elfzelzd 10095	. . . . . . . . . . . . . 14
64	19	nnzd 9441	. . . . . . . . . . . . . . 15 $/\$
65	64, 26	zsubcld 9447	. . . . . . . . . . . . . 14 $/\$
66		zdceq 9395	. . . . . . . . . . . . . 14 $/\$ DECID
67	63, 65, 66	syl2anr 290	. . . . . . . . . . . . 13 $/\$ $/\$ DECID
68	67	ralrimiva 2567	. . . . . . . . . . . 12 $/\$ DECID
69	57, 68	ssfirab 6992	. . . . . . . . . . 11 $/\$
70		fveqeq2 5564	. . . . . . . . . . . . . . . . . . . 20
71	70	elrab 2917	. . . . . . . . . . . . . . . . . . 19 $/\$
72	71	simprbi 275	. . . . . . . . . . . . . . . . . 18
73	72	ad2antll 491	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
74	73	oveq2d 5935	. . . . . . . . . . . . . . . 16 $/\$ $/\$
75	19	nncnd 8998	. . . . . . . . . . . . . . . . . 18 $/\$
76	75	adantrr 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
77	26	zcnd 9443	. . . . . . . . . . . . . . . . . 18 $/\$
78	77	adantrr 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
79	76, 78	nncand 8337	. . . . . . . . . . . . . . . 16 $/\$ $/\$
80	74, 79	eqtrd 2226	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	80	oveq1d 5934	. . . . . . . . . . . . . 14 $/\$ $/\$
82	24	zcnd 9443	. . . . . . . . . . . . . . . 16 $/\$
83	82	adantrr 479	. . . . . . . . . . . . . . 15 $/\$ $/\$
84		2cnd 9057	. . . . . . . . . . . . . . 15 $/\$ $/\$
85		2ap0 9077	. . . . . . . . . . . . . . . 16 #
86	85	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ #
87	83, 84, 86	divcanap3d 8816	. . . . . . . . . . . . . 14 $/\$ $/\$
88	81, 87	eqtrd 2226	. . . . . . . . . . . . 13 $/\$ $/\$
89	88	ralrimivva 2576	. . . . . . . . . . . 12
90		invdisj 4024	. . . . . . . . . . . 12 Disj
91	89, 90	syl 14	. . . . . . . . . . 11 Disj
92	14, 69, 91	hashiun 11624	. . . . . . . . . 10 ♯ ♯
93		iunrab 3961	. . . . . . . . . . . 12
94		eldifsni 3748	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
95	5, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22
96	95	necomd 2450	. . . . . . . . . . . . . . . . . . . . 21
97	96	neneqd 2385	. . . . . . . . . . . . . . . . . . . 20
98	97	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
99		uzid 9609	. . . . . . . . . . . . . . . . . . . . 21
100	22, 99	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
101	5	eldifad 3165	. . . . . . . . . . . . . . . . . . . . 21
102	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
103		dvdsprm 12278	. . . . . . . . . . . . . . . . . . . 20 $/\$
104	100, 102, 103	sylancr 414	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
105	98, 104	mtbird 674	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
106	18	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	nncnd 8998	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
108	26	adantlr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
109	108	zcnd 9443	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
110	107, 109	npcand 8336	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
111	110	breq2d 4042	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
112	105, 111	mtbird 674	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
113	23	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114		dvdsmul1 11959	. . . . . . . . . . . . . . . . . . 19 $/\$
115	22, 113, 114	sylancr 414	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
116	22	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
117	106	nnzd 9441	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
118	117, 108	zsubcld 9447	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
119		dvds2add 11971	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
120	116, 118, 108, 119	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
121	115, 120	mpan2d 428	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
122	112, 121	mtod 664	. . . . . . . . . . . . . . . 16 $/\$ $/\$
123		breq2 4034	. . . . . . . . . . . . . . . . 17
124	123	notbid 668	. . . . . . . . . . . . . . . 16
125	122, 124	syl5ibrcom 157	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	125	rexlimdva 2611	. . . . . . . . . . . . . 14 $/\$
127		simpr 110	. . . . . . . . . . . . . . . . . 18 $/\$
128	59, 127	sselid 3178	. . . . . . . . . . . . . . . . 17 $/\$
129	128, 61	syl 14	. . . . . . . . . . . . . . . 16 $/\$
130		elfzelz 10094	. . . . . . . . . . . . . . . 16
131		odd2np1 12017	. . . . . . . . . . . . . . . 16
132	129, 130, 131	3syl 17	. . . . . . . . . . . . . . 15 $/\$
133	11	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
134	133	flqcld 10349	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
135	134	peano2zd 9445	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
136	7	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	136	nnzd 9441	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138		simprl 529	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
139	137, 138	zsubcld 9447	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
140	134	zred 9442	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
141	7	nnred 8997	. . . . . . . . . . . . . . . . . . . . . 22
142	141	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
143	142	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
144	139	zred 9442	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
145		flqle 10350	. . . . . . . . . . . . . . . . . . . . 21
146	133, 145	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
147		zre 9324	. . . . . . . . . . . . . . . . . . . . . 22
148	147	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
149		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
150	129	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
151	149, 150	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
152		elfzle2 10097	. . . . . . . . . . . . . . . . . . . . . . . . 25
153	151, 152	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
154		zmulcl 9373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155	22, 138, 154	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156		zltp1le 9374	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
157	155, 137, 156	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
158	153, 157	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159		2re 9054	. . . . . . . . . . . . . . . . . . . . . . . . 25
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
161		2pos 9075	. . . . . . . . . . . . . . . . . . . . . . . . 25
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
163		ltmuldiv2 8896	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
164	148, 142, 160, 162, 163	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
165	158, 164	mpbid 147	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
166	143	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
167	7	nncnd 8998	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	167	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	168	2halvesd 9231	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
170	166, 166, 169	mvlraddd 8385	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
171	165, 170	breqtrd 4056	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
172	148, 142, 143, 171	ltsub13d 8572	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
173	140, 143, 144, 146, 172	lelttrd 8146	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
174		zltp1le 9374	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	134, 139, 174	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
176	173, 175	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
177		2t0e0 9144	. . . . . . . . . . . . . . . . . . . . 21
178		2cn 9055	. . . . . . . . . . . . . . . . . . . . . . . . 25
179		zcn 9325	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	179	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181		mulcl 8001	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
182	178, 180, 181	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
183		pncan 8227	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
184	182, 47, 183	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185		elfznn 10123	. . . . . . . . . . . . . . . . . . . . . . . 24
186		nnm1nn0 9284	. . . . . . . . . . . . . . . . . . . . . . . 24
187	151, 185, 186	3syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
188	184, 187	eqeltrrd 2271	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
189	188	nn0ge0d 9299	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
190	177, 189	eqbrtrid 4065	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
191		0red 8022	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
192		lemul2 8878	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
193	191, 148, 160, 162, 192	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
194	190, 193	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
195	142, 148	subge02d 8558	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
196	194, 195	mpbid 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
197	135, 137, 139, 176, 196	elfzd 10085	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
198	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
199		prmnn 12251	. . . . . . . . . . . . . . . . . . . . 21
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
201	200	nncnd 8998	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
202		peano2cn 8156	. . . . . . . . . . . . . . . . . . . 20
203	182, 202	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
204	201, 203	nncand 8337	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		1cnd 8037	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
206	201, 182, 205	sub32d 8364	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	201, 182, 205	subsub4d 8363	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
208		2cnd 9057	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
209	208, 168, 180	subdid 8435	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
210	6	oveq2i 5930	. . . . . . . . . . . . . . . . . . . . . . 23
211	18	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
212	211	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
213		peano2zm 9358	. . . . . . . . . . . . . . . . . . . . . . . . . 26
214	212, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
215	214	zcnd 9443	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
216	160, 162	gt0ap0d 8650	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ #
217	215, 208, 216	divcanap2d 8813	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
218	210, 217	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
219	218	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
220	209, 219	eqtr2d 2227	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
221	206, 207, 220	3eqtr3d 2234	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
222	221	oveq2d 5935	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
223	204, 222, 149	3eqtr3rd 2235	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
224		oveq2 5927	. . . . . . . . . . . . . . . . . . 19
225	224	oveq2d 5935	. . . . . . . . . . . . . . . . . 18
226	225	rspceeqv 2883	. . . . . . . . . . . . . . . . 17 $/\$
227	197, 223, 226	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
228	227	rexlimdvaa 2612	. . . . . . . . . . . . . . 15 $/\$
229	132, 228	sylbid 150	. . . . . . . . . . . . . 14 $/\$
230	126, 229	impbid 129	. . . . . . . . . . . . 13 $/\$
231	230	rabbidva 2748	. . . . . . . . . . . 12
232	93, 231	eqtrid 2238	. . . . . . . . . . 11
233	232	fveq2d 5559	. . . . . . . . . 10 ♯ ♯
234		ssrab2 3265	. . . . . . . . . . . . . . 15
235	36	relopabiv 4786	. . . . . . . . . . . . . . 15
236		relss 4747	. . . . . . . . . . . . . . 15
237	234, 235, 236	mp2 16	. . . . . . . . . . . . . 14
238		relxp 4769	. . . . . . . . . . . . . 14
239	36	eleq2i 2260	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
240		opabidw 4288	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
241	239, 240	bitri 184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
242		anass 401	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
243	31	peano2zd 9445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244	243	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
245	244	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
246	16	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26
247	246	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
248		nnre 8991	. . . . . . . . . . . . . . . . . . . . . . . . . 26
249	248	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
250		lesub 8462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
251	245, 247, 249, 250	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
252	246	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
253	252	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
254	75, 253	mulcomd 8043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
255	77, 253	mulcomd 8043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
256	19	nnap0d 9030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ #
257	253, 75, 256	divcanap1d 8812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
258	257	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
259	246, 18	nndivred 9034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260	259	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
261	260	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
262	261, 75, 77	mul32d 8174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
263	255, 258, 262	3eqtr2d 2232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
264	254, 263	oveq12d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
265	75, 77, 253	subdird 8436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	26	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
267	260, 266	remulcld 8052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
268	267	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
269	253, 268, 75	subdird 8436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
270	264, 265, 269	3eqtr4d 2236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
271	270	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
272	271	breq2d 4042	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
273	267	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
274	247, 273	resubcld 8402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
275	19	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
276	275	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
277	275	nngt0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
278		ltmul1 8613	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
279	249, 274, 276, 277, 278	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
280		ltsub13 8464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
281	249, 247, 273, 280	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
282	272, 279, 281	3bitr2d 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
283	16	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
284	283	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
285		nnz 9339	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
286		zsubcl 9361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
287	284, 285, 286	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
288		flqlt 10355	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
289	30, 287, 288	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
290		zltp1le 9374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
291	31, 287, 290	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
292	282, 289, 291	3bitrd 214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
293	35	oveq2i 5930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
294		peano2rem 8288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
295	252, 294	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
296	295	recnd 8050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
297		2cnd 9057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
298	85	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ #
299	296, 297, 298	divcanap2d 8813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
300	293, 299	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
301	300	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
302		1cnd 8037	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
303	31	zcnd 9443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
304	253, 302, 303	sub32d 8364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
305	253, 303, 302	subsub4d 8363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
306	301, 304, 305	3eqtrd 2230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
307	306	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
308	307	breq2d 4042	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
309	251, 292, 308	3bitr4d 220	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310	309	anbi2d 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
311	15, 35	gausslemma2dlem0b 15207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
312		nnmulcl 9005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
313	9, 311, 312	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314	313	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
315	314	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
316	311	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
317	316	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
318	31	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
319	311	nncnd 8998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
320	319	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
321	320	2timesd 9228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
322	320, 320, 321	mvrladdd 8388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
323	252	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
324	252	ltm1d 8953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
325	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
326	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
327		ltdiv1 8889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
328	295, 252, 325, 326, 327	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
329	324, 328	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
330	35, 329	eqbrtrid 4065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
331	317, 323, 330	ltled 8140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
332	253, 297, 75, 298	div32apd 8835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
333	141	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
334	333	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
335	13	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
336	335	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
337	24	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
338	11	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
339		flqltp1 10351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
340	338, 339	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
341		elfzle1 10096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
342	341	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
343	334, 336, 337, 340, 342	ltletrd 8444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
344		ltdivmul 8897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
345	333, 337, 325, 326, 344	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
346	343, 345	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
347	6, 346	eqbrtrrid 4066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
348	19	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
349		peano2rem 8288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
350	348, 349	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
351		ltdivmul 8897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
352	350, 266, 325, 326, 351	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
353	347, 352	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
354		zmulcl 9373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
355	22, 26, 354	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
356		zlem1lt 9376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
357	211, 355, 356	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
358	353, 357	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
359		ledivmul 8898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
360	348, 266, 325, 326, 359	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
361	358, 360	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
362	348	rehalfcld 9232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
363	283	nngt0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
364		lemul2 8878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
365	362, 266, 252, 363, 364	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
366	361, 365	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
367	332, 366	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
368	252, 266	remulcld 8052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
369	19	nngt0d 9028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
370		lemuldiv 8902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
371	323, 368, 348, 369, 370	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
372	367, 371	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
373	253, 77, 75, 256	div23apd 8849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
374	372, 373	breqtrd 4056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
375	317, 323, 267, 331, 374	letrd 8145	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
376	311	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
377	376	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
378		flqge 10354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
379	30, 377, 378	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
380	375, 379	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
381	322, 380	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
382	315, 317, 318, 381	subled 8569	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
383	382	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
384	314	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
385	384, 31	zsubcld 9447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
386	385	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
387	386	zred 9442	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
388	311	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
389	388	nnred 8997	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
390		letr 8104	. . . . . . . . . . . . . . . . . . . . . . . . 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 9447	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
401		elfzle2 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402	401	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
403	402, 6	breqtrdi 4071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
404		lemuldiv2 8903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
405	337, 350, 325, 326, 404	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
406	403, 405	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
407	348	ltm1d 8953	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
408	266, 350, 348, 406, 407	lelttrd 8146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
409	266, 348	posdifd 8553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
410	408, 409	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
411		elnnz 9330	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
412	400, 410, 411	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
413	75, 77, 302	sub32d 8364	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
414	6, 6	oveq12i 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
415	64, 213	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
416	415	zcnd 9443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
417	416	2halvesd 9231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
418	414, 417	eqtrid 2238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
419	418	oveq1d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
420	167	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
421	420, 420	pncan2d 8334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
422	419, 421	eqtr3d 2228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
423	422, 346	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
424	350, 333, 266, 423	ltsub23d 8571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
425	413, 424	eqbrtrd 4052	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
426	7	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
427	426	nnzd 9441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
428		zlem1lt 9376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
429	400, 427, 428	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
430	425, 429	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
431		fznn 10158	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
432	427, 431	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
433	412, 430, 432	mpbir2and 946	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
434	433	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
435	398, 434	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
436	435	biantrurd 305	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
437	376	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
438		fznn 10158	. . . . . . . . . . . . . . . . . . . . 21 $/\$
439	437, 438	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
440	436, 439	bitr3d 190	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
441	398	oveq1d 5934	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
442	441	breq2d 4042	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
443	440, 442	anbi12d 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
444	385	adantr 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
445		fznn 10158	. . . . . . . . . . . . . . . . . . 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 2763	. . . . . . . . . . . . . . . . . . 19
451		vex 2763	. . . . . . . . . . . . . . . . . . 19
452	450, 451	op1std 6203	. . . . . . . . . . . . . . . . . 18
453	452	eqeq1d 2202	. . . . . . . . . . . . . . . . 17
454	453	elrab 2917	. . . . . . . . . . . . . . . 16 $/\$
455	454	biancomi 270	. . . . . . . . . . . . . . 15 $/\$
456		opelxp 4690	. . . . . . . . . . . . . . . 16 $/\$
457		velsn 3636	. . . . . . . . . . . . . . . . 17
458	457	anbi1i 458	. . . . . . . . . . . . . . . 16 $/\$ $/\$
459	456, 458	bitri 184	. . . . . . . . . . . . . . 15 $/\$
460	449, 455, 459	3bitr4g 223	. . . . . . . . . . . . . 14 $/\$
461	237, 238, 460	eqrelrdv 4756	. . . . . . . . . . . . 13 $/\$
462	461	fveq2d 5559	. . . . . . . . . . . 12 $/\$ ♯ ♯
463		1zzd 9347	. . . . . . . . . . . . . . 15 $/\$
464	463, 385	fzfigd 10505	. . . . . . . . . . . . . 14 $/\$
465		xpsnen2g 6885	. . . . . . . . . . . . . 14 $/\$
466	400, 464, 465	syl2anc 411	. . . . . . . . . . . . 13 $/\$
467	461, 69	eqeltrrd 2271	. . . . . . . . . . . . . 14 $/\$
468		hashen 10858	. . . . . . . . . . . . . 14 $/\$ ♯ ♯
469	467, 464, 468	syl2anc 411	. . . . . . . . . . . . 13 $/\$ ♯ ♯
470	466, 469	mpbird 167	. . . . . . . . . . . 12 $/\$ ♯ ♯
471		ltmul2 8877	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
472	266, 348, 252, 363, 471	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$
473	408, 472	mpbid 147	. . . . . . . . . . . . . . . . . . 19 $/\$
474		ltdivmul2 8899	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
475	368, 252, 348, 369, 474	syl112anc 1253	. . . . . . . . . . . . . . . . . . 19 $/\$
476	473, 475	mpbird 167	. . . . . . . . . . . . . . . . . 18 $/\$
477	373, 476	eqbrtrrd 4054	. . . . . . . . . . . . . . . . 17 $/\$
478		flqlt 10355	. . . . . . . . . . . . . . . . . 18 $/\$
479	30, 284, 478	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$
480	477, 479	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$
481		zltlem1 9377	. . . . . . . . . . . . . . . . 17 $/\$
482	31, 284, 481	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$
483	480, 482	mpbid 147	. . . . . . . . . . . . . . 15 $/\$
484	483, 300	breqtrrd 4058	. . . . . . . . . . . . . 14 $/\$
485		eluz2 9601	. . . . . . . . . . . . . 14 $/\$ $/\$
486	31, 384, 484, 485	syl3anbrc 1183	. . . . . . . . . . . . 13 $/\$
487		uznn0sub 9627	. . . . . . . . . . . . 13
488		hashfz1 10857	. . . . . . . . . . . . 13 ♯
489	486, 487, 488	3syl 17	. . . . . . . . . . . 12 $/\$ ♯
490	462, 470, 489	3eqtrd 2230	. . . . . . . . . . 11 $/\$ ♯
491	490	sumeq2dv 11514	. . . . . . . . . 10 ♯
492	92, 233, 491	3eqtr3rd 2235	. . . . . . . . 9 ♯
493	313	nncnd 8998	. . . . . . . . . . 11
494	493	adantr 276	. . . . . . . . . 10 $/\$
495	14, 494, 303	fsumsub 11598	. . . . . . . . 9
496	492, 495	eqtr3d 2228	. . . . . . . 8 ♯
497	496	oveq2d 5935	. . . . . . 7 ♯
498	32	zcnd 9443	. . . . . . . 8
499	14, 384	fsumzcl 11548	. . . . . . . . 9
500	499	zcnd 9443	. . . . . . . 8
501	498, 500	pncan3d 8335	. . . . . . 7
502		fsumconst 11600	. . . . . . . . 9 $/\$ ♯
503	14, 493, 502	syl2anc 411	. . . . . . . 8 ♯
504		hashcl 10855	. . . . . . . . . . 11 ♯
505	14, 504	syl 14	. . . . . . . . . 10 ♯
506	505	nn0cnd 9298	. . . . . . . . 9 ♯
507		2cnd 9057	. . . . . . . . 9
508	506, 507, 319	mul12d 8173	. . . . . . . 8 ♯ ♯
509	503, 508	eqtrd 2226	. . . . . . 7 ♯
510	497, 501, 509	3eqtrd 2230	. . . . . 6 ♯ ♯
511	510	oveq2d 5935	. . . . 5 ♯ ♯
512	22	a1i 9	. . . . . 6
513	505	nn0zd 9440	. . . . . . 7 ♯
514	513, 376	zmulcld 9448	. . . . . 6 ♯
515		expmulzap 10659	. . . . . 6 $/\$ # $/\$ $/\$ ♯ ♯ ♯
516	2, 4, 512, 514, 515	syl22anc 1250	. . . . 5 ♯ ♯
517		neg1sqe1 10708	. . . . . . 7
518	517	oveq1i 5929	. . . . . 6 ♯ ♯
519		1exp 10642	. . . . . . 7 ♯ ♯
520	514, 519	syl 14	. . . . . 6 ♯
521	518, 520	eqtrid 2238	. . . . 5 ♯
522	511, 516, 521	3eqtrd 2230	. . . 4 ♯
523	44, 55, 522	3eqtr4d 2236	. . 3 ♯ ♯ ♯
524		expaddzap 10657	. . . 4 $/\$ # $/\$ $/\$ ♯ ♯ ♯
525	2, 4, 32, 42, 524	syl22anc 1250	. . 3 ♯ ♯
526	523, 525	eqtr2d 2227	. 2 ♯ ♯ ♯
527	33, 41, 41, 43, 526	mulcanap2ad 8685	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 DECID wdc 835

wceq 1364

wcel 2164

wne 2364

wral 2472

wrex 2473

crab 2476 $\$ cdif 3151

wss 3154

csn 3619

cop 3622

ciun 3913 Disj wdisj 4007 class class class wbr 4030

copab 4090

cxp 4658

wrel 4665

cfv 5255 (class class class)co 5919

c1st 6193

cen 6794

cfn 6796

cc 7872

cr 7873

cc0 7874

c1 7875

caddc 7877

cmul 7879

clt 8056

cle 8057

cmin 8192

cneg 8193 # cap 8602

cdiv 8693

cn 8984

c2 9035

cn0 9243

cz 9320

cuz 9595

cq 9687

cfz 10077

cfl 10340

cexp 10612 ♯chash 10849

csu 11499

cdvds 11933

cprime 12248

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4145 ax-sep 4148 ax-nul 4156 ax-pow 4204 ax-pr 4239 ax-un 4465 ax-setind 4570 ax-iinf 4621 ax-cnex 7965 ax-resscn 7966 ax-1cn 7967 ax-1re 7968 ax-icn 7969 ax-addcl 7970 ax-addrcl 7971 ax-mulcl 7972 ax-mulrcl 7973 ax-addcom 7974 ax-mulcom 7975 ax-addass 7976 ax-mulass 7977 ax-distr 7978 ax-i2m1 7979 ax-0lt1 7980 ax-1rid 7981 ax-0id 7982 ax-rnegex 7983 ax-precex 7984 ax-cnre 7985 ax-pre-ltirr 7986 ax-pre-ltwlin 7987 ax-pre-lttrn 7988 ax-pre-apti 7989 ax-pre-ltadd 7990 ax-pre-mulgt0 7991 ax-pre-mulext 7992 ax-arch 7993 ax-caucvg 7994

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 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2987 df-csb 3082 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3448 df-if 3559 df-pw 3604 df-sn 3625 df-pr 3626 df-op 3628 df-uni 3837 df-int 3872 df-iun 3915 df-disj 4008 df-br 4031 df-opab 4092 df-mpt 4093 df-tr 4129 df-id 4325 df-po 4328 df-iso 4329 df-iord 4398 df-on 4400 df-ilim 4401 df-suc 4403 df-iom 4624 df-xp 4666 df-rel 4667 df-cnv 4668 df-co 4669 df-dm 4670 df-rn 4671 df-res 4672 df-ima 4673 df-iota 5216 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-isom 5264 df-riota 5874 df-ov 5922 df-oprab 5923 df-mpo 5924 df-1st 6195 df-2nd 6196 df-recs 6360 df-irdg 6425 df-frec 6446 df-1o 6471 df-2o 6472 df-oadd 6475 df-er 6589 df-en 6797 df-dom 6798 df-fin 6799 df-pnf 8058 df-mnf 8059 df-xr 8060 df-ltxr 8061 df-le 8062 df-sub 8194 df-neg 8195 df-reap 8596 df-ap 8603 df-div 8694 df-inn 8985 df-2 9043 df-3 9044 df-4 9045 df-n0 9244 df-z 9321 df-uz 9596 df-q 9688 df-rp 9723 df-fz 10078 df-fzo 10212 df-fl 10342 df-mod 10397 df-seqfrec 10522 df-exp 10613 df-ihash 10850 df-cj 10989 df-re 10990 df-im 10991 df-rsqrt 11145 df-abs 11146 df-clim 11425 df-sumdc 11500 df-dvds 11934 df-prm 12249

This theorem is referenced by: lgsquadlem2 15235

W3C validator