lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 15742

Description: Lemma for lgsquad 15744. Count the members of

with even coordinates, and combine with lgsquadlem1 15741 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 15738	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 6005	. . . . 5
7	6	sumeq1i 11860	. . . 4
8	1, 5	gausslemma2dlem0b 15714	. . . . . . . . . . 11
9	8	nnzd 9556	. . . . . . . . . 10
10		2nn 9260	. . . . . . . . . 10
11		znq 9807	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 413	. . . . . . . . 9
13	12	flqcld 10484	. . . . . . . 8
14	13	zred 9557	. . . . . . 7
15	14	ltp1d 9065	. . . . . 6
16		fzdisj 10236	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 9878	. . . . . . . . . . 11
19	18	rphalfcld 9893	. . . . . . . . . 10
20	19	rpge0d 9884	. . . . . . . . 9
21		flqge0nn0 10500	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 411	. . . . . . . 8
23	8	nnnn0d 9410	. . . . . . . 8
24	8	nnred 9111	. . . . . . . . 9
25		rphalflt 9867	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10490	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 411	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8253	. . . . . . . 8
31		elfz2nn0 10296	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1205	. . . . . . 7
33		nn0uz 9745	. . . . . . . . 9
34	23, 33	eleqtrdi 2322	. . . . . . . 8
35		elfzp12 10283	. . . . . . . 8 $\/$
36	34, 35	syl 14	. . . . . . 7 $\/$
37	32, 36	mpbid 147	. . . . . 6 $\/$
38		un0 3525	. . . . . . . . 9
39		uncom 3348	. . . . . . . . 9
40	38, 39	eqtr3i 2252	. . . . . . . 8
41		oveq2 6002	. . . . . . . . . 10
42		fz10 10230	. . . . . . . . . 10
43	41, 42	eqtrdi 2278	. . . . . . . . 9
44		oveq1 6001	. . . . . . . . . . 11
45		0p1e1 9212	. . . . . . . . . . 11
46	44, 45	eqtrdi 2278	. . . . . . . . . 10
47	46	oveq1d 6009	. . . . . . . . 9
48	43, 47	uneq12d 3359	. . . . . . . 8
49	40, 48	eqtr4id 2281	. . . . . . 7
50		fzsplit 10235	. . . . . . . 8
51	45	oveq1i 6004	. . . . . . . 8
52	50, 51	eleq2s 2324	. . . . . . 7
53	49, 52	jaoi 721	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9461	. . . . . 6
56	55, 9	fzfigd 10640	. . . . 5
57	2	gausslemma2dlem0a 15713	. . . . . . . . . 10
58	57	nnzd 9556	. . . . . . . . 9
59	1	gausslemma2dlem0a 15713	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 9807	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 597	. . . . . . . 8 $/\$
63		elfznn 10238	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9119	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 414	. . . . . . . . . 10 $/\$
67	66	nnzd 9556	. . . . . . . . 9 $/\$
68		zq 9809	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 9820	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 411	. . . . . . 7 $/\$
72	57	nnrpd 9878	. . . . . . . . . . 11
73	59	nnrpd 9878	. . . . . . . . . . 11
74	72, 73	rpdivcld 9898	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 9878	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 9897	. . . . . . . 8 $/\$
78	77	rpge0d 9884	. . . . . . 7 $/\$
79		flqge0nn0 10500	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 411	. . . . . 6 $/\$
81	80	nn0cnd 9412	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 11904	. . . 4
83	7, 82	eqtr3id 2276	. . 3
84	83	oveq2d 6010	. 2
85		neg1cn 9203	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9560	. . . . . 6
88	87, 9	fzfigd 10640	. . . . 5
89		ssun2 3368	. . . . . . . 8
90	89, 54	sseqtrrid 3275	. . . . . . 7
91	90	sselda 3224	. . . . . 6 $/\$
92	91, 80	syldan 282	. . . . 5 $/\$
93	88, 92	fsumnn0cl 11900	. . . 4
94	55, 13	fzfigd 10640	. . . . 5
95		ssun1 3367	. . . . . . . 8
96	95, 54	sseqtrrid 3275	. . . . . . 7
97	96	sselda 3224	. . . . . 6 $/\$
98	97, 80	syldan 282	. . . . 5 $/\$
99	94, 98	fsumnn0cl 11900	. . . 4
100	86, 93, 99	expaddd 10884	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 15740	. . . . . 6
104		hashcl 10990	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 15739	. . . . . . 7
107		opabssxp 4790	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3256	. . . . . . . . . . . . 13
109	108	sseli 3220	. . . . . . . . . . . 12
110		xp1st 6301	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10210	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 12295	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 414	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2603	. . . . . . 7 DECID
117	106, 116	ssfirab 7086	. . . . . 6
118		hashcl 10990	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 10884	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9461	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9555	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10640	. . . . . . . . . . 11 $/\$
125		xpsnen2g 6976	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 411	. . . . . . . . . 10 $/\$
127		snfig 6957	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 7082	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 411	. . . . . . . . . . 11 $/\$
131		hashen 10993	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 411	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3309	. . . . . . . . . . . . 13
135	102	relopabiv 4842	. . . . . . . . . . . . 13
136		relss 4803	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4825	. . . . . . . . . . . 12
139	102	eleq2i 2296	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4344	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 401	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 9111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 9111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 9111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 9017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 9067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 9003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4117	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8259	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 9878	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 9867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
184	181, 182, 183	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
186	1	eldifad 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		prmz 12619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 12341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 667	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12653	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12600	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 12311	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4086	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
211	210	necon3bd 2443	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
214	213, 145	nnmulcld 9147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9556	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9556	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9513	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 9105	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 9111	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9142	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 9016	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 9112	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 9112	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 9112	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8764	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 8963	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4094	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 9111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 8991	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9171	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 8825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 8826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4108	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 9111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8727	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8163	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 8965	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 6005	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 8080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9316	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4121	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4106	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 15714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 9111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8678	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8270	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8208	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9494	. . . . . . . . . . . . . . . . . . . . . . 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 10489	. . . . . . . . . . . . . . . . . . . . 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 9746	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2322	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10201	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	296, 297, 298	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 $/\$
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
302	294, 301	eqeltrd 2306	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
304	271	nnzd 9556	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10273	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 6001	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 9112	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 9112	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8156	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2284	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4094	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10484	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10273	. . . . . . . . . . . . . . . . . 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 2802	. . . . . . . . . . . . . . . . . 18
324		vex 2802	. . . . . . . . . . . . . . . . . 18
325	323, 324	op1std 6284	. . . . . . . . . . . . . . . . 17
326	325	eqeq2d 2241	. . . . . . . . . . . . . . . 16
327		eqcom 2231	. . . . . . . . . . . . . . . 16
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15
329	328	elrab 2959	. . . . . . . . . . . . . 14 $/\$
330	329	biancomi 270	. . . . . . . . . . . . 13 $/\$
331		opelxp 4746	. . . . . . . . . . . . . 14 $/\$
332		velsn 3683	. . . . . . . . . . . . . . 15
333	332	anbi1i 458	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4812	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2235	. . . . . . . . . 10 $/\$
338	337	fveq2d 5627	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 10992	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2271	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 11865	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9510	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2603	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 7086	. . . . . . . 8 $/\$
349		fveq2 5623	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2241	. . . . . . . . . . . . . . 15
351	350	elrab 2959	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 491	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 6009	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 9112	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 479	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9171	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9191	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 8930	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2264	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2612	. . . . . . . . 9
363		invdisj 4075	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 11975	. . . . . . 7 ♯ ♯
366		iunrab 4012	. . . . . . . . 9
367		2cn 9169	. . . . . . . . . . . . . 14
368		zcn 9439	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8116	. . . . . . . . . . . . . 14 $/\$
371	367, 369, 370	sylancr 414	. . . . . . . . . . . . 13 $/\$ $/\$
372	371	eqeq1d 2238	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidva 2527	. . . . . . . . . . 11 $/\$
374	152	anim1i 340	. . . . . . . . . . . . 13 $/\$ $/\$
375	374	reximi2 2626	. . . . . . . . . . . 12
376		simprr 531	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	108, 377	sselid 3222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
381		elfzle2 10212	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4104	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9438	. . . . . . . . . . . . . . . . . . . 20
385	384	ad2antrl 490	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
386	24	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
387	159	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
388	161	a1i 9	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
389	385, 386, 387, 388, 163	syl112anc 1275	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
390	383, 389	mpbid 147	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
391	12	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
392		simprl 529	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
393	391, 392, 153	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
394	390, 393	mpbid 147	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
395		2t0e0 9258	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10238	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2306	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9142	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4117	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8135	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 8991	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1275	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9444	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 417	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2322	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10201	. . . . . . . . . . . . . . . . 17 $/\$
410	407, 408, 409	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
411	394, 410	mpbird 167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
412	411, 376	jca 306	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
413	412	ex 115	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
414	413	reximdv2 2629	. . . . . . . . . . . 12 $/\$
415	375, 414	impbid2 143	. . . . . . . . . . 11 $/\$
416		2z 9462	. . . . . . . . . . . 12
417	379	elfzelzd 10210	. . . . . . . . . . . 12 $/\$
418		divides 12286	. . . . . . . . . . . 12 $/\$
419	416, 417, 418	sylancr 414	. . . . . . . . . . 11 $/\$
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 $/\$
421	420	rabbidva 2787	. . . . . . . . 9
422	366, 421	eqtrid 2274	. . . . . . . 8
423	422	fveq2d 5627	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2268	. . . . . 6 ♯
425	424	oveq2d 6010	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 15741	. . . . 5 ♯
427	425, 426	oveq12d 6012	. . . 4 ♯ ♯
428	120, 427	eqtr4d 2265	. . 3 ♯ ♯
429		inrab 3476	. . . . . . 7 $/\$
430		pm3.24 698	. . . . . . . . . 10 $/\$
431	430	a1i 9	. . . . . . . . 9 $/\$
432	431	ralrimivw 2604	. . . . . . . 8 $/\$
433		rabeq0 3521	. . . . . . . 8 $/\$ $/\$
434	432, 433	sylibr 134	. . . . . . 7 $/\$
435	429, 434	eqtrid 2274	. . . . . 6
436		hashun 11014	. . . . . 6 $/\$ $/\$ ♯ ♯ ♯
437	117, 103, 435, 436	syl3anc 1271	. . . . 5 ♯ ♯ ♯
438		unrab 3475	. . . . . . 7 $\/$
439		rabid2 2708	. . . . . . . 8 $\/$ $\/$
440	10, 112, 114	sylancr 414	. . . . . . . . 9 DECID
441		exmiddc 841	. . . . . . . . 9 DECID $\/$
442	440, 441	syl 14	. . . . . . . 8 $\/$
443	439, 442	mprgbir 2588	. . . . . . 7 $\/$
444	438, 443	eqtr4i 2253	. . . . . 6
445	444	fveq2i 5626	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2277	. . . 4 ♯ ♯ ♯
447	446	oveq2d 6010	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2268	. 2 ♯
449	4, 84, 448	3eqtrd 2266	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

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

