lgsquadlem2 - Intuitionistic Logic Explorer

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

Theorem lgsquadlem2 15605

Description: Lemma for lgsquad 15607. Count the members of

with even coordinates, and combine with lgsquadlem1 15604 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 15601	. 2
5		lgsquad.4	. . . . . 6
6	5	oveq2i 5965	. . . . 5
7	6	sumeq1i 11724	. . . 4
8	1, 5	gausslemma2dlem0b 15577	. . . . . . . . . . 11
9	8	nnzd 9507	. . . . . . . . . 10
10		2nn 9211	. . . . . . . . . 10
11		znq 9758	. . . . . . . . . 10 $/\$
12	9, 10, 11	sylancl 413	. . . . . . . . 9
13	12	flqcld 10433	. . . . . . . 8
14	13	zred 9508	. . . . . . 7
15	14	ltp1d 9016	. . . . . 6
16		fzdisj 10187	. . . . . 6
17	15, 16	syl 14	. . . . 5
18	8	nnrpd 9829	. . . . . . . . . . 11
19	18	rphalfcld 9844	. . . . . . . . . 10
20	19	rpge0d 9835	. . . . . . . . 9
21		flqge0nn0 10449	. . . . . . . . 9 $/\$
22	12, 20, 21	syl2anc 411	. . . . . . . 8
23	8	nnnn0d 9361	. . . . . . . 8
24	8	nnred 9062	. . . . . . . . 9
25		rphalflt 9818	. . . . . . . . . . 11
26	18, 25	syl 14	. . . . . . . . . 10
27		flqlt 10439	. . . . . . . . . . 11 $/\$
28	12, 9, 27	syl2anc 411	. . . . . . . . . 10
29	26, 28	mpbid 147	. . . . . . . . 9
30	14, 24, 29	ltled 8204	. . . . . . . 8
31		elfz2nn0 10247	. . . . . . . 8 $/\$ $/\$
32	22, 23, 30, 31	syl3anbrc 1184	. . . . . . 7
33		nn0uz 9696	. . . . . . . . 9
34	23, 33	eleqtrdi 2299	. . . . . . . 8
35		elfzp12 10234	. . . . . . . 8 $\/$
36	34, 35	syl 14	. . . . . . 7 $\/$
37	32, 36	mpbid 147	. . . . . 6 $\/$
38		un0 3496	. . . . . . . . 9
39		uncom 3319	. . . . . . . . 9
40	38, 39	eqtr3i 2229	. . . . . . . 8
41		oveq2 5962	. . . . . . . . . 10
42		fz10 10181	. . . . . . . . . 10
43	41, 42	eqtrdi 2255	. . . . . . . . 9
44		oveq1 5961	. . . . . . . . . . 11
45		0p1e1 9163	. . . . . . . . . . 11
46	44, 45	eqtrdi 2255	. . . . . . . . . 10
47	46	oveq1d 5969	. . . . . . . . 9
48	43, 47	uneq12d 3330	. . . . . . . 8
49	40, 48	eqtr4id 2258	. . . . . . 7
50		fzsplit 10186	. . . . . . . 8
51	45	oveq1i 5964	. . . . . . . 8
52	50, 51	eleq2s 2301	. . . . . . 7
53	49, 52	jaoi 718	. . . . . 6 $\/$
54	37, 53	syl 14	. . . . 5
55		1zzd 9412	. . . . . 6
56	55, 9	fzfigd 10589	. . . . 5
57	2	gausslemma2dlem0a 15576	. . . . . . . . . 10
58	57	nnzd 9507	. . . . . . . . 9
59	1	gausslemma2dlem0a 15576	. . . . . . . . . 10
60	59	adantr 276	. . . . . . . . 9 $/\$
61		znq 9758	. . . . . . . . 9 $/\$
62	58, 60, 61	syl2an2r 595	. . . . . . . 8 $/\$
63		elfznn 10189	. . . . . . . . . . . 12
64	63	adantl 277	. . . . . . . . . . 11 $/\$
65		nnmulcl 9070	. . . . . . . . . . 11 $/\$
66	10, 64, 65	sylancr 414	. . . . . . . . . 10 $/\$
67	66	nnzd 9507	. . . . . . . . 9 $/\$
68		zq 9760	. . . . . . . . 9
69	67, 68	syl 14	. . . . . . . 8 $/\$
70		qmulcl 9771	. . . . . . . 8 $/\$
71	62, 69, 70	syl2anc 411	. . . . . . 7 $/\$
72	57	nnrpd 9829	. . . . . . . . . . 11
73	59	nnrpd 9829	. . . . . . . . . . 11
74	72, 73	rpdivcld 9849	. . . . . . . . . 10
75	74	adantr 276	. . . . . . . . 9 $/\$
76	66	nnrpd 9829	. . . . . . . . 9 $/\$
77	75, 76	rpmulcld 9848	. . . . . . . 8 $/\$
78	77	rpge0d 9835	. . . . . . 7 $/\$
79		flqge0nn0 10449	. . . . . . 7 $/\$
80	71, 78, 79	syl2anc 411	. . . . . 6 $/\$
81	80	nn0cnd 9363	. . . . 5 $/\$
82	17, 54, 56, 81	fsumsplit 11768	. . . 4
83	7, 82	eqtr3id 2253	. . 3
84	83	oveq2d 5970	. 2
85		neg1cn 9154	. . . . 5
86	85	a1i 9	. . . 4
87	13	peano2zd 9511	. . . . . 6
88	87, 9	fzfigd 10589	. . . . 5
89		ssun2 3339	. . . . . . . 8
90	89, 54	sseqtrrid 3246	. . . . . . 7
91	90	sselda 3195	. . . . . 6 $/\$
92	91, 80	syldan 282	. . . . 5 $/\$
93	88, 92	fsumnn0cl 11764	. . . 4
94	55, 13	fzfigd 10589	. . . . 5
95		ssun1 3338	. . . . . . . 8
96	95, 54	sseqtrrid 3246	. . . . . . 7
97	96	sselda 3195	. . . . . 6 $/\$
98	97, 80	syldan 282	. . . . 5 $/\$
99	94, 98	fsumnn0cl 11764	. . . 4
100	86, 93, 99	expaddd 10833	. . 3
101		lgsquad.5	. . . . . . 7
102		lgsquad.6	. . . . . . 7 $/\$ $/\$
103	1, 2, 3, 5, 101, 102	lgsquadlemofi 15603	. . . . . 6
104		hashcl 10939	. . . . . 6 ♯
105	103, 104	syl 14	. . . . 5 ♯
106	1, 2, 3, 5, 101, 102	lgsquadlemsfi 15602	. . . . . . 7
107		opabssxp 4754	. . . . . . . . . . . . . 14 $/\$ $/\$
108	102, 107	eqsstri 3227	. . . . . . . . . . . . 13
109	108	sseli 3191	. . . . . . . . . . . 12
110		xp1st 6261	. . . . . . . . . . . 12
111	109, 110	syl 14	. . . . . . . . . . 11
112	111	elfzelzd 10161	. . . . . . . . . 10
113	112	adantl 277	. . . . . . . . 9 $/\$
114		dvdsdc 12159	. . . . . . . . 9 $/\$ DECID
115	10, 113, 114	sylancr 414	. . . . . . . 8 $/\$ DECID
116	115	ralrimiva 2580	. . . . . . 7 DECID
117	106, 116	ssfirab 7045	. . . . . 6
118		hashcl 10939	. . . . . 6 ♯
119	117, 118	syl 14	. . . . 5 ♯
120	86, 105, 119	expaddd 10833	. . . 4 ♯ ♯ ♯ ♯
121	97, 66	syldan 282	. . . . . . . . . . 11 $/\$
122		1zzd 9412	. . . . . . . . . . . 12 $/\$
123	98	nn0zd 9506	. . . . . . . . . . . 12 $/\$
124	122, 123	fzfigd 10589	. . . . . . . . . . 11 $/\$
125		xpsnen2g 6936	. . . . . . . . . . 11 $/\$
126	121, 124, 125	syl2anc 411	. . . . . . . . . 10 $/\$
127		snfig 6917	. . . . . . . . . . . . 13
128	121, 127	syl 14	. . . . . . . . . . . 12 $/\$
129		xpfi 7041	. . . . . . . . . . . 12 $/\$
130	128, 124, 129	syl2anc 411	. . . . . . . . . . 11 $/\$
131		hashen 10942	. . . . . . . . . . 11 $/\$ ♯ ♯
132	130, 124, 131	syl2anc 411	. . . . . . . . . 10 $/\$ ♯ ♯
133	126, 132	mpbird 167	. . . . . . . . 9 $/\$ ♯ ♯
134		ssrab2 3280	. . . . . . . . . . . . 13
135	102	relopabiv 4806	. . . . . . . . . . . . 13
136		relss 4767	. . . . . . . . . . . . 13
137	134, 135, 136	mp2 16	. . . . . . . . . . . 12
138		relxp 4789	. . . . . . . . . . . 12
139	102	eleq2i 2273	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140		opabidw 4308	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	139, 140	bitri 184	. . . . . . . . . . . . . . 15 $/\$ $/\$
142		anass 401	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
143	121	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
144	143	nnred 9062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
145	59	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
146	145	nnred 9062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
147	146	rehalfcld 9297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
148	24	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
149	148	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
150		elfzle2 10163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151	150	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
152		elfzelz 10160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153		flqge 10438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
154	12, 152, 153	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
155	151, 154	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
156		elfznn 10189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
157	156	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
158	157	nnred 9062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
159		2re 9119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
161		2pos 9140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
163		lemuldiv2 8968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
164	158, 148, 160, 162, 163	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
165	155, 164	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
166	165	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
167	146	ltm1d 9018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
168		peano2rem 8352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
169	146, 168	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
170	159	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
171	161	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
172		ltdiv1 8954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
173	169, 146, 170, 171, 172	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
174	167, 173	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
175	5, 174	eqbrtrid 4083	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
176	144, 149, 147, 166, 175	lelttrd 8210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	145	nnrpd 9829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
178		rphalflt 9818	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	177, 178	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
180	144, 147, 146, 176, 179	lttrd 8211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	143	nnzd 9507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
182	145	nnzd 9507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
183		zltnle 9431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
184	181, 182, 183	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
185	180, 184	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
186	1	eldifad 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		prmz 12483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
189	187, 188	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
190		dvdsle 12205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
191	189, 143, 190	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	185, 191	mtod 665	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
193	2	eldifad 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194		prmrp 12517	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	198, 199	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
201		coprmdvds 12464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
202	189, 200, 181, 201	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
203	197, 202	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	192, 203	mtod 665	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		nnz 9404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
206	205	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
207		dvdsmul2 12175	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	206, 189, 207	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209		breq2 4052	. . . . . . . . . . . . . . . . . . . . . . . . 25
210	208, 209	syl5ibrcom 157	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
211	210	necon3bd 2420	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
212	204, 211	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
213		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
214	213, 145	nnmulcld 9098	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
215	214	nnzd 9507	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
216	57	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
217	216, 121	nnmulcld 9098	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
218	217	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
219	218	nnzd 9507	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220		zltlen 9464	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
221	215, 219, 220	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
222	212, 221	mpbiran2d 442	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
223		nnre 9056	. . . . . . . . . . . . . . . . . . . . . . 23
224	223	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	218	nnred 9062	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
226	145	nngt0d 9093	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
227		lemuldiv 8967	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
228	224, 225, 146, 226, 227	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
229	216	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
230	229	nncnd 9063	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
231	143	nncnd 9063	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
232	145	nncnd 9063	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
233	146, 226	gt0ap0d 8715	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ #
234	230, 231, 232, 233	div23apd 8914	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
235	234	breq2d 4060	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
236	222, 228, 235	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
237	229	nnred 9062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
238	229	nngt0d 9093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
239		ltmul2 8942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
240	144, 147, 237, 238, 239	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
241	176, 240	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
242		2cnd 9122	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
243	170, 171	gt0ap0d 8715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ #
244		divassap 8776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
245		div23ap 8777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ #
246	244, 245	eqtr3d 2241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ #
247	230, 232, 242, 243, 246	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
248	241, 247	breqtrd 4074	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
249	214	nnred 9062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
250	237	rehalfcld 9297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
251	250, 146	remulcld 8116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
252		lttr 8159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
253	249, 225, 251, 252	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
254	248, 253	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
255		ltmul1 8678	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
256	224, 250, 146, 226, 255	syl112anc 1254	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
257	254, 256	sylibrd 169	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
258		peano2rem 8352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
259	237, 258	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
260	259	recnd 8114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
261	230, 260, 242, 243	divsubdirapd 8916	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
262	101	oveq2i 5965	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
263	261, 262	eqtr4di 2257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
264		ax-1cn 8031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
265		nncan 8314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
266	230, 264, 265	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
267	266	oveq1d 5969	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
268		halflt1 9267	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
269	267, 268	eqbrtrdi 4087	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
270	263, 269	eqbrtrrd 4072	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	2, 101	gausslemma2dlem0b 15577	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
272	271	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
273	272	nnred 9062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
274		1red 8100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
275	250, 273, 274	ltsubadd2d 8629	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
276	270, 275	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
277		peano2re 8221	. . . . . . . . . . . . . . . . . . . . . . . . . 26
278	273, 277	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
279		lttr 8159	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
280	224, 250, 278, 279	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
281	276, 280	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
282	257, 281	syld 45	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
283		nnleltp1 9445	. . . . . . . . . . . . . . . . . . . . . . 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 10438	. . . . . . . . . . . . . . . . . . . . 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 9697	. . . . . . . . . . . . . . . . . . . . . . . 24
296	121, 295	eleqtrdi 2299	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
297	9	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
298		elfz5 10152	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
299	296, 297, 298	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	165, 299	mpbird 167	. . . . . . . . . . . . . . . . . . . . 21 $/\$
301	300	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
302	294, 301	eqeltrd 2283	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
303	302	biantrurd 305	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
304	271	nnzd 9507	. . . . . . . . . . . . . . . . . . . 20
305	304	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
306		fznn 10224	. . . . . . . . . . . . . . . . . . 19 $/\$
307	305, 306	syl 14	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
308	303, 307	bitr3d 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
309		oveq1 5961	. . . . . . . . . . . . . . . . . . 19
310	121	nncnd 9063	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	216	nncnd 9063	. . . . . . . . . . . . . . . . . . . 20 $/\$
312	310, 311	mulcomd 8107	. . . . . . . . . . . . . . . . . . 19 $/\$
313	309, 312	sylan9eqr 2261	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
314	313	breq2d 4060	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
315	308, 314	anbi12d 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
316	287	flqcld 10433	. . . . . . . . . . . . . . . . . 18 $/\$
317		fznn 10224	. . . . . . . . . . . . . . . . . 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 2776	. . . . . . . . . . . . . . . . . 18
324		vex 2776	. . . . . . . . . . . . . . . . . 18
325	323, 324	op1std 6244	. . . . . . . . . . . . . . . . 17
326	325	eqeq2d 2218	. . . . . . . . . . . . . . . 16
327		eqcom 2208	. . . . . . . . . . . . . . . 16
328	326, 327	bitrdi 196	. . . . . . . . . . . . . . 15
329	328	elrab 2931	. . . . . . . . . . . . . 14 $/\$
330	329	biancomi 270	. . . . . . . . . . . . 13 $/\$
331		opelxp 4710	. . . . . . . . . . . . . 14 $/\$
332		velsn 3652	. . . . . . . . . . . . . . 15
333	332	anbi1i 458	. . . . . . . . . . . . . 14 $/\$ $/\$
334	331, 333	bitri 184	. . . . . . . . . . . . 13 $/\$
335	322, 330, 334	3bitr4g 223	. . . . . . . . . . . 12 $/\$
336	137, 138, 335	eqrelrdv 4776	. . . . . . . . . . 11 $/\$
337	336	eqcomd 2212	. . . . . . . . . 10 $/\$
338	337	fveq2d 5590	. . . . . . . . 9 $/\$ ♯ ♯
339		hashfz1 10941	. . . . . . . . . 10 ♯
340	98, 339	syl 14	. . . . . . . . 9 $/\$ ♯
341	133, 338, 340	3eqtr3rd 2248	. . . . . . . 8 $/\$ ♯
342	341	sumeq2dv 11729	. . . . . . 7 ♯
343	106	adantr 276	. . . . . . . . 9 $/\$
344	97, 67	syldan 282	. . . . . . . . . . 11 $/\$
345		zdceq 9461	. . . . . . . . . . 11 $/\$ DECID
346	344, 112, 345	syl2an 289	. . . . . . . . . 10 $/\$ $/\$ DECID
347	346	ralrimiva 2580	. . . . . . . . 9 $/\$ DECID
348	343, 347	ssfirab 7045	. . . . . . . 8 $/\$
349		fveq2 5586	. . . . . . . . . . . . . . . 16
350	349	eqeq2d 2218	. . . . . . . . . . . . . . 15
351	350	elrab 2931	. . . . . . . . . . . . . 14 $/\$
352	351	simprbi 275	. . . . . . . . . . . . 13
353	352	ad2antll 491	. . . . . . . . . . . 12 $/\$ $/\$
354	353	oveq1d 5969	. . . . . . . . . . 11 $/\$ $/\$
355	157	nncnd 9063	. . . . . . . . . . . . 13 $/\$
356	355	adantrr 479	. . . . . . . . . . . 12 $/\$ $/\$
357		2cnd 9122	. . . . . . . . . . . 12 $/\$ $/\$
358		2ap0 9142	. . . . . . . . . . . . 13 #
359	358	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ #
360	356, 357, 359	divcanap3d 8881	. . . . . . . . . . 11 $/\$ $/\$
361	354, 360	eqtr3d 2241	. . . . . . . . . 10 $/\$ $/\$
362	361	ralrimivva 2589	. . . . . . . . 9
363		invdisj 4041	. . . . . . . . 9 Disj
364	362, 363	syl 14	. . . . . . . 8 Disj
365	94, 348, 364	hashiun 11839	. . . . . . 7 ♯ ♯
366		iunrab 3978	. . . . . . . . 9
367		2cn 9120	. . . . . . . . . . . . . 14
368		zcn 9390	. . . . . . . . . . . . . . 15
369	368	adantl 277	. . . . . . . . . . . . . 14 $/\$ $/\$
370		mulcom 8067	. . . . . . . . . . . . . 14 $/\$
371	367, 369, 370	sylancr 414	. . . . . . . . . . . . 13 $/\$ $/\$
372	371	eqeq1d 2215	. . . . . . . . . . . 12 $/\$ $/\$
373	372	rexbidva 2504	. . . . . . . . . . 11 $/\$
374	152	anim1i 340	. . . . . . . . . . . . 13 $/\$ $/\$
375	374	reximi2 2603	. . . . . . . . . . . 12
376		simprr 531	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
377		simpr 110	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	108, 377	sselid 3193	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
379	378, 110	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$
380	379	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
381		elfzle2 10163	. . . . . . . . . . . . . . . . . . . 20
382	380, 381	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
383	376, 382	eqbrtrd 4070	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
384		zre 9389	. . . . . . . . . . . . . . . . . . . 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 1254	. . . . . . . . . . . . . . . . . 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 9209	. . . . . . . . . . . . . . . . . . . . 21
396		elfznn 10189	. . . . . . . . . . . . . . . . . . . . . . . 24
397	380, 396	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
398	376, 397	eqeltrd 2283	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
399	398	nngt0d 9093	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
400	395, 399	eqbrtrid 4083	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
401		0red 8086	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
402		ltmul2 8942	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
403	401, 385, 387, 388, 402	syl112anc 1254	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
404	400, 403	mpbird 167	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
405		elnnz 9395	. . . . . . . . . . . . . . . . . . 19 $/\$
406	392, 404, 405	sylanbrc 417	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
407	406, 295	eleqtrdi 2299	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
408	13	ad2antrr 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
409		elfz5 10152	. . . . . . . . . . . . . . . . 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 2606	. . . . . . . . . . . 12 $/\$
415	375, 414	impbid2 143	. . . . . . . . . . 11 $/\$
416		2z 9413	. . . . . . . . . . . 12
417	379	elfzelzd 10161	. . . . . . . . . . . 12 $/\$
418		divides 12150	. . . . . . . . . . . 12 $/\$
419	416, 417, 418	sylancr 414	. . . . . . . . . . 11 $/\$
420	373, 415, 419	3bitr4d 220	. . . . . . . . . 10 $/\$
421	420	rabbidva 2761	. . . . . . . . 9
422	366, 421	eqtrid 2251	. . . . . . . 8
423	422	fveq2d 5590	. . . . . . 7 ♯ ♯
424	342, 365, 423	3eqtr2d 2245	. . . . . 6 ♯
425	424	oveq2d 5970	. . . . 5 ♯
426	1, 2, 3, 5, 101, 102	lgsquadlem1 15604	. . . . 5 ♯
427	425, 426	oveq12d 5972	. . . 4 ♯ ♯
428	120, 427	eqtr4d 2242	. . 3 ♯ ♯
429		inrab 3447	. . . . . . 7 $/\$
430		pm3.24 695	. . . . . . . . . 10 $/\$
431	430	a1i 9	. . . . . . . . 9 $/\$
432	431	ralrimivw 2581	. . . . . . . 8 $/\$
433		rabeq0 3492	. . . . . . . 8 $/\$ $/\$
434	432, 433	sylibr 134	. . . . . . 7 $/\$
435	429, 434	eqtrid 2251	. . . . . 6
436		hashun 10963	. . . . . 6 $/\$ $/\$ ♯ ♯ ♯
437	117, 103, 435, 436	syl3anc 1250	. . . . 5 ♯ ♯ ♯
438		unrab 3446	. . . . . . 7 $\/$
439		rabid2 2684	. . . . . . . 8 $\/$ $\/$
440	10, 112, 114	sylancr 414	. . . . . . . . 9 DECID
441		exmiddc 838	. . . . . . . . 9 DECID $\/$
442	440, 441	syl 14	. . . . . . . 8 $\/$
443	439, 442	mprgbir 2565	. . . . . . 7 $\/$
444	438, 443	eqtr4i 2230	. . . . . 6
445	444	fveq2i 5589	. . . . 5 ♯ ♯
446	437, 445	eqtr3di 2254	. . . 4 ♯ ♯ ♯
447	446	oveq2d 5970	. . 3 ♯ ♯ ♯
448	100, 428, 447	3eqtr2d 2245	. 2 ♯
449	4, 84, 448	3eqtrd 2243	1 ♯

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710 DECID wdc 836 $/\$ w3a 981

