lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 15329

Description: Lemma for lgsquad 15331. Count the members of

with even coordinates, and combine with lgsquadlem1 15328 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 15325	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 5934	. . . . 5
7	6	sumeq1i 11530	. . . 4
8	1, 5	gausslemma2dlem0b 15301	. . . . . . . . . . 11
9	8	nnzd 9449	. . . . . . . . . 10
10		2nn 9154	. . . . . . . . . 10
11		znq 9700	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 413	. . . . . . . . 9
13	12	flqcld 10369	. . . . . . . 8
14	13	zred 9450	. . . . . . 7
15	14	ltp1d 8959	. . . . . 6
16		fzdisj 10129	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 9771	. . . . . . . . . . 11
19	18	rphalfcld 9786	. . . . . . . . . 10
20	19	rpge0d 9777	. . . . . . . . 9
21		flqge0nn0 10385	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 411	. . . . . . . 8
23	8	nnnn0d 9304	. . . . . . . 8
24	8	nnred 9005	. . . . . . . . 9
25		rphalflt 9760	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10375	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 411	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8147	. . . . . . . 8
31		elfz2nn0 10189	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1183	. . . . . . 7
33		nn0uz 9638	. . . . . . . . 9
34	23, 33	eleqtrdi 2289	. . . . . . . 8
35		elfzp12 10176	. . . . . . . 8 $\/$
36	34, 35	syl 14	. . . . . . 7 $\/$
37	32, 36	mpbid 147	. . . . . 6 $\/$
38		un0 3485	. . . . . . . . 9
39		uncom 3308	. . . . . . . . 9
40	38, 39	eqtr3i 2219	. . . . . . . 8
41		oveq2 5931	. . . . . . . . . 10
42		fz10 10123	. . . . . . . . . 10
43	41, 42	eqtrdi 2245	. . . . . . . . 9
44		oveq1 5930	. . . . . . . . . . 11
45		0p1e1 9106	. . . . . . . . . . 11
46	44, 45	eqtrdi 2245	. . . . . . . . . 10
47	46	oveq1d 5938	. . . . . . . . 9
48	43, 47	uneq12d 3319	. . . . . . . 8
49	40, 48	eqtr4id 2248	. . . . . . 7
50		fzsplit 10128	. . . . . . . 8
51	45	oveq1i 5933	. . . . . . . 8
52	50, 51	eleq2s 2291	. . . . . . 7
53	49, 52	jaoi 717	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9355	. . . . . 6
56	55, 9	fzfigd 10525	. . . . 5
57	2	gausslemma2dlem0a 15300	. . . . . . . . . 10
58	57	nnzd 9449	. . . . . . . . 9
59	1	gausslemma2dlem0a 15300	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 9700	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 595	. . . . . . . 8 $/\$
63		elfznn 10131	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9013	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 414	. . . . . . . . . 10 $/\$
67	66	nnzd 9449	. . . . . . . . 9 $/\$
68		zq 9702	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 9713	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 411	. . . . . . 7 $/\$
72	57	nnrpd 9771	. . . . . . . . . . 11
73	59	nnrpd 9771	. . . . . . . . . . 11
74	72, 73	rpdivcld 9791	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 9771	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 9790	. . . . . . . 8 $/\$
78	77	rpge0d 9777	. . . . . . 7 $/\$
79		flqge0nn0 10385	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 411	. . . . . 6 $/\$
81	80	nn0cnd 9306	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 11574	. . . 4
83	7, 82	eqtr3id 2243	. . 3
84	83	oveq2d 5939	. 2
85		neg1cn 9097	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9453	. . . . . 6
88	87, 9	fzfigd 10525	. . . . 5
89		ssun2 3328	. . . . . . . 8
90	89, 54	sseqtrrid 3235	. . . . . . 7
91	90	sselda 3184	. . . . . 6 $/\$
92	91, 80	syldan 282	. . . . 5 $/\$
93	88, 92	fsumnn0cl 11570	. . . 4
94	55, 13	fzfigd 10525	. . . . 5
95		ssun1 3327	. . . . . . . 8
96	95, 54	sseqtrrid 3235	. . . . . . 7
97	96	sselda 3184	. . . . . 6 $/\$
98	97, 80	syldan 282	. . . . 5 $/\$
99	94, 98	fsumnn0cl 11570	. . . 4
100	86, 93, 99	expaddd 10769	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 15327	. . . . . 6
104		hashcl 10875	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 15326	. . . . . . 7
107		opabssxp 4738	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3216	. . . . . . . . . . . . 13
109	108	sseli 3180	. . . . . . . . . . . 12
110		xp1st 6224	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10103	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 11965	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 414	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2570	. . . . . . 7 DECID
117	106, 116	ssfirab 6998	. . . . . 6
118		hashcl 10875	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 10769	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9355	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9448	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10525	. . . . . . . . . . 11 $/\$
125		xpsnen2g 6889	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 411	. . . . . . . . . 10 $/\$
127		snfig 6874	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 6994	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 411	. . . . . . . . . . 11 $/\$
131		hashen 10878	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 411	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3269	. . . . . . . . . . . . 13
135	102	relopabiv 4790	. . . . . . . . . . . . 13
136		relss 4751	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4773	. . . . . . . . . . . 12
139	102	eleq2i 2263	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4292	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 401	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 9005	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 9005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 9005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 8911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 8961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 8897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 9771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 9760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8154	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
184	181, 182, 183	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
186	1	eldifad 3168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		prmz 12289	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 12011	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 664	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12323	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12289	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 664	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9347	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 11981	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4038	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
211	210	necon3bd 2410	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
214	213, 145	nnmulcld 9041	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9449	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9041	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9449	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9406	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 8999	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 9005	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9036	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 8910	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 9006	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 9006	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 9006	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8658	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 8857	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4046	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 9005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 8885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9065	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 8719	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 8720	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4060	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 9005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8059	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8621	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8057	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 8859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 7974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 5938	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4073	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4058	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 15301	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 9005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8043	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8572	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8164	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8102	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9387	. . . . . . . . . . . . . . . . . . . . . . 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 10374	. . . . . . . . . . . . . . . . . . . . 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 9639	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2289	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10094	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	296, 297, 298	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 $/\$
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
302	294, 301	eqeltrd 2273	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
304	271	nnzd 9449	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10166	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 5930	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 9006	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 9006	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8050	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2251	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4046	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10369	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10166	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . . . 18
324		vex 2766	. . . . . . . . . . . . . . . . . 18
325	323, 324	op1std 6207	. . . . . . . . . . . . . . . . 17
326	325	eqeq2d 2208	. . . . . . . . . . . . . . . 16
327		eqcom 2198	. . . . . . . . . . . . . . . 16
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15
329	328	elrab 2920	. . . . . . . . . . . . . 14 $/\$
330	329	biancomi 270	. . . . . . . . . . . . 13 $/\$
331		opelxp 4694	. . . . . . . . . . . . . 14 $/\$
332		velsn 3640	. . . . . . . . . . . . . . 15
333	332	anbi1i 458	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4760	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2202	. . . . . . . . . 10 $/\$
338	337	fveq2d 5563	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 10877	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2238	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 11535	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9403	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2570	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 6998	. . . . . . . 8 $/\$
349		fveq2 5559	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2208	. . . . . . . . . . . . . . 15
351	350	elrab 2920	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 491	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 5938	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 9006	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 479	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9065	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9085	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 8824	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2231	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2579	. . . . . . . . 9
363		invdisj 4028	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 11645	. . . . . . 7 ♯ ♯
366		iunrab 3965	. . . . . . . . 9
367		2cn 9063	. . . . . . . . . . . . . 14
368		zcn 9333	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8010	. . . . . . . . . . . . . 14 $/\$
371	367, 369, 370	sylancr 414	. . . . . . . . . . . . 13 $/\$ $/\$
372	371	eqeq1d 2205	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidva 2494	. . . . . . . . . . 11 $/\$
374	152	anim1i 340	. . . . . . . . . . . . 13 $/\$ $/\$
375	374	reximi2 2593	. . . . . . . . . . . 12
376		simprr 531	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	108, 377	sselid 3182	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
381		elfzle2 10105	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4056	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9332	. . . . . . . . . . . . . . . . . . . 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 1253	. . . . . . . . . . . . . . . . . 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 9152	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10131	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2273	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9036	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4069	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8029	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 8885	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9338	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 417	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10094	. . . . . . . . . . . . . . . . 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 2596	. . . . . . . . . . . 12 $/\$
415	375, 414	impbid2 143	. . . . . . . . . . 11 $/\$
416		2z 9356	. . . . . . . . . . . 12
417	379	elfzelzd 10103	. . . . . . . . . . . 12 $/\$
418		divides 11956	. . . . . . . . . . . 12 $/\$
419	416, 417, 418	sylancr 414	. . . . . . . . . . 11 $/\$
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 $/\$
421	420	rabbidva 2751	. . . . . . . . 9
422	366, 421	eqtrid 2241	. . . . . . . 8
423	422	fveq2d 5563	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2235	. . . . . 6 ♯
425	424	oveq2d 5939	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 15328	. . . . 5 ♯
427	425, 426	oveq12d 5941	. . . 4 ♯ ♯
428	120, 427	eqtr4d 2232	. . 3 ♯ ♯
429		inrab 3436	. . . . . . 7 $/\$
430		pm3.24 694	. . . . . . . . . 10 $/\$
431	430	a1i 9	. . . . . . . . 9 $/\$
432	431	ralrimivw 2571	. . . . . . . 8 $/\$
433		rabeq0 3481	. . . . . . . 8 $/\$ $/\$
434	432, 433	sylibr 134	. . . . . . 7 $/\$
435	429, 434	eqtrid 2241	. . . . . 6
436		hashun 10899	. . . . . 6 $/\$ $/\$ ♯ ♯ ♯
437	117, 103, 435, 436	syl3anc 1249	. . . . 5 ♯ ♯ ♯
438		unrab 3435	. . . . . . 7 $\/$
439		rabid2 2674	. . . . . . . 8 $\/$ $\/$
440	10, 112, 114	sylancr 414	. . . . . . . . 9 DECID
441		exmiddc 837	. . . . . . . . 9 DECID $\/$
442	440, 441	syl 14	. . . . . . . 8 $\/$
443	439, 442	mprgbir 2555	. . . . . . 7 $\/$
444	438, 443	eqtr4i 2220	. . . . . 6
445	444	fveq2i 5562	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2244	. . . 4 ♯ ♯ ♯
447	446	oveq2d 5939	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2235	. 2 ♯
449	4, 84, 448	3eqtrd 2233	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835 $/\$ w3a 980