wceq 1395

wcel 2200

wne 2400

wral 2508

wrex 2509

crab 2512 $\$ cdif 3194

cun 3195

cin 3196

wss 3197

c0 3491

csn 3666

cop 3669

ciun 3964 Disj wdisj 4058 class class class wbr 4082

copab 4143

cxp 4714

wrel 4721

cfv 5314 (class class class)co 5994

c1st 6274

cen 6875

cfn 6877

cc 7985

cr 7986

cc0 7987

c1 7988

caddc 7990

cmul 7992

clt 8169

cle 8170

cmin 8305

cneg 8306 # cap 8716

cdiv 8807

cn 9098

c2 9149

cn0 9357

cz 9434

cuz 9710

cq 9802

crp 9837

cfz 10192

cfl 10475

cexp 10747 ♯chash 10984

csu 11850

cdvds 12284

cgcd 12460

cprime 12615

clgs 15661

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-setind 4626 ax-iinf 4677 ax-cnex 8078 ax-resscn 8079 ax-1cn 8080 ax-1re 8081 ax-icn 8082 ax-addcl 8083 ax-addrcl 8084 ax-mulcl 8085 ax-mulrcl 8086 ax-addcom 8087 ax-mulcom 8088 ax-addass 8089 ax-mulass 8090 ax-distr 8091 ax-i2m1 8092 ax-0lt1 8093 ax-1rid 8094 ax-0id 8095 ax-rnegex 8096 ax-precex 8097 ax-cnre 8098 ax-pre-ltirr 8099 ax-pre-ltwlin 8100 ax-pre-lttrn 8101 ax-pre-apti 8102 ax-pre-ltadd 8103 ax-pre-mulgt0 8104 ax-pre-mulext 8105 ax-arch 8106 ax-caucvg 8107 ax-addf 8109 ax-mulf 8110

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-xor 1418 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-tp 3674 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-disj 4059 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4381 df-po 4384 df-iso 4385 df-iord 4454 df-on 4456 df-ilim 4457 df-suc 4459 df-iom 4680 df-xp 4722 df-rel 4723 df-cnv 4724 df-co 4725 df-dm 4726 df-rn 4727 df-res 4728 df-ima 4729 df-iota 5274 df-fun 5316 df-fn 5317 df-f 5318 df-f1 5319 df-fo 5320 df-f1o 5321 df-fv 5322 df-isom 5323 df-riota 5947 df-ov 5997 df-oprab 5998 df-mpo 5999 df-of 6208 df-1st 6276 df-2nd 6277 df-tpos 6381 df-recs 6441 df-irdg 6506 df-frec 6527 df-1o 6552 df-2o 6553 df-oadd 6556 df-er 6670 df-ec 6672 df-qs 6676 df-map 6787 df-en 6878 df-dom 6879 df-fin 6880 df-sup 7139 df-inf 7140 df-pnf 8171 df-mnf 8172 df-xr 8173 df-ltxr 8174 df-le 8175 df-sub 8307 df-neg 8308 df-reap 8710 df-ap 8717 df-div 8808 df-inn 9099 df-2 9157 df-3 9158 df-4 9159 df-5 9160 df-6 9161 df-7 9162 df-8 9163 df-9 9164 df-n0 9358 df-z 9435 df-dec 9567 df-uz 9711 df-q 9803 df-rp 9838 df-fz 10193 df-fzo 10327 df-fl 10477 df-mod 10532 df-seqfrec 10657 df-exp 10748 df-ihash 10985 df-cj 11339 df-re 11340 df-im 11341 df-rsqrt 11495 df-abs 11496 df-clim 11776 df-sumdc 11851 df-proddc 12048 df-dvds 12285 df-gcd 12461 df-prm 12616 df-phi 12719 df-pc 12794 df-struct 13020 df-ndx 13021 df-slot 13022 df-base 13024 df-sets 13025 df-iress 13026 df-plusg 13109 df-mulr 13110 df-starv 13111 df-sca 13112 df-vsca 13113 df-ip 13114 df-tset 13115 df-ple 13116 df-ds 13118 df-unif 13119 df-0g 13277 df-igsum 13278 df-topgen 13279 df-iimas 13321 df-qus 13322 df-mgm 13375 df-sgrp 13421 df-mnd 13436 df-mhm 13478 df-submnd 13479 df-grp 13522 df-minusg 13523 df-sbg 13524 df-mulg 13643 df-subg 13693 df-nsg 13694 df-eqg 13695 df-ghm 13764 df-cmn 13809 df-abl 13810 df-mgp 13870 df-rng 13882 df-ur 13909 df-srg 13913 df-ring 13947 df-cring 13948 df-oppr 14017 df-dvdsr 14038 df-unit 14039 df-invr 14070 df-dvr 14081 df-rhm 14101 df-nzr 14129 df-subrg 14168 df-domn 14208 df-idom 14209 df-lmod 14238 df-lssm 14302 df-lsp 14336 df-sra 14384 df-rgmod 14385 df-lidl 14418 df-rsp 14419 df-2idl 14449 df-bl 14495 df-mopn 14496 df-fg 14498 df-metu 14499 df-cnfld 14506 df-zring 14540 df-zrh 14563 df-zn 14565 df-lgs 15662

This theorem is referenced by: lgsquadlem3 15743

W3C validator