wceq 1373

wcel 2177

wne 2377

wral 2485

wrex 2486

crab 2489 $\$ cdif 3165

cun 3166

cin 3167

wss 3168

c0 3462

csn 3635

cop 3638

ciun 3930 Disj wdisj 4024 class class class wbr 4048

copab 4109

cxp 4678

wrel 4685

cfv 5277 (class class class)co 5954

c1st 6234

cen 6835

cfn 6837

cc 7936

cr 7937

cc0 7938

c1 7939

caddc 7941

cmul 7943

clt 8120

cle 8121

cmin 8256

cneg 8257 # cap 8667

cdiv 8758

cn 9049

c2 9100

cn0 9308

cz 9385

cuz 9661

cq 9753

crp 9788

cfz 10143

cfl 10424

cexp 10696 ♯chash 10933

csu 11714

cdvds 12148

cgcd 12324

cprime 12479

clgs 15524

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4164 ax-sep 4167 ax-nul 4175 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-iinf 4641 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053 ax-pre-ltadd 8054 ax-pre-mulgt0 8055 ax-pre-mulext 8056 ax-arch 8057 ax-caucvg 8058 ax-addf 8060 ax-mulf 8061

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-xor 1396 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3001 df-csb 3096 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-nul 3463 df-if 3574 df-pw 3620 df-sn 3641 df-pr 3642 df-tp 3643 df-op 3644 df-uni 3854 df-int 3889 df-iun 3932 df-disj 4025 df-br 4049 df-opab 4111 df-mpt 4112 df-tr 4148 df-id 4345 df-po 4348 df-iso 4349 df-iord 4418 df-on 4420 df-ilim 4421 df-suc 4423 df-iom 4644 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-ima 4693 df-iota 5238 df-fun 5279 df-fn 5280 df-f 5281 df-f1 5282 df-fo 5283 df-f1o 5284 df-fv 5285 df-isom 5286 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-of 6168 df-1st 6236 df-2nd 6237 df-tpos 6341 df-recs 6401 df-irdg 6466 df-frec 6487 df-1o 6512 df-2o 6513 df-oadd 6516 df-er 6630 df-ec 6632 df-qs 6636 df-map 6747 df-en 6838 df-dom 6839 df-fin 6840 df-sup 7098 df-inf 7099 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126 df-sub 8258 df-neg 8259 df-reap 8661 df-ap 8668 df-div 8759 df-inn 9050 df-2 9108 df-3 9109 df-4 9110 df-5 9111 df-6 9112 df-7 9113 df-8 9114 df-9 9115 df-n0 9309 df-z 9386 df-dec 9518 df-uz 9662 df-q 9754 df-rp 9789 df-fz 10144 df-fzo 10278 df-fl 10426 df-mod 10481 df-seqfrec 10606 df-exp 10697 df-ihash 10934 df-cj 11203 df-re 11204 df-im 11205 df-rsqrt 11359 df-abs 11360 df-clim 11640 df-sumdc 11715 df-proddc 11912 df-dvds 12149 df-gcd 12325 df-prm 12480 df-phi 12583 df-pc 12658 df-struct 12884 df-ndx 12885 df-slot 12886 df-base 12888 df-sets 12889 df-iress 12890 df-plusg 12972 df-mulr 12973 df-starv 12974 df-sca 12975 df-vsca 12976 df-ip 12977 df-tset 12978 df-ple 12979 df-ds 12981 df-unif 12982 df-0g 13140 df-igsum 13141 df-topgen 13142 df-iimas 13184 df-qus 13185 df-mgm 13238 df-sgrp 13284 df-mnd 13299 df-mhm 13341 df-submnd 13342 df-grp 13385 df-minusg 13386 df-sbg 13387 df-mulg 13506 df-subg 13556 df-nsg 13557 df-eqg 13558 df-ghm 13627 df-cmn 13672 df-abl 13673 df-mgp 13733 df-rng 13745 df-ur 13772 df-srg 13776 df-ring 13810 df-cring 13811 df-oppr 13880 df-dvdsr 13901 df-unit 13902 df-invr 13933 df-dvr 13944 df-rhm 13964 df-nzr 13992 df-subrg 14031 df-domn 14071 df-idom 14072 df-lmod 14101 df-lssm 14165 df-lsp 14199 df-sra 14247 df-rgmod 14248 df-lidl 14281 df-rsp 14282 df-2idl 14312 df-bl 14358 df-mopn 14359 df-fg 14361 df-metu 14362 df-cnfld 14369 df-zring 14403 df-zrh 14426 df-zn 14428 df-lgs 15525

This theorem is referenced by: lgsquadlem3 15606

W3C validator