lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 15800

Description: Lemma for lgsquad 15802. Count the members of

with even coordinates, and combine with lgsquadlem1 15799 to get the total count of lattice points in

(up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)

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

**Assertion**
Ref	Expression
lgsquadlem2	♯

Distinct variable groups:

Proof of Theorem lgsquadlem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgseisen.1	. . 3 $\$
2		lgseisen.2	. . 3 $\$
3		lgseisen.3	. . 3
4	1, 2, 3	lgseisen 15796	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 6024	. . . . 5
7	6	sumeq1i 11917	. . . 4
8	1, 5	gausslemma2dlem0b 15772	. . . . . . . . . . 11
9	8	nnzd 9594	. . . . . . . . . 10
10		2nn 9298	. . . . . . . . . 10
11		znq 9851	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 413	. . . . . . . . 9
13	12	flqcld 10530	. . . . . . . 8
14	13	zred 9595	. . . . . . 7
15	14	ltp1d 9103	. . . . . 6
16		fzdisj 10280	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 9922	. . . . . . . . . . 11
19	18	rphalfcld 9937	. . . . . . . . . 10
20	19	rpge0d 9928	. . . . . . . . 9
21		flqge0nn0 10546	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 411	. . . . . . . 8
23	8	nnnn0d 9448	. . . . . . . 8
24	8	nnred 9149	. . . . . . . . 9
25		rphalflt 9911	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10536	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 411	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8291	. . . . . . . 8
31		elfz2nn0 10340	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1205	. . . . . . 7
33		nn0uz 9784	. . . . . . . . 9
34	23, 33	eleqtrdi 2322	. . . . . . . 8
35		elfzp12 10327	. . . . . . . 8 $\/$
36	34, 35	syl 14	. . . . . . 7 $\/$
37	32, 36	mpbid 147	. . . . . 6 $\/$
38		un0 3526	. . . . . . . . 9
39		uncom 3349	. . . . . . . . 9
40	38, 39	eqtr3i 2252	. . . . . . . 8
41		oveq2 6021	. . . . . . . . . 10
42		fz10 10274	. . . . . . . . . 10
43	41, 42	eqtrdi 2278	. . . . . . . . 9
44		oveq1 6020	. . . . . . . . . . 11
45		0p1e1 9250	. . . . . . . . . . 11
46	44, 45	eqtrdi 2278	. . . . . . . . . 10
47	46	oveq1d 6028	. . . . . . . . 9
48	43, 47	uneq12d 3360	. . . . . . . 8
49	40, 48	eqtr4id 2281	. . . . . . 7
50		fzsplit 10279	. . . . . . . 8
51	45	oveq1i 6023	. . . . . . . 8
52	50, 51	eleq2s 2324	. . . . . . 7
53	49, 52	jaoi 721	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9499	. . . . . 6
56	55, 9	fzfigd 10686	. . . . 5
57	2	gausslemma2dlem0a 15771	. . . . . . . . . 10
58	57	nnzd 9594	. . . . . . . . 9
59	1	gausslemma2dlem0a 15771	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 9851	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 597	. . . . . . . 8 $/\$
63		elfznn 10282	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9157	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 414	. . . . . . . . . 10 $/\$
67	66	nnzd 9594	. . . . . . . . 9 $/\$
68		zq 9853	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 9864	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 411	. . . . . . 7 $/\$
72	57	nnrpd 9922	. . . . . . . . . . 11
73	59	nnrpd 9922	. . . . . . . . . . 11
74	72, 73	rpdivcld 9942	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 9922	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 9941	. . . . . . . 8 $/\$
78	77	rpge0d 9928	. . . . . . 7 $/\$
79		flqge0nn0 10546	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 411	. . . . . 6 $/\$
81	80	nn0cnd 9450	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 11961	. . . 4
83	7, 82	eqtr3id 2276	. . 3
84	83	oveq2d 6029	. 2
85		neg1cn 9241	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9598	. . . . . 6
88	87, 9	fzfigd 10686	. . . . 5
89		ssun2 3369	. . . . . . . 8
90	89, 54	sseqtrrid 3276	. . . . . . 7
91	90	sselda 3225	. . . . . 6 $/\$
92	91, 80	syldan 282	. . . . 5 $/\$
93	88, 92	fsumnn0cl 11957	. . . 4
94	55, 13	fzfigd 10686	. . . . 5
95		ssun1 3368	. . . . . . . 8
96	95, 54	sseqtrrid 3276	. . . . . . 7
97	96	sselda 3225	. . . . . 6 $/\$
98	97, 80	syldan 282	. . . . 5 $/\$
99	94, 98	fsumnn0cl 11957	. . . 4
100	86, 93, 99	expaddd 10930	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 15798	. . . . . 6
104		hashcl 11036	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 15797	. . . . . . 7
107		opabssxp 4798	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3257	. . . . . . . . . . . . 13
109	108	sseli 3221	. . . . . . . . . . . 12
110		xp1st 6323	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10254	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 12352	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 414	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2603	. . . . . . 7 DECID
117	106, 116	ssfirab 7123	. . . . . 6
118		hashcl 11036	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 10930	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9499	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9593	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10686	. . . . . . . . . . 11 $/\$
125		xpsnen2g 7008	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 411	. . . . . . . . . 10 $/\$
127		snfig 6984	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 7119	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 411	. . . . . . . . . . 11 $/\$
131		hashen 11039	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 411	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3310	. . . . . . . . . . . . 13
135	102	relopabiv 4851	. . . . . . . . . . . . 13
136		relss 4811	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4833	. . . . . . . . . . . 12
139	102	eleq2i 2296	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4349	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 401	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 9149	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 9149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 9149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 9055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 9105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 9041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 9922	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 9911	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8298	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
184	181, 182, 183	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
186	1	eldifad 3209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		prmz 12676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 12398	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 667	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
195	186, 193, 194	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
196	3, 195	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . 26
197	196	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
198	193	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
199		prmz 12676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 12368	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4090	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
211	210	necon3bd 2443	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
214	213, 145	nnmulcld 9185	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9594	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9185	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9594	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9551	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 9143	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 9149	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9180	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 9054	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 9150	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 9150	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 9150	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8802	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 9001	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4098	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 9149	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9180	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 9029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 8863	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 8864	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 9149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8246	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8765	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 9003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 6024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 8118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 6028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9354	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 15772	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 9149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8187	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8716	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8308	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8246	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9532	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
284	213, 272, 283	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
285	282, 284	sylibrd 169	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
286	285	pm4.71rd 394	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
287	97, 71	syldan 282	. . . . . . . . . . . . . . . . . . . . 21 $/\$
288		flqge 10535	. . . . . . . . . . . . . . . . . . . . 21 $/\$
289	287, 205, 288	syl2an 289	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
290	236, 286, 289	3bitr3d 218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
291	290	pm5.32da 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
292	142, 291	bitrid 192	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
293	292	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
294		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
295		nnuz 9785	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2322	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10245	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	296, 297, 298	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 $/\$
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
302	294, 301	eqeltrd 2306	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
304	271	nnzd 9594	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10317	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 6020	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 9150	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 9150	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8194	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2284	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4098	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10530	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10317	. . . . . . . . . . . . . . . . . 18 $/\$
318	316, 317	syl 14	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
319	318	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
320	293, 315, 319	3bitr4d 220	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
321	141, 320	bitrid 192	. . . . . . . . . . . . . 14 $/\$ $/\$
322	321	pm5.32da 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
323		vex 2803	. . . . . . . . . . . . . . . . . 18
324		vex 2803	. . . . . . . . . . . . . . . . . 18
325	323, 324	op1std 6306	. . . . . . . . . . . . . . . . 17
326	325	eqeq2d 2241	. . . . . . . . . . . . . . . 16
327		eqcom 2231	. . . . . . . . . . . . . . . 16
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15
329	328	elrab 2960	. . . . . . . . . . . . . 14 $/\$
330	329	biancomi 270	. . . . . . . . . . . . 13 $/\$
331		opelxp 4753	. . . . . . . . . . . . . 14 $/\$
332		velsn 3684	. . . . . . . . . . . . . . 15
333	332	anbi1i 458	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4820	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2235	. . . . . . . . . 10 $/\$
338	337	fveq2d 5639	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 11038	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2271	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 11922	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9548	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2603	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 7123	. . . . . . . 8 $/\$
349		fveq2 5635	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2241	. . . . . . . . . . . . . . 15
351	350	elrab 2960	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 491	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 6028	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 9150	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 479	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9209	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9229	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 8968	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2264	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2612	. . . . . . . . 9
363		invdisj 4079	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 12032	. . . . . . 7 ♯ ♯
366		iunrab 4016	. . . . . . . . 9
367		2cn 9207	. . . . . . . . . . . . . 14
368		zcn 9477	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8154	. . . . . . . . . . . . . 14 $/\$
371	367, 369, 370	sylancr 414	. . . . . . . . . . . . 13 $/\$ $/\$
372	371	eqeq1d 2238	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidva 2527	. . . . . . . . . . 11 $/\$
374	152	anim1i 340	. . . . . . . . . . . . 13 $/\$ $/\$
375	374	reximi2 2626	. . . . . . . . . . . 12
376		simprr 531	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	108, 377	sselid 3223	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
381		elfzle2 10256	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4108	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9476	. . . . . . . . . . . . . . . . . . . 20
385	384	ad2antrl 490	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
386	24	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
387	159	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
388	161	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
389	385, 386, 387, 388, 163	syl112anc 1275	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
390	383, 389	mpbid 147	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
391	12	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
392		simprl 529	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
393	391, 392, 153	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
394	390, 393	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
395		2t0e0 9296	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10282	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9180	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4121	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8173	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 9029	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1275	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9482	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 417	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2322	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10245	. . . . . . . . . . . . . . . . 17 $/\$
410	407, 408, 409	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
411	394, 410	mpbird 167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
412	411, 376	jca 306	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
413	412	ex 115	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
414	413	reximdv2 2629	. . . . . . . . . . . 12 $/\$
415	375, 414	impbid2 143	. . . . . . . . . . 11 $/\$
416		2z 9500	. . . . . . . . . . . 12
417	379	elfzelzd 10254	. . . . . . . . . . . 12 $/\$
418		divides 12343	. . . . . . . . . . . 12 $/\$
419	416, 417, 418	sylancr 414	. . . . . . . . . . 11 $/\$
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 $/\$
421	420	rabbidva 2788	. . . . . . . . 9
422	366, 421	eqtrid 2274	. . . . . . . 8
423	422	fveq2d 5639	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2268	. . . . . 6 ♯
425	424	oveq2d 6029	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 15799	. . . . 5 ♯
427	425, 426	oveq12d 6031	. . . 4 ♯ ♯
428	120, 427	eqtr4d 2265	. . 3 ♯ ♯
429		inrab 3477	. . . . . . 7 $/\$
430		pm3.24 698	. . . . . . . . . 10 $/\$
431	430	a1i 9	. . . . . . . . 9 $/\$
432	431	ralrimivw 2604	. . . . . . . 8 $/\$
433		rabeq0 3522	. . . . . . . 8 $/\$ $/\$
434	432, 433	sylibr 134	. . . . . . 7 $/\$
435	429, 434	eqtrid 2274	. . . . . 6
436		hashun 11061	. . . . . 6 $/\$ $/\$ ♯ ♯ ♯
437	117, 103, 435, 436	syl3anc 1271	. . . . 5 ♯ ♯ ♯
438		unrab 3476	. . . . . . 7 $\/$
439		rabid2 2708	. . . . . . . 8 $\/$ $\/$
440	10, 112, 114	sylancr 414	. . . . . . . . 9 DECID
441		exmiddc 841	. . . . . . . . 9 DECID $\/$
442	440, 441	syl 14	. . . . . . . 8 $\/$
443	439, 442	mprgbir 2588	. . . . . . 7 $\/$
444	438, 443	eqtr4i 2253	. . . . . 6
445	444	fveq2i 5638	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2277	. . . 4 ♯ ♯ ♯
447	446	oveq2d 6029	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2268	. 2 ♯
449	4, 84, 448	3eqtrd 2266	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 713 DECID wdc 839 $/\$ w3a 1002

