lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 16180

Description: Lemma for lgsquad 16182. Count the members of

with even coordinates, and combine with lgsquadlem1 16179 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 16176	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 6090	. . . . 5
7	6	sumeq1i 12112	. . . 4
8	1, 5	gausslemma2dlem0b 16152	. . . . . . . . . . 11
9	8	nnzd 9750	. . . . . . . . . 10
10		2nn 9449	. . . . . . . . . 10
11		znq 10007	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 417	. . . . . . . . 9
13	12	flqcld 10695	. . . . . . . 8
14	13	zred 9751	. . . . . . 7
15	14	ltp1d 9254	. . . . . 6
16		fzdisj 10440	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 10078	. . . . . . . . . . 11
19	18	rphalfcld 10093	. . . . . . . . . 10
20	19	rpge0d 10084	. . . . . . . . 9
21		flqge0nn0 10711	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 415	. . . . . . . 8
23	8	nnnn0d 9603	. . . . . . . 8
24	8	nnred 9300	. . . . . . . . 9
25		rphalflt 10067	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10701	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 415	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8439	. . . . . . . 8
31		elfz2nn0 10502	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1212	. . . . . . 7
33		nn0uz 9940	. . . . . . . . 9
34	23, 33	eleqtrdi 2331	. . . . . . . 8
35		elfzp12 10489	. . . . . . . 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 6087	. . . . . . . . . 10
42		fz10 10433	. . . . . . . . . 10
43	41, 42	eqtrdi 2287	. . . . . . . . 9
44		oveq1 6086	. . . . . . . . . . 11
45		0p1e1 9401	. . . . . . . . . . 11
46	44, 45	eqtrdi 2287	. . . . . . . . . 10
47	46	oveq1d 6094	. . . . . . . . 9
48	43, 47	uneq12d 3384	. . . . . . . 8
49	40, 48	eqtr4id 2290	. . . . . . 7
50		fzsplit 10439	. . . . . . . 8
51	45	oveq1i 6089	. . . . . . . 8
52	50, 51	eleq2s 2333	. . . . . . 7
53	49, 52	jaoi 728	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9654	. . . . . 6
56	55, 9	fzfigd 10851	. . . . 5
57	2	gausslemma2dlem0a 16151	. . . . . . . . . 10
58	57	nnzd 9750	. . . . . . . . 9
59	1	gausslemma2dlem0a 16151	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 10007	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 603	. . . . . . . 8 $/\$
63		elfznn 10443	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9308	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 418	. . . . . . . . . 10 $/\$
67	66	nnzd 9750	. . . . . . . . 9 $/\$
68		zq 10009	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 10020	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 415	. . . . . . 7 $/\$
72	57	nnrpd 10078	. . . . . . . . . . 11
73	59	nnrpd 10078	. . . . . . . . . . 11
74	72, 73	rpdivcld 10098	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 10078	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 10097	. . . . . . . 8 $/\$
78	77	rpge0d 10084	. . . . . . 7 $/\$
79		flqge0nn0 10711	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 415	. . . . . 6 $/\$
81	80	nn0cnd 9605	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 12157	. . . 4
83	7, 82	eqtr3id 2285	. . 3
84	83	oveq2d 6095	. 2
85		neg1cn 9392	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9754	. . . . . 6
88	87, 9	fzfigd 10851	. . . . 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 12153	. . . 4
94	55, 13	fzfigd 10851	. . . . 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 12153	. . . 4
100	86, 93, 99	expaddd 11096	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 16178	. . . . . 6
104		hashcl 11203	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 16177	. . . . . . 7
107		opabssxp 4847	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3280	. . . . . . . . . . . . 13
109	108	sseli 3244	. . . . . . . . . . . 12
110		xp1st 6393	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10412	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 12548	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 418	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2623	. . . . . . 7 DECID
117	106, 116	ssfirab 7238	. . . . . 6
118		hashcl 11203	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 11096	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9654	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9749	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10851	. . . . . . . . . . 11 $/\$
125		xpsnen2g 7121	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 415	. . . . . . . . . 10 $/\$
127		snfig 7097	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 7233	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 415	. . . . . . . . . . 11 $/\$
131		hashen 11206	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 415	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3333	. . . . . . . . . . . . 13
135	102	relopabiv 4901	. . . . . . . . . . . . 13
136		relss 4860	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4882	. . . . . . . . . . . 12
139	102	eleq2i 2305	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4397	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 405	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9535	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 9206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 9256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 9192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4163	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 10078	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 10067	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9673	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 12872	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 12594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 673	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12872	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12853	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 12564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4132	. . . . . . . . . . . . . . . . . . . . . . . . 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 9336	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9336	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9750	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9707	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 446	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 9294	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 9300	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9331	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 9205	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 9301	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 9301	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 9301	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8951	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 9152	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4140	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 9180	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8951	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 9014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 9015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4154	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9535	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8393	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8914	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1282	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8348	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 9154	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 6090	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 8266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4167	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4152	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 16152	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 9300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8335	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8865	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8456	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8393	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 432	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9687	. . . . . . . . . . . . . . . . . . . . . . 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 10700	. . . . . . . . . . . . . . . . . . . . 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 9941	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2331	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10403	. . . . . . . . . . . . . . . . . . . . . . 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 9750	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10479	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 6086	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 9301	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 9301	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8341	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2293	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4140	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10695	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10479	. . . . . . . . . . . . . . . . . 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 6376	. . . . . . . . . . . . . . . . 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 4802	. . . . . . . . . . . . . 14 $/\$
332		velsn 3725	. . . . . . . . . . . . . . 15
333	332	anbi1i 462	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4869	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2244	. . . . . . . . . 10 $/\$
338	337	fveq2d 5697	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 11205	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2280	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 12117	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9703	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2623	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 7238	. . . . . . . 8 $/\$
349		fveq2 5693	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2250	. . . . . . . . . . . . . . 15
351	350	elrab 2982	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 495	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 6094	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 9301	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 483	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9360	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9380	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 9119	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2273	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2632	. . . . . . . . 9
363		invdisj 4121	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 12228	. . . . . . 7 ♯ ♯
366		iunrab 4058	. . . . . . . . 9
367		2cn 9358	. . . . . . . . . . . . . 14
368		zcn 9632	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8302	. . . . . . . . . . . . . 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 10415	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4150	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9631	. . . . . . . . . . . . . . . . . . . 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 9447	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10443	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2315	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9331	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4163	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8321	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 9180	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1282	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9637	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 421	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2331	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 492	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10403	. . . . . . . . . . . . . . . . 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 9655	. . . . . . . . . . . 12
417	379	elfzelzd 10412	. . . . . . . . . . . 12 $/\$
418		divides 12539	. . . . . . . . . . . 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 5697	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2277	. . . . . 6 ♯
425	424	oveq2d 6095	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 16179	. . . . 5 ♯
427	425, 426	oveq12d 6097	. . . 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 11228	. . . . . 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 5696	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2286	. . . 4 ♯ ♯ ♯
447	446	oveq2d 6095	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2277	. 2 ♯
449	4, 84, 448	3eqtrd 2275	1 ♯