wceq 1364

wcel 2167

wne 2367

wral 2475

wrex 2476

crab 2479 $\$ cdif 3154

cun 3155

cin 3156

wss 3157

c0 3451

csn 3623

cop 3626

ciun 3917 Disj wdisj 4011 class class class wbr 4034

copab 4094

cxp 4662

wrel 4669

cfv 5259 (class class class)co 5923

c1st 6197

cen 6798

cfn 6800

cc 7879

cr 7880

cc0 7881

c1 7882

caddc 7884

cmul 7886

clt 8063

cle 8064

cmin 8199

cneg 8200 # cap 8610

cdiv 8701

cn 8992

c2 9043

cn0 9251

cz 9328

cuz 9603

cq 9695

crp 9730

cfz 10085

cfl 10360

cexp 10632 ♯chash 10869

csu 11520

cdvds 11954

cgcd 12130

cprime 12285

clgs 15248

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7972 ax-resscn 7973 ax-1cn 7974 ax-1re 7975 ax-icn 7976 ax-addcl 7977 ax-addrcl 7978 ax-mulcl 7979 ax-mulrcl 7980 ax-addcom 7981 ax-mulcom 7982 ax-addass 7983 ax-mulass 7984 ax-distr 7985 ax-i2m1 7986 ax-0lt1 7987 ax-1rid 7988 ax-0id 7989 ax-rnegex 7990 ax-precex 7991 ax-cnre 7992 ax-pre-ltirr 7993 ax-pre-ltwlin 7994 ax-pre-lttrn 7995 ax-pre-apti 7996 ax-pre-ltadd 7997 ax-pre-mulgt0 7998 ax-pre-mulext 7999 ax-arch 8000 ax-caucvg 8001 ax-addf 8003 ax-mulf 8004

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-xor 1387 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-tp 3631 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-disj 4012 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-of 6136 df-1st 6199 df-2nd 6200 df-tpos 6304 df-recs 6364 df-irdg 6429 df-frec 6450 df-1o 6475 df-2o 6476 df-oadd 6479 df-er 6593 df-ec 6595 df-qs 6599 df-map 6710 df-en 6801 df-dom 6802 df-fin 6803 df-sup 7051 df-inf 7052 df-pnf 8065 df-mnf 8066 df-xr 8067 df-ltxr 8068 df-le 8069 df-sub 8201 df-neg 8202 df-reap 8604 df-ap 8611 df-div 8702 df-inn 8993 df-2 9051 df-3 9052 df-4 9053 df-5 9054 df-6 9055 df-7 9056 df-8 9057 df-9 9058 df-n0 9252 df-z 9329 df-dec 9460 df-uz 9604 df-q 9696 df-rp 9731 df-fz 10086 df-fzo 10220 df-fl 10362 df-mod 10417 df-seqfrec 10542 df-exp 10633 df-ihash 10870 df-cj 11009 df-re 11010 df-im 11011 df-rsqrt 11165 df-abs 11166 df-clim 11446 df-sumdc 11521 df-proddc 11718 df-dvds 11955 df-gcd 12131 df-prm 12286 df-phi 12389 df-pc 12464 df-struct 12690 df-ndx 12691 df-slot 12692 df-base 12694 df-sets 12695 df-iress 12696 df-plusg 12778 df-mulr 12779 df-starv 12780 df-sca 12781 df-vsca 12782 df-ip 12783 df-tset 12784 df-ple 12785 df-ds 12787 df-unif 12788 df-0g 12939 df-igsum 12940 df-topgen 12941 df-iimas 12955 df-qus 12956 df-mgm 13009 df-sgrp 13055 df-mnd 13068 df-mhm 13101 df-submnd 13102 df-grp 13145 df-minusg 13146 df-sbg 13147 df-mulg 13260 df-subg 13310 df-nsg 13311 df-eqg 13312 df-ghm 13381 df-cmn 13426 df-abl 13427 df-mgp 13487 df-rng 13499 df-ur 13526 df-srg 13530 df-ring 13564 df-cring 13565 df-oppr 13634 df-dvdsr 13655 df-unit 13656 df-invr 13687 df-dvr 13698 df-rhm 13718 df-nzr 13746 df-subrg 13785 df-domn 13825 df-idom 13826 df-lmod 13855 df-lssm 13919 df-lsp 13953 df-sra 14001 df-rgmod 14002 df-lidl 14035 df-rsp 14036 df-2idl 14066 df-bl 14112 df-mopn 14113 df-fg 14115 df-metu 14116 df-cnfld 14123 df-zring 14157 df-zrh 14180 df-zn 14182 df-lgs 15249

This theorem is referenced by: lgsquadlem3 15330

W3C validator