lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 15194

Description: Lemma for lgsquad 15196. Count the members of

with even coordinates, and combine with lgsquadlem1 15193 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 15190	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 5929	. . . . 5
7	6	sumeq1i 11506	. . . 4
8	1, 5	gausslemma2dlem0b 15166	. . . . . . . . . . 11
9	8	nnzd 9438	. . . . . . . . . 10
10		2nn 9143	. . . . . . . . . 10
11		znq 9689	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 413	. . . . . . . . 9
13	12	flqcld 10346	. . . . . . . 8
14	13	zred 9439	. . . . . . 7
15	14	ltp1d 8949	. . . . . 6
16		fzdisj 10118	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 9760	. . . . . . . . . . 11
19	18	rphalfcld 9775	. . . . . . . . . 10
20	19	rpge0d 9766	. . . . . . . . 9
21		flqge0nn0 10362	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 411	. . . . . . . 8
23	8	nnnn0d 9293	. . . . . . . 8
24	8	nnred 8995	. . . . . . . . 9
25		rphalflt 9749	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10352	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 411	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8138	. . . . . . . 8
31		elfz2nn0 10178	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1183	. . . . . . 7
33		nn0uz 9627	. . . . . . . . 9
34	23, 33	eleqtrdi 2286	. . . . . . . 8
35		elfzp12 10165	. . . . . . . 8 $\/$
36	34, 35	syl 14	. . . . . . 7 $\/$
37	32, 36	mpbid 147	. . . . . 6 $\/$
38		un0 3480	. . . . . . . . 9
39		uncom 3303	. . . . . . . . 9
40	38, 39	eqtr3i 2216	. . . . . . . 8
41		oveq2 5926	. . . . . . . . . 10
42		fz10 10112	. . . . . . . . . 10
43	41, 42	eqtrdi 2242	. . . . . . . . 9
44		oveq1 5925	. . . . . . . . . . 11
45		0p1e1 9096	. . . . . . . . . . 11
46	44, 45	eqtrdi 2242	. . . . . . . . . 10
47	46	oveq1d 5933	. . . . . . . . 9
48	43, 47	uneq12d 3314	. . . . . . . 8
49	40, 48	eqtr4id 2245	. . . . . . 7
50		fzsplit 10117	. . . . . . . 8
51	45	oveq1i 5928	. . . . . . . 8
52	50, 51	eleq2s 2288	. . . . . . 7
53	49, 52	jaoi 717	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9344	. . . . . 6
56	55, 9	fzfigd 10502	. . . . 5
57	2	gausslemma2dlem0a 15165	. . . . . . . . . 10
58	57	nnzd 9438	. . . . . . . . 9
59	1	gausslemma2dlem0a 15165	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 9689	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 595	. . . . . . . 8 $/\$
63		elfznn 10120	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9003	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 414	. . . . . . . . . 10 $/\$
67	66	nnzd 9438	. . . . . . . . 9 $/\$
68		zq 9691	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 9702	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 411	. . . . . . 7 $/\$
72	57	nnrpd 9760	. . . . . . . . . . 11
73	59	nnrpd 9760	. . . . . . . . . . 11
74	72, 73	rpdivcld 9780	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 9760	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 9779	. . . . . . . 8 $/\$
78	77	rpge0d 9766	. . . . . . 7 $/\$
79		flqge0nn0 10362	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 411	. . . . . 6 $/\$
81	80	nn0cnd 9295	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 11550	. . . 4
83	7, 82	eqtr3id 2240	. . 3
84	83	oveq2d 5934	. 2
85		neg1cn 9087	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9442	. . . . . 6
88	87, 9	fzfigd 10502	. . . . 5
89		ssun2 3323	. . . . . . . 8
90	89, 54	sseqtrrid 3230	. . . . . . 7
91	90	sselda 3179	. . . . . 6 $/\$
92	91, 80	syldan 282	. . . . 5 $/\$
93	88, 92	fsumnn0cl 11546	. . . 4
94	55, 13	fzfigd 10502	. . . . 5
95		ssun1 3322	. . . . . . . 8
96	95, 54	sseqtrrid 3230	. . . . . . 7
97	96	sselda 3179	. . . . . 6 $/\$
98	97, 80	syldan 282	. . . . 5 $/\$
99	94, 98	fsumnn0cl 11546	. . . 4
100	86, 93, 99	expaddd 10746	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 15192	. . . . . 6
104		hashcl 10852	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 15191	. . . . . . 7
107		opabssxp 4733	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3211	. . . . . . . . . . . . 13
109	108	sseli 3175	. . . . . . . . . . . 12
110		xp1st 6218	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10092	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 11941	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 414	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2567	. . . . . . 7 DECID
117	106, 116	ssfirab 6990	. . . . . 6
118		hashcl 10852	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 10746	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9344	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9437	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10502	. . . . . . . . . . 11 $/\$
125		xpsnen2g 6883	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 411	. . . . . . . . . 10 $/\$
127		snfig 6868	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 6986	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 411	. . . . . . . . . . 11 $/\$
131		hashen 10855	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 411	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3264	. . . . . . . . . . . . 13
135	102	relopabiv 4785	. . . . . . . . . . . . 13
136		relss 4746	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4768	. . . . . . . . . . . 12
139	102	eleq2i 2260	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4287	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 401	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 8901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 8951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 8887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8144	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 9760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 9749	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8145	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
184	181, 182, 183	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
186	1	eldifad 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		prmz 12249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 11986	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 664	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12283	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 664	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9336	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 11957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4033	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
211	210	necon3bd 2407	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
214	213, 145	nnmulcld 9031	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9031	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9395	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 8989	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 8995	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9026	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 8900	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8648	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 8847	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4041	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9026	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 8875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8648	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 8709	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 8710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4055	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8093	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8611	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 8849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 5929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 7965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 5933	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4068	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4053	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 15166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 8995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8562	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8155	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8093	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9376	. . . . . . . . . . . . . . . . . . . . . . 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 10351	. . . . . . . . . . . . . . . . . . . . 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 9628	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2286	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10083	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	296, 297, 298	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 $/\$
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
302	294, 301	eqeltrd 2270	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
304	271	nnzd 9438	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10155	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 5925	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 8996	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 8996	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8041	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2248	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4041	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10346	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10155	. . . . . . . . . . . . . . . . . 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 2763	. . . . . . . . . . . . . . . . . 18
324		vex 2763	. . . . . . . . . . . . . . . . . 18
325	323, 324	op1std 6201	. . . . . . . . . . . . . . . . 17
326	325	eqeq2d 2205	. . . . . . . . . . . . . . . 16
327		eqcom 2195	. . . . . . . . . . . . . . . 16
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15
329	328	elrab 2916	. . . . . . . . . . . . . 14 $/\$
330	329	biancomi 270	. . . . . . . . . . . . 13 $/\$
331		opelxp 4689	. . . . . . . . . . . . . 14 $/\$
332		velsn 3635	. . . . . . . . . . . . . . 15
333	332	anbi1i 458	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4755	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2199	. . . . . . . . . 10 $/\$
338	337	fveq2d 5558	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 10854	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2235	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 11511	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9392	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2567	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 6990	. . . . . . . 8 $/\$
349		fveq2 5554	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2205	. . . . . . . . . . . . . . 15
351	350	elrab 2916	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 491	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 5933	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 8996	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 479	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9055	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9075	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 8814	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2228	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2576	. . . . . . . . 9
363		invdisj 4023	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 11621	. . . . . . 7 ♯ ♯
366		iunrab 3960	. . . . . . . . 9
367		2cn 9053	. . . . . . . . . . . . . 14
368		zcn 9322	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8001	. . . . . . . . . . . . . 14 $/\$
371	367, 369, 370	sylancr 414	. . . . . . . . . . . . 13 $/\$ $/\$
372	371	eqeq1d 2202	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidva 2491	. . . . . . . . . . 11 $/\$
374	152	anim1i 340	. . . . . . . . . . . . 13 $/\$ $/\$
375	374	reximi2 2590	. . . . . . . . . . . 12
376		simprr 531	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	108, 377	sselid 3177	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
381		elfzle2 10094	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4051	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9321	. . . . . . . . . . . . . . . . . . . 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 9141	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10120	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2270	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9026	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4064	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8020	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 8875	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9327	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 417	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2286	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10083	. . . . . . . . . . . . . . . . 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 2593	. . . . . . . . . . . 12 $/\$
415	375, 414	impbid2 143	. . . . . . . . . . 11 $/\$
416		2z 9345	. . . . . . . . . . . 12
417	379	elfzelzd 10092	. . . . . . . . . . . 12 $/\$
418		divides 11932	. . . . . . . . . . . 12 $/\$
419	416, 417, 418	sylancr 414	. . . . . . . . . . 11 $/\$
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 $/\$
421	420	rabbidva 2748	. . . . . . . . 9
422	366, 421	eqtrid 2238	. . . . . . . 8
423	422	fveq2d 5558	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2232	. . . . . 6 ♯
425	424	oveq2d 5934	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 15193	. . . . 5 ♯
427	425, 426	oveq12d 5936	. . . 4 ♯ ♯
428	120, 427	eqtr4d 2229	. . 3 ♯ ♯
429		inrab 3431	. . . . . . 7 $/\$
430		pm3.24 694	. . . . . . . . . 10 $/\$
431	430	a1i 9	. . . . . . . . 9 $/\$
432	431	ralrimivw 2568	. . . . . . . 8 $/\$
433		rabeq0 3476	. . . . . . . 8 $/\$ $/\$
434	432, 433	sylibr 134	. . . . . . 7 $/\$
435	429, 434	eqtrid 2238	. . . . . 6
436		hashun 10876	. . . . . 6 $/\$ $/\$ ♯ ♯ ♯
437	117, 103, 435, 436	syl3anc 1249	. . . . 5 ♯ ♯ ♯
438		unrab 3430	. . . . . . 7 $\/$
439		rabid2 2671	. . . . . . . 8 $\/$ $\/$
440	10, 112, 114	sylancr 414	. . . . . . . . 9 DECID
441		exmiddc 837	. . . . . . . . 9 DECID $\/$
442	440, 441	syl 14	. . . . . . . 8 $\/$
443	439, 442	mprgbir 2552	. . . . . . 7 $\/$
444	438, 443	eqtr4i 2217	. . . . . 6
445	444	fveq2i 5557	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2241	. . . 4 ♯ ♯ ♯
447	446	oveq2d 5934	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2232	. 2 ♯
449	4, 84, 448	3eqtrd 2230	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 2164