Colors of variables: wff set class

Syntax hints:

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 3708

cop 3711

ciun 4010 Disj wdisj 4104 class class class wbr 4128

copab 4189

cxp 4770

wrel 4777

cfv 5375 (class class class)co 6079

c1st 6366

cen 7014

cfn 7016

cc 8171

cr 8172

cc0 8173

c1 8174

caddc 8176

cmul 8178

clt 8354

cle 8355

cmin 8491

cneg 8492 # cap 8903

cdiv 8996

cn 9287

c2 9338

cn0 9546

cz 9627

cuz 9904

cq 10002

crp 10037

cfz 10394

cfl 10686

cexp 10958 ♯chash 11197

csu 12102

cdvds 12537

cgcd 12713

cprime 12868

clgs 16099

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 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 4244 ax-sep 4247 ax-nul 4257 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-iinf 4733 ax-cnex 8264 ax-resscn 8265 ax-1cn 8266 ax-1re 8267 ax-icn 8268 ax-addcl 8269 ax-addrcl 8270 ax-mulcl 8271 ax-mulrcl 8272 ax-addcom 8273 ax-mulcom 8274 ax-addass 8275 ax-mulass 8276 ax-distr 8277 ax-i2m1 8278 ax-0lt1 8279 ax-1rid 8280 ax-0id 8281 ax-rnegex 8282 ax-precex 8283 ax-cnre 8284 ax-pre-ltirr 8285 ax-pre-ltwlin 8286 ax-pre-lttrn 8287 ax-pre-apti 8288 ax-pre-ltadd 8289 ax-pre-mulgt0 8290 ax-pre-mulext 8291 ax-arch 8292 ax-caucvg 8293 ax-addf 8295 ax-mulf 8296

