lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 16209

Description: Lemma for lgsquad 16211. Count the members of

with even coordinates, and combine with lgsquadlem1 16208 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 16205	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 6096	. . . . 5
7	6	sumeq1i 12131	. . . 4
8	1, 5	gausslemma2dlem0b 16181	. . . . . . . . . . 11
9	8	nnzd 9769	. . . . . . . . . 10
10		2nn 9468	. . . . . . . . . 10
11		znq 10026	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 417	. . . . . . . . 9
13	12	flqcld 10714	. . . . . . . 8
14	13	zred 9770	. . . . . . 7
15	14	ltp1d 9261	. . . . . 6
16		fzdisj 10459	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 10097	. . . . . . . . . . 11
19	18	rphalfcld 10112	. . . . . . . . . 10
20	19	rpge0d 10103	. . . . . . . . 9
21		flqge0nn0 10730	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 415	. . . . . . . 8
23	8	nnnn0d 9622	. . . . . . . 8
24	8	nnred 9318	. . . . . . . . 9
25		rphalflt 10086	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10720	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 415	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8445	. . . . . . . 8
31		elfz2nn0 10521	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1212	. . . . . . 7
33		nn0uz 9959	. . . . . . . . 9
34	23, 33	eleqtrdi 2331	. . . . . . . 8
35		elfzp12 10508	. . . . . . . 8 $\/$
36	34, 35	syl 14	. . . . . . 7 $\/$
37	32, 36	mpbid 147	. . . . . 6 $\/$
38		un0 3556	. . . . . . . . 9
39		uncom 3373	. . . . . . . . 9
40	38, 39	eqtr3i 2261	. . . . . . . 8
41		oveq2 6093	. . . . . . . . . 10
42		fz10 10452	. . . . . . . . . 10
43	41, 42	eqtrdi 2287	. . . . . . . . 9
44		oveq1 6092	. . . . . . . . . . 11
45		0p1e1 9419	. . . . . . . . . . 11
46	44, 45	eqtrdi 2287	. . . . . . . . . 10
47	46	oveq1d 6100	. . . . . . . . 9
48	43, 47	uneq12d 3384	. . . . . . . 8
49	40, 48	eqtr4id 2290	. . . . . . 7
50		fzsplit 10458	. . . . . . . 8
51	45	oveq1i 6095	. . . . . . . 8
52	50, 51	eleq2s 2333	. . . . . . 7
53	49, 52	jaoi 728	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9673	. . . . . 6
56	55, 9	fzfigd 10870	. . . . 5
57	2	gausslemma2dlem0a 16180	. . . . . . . . . 10
58	57	nnzd 9769	. . . . . . . . 9
59	1	gausslemma2dlem0a 16180	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 10026	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 603	. . . . . . . 8 $/\$
63		elfznn 10462	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9326	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 418	. . . . . . . . . 10 $/\$
67	66	nnzd 9769	. . . . . . . . 9 $/\$
68		zq 10028	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 10039	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 415	. . . . . . 7 $/\$
72	57	nnrpd 10097	. . . . . . . . . . 11
73	59	nnrpd 10097	. . . . . . . . . . 11
74	72, 73	rpdivcld 10117	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 10097	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 10116	. . . . . . . 8 $/\$
78	77	rpge0d 10103	. . . . . . 7 $/\$
79		flqge0nn0 10730	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 415	. . . . . 6 $/\$
81	80	nn0cnd 9624	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 12176	. . . 4
83	7, 82	eqtr3id 2285	. . 3
84	83	oveq2d 6101	. 2
85		neg1cn 9410	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9773	. . . . . 6
88	87, 9	fzfigd 10870	. . . . 5
89		ssun2 3393	. . . . . . . 8
90	89, 54	sseqtrrid 3299	. . . . . . 7
91	90	sselda 3248	. . . . . 6 $/\$
92	91, 80	syldan 282	. . . . 5 $/\$
93	88, 92	fsumnn0cl 12172	. . . 4
94	55, 13	fzfigd 10870	. . . . 5
95		ssun1 3392	. . . . . . . 8
96	95, 54	sseqtrrid 3299	. . . . . . 7
97	96	sselda 3248	. . . . . 6 $/\$
98	97, 80	syldan 282	. . . . 5 $/\$
99	94, 98	fsumnn0cl 12172	. . . 4
100	86, 93, 99	expaddd 11115	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 16207	. . . . . 6
104		hashcl 11222	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 16206	. . . . . . 7
107		opabssxp 4849	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3280	. . . . . . . . . . . . 13
109	108	sseli 3244	. . . . . . . . . . . 12
110		xp1st 6399	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10431	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 12567	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 418	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2623	. . . . . . 7 DECID
117	106, 116	ssfirab 7244	. . . . . 6
118		hashcl 11222	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 11115	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9673	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9768	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10870	. . . . . . . . . . 11 $/\$
125		xpsnen2g 7127	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 415	. . . . . . . . . 10 $/\$
127		snfig 7103	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 7239	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 415	. . . . . . . . . . 11 $/\$
131		hashen 11225	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 415	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3333	. . . . . . . . . . . . 13
135	102	relopabiv 4903	. . . . . . . . . . . . 13
136		relss 4862	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4884	. . . . . . . . . . . 12
139	102	eleq2i 2305	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4399	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 405	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 9213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 9263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 9199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4165	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 10086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
184	181, 182, 183	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
186	1	eldifad 3231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		prmz 12891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 12613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 673	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12925	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
195	186, 193, 194	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
196	3, 195	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . 26
197	196	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
198	193	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
199		prmz 12891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12872	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 12583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4134	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
211	210	necon3bd 2463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
214	213, 145	nnmulcld 9354	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9354	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9769	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9726	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 446	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 9312	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 9318	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9349	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 9212	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 9319	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 9319	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 9319	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8958	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 9159	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4142	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 9187	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9378	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 9021	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 9022	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4156	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9554	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8921	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8354	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 9161	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 6096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 8272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 6100	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4169	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4154	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 16181	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 9318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8871	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8462	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8399	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9706	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
284	213, 272, 283	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
285	282, 284	sylibrd 169	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
286	285	pm4.71rd 398	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
287	97, 71	syldan 282	. . . . . . . . . . . . . . . . . . . . 21 $/\$
288		flqge 10719	. . . . . . . . . . . . . . . . . . . . 21 $/\$
289	287, 205, 288	syl2an 289	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
290	236, 286, 289	3bitr3d 218	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
291	290	pm5.32da 456	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
292	142, 291	bitrid 192	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
293	292	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
294		simpr 110	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
295		nnuz 9960	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10422	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	296, 297, 298	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 $/\$
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
302	294, 301	eqeltrd 2315	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
304	271	nnzd 9769	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10498	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 6092	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 9319	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 9319	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8347	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2293	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4142	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10714	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10498	. . . . . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
323		vex 2824	. . . . . . . . . . . . . . . . . 18
324		vex 2824	. . . . . . . . . . . . . . . . . 18
325	323, 324	op1std 6382	. . . . . . . . . . . . . . . . 17
326	325	eqeq2d 2250	. . . . . . . . . . . . . . . 16
327		eqcom 2240	. . . . . . . . . . . . . . . 16
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15
329	328	elrab 2982	. . . . . . . . . . . . . 14 $/\$
330	329	biancomi 270	. . . . . . . . . . . . 13 $/\$
331		opelxp 4804	. . . . . . . . . . . . . 14 $/\$
332		velsn 3726	. . . . . . . . . . . . . . 15
333	332	anbi1i 462	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4871	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2244	. . . . . . . . . 10 $/\$
338	337	fveq2d 5699	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 11224	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2280	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 12136	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9722	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2623	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 7244	. . . . . . . 8 $/\$
349		fveq2 5695	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2250	. . . . . . . . . . . . . . 15
351	350	elrab 2982	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 495	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 6100	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 9319	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 483	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9378	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9398	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 9126	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2273	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2632	. . . . . . . . 9
363		invdisj 4123	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 12247	. . . . . . 7 ♯ ♯
366		iunrab 4060	. . . . . . . . 9
367		2cn 9376	. . . . . . . . . . . . . 14
368		zcn 9651	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8308	. . . . . . . . . . . . . 14 $/\$
371	367, 369, 370	sylancr 418	. . . . . . . . . . . . 13 $/\$ $/\$
372	371	eqeq1d 2247	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidva 2547	. . . . . . . . . . 11 $/\$
374	152	anim1i 340	. . . . . . . . . . . . 13 $/\$ $/\$
375	374	reximi2 2646	. . . . . . . . . . . 12
376		simprr 537	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	108, 377	sselid 3246	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
381		elfzle2 10434	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4152	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9650	. . . . . . . . . . . . . . . . . . . 20
385	384	ad2antrl 494	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
386	24	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
387	159	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
388	161	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
389	385, 386, 387, 388, 163	syl112anc 1282	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
390	383, 389	mpbid 147	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
391	12	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
392		simprl 535	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
393	391, 392, 153	syl2anc 415	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
394	390, 393	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
395		2t0e0 9466	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10462	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9349	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4165	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8327	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 9187	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1282	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9656	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 421	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2331	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 492	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10422	. . . . . . . . . . . . . . . . 17 $/\$
410	407, 408, 409	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
411	394, 410	mpbird 167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
412	411, 376	jca 306	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
413	412	ex 115	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
414	413	reximdv2 2649	. . . . . . . . . . . 12 $/\$
415	375, 414	impbid2 143	. . . . . . . . . . 11 $/\$
416		2z 9674	. . . . . . . . . . . 12
417	379	elfzelzd 10431	. . . . . . . . . . . 12 $/\$
418		divides 12558	. . . . . . . . . . . 12 $/\$
419	416, 417, 418	sylancr 418	. . . . . . . . . . 11 $/\$
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 $/\$
421	420	rabbidva 2809	. . . . . . . . 9
422	366, 421	eqtrid 2283	. . . . . . . 8
423	422	fveq2d 5699	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2277	. . . . . 6 ♯
425	424	oveq2d 6101	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 16208	. . . . 5 ♯
427	425, 426	oveq12d 6103	. . . 4 ♯ ♯
428	120, 427	eqtr4d 2274	. . 3 ♯ ♯
429		inrab 3505	. . . . . . 7 $/\$
430		pm3.24 705	. . . . . . . . . 10 $/\$
431	430	a1i 9	. . . . . . . . 9 $/\$
432	431	ralrimivw 2624	. . . . . . . 8 $/\$
433		rabeq0 3552	. . . . . . . 8 $/\$ $/\$
434	432, 433	sylibr 134	. . . . . . 7 $/\$
435	429, 434	eqtrid 2283	. . . . . 6
436		hashun 11247	. . . . . 6 $/\$ $/\$ ♯ ♯ ♯
437	117, 103, 435, 436	syl3anc 1278	. . . . 5 ♯ ♯ ♯
438		unrab 3504	. . . . . . 7 $\/$
439		rabid2 2729	. . . . . . . 8 $\/$ $\/$
440	10, 112, 114	sylancr 418	. . . . . . . . 9 DECID
441		exmiddc 848	. . . . . . . . 9 DECID $\/$
442	440, 441	syl 14	. . . . . . . 8 $\/$
443	439, 442	mprgbir 2608	. . . . . . 7 $\/$
444	438, 443	eqtr4i 2262	. . . . . 6
445	444	fveq2i 5698	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2286	. . . 4 ♯ ♯ ♯
447	446	oveq2d 6101	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2277	. 2 ♯
449	4, 84, 448	3eqtrd 2275	1 ♯

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720 DECID wdc 846 $/\$ w3a 1009

