4sqlem11 - Intuitionistic Logic Explorer

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

Theorem 4sqlem11 13124

Description: Lemma for 4sq 13133. Use the pigeonhole principle to show that the sets

and

have a common element,

. Note that although the conclusion is stated in terms of

being nonempty, it is also inhabited by 4sqleminfi 13120 and fin0 7155. (Contributed by Mario Carneiro, 15-Jul-2014.)

**Hypotheses**
Ref	Expression
4sqlem11.1
4sq.2
4sq.3
4sq.4
4sqlem11.5
4sqlem11.6

**Assertion**
Ref	Expression
4sqlem11

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem 4sqlem11 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4sq.2	. . . . . . 7
2		4sq.4	. . . . . . . 8
3		prmnn 12832	. . . . . . . 8
4	2, 3	syl 14	. . . . . . 7
5		4sqlem11.5	. . . . . . 7
6	1, 4, 5	4sqlemafi 13118	. . . . . 6
7		4sqlem11.6	. . . . . . 7
8	1, 4, 5, 7	4sqlemffi 13119	. . . . . 6
9	1, 4, 5, 7	4sqleminfi 13120	. . . . . 6
10		unfiin 7199	. . . . . 6 $/\$ $/\$
11	6, 8, 9, 10	syl3anc 1274	. . . . 5
12		hashcl 11169	. . . . 5 ♯
13	11, 12	syl 14	. . . 4 ♯
14	13	nn0red 9571	. . 3 ♯
15		prmz 12833	. . . . 5
16	2, 15	syl 14	. . . 4
17	16	zred 9718	. . 3
18		0zd 9606	. . . . . . 7
19		peano2zm 9632	. . . . . . . 8
20	16, 19	syl 14	. . . . . . 7
21	18, 20	fzfigd 10817	. . . . . 6
22		elfzelz 10378	. . . . . . . . . . . . 13
23		zsqcl 10996	. . . . . . . . . . . . 13
24	22, 23	syl 14	. . . . . . . . . . . 12
25		zmodfz 10732	. . . . . . . . . . . 12 $/\$
26	24, 4, 25	syl2anr 290	. . . . . . . . . . 11 $/\$
27		eleq1a 2306	. . . . . . . . . . 11
28	26, 27	syl 14	. . . . . . . . . 10 $/\$
29	28	rexlimdva 2662	. . . . . . . . 9
30	29	abssdv 3316	. . . . . . . 8
31	5, 30	eqsstrid 3288	. . . . . . 7
32	20	zcnd 9719	. . . . . . . . . . . . 13
33	32	addlidd 8439	. . . . . . . . . . . 12
34	33	oveq1d 6073	. . . . . . . . . . 11
35	34	adantr 276	. . . . . . . . . 10 $/\$
36	31	sselda 3242	. . . . . . . . . . 11 $/\$
37		fzrev3i 10444	. . . . . . . . . . 11
38	36, 37	syl 14	. . . . . . . . . 10 $/\$
39	35, 38	eqeltrrd 2312	. . . . . . . . 9 $/\$
40	39, 7	fmptd 5836	. . . . . . . 8
41	40	frnd 5523	. . . . . . 7
42	31, 41	unssd 3399	. . . . . 6
43		ssdomg 7031	. . . . . 6
44	21, 42, 43	sylc 62	. . . . 5
45		fihashdom 11192	. . . . . 6 $/\$ ♯ ♯
46	11, 21, 45	syl2anc 411	. . . . 5 ♯ ♯
47	44, 46	mpbird 167	. . . 4 ♯ ♯
48		fz01en 10408	. . . . . . 7
49	16, 48	syl 14	. . . . . 6
50		1zzd 9621	. . . . . . . 8
51	50, 16	fzfigd 10817	. . . . . . 7
52		hashen 11172	. . . . . . 7 $/\$ ♯ ♯
53	21, 51, 52	syl2anc 411	. . . . . 6 ♯ ♯
54	49, 53	mpbird 167	. . . . 5 ♯ ♯
55	4	nnnn0d 9570	. . . . . 6
56		hashfz1 11171	. . . . . 6 ♯
57	55, 56	syl 14	. . . . 5 ♯
58	54, 57	eqtrd 2267	. . . 4 ♯
59	47, 58	breqtrd 4140	. . 3 ♯
60	14, 17, 59	lensymd 8411	. 2 ♯
61	17	adantr 276	. . . . . 6 $/\$
62	61	ltp1d 9221	. . . . 5 $/\$
63	1	nncnd 9268	. . . . . . . . 9
64		1cnd 8306	. . . . . . . . 9
65	63, 63, 64, 64	add4d 8458	. . . . . . . 8
66		4sq.3	. . . . . . . . . 10
67	66	oveq1d 6073	. . . . . . . . 9
68		2cn 9325	. . . . . . . . . . 11
69		mulcl 8270	. . . . . . . . . . 11 $/\$
70	68, 63, 69	sylancr 414	. . . . . . . . . 10
71	70, 64, 64	addassd 8312	. . . . . . . . 9
72	63	2timesd 9498	. . . . . . . . . 10
73	72	oveq1d 6073	. . . . . . . . 9
74	67, 71, 73	3eqtrd 2271	. . . . . . . 8
75	1	nnzd 9717	. . . . . . . . . . . . . . 15
76	18, 75	fzfigd 10817	. . . . . . . . . . . . . 14
77	26	ex 115	. . . . . . . . . . . . . . . . 17
78	4	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
79	22	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
80	79, 23	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
81		elfzelz 10378	. . . . . . . . . . . . . . . . . . . . . . . 24
82	81	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
83		zsqcl 10996	. . . . . . . . . . . . . . . . . . . . . . 23
84	82, 83	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85		moddvds 12510	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
86	78, 80, 84, 85	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
87	79	zcnd 9719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
88	82	zcnd 9719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89		subsq 11032	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
90	87, 88, 89	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
91	90	breq2d 4126	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
92	2	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
93	79, 82	zaddcld 9722	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
94	79, 82	zsubcld 9723	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
95		euclemma 12868	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
96	92, 93, 94, 95	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$
97	86, 91, 96	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$
98		zdceq 9670	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ DECID
99	79, 82, 98	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ DECID
100	93	zred 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
101		2re 9324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102	1	nnred 9267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103		remulcl 8271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
104	101, 102, 103	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
105	104	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
106	92, 15	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
107	106	zred 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
108	79	zred 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
109	82	zred 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
110	102	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
111		elfzle2 10382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
112	111	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
113		elfzle2 10382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
114	113	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
115	108, 109, 110, 110, 112, 114	le2addd 8854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
116	63	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
117	116	2timesd 9498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
118	115, 117	breqtrrd 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
119	104	ltp1d 9221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
120	119, 66	breqtrrd 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
121	120	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
122	100, 105, 107, 118, 121	lelttrd 8414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
123		zltnle 9640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
124	93, 106, 123	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
125	122, 124	mpbid 147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
126	125	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
127	16	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
128	93	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
129		1red 8305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
130		nn0abscl 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
131	94, 130	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
132	131	nn0red 9571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
133	132	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
134	128	zred 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
135	131	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
136	135	nn0zd 9716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
137	94	zcnd 9719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
138	137	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
139	87, 88	subeq0ad 8610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
140	139	necon3bid 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
141	140	biimpar 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
142		0zd 9606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
143		zapne 9669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ #
144	94, 142, 143	syl2an2r 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ #
145	141, 144	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ #
146	138, 145	absrpclapd 11898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
147	146	rpgt0d 10050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
148		elnnz 9604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
149	136, 147, 148	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
150	149	nnge1d 9297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
151		0cnd 8283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
152	87, 88, 151	abs3difd 11910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
153	87	subid1d 8589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
154	153	fveq2d 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
155		elfzle1 10381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
156	155	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
157	108, 156	absidd 11877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
158	154, 157	eqtrd 2267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
159		0cn 8282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
160		abssub 11811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
161	159, 88, 160	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
162	88	subid1d 8589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
163	162	fveq2d 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
164		elfzle1 10381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
165	164	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
166	109, 165	absidd 11877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
167	161, 163, 166	3eqtrd 2271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
168	158, 167	oveq12d 6076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
169	152, 168	breqtrd 4140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
170	169	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
171	129, 133, 134, 150, 170	letrd 8413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
172		elnnz1 9617	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
173	128, 171, 172	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
174		dvdsle 12555	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
175	127, 173, 174	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
176	126, 175	mtod 669	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
177	176	ex 115	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
178	177	a1d 22	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ DECID
179	178	necon4addc 2484	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ DECID
180	99, 179	mpd 13	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
181		dvdsabsb 12521	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
182	106, 94, 181	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
183		letr 8372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
184	107, 132, 100, 183	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
185	169, 184	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
186	125, 185	mtod 669	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
187	186	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
188		dvdsle 12555	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
189	106, 149, 188	syl2an2r 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
190	187, 189	mtod 669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
191	190	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	191	a1d 22	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ DECID
193	192	necon4addc 2484	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ DECID
194	99, 193	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
195	182, 194	sylbid 150	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
196	180, 195	jaod 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$
197	97, 196	sylbid 150	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
198		oveq1 6065	. . . . . . . . . . . . . . . . . . . 20
199	198	oveq1d 6073	. . . . . . . . . . . . . . . . . . 19
200	197, 199	impbid1 142	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
201	200	ex 115	. . . . . . . . . . . . . . . . 17 $/\$
202	77, 201	dom2lem 7024	. . . . . . . . . . . . . . . 16
203		f1f1orn 5630	. . . . . . . . . . . . . . . 16
204	202, 203	syl 14	. . . . . . . . . . . . . . 15
205		eqid 2234	. . . . . . . . . . . . . . . . . 18
206	205	rnmpt 5010	. . . . . . . . . . . . . . . . 17
207	5, 206	eqtr4i 2258	. . . . . . . . . . . . . . . 16
208		f1oeq3 5609	. . . . . . . . . . . . . . . 16
209	207, 208	ax-mp 5	. . . . . . . . . . . . . . 15
210	204, 209	sylibr 134	. . . . . . . . . . . . . 14
211		f1oeng 7009	. . . . . . . . . . . . . 14 $/\$
212	76, 210, 211	syl2anc 411	. . . . . . . . . . . . 13
213	212	ensymd 7036	. . . . . . . . . . . 12
214		ax-1cn 8236	. . . . . . . . . . . . . . 15
215		pncan 8495	. . . . . . . . . . . . . . 15 $/\$
216	63, 214, 215	sylancl 413	. . . . . . . . . . . . . 14
217	216	oveq2d 6074	. . . . . . . . . . . . 13
218	1	nnnn0d 9570	. . . . . . . . . . . . . . . 16
219		peano2nn0 9553	. . . . . . . . . . . . . . . 16
220	218, 219	syl 14	. . . . . . . . . . . . . . 15
221	220	nn0zd 9716	. . . . . . . . . . . . . 14
222		fz01en 10408	. . . . . . . . . . . . . 14
223	221, 222	syl 14	. . . . . . . . . . . . 13
224	217, 223	eqbrtrrd 4138	. . . . . . . . . . . 12
225		entr 7037	. . . . . . . . . . . 12 $/\$
226	213, 224, 225	syl2anc 411	. . . . . . . . . . 11
227	50, 221	fzfigd 10817	. . . . . . . . . . . 12
228		hashen 11172	. . . . . . . . . . . 12 $/\$ ♯ ♯
229	6, 227, 228	syl2anc 411	. . . . . . . . . . 11 ♯ ♯
230	226, 229	mpbird 167	. . . . . . . . . 10 ♯ ♯
231		hashfz1 11171	. . . . . . . . . . 11 ♯
232	220, 231	syl 14	. . . . . . . . . 10 ♯
233	230, 232	eqtrd 2267	. . . . . . . . 9 ♯
234	39	ex 115	. . . . . . . . . . . . . 14
235	32	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$
236		fzssuz 10420	. . . . . . . . . . . . . . . . . . . 20
237		uzssz 9892	. . . . . . . . . . . . . . . . . . . . 21
238		zsscn 9602	. . . . . . . . . . . . . . . . . . . . 21
239	237, 238	sstri 3251	. . . . . . . . . . . . . . . . . . . 20
240	236, 239	sstri 3251	. . . . . . . . . . . . . . . . . . 19
241	31, 240	sstrdi 3254	. . . . . . . . . . . . . . . . . 18
242	241	sselda 3242	. . . . . . . . . . . . . . . . 17 $/\$
243	242	adantrr 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$
244	241	sselda 3242	. . . . . . . . . . . . . . . . 17 $/\$
245	244	adantrl 478	. . . . . . . . . . . . . . . 16 $/\$ $/\$
246	235, 243, 245	subcanad 8643	. . . . . . . . . . . . . . 15 $/\$ $/\$
247	246	ex 115	. . . . . . . . . . . . . 14 $/\$
248	234, 247	dom2lem 7024	. . . . . . . . . . . . 13
249		f1eq1 5573	. . . . . . . . . . . . . 14
250	7, 249	ax-mp 5	. . . . . . . . . . . . 13
251	248, 250	sylibr 134	. . . . . . . . . . . 12
252		f1f1orn 5630	. . . . . . . . . . . 12
253	251, 252	syl 14	. . . . . . . . . . 11
254	6, 253	fihasheqf1od 11177	. . . . . . . . . 10 ♯ ♯
255	254, 233	eqtr3d 2269	. . . . . . . . 9 ♯
256	233, 255	oveq12d 6076	. . . . . . . 8 ♯ ♯
257	65, 74, 256	3eqtr4d 2277	. . . . . . 7 ♯ ♯
258	257	adantr 276	. . . . . 6 $/\$ ♯ ♯
259	6	adantr 276	. . . . . . 7 $/\$
260	8	adantr 276	. . . . . . 7 $/\$
261		simpr 110	. . . . . . 7 $/\$
262		hashun 11194	. . . . . . 7 $/\$ $/\$ ♯ ♯ ♯
263	259, 260, 261, 262	syl3anc 1274	. . . . . 6 $/\$ ♯ ♯ ♯
264	258, 263	eqtr4d 2270	. . . . 5 $/\$ ♯
265	62, 264	breqtrd 4140	. . . 4 $/\$ ♯
266	265	ex 115	. . 3 ♯
267	266	necon3bd 2457	. 2 ♯
268	60, 267	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 716 DECID wdc 842