This theorem 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 3714 df-pr 3715 df-tp 3716 df-op 3717 df-uni 3934 df-int 3969 df-iun 4012 df-disj 4105 df-br 4129 df-opab 4191 df-mpt 4192 df-tr 4228 df-id 4436 df-po 4439 df-iso 4440 df-iord 4509 df-on 4511 df-ilim 4512 df-suc 4514 df-iom 4736 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-ima 4785 df-iota 5335 df-fun 5377 df-fn 5378 df-f 5379 df-f1 5380 df-fo 5381 df-f1o 5382 df-fv 5383 df-isom 5384 df-riota 6032 df-ov 6082 df-oprab 6083 df-mpo 6084 df-of 6296 df-1st 6368 df-2nd 6369 df-tpos 6510 df-recs 6570 df-irdg 6635 df-frec 6656 df-1o 6681 df-2o 6682 df-oadd 6685 df-er 6801 df-ec 6803 df-qs 6807 df-map 6918 df-en 7017 df-dom 7018 df-fin 7019 df-sup 7318 df-inf 7319 df-pnf 8356 df-mnf 8357 df-xr 8358 df-ltxr 8359 df-le 8360 df-sub 8493 df-neg 8494 df-reap 8897 df-ap 8904 df-div 8997 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-5 9349 df-6 9350 df-7 9351 df-8 9352 df-9 9353 df-n0 9547 df-z 9628 df-dec 9761 df-uz 9905 df-q 10003 df-rp 10038 df-fz 10395 df-fzo 10533 df-fl 10688 df-mod 10743 df-seqfrec 10868 df-exp 10959 df-ihash 11198 df-cj 11590 df-re 11591 df-im 11592 df-rsqrt 11747 df-abs 11748 df-clim 12028 df-sumdc 12103 df-proddc 12301 df-dvds 12538 df-gcd 12714 df-prm 12869 df-phi 12972 df-pc 13047 df-struct 13337 df-ndx 13338 df-slot 13339 df-base 13341 df-sets 13342 df-iress 13343 df-plusg 13427 df-mulr 13428 df-starv 13429 df-sca 13430 df-vsca 13431 df-ip 13432 df-tset 13433 df-ple 13434 df-ds 13436 df-unif 13437 df-0g 13595 df-gzsum 13596 df-topgen 13597 df-iimas 13607 df-qus 13608 df-mgm 13659 df-sgrp 13700 df-mnd 13713 df-mhm 13749 df-submnd 13750 df-grp 13791 df-minusg 13792 df-sbg 13793 df-mulg 13906 df-subg 13956 df-nsg 13957 df-eqg 13958 df-ghm 14027 df-cmn 14072 df-abl 14073 df-gsumfi 14134 df-mgp 14201 df-rng 14215 df-ur 14246 df-srg 14251 df-ring 14285 df-cring 14286 df-oppr 14356 df-dvdsr 14378 df-unit 14379 df-invr 14411 df-dvr 14422 df-rhm 14442 df-nzr 14470 df-subrg 14510 df-domn 14550 df-idom 14551 df-lmod 14608 df-lssm 14673 df-lsp 14707 df-sra 14755 df-rgmod 14756 df-lidl 14789 df-rsp 14790 df-2idl 14820 df-bl 14866 df-mopn 14867 df-fg 14869 df-metu 14870 df-cnfld 14877 df-zring 14909 df-zrh 14932 df-zn 14934 df-lgs 16100

This theorem is referenced by: lgsquadlem3 16181

W3C validator