wceq 1395

wcel 2200

wne 2400

wral 2508

wrex 2509

crab 2512 $\$ cdif 3195

cun 3196

cin 3197

wss 3198

c0 3492

csn 3667

cop 3670

ciun 3968 Disj wdisj 4062 class class class wbr 4086

copab 4147

cxp 4721

wrel 4728

cfv 5324 (class class class)co 6013

c1st 6296

cen 6902

cfn 6904

cc 8023

cr 8024

cc0 8025

c1 8026

caddc 8028

cmul 8030

clt 8207

cle 8208

cmin 8343

cneg 8344 # cap 8754

cdiv 8845

cn 9136

c2 9187

cn0 9395

cz 9472

cuz 9748

cq 9846

crp 9881

cfz 10236

cfl 10521

cexp 10793 ♯chash 11030

csu 11907

cdvds 12341

cgcd 12517

cprime 12672

clgs 15719

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684 ax-cnex 8116 ax-resscn 8117 ax-1cn 8118 ax-1re 8119 ax-icn 8120 ax-addcl 8121 ax-addrcl 8122 ax-mulcl 8123 ax-mulrcl 8124 ax-addcom 8125 ax-mulcom 8126 ax-addass 8127 ax-mulass 8128 ax-distr 8129 ax-i2m1 8130 ax-0lt1 8131 ax-1rid 8132 ax-0id 8133 ax-rnegex 8134 ax-precex 8135 ax-cnre 8136 ax-pre-ltirr 8137 ax-pre-ltwlin 8138 ax-pre-lttrn 8139 ax-pre-apti 8140 ax-pre-ltadd 8141 ax-pre-mulgt0 8142 ax-pre-mulext 8143 ax-arch 8144 ax-caucvg 8145 ax-addf 8147 ax-mulf 8148

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-xor 1418 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-tp 3675 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-disj 4063 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-id 4388 df-po 4391 df-iso 4392 df-iord 4461 df-on 4463 df-ilim 4464 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-isom 5333 df-riota 5966 df-ov 6016 df-oprab 6017 df-mpo 6018 df-of 6230 df-1st 6298 df-2nd 6299 df-tpos 6406 df-recs 6466 df-irdg 6531 df-frec 6552 df-1o 6577 df-2o 6578 df-oadd 6581 df-er 6697 df-ec 6699 df-qs 6703 df-map 6814 df-en 6905 df-dom 6906 df-fin 6907 df-sup 7177 df-inf 7178 df-pnf 8209 df-mnf 8210 df-xr 8211 df-ltxr 8212 df-le 8213 df-sub 8345 df-neg 8346 df-reap 8748 df-ap 8755 df-div 8846 df-inn 9137 df-2 9195 df-3 9196 df-4 9197 df-5 9198 df-6 9199 df-7 9200 df-8 9201 df-9 9202 df-n0 9396 df-z 9473 df-dec 9605 df-uz 9749 df-q 9847 df-rp 9882 df-fz 10237 df-fzo 10371 df-fl 10523 df-mod 10578 df-seqfrec 10703 df-exp 10794 df-ihash 11031 df-cj 11396 df-re 11397 df-im 11398 df-rsqrt 11552 df-abs 11553 df-clim 11833 df-sumdc 11908 df-proddc 12105 df-dvds 12342 df-gcd 12518 df-prm 12673 df-phi 12776 df-pc 12851 df-struct 13077 df-ndx 13078 df-slot 13079 df-base 13081 df-sets 13082 df-iress 13083 df-plusg 13166 df-mulr 13167 df-starv 13168 df-sca 13169 df-vsca 13170 df-ip 13171 df-tset 13172 df-ple 13173 df-ds 13175 df-unif 13176 df-0g 13334 df-igsum 13335 df-topgen 13336 df-iimas 13378 df-qus 13379 df-mgm 13432 df-sgrp 13478 df-mnd 13493 df-mhm 13535 df-submnd 13536 df-grp 13579 df-minusg 13580 df-sbg 13581 df-mulg 13700 df-subg 13750 df-nsg 13751 df-eqg 13752 df-ghm 13821 df-cmn 13866 df-abl 13867 df-mgp 13927 df-rng 13939 df-ur 13966 df-srg 13970 df-ring 14004 df-cring 14005 df-oppr 14074 df-dvdsr 14095 df-unit 14096 df-invr 14128 df-dvr 14139 df-rhm 14159 df-nzr 14187 df-subrg 14226 df-domn 14266 df-idom 14267 df-lmod 14296 df-lssm 14360 df-lsp 14394 df-sra 14442 df-rgmod 14443 df-lidl 14476 df-rsp 14477 df-2idl 14507 df-bl 14553 df-mopn 14554 df-fg 14556 df-metu 14557 df-cnfld 14564 df-zring 14598 df-zrh 14621 df-zn 14623 df-lgs 15720

This theorem is referenced by: lgsquadlem3 15801

W3C validator