wne 2364

wral 2472

wrex 2473

crab 2476 $\$ cdif 3150

cun 3151

cin 3152

wss 3153

c0 3446

csn 3618

cop 3621

ciun 3912 Disj wdisj 4006 class class class wbr 4029

copab 4089

cxp 4657

wrel 4664

cfv 5254 (class class class)co 5918

c1st 6191

cen 6792

cfn 6794

cc 7870

cr 7871

cc0 7872

c1 7873

caddc 7875

cmul 7877

clt 8054

cle 8055

cmin 8190

cneg 8191 # cap 8600

cdiv 8691

cn 8982

c2 9033

cn0 9240

cz 9317

cuz 9592

cq 9684

crp 9719

cfz 10074

cfl 10337

cexp 10609 ♯chash 10846

csu 11496

cdvds 11930

cgcd 12079

cprime 12245

clgs 15113

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991 ax-caucvg 7992 ax-addf 7994 ax-mulf 7995

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 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-tp 3626 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-disj 4007 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-isom 5263 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-of 6130 df-1st 6193 df-2nd 6194 df-tpos 6298 df-recs 6358 df-irdg 6423 df-frec 6444 df-1o 6469 df-2o 6470 df-oadd 6473 df-er 6587 df-ec 6589 df-qs 6593 df-map 6704 df-en 6795 df-dom 6796 df-fin 6797 df-sup 7043 df-inf 7044 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-5 9044 df-6 9045 df-7 9046 df-8 9047 df-9 9048 df-n0 9241 df-z 9318 df-dec 9449 df-uz 9593 df-q 9685 df-rp 9720 df-fz 10075 df-fzo 10209 df-fl 10339 df-mod 10394 df-seqfrec 10519 df-exp 10610 df-ihash 10847 df-cj 10986 df-re 10987 df-im 10988 df-rsqrt 11142 df-abs 11143 df-clim 11422 df-sumdc 11497 df-proddc 11694 df-dvds 11931 df-gcd 12080 df-prm 12246 df-phi 12349 df-pc 12423 df-struct 12620 df-ndx 12621 df-slot 12622 df-base 12624 df-sets 12625 df-iress 12626 df-plusg 12708 df-mulr 12709 df-starv 12710 df-sca 12711 df-vsca 12712 df-ip 12713 df-ple 12715 df-0g 12869 df-igsum 12870 df-iimas 12885 df-qus 12886 df-mgm 12939 df-sgrp 12985 df-mnd 12998 df-mhm 13031 df-submnd 13032 df-grp 13075 df-minusg 13076 df-sbg 13077 df-mulg 13190 df-subg 13240 df-nsg 13241 df-eqg 13242 df-ghm 13311 df-cmn 13356 df-abl 13357 df-mgp 13417 df-rng 13429 df-ur 13456 df-srg 13460 df-ring 13494 df-cring 13495 df-oppr 13564 df-dvdsr 13585 df-unit 13586 df-invr 13617 df-dvr 13628 df-rhm 13648 df-nzr 13676 df-subrg 13715 df-domn 13755 df-idom 13756 df-lmod 13785 df-lssm 13849 df-lsp 13883 df-sra 13931 df-rgmod 13932 df-lidl 13965 df-rsp 13966 df-2idl 13996 df-icnfld 14048 df-zring 14079 df-zrh 14102 df-zn 14104 df-lgs 15114

This theorem is referenced by: lgsquadlem3 15195

W3C validator