wceq 1402

wcel 2209

wne 2420

wral 2528

wrex 2529

crab 2532 $\$ cdif 3217

cun 3218

cin 3219

wss 3220

c0 3520

csn 3709

cop 3712

ciun 4012 Disj wdisj 4106 class class class wbr 4130

copab 4191

cxp 4772

wrel 4779

cfv 5377 (class class class)co 6085

c1st 6372

cen 7020

cfn 7022

cc 8177

cr 8178

cc0 8179

c1 8180

caddc 8182

cmul 8184

clt 8360

cle 8361

cmin 8497

cneg 8498 # cap 8910

cdiv 9003

cn 9305

c2 9356

cn0 9565

cz 9646

cuz 9923

cq 10021

crp 10056

cfz 10413

cfl 10705

cexp 10977 ♯chash 11216

csu 12121

cdvds 12556

cgcd 12732

cprime 12887

clgs 16128

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

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-xor 1425 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-tp 3717 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-of 6302 df-1st 6374 df-2nd 6375 df-tpos 6516 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-ec 6809 df-qs 6813 df-map 6924 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8904 df-ap 8911 df-div 9004 df-inn 9306 df-2 9364 df-3 9365 df-4 9366 df-5 9367 df-6 9368 df-7 9369 df-8 9370 df-9 9371 df-n0 9566 df-z 9647 df-dec 9780 df-uz 9924 df-q 10022 df-rp 10057 df-fz 10414 df-fzo 10552 df-fl 10707 df-mod 10762 df-seqfrec 10887 df-exp 10978 df-ihash 11217 df-cj 11609 df-re 11610 df-im 11611 df-rsqrt 11766 df-abs 11767 df-clim 12047 df-sumdc 12122 df-proddc 12320 df-dvds 12557 df-gcd 12733 df-prm 12888 df-phi 12991 df-pc 13066 df-struct 13356 df-ndx 13357 df-slot 13358 df-base 13360 df-sets 13361 df-iress 13362 df-plusg 13446 df-mulr 13447 df-starv 13448 df-sca 13449 df-vsca 13450 df-ip 13451 df-tset 13452 df-ple 13453 df-ds 13455 df-unif 13456 df-0g 13614 df-gzsum 13615 df-topgen 13616 df-iimas 13626 df-qus 13627 df-mgm 13678 df-sgrp 13719 df-mnd 13732 df-mhm 13768 df-submnd 13769 df-grp 13810 df-minusg 13811 df-sbg 13812 df-mulg 13925 df-subg 13975 df-nsg 13976 df-eqg 13977 df-ghm 14046 df-cmn 14091 df-abl 14092 df-gsumfi 14153 df-mgp 14220 df-rng 14234 df-ur 14265 df-srg 14270 df-ring 14304 df-cring 14305 df-oppr 14375 df-dvdsr 14397 df-unit 14398 df-invr 14430 df-dvr 14441 df-rhm 14461 df-nzr 14489 df-subrg 14529 df-domn 14569 df-idom 14570 df-lmod 14627 df-lssm 14692 df-lsp 14726 df-sra 14774 df-rgmod 14775 df-lidl 14808 df-rsp 14809 df-2idl 14839 df-bl 14885 df-mopn 14886 df-fg 14888 df-metu 14889 df-cnfld 14896 df-zring 14928 df-zrh 14951 df-zn 14953 df-lgs 16129

This theorem is used by: lgsquadlem3 16210

W3C validator