wceq 1398

wcel 2205

cab 2220

wne 2414

wrex 2523

cun 3212

cin 3213

wss 3214

c0 3512 class class class wbr 4114

cmpt 4176

crn 4755

wf1 5354

wf1o 5356

cfv 5357 (class class class)co 6058

cen 6986

cdom 6987

cfn 6988

cc 8141

cr 8142

cc0 8143

c1 8144

caddc 8146

cmul 8148

clt 8324

cle 8325

cmin 8460 # cap 8872

cn 9254

c2 9305

cn0 9513

cz 9594

cuz 9871

cfz 10361

cmo 10708

cexp 10924 ♯chash 11163

cabs 11707

cdvds 12498

cprime 12829

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261 ax-arch 8262 ax-caucvg 8263

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-irdg 6614 df-frec 6635 df-1o 6660 df-2o 6661 df-oadd 6664 df-er 6780 df-en 6989 df-dom 6990 df-fin 6991 df-sup 7288 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-reap 8866 df-ap 8873 df-div 8964 df-inn 9255 df-2 9313 df-3 9314 df-4 9315 df-n0 9514 df-z 9595 df-uz 9872 df-q 9970 df-rp 10005 df-fz 10362 df-fzo 10499 df-fl 10654 df-mod 10709 df-seqfrec 10834 df-exp 10925 df-ihash 11164 df-cj 11552 df-re 11553 df-im 11554 df-rsqrt 11708 df-abs 11709 df-dvds 12499 df-gcd 12675 df-prm 12830

This theorem is referenced by: 4sqlem12 13125

W3C validator