4sqlem11 - Intuitionistic Logic Explorer

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

Theorem 4sqlem11 12839

Description: Lemma for 4sq 12848. 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 12835 and fin0 7008. (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 12547	. . . . . . . 8
4	2, 3	syl 14	. . . . . . 7
5		4sqlem11.5	. . . . . . 7
6	1, 4, 5	4sqlemafi 12833	. . . . . 6
7		4sqlem11.6	. . . . . . 7
8	1, 4, 5, 7	4sqlemffi 12834	. . . . . 6
9	1, 4, 5, 7	4sqleminfi 12835	. . . . . 6
10		unfiin 7049	. . . . . 6 $/\$ $/\$
11	6, 8, 9, 10	syl3anc 1250	. . . . 5
12		hashcl 10963	. . . . 5 ♯
13	11, 12	syl 14	. . . 4 ♯
14	13	nn0red 9384	. . 3 ♯
15		prmz 12548	. . . . 5
16	2, 15	syl 14	. . . 4
17	16	zred 9530	. . 3
18		0zd 9419	. . . . . . 7
19		peano2zm 9445	. . . . . . . 8
20	16, 19	syl 14	. . . . . . 7
21	18, 20	fzfigd 10613	. . . . . 6
22		elfzelz 10182	. . . . . . . . . . . . 13
23		zsqcl 10792	. . . . . . . . . . . . 13
24	22, 23	syl 14	. . . . . . . . . . . 12
25		zmodfz 10528	. . . . . . . . . . . 12 $/\$
26	24, 4, 25	syl2anr 290	. . . . . . . . . . 11 $/\$
27		eleq1a 2279	. . . . . . . . . . 11
28	26, 27	syl 14	. . . . . . . . . 10 $/\$
29	28	rexlimdva 2625	. . . . . . . . 9
30	29	abssdv 3275	. . . . . . . 8
31	5, 30	eqsstrid 3247	. . . . . . 7
32	20	zcnd 9531	. . . . . . . . . . . . 13
33	32	addlidd 8257	. . . . . . . . . . . 12
34	33	oveq1d 5982	. . . . . . . . . . 11
35	34	adantr 276	. . . . . . . . . 10 $/\$
36	31	sselda 3201	. . . . . . . . . . 11 $/\$
37		fzrev3i 10245	. . . . . . . . . . 11
38	36, 37	syl 14	. . . . . . . . . 10 $/\$
39	35, 38	eqeltrrd 2285	. . . . . . . . 9 $/\$
40	39, 7	fmptd 5757	. . . . . . . 8
41	40	frnd 5455	. . . . . . 7
42	31, 41	unssd 3357	. . . . . 6
43		ssdomg 6893	. . . . . 6
44	21, 42, 43	sylc 62	. . . . 5
45		fihashdom 10985	. . . . . 6 $/\$ ♯ ♯
46	11, 21, 45	syl2anc 411	. . . . 5 ♯ ♯
47	44, 46	mpbird 167	. . . 4 ♯ ♯
48		fz01en 10210	. . . . . . 7
49	16, 48	syl 14	. . . . . 6
50		1zzd 9434	. . . . . . . 8
51	50, 16	fzfigd 10613	. . . . . . 7
52		hashen 10966	. . . . . . 7 $/\$ ♯ ♯
53	21, 51, 52	syl2anc 411	. . . . . 6 ♯ ♯
54	49, 53	mpbird 167	. . . . 5 ♯ ♯
55	4	nnnn0d 9383	. . . . . 6
56		hashfz1 10965	. . . . . 6 ♯
57	55, 56	syl 14	. . . . 5 ♯
58	54, 57	eqtrd 2240	. . . 4 ♯
59	47, 58	breqtrd 4085	. . 3 ♯
60	14, 17, 59	lensymd 8229	. 2 ♯
61	17	adantr 276	. . . . . 6 $/\$
62	61	ltp1d 9038	. . . . 5 $/\$
63	1	nncnd 9085	. . . . . . . . 9
64		1cnd 8123	. . . . . . . . 9
65	63, 63, 64, 64	add4d 8276	. . . . . . . 8
66		4sq.3	. . . . . . . . . 10
67	66	oveq1d 5982	. . . . . . . . 9
68		2cn 9142	. . . . . . . . . . 11
69		mulcl 8087	. . . . . . . . . . 11 $/\$
70	68, 63, 69	sylancr 414	. . . . . . . . . 10
71	70, 64, 64	addassd 8130	. . . . . . . . 9
72	63	2timesd 9315	. . . . . . . . . 10
73	72	oveq1d 5982	. . . . . . . . 9
74	67, 71, 73	3eqtrd 2244	. . . . . . . 8
75	1	nnzd 9529	. . . . . . . . . . . . . . 15
76	18, 75	fzfigd 10613	. . . . . . . . . . . . . 14
77	26	ex 115	. . . . . . . . . . . . . . . . 17
78	4	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
79	22	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
80	79, 23	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
81		elfzelz 10182	. . . . . . . . . . . . . . . . . . . . . . . 24
82	81	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
83		zsqcl 10792	. . . . . . . . . . . . . . . . . . . . . . 23
84	82, 83	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
85		moddvds 12225	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
86	78, 80, 84, 85	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
87	79	zcnd 9531	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
88	82	zcnd 9531	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
89		subsq 10828	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
90	87, 88, 89	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
91	90	breq2d 4071	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
92	2	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
93	79, 82	zaddcld 9534	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
94	79, 82	zsubcld 9535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
95		euclemma 12583	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
96	92, 93, 94, 95	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$
97	86, 91, 96	3bitrd 214	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$
98		zdceq 9483	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ DECID
99	79, 82, 98	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ DECID
100	93	zred 9530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
101		2re 9141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102	1	nnred 9084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103		remulcl 8088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
104	101, 102, 103	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
105	104	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
106	92, 15	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
107	106	zred 9530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
108	79	zred 9530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
109	82	zred 9530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
110	102	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
111		elfzle2 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
112	111	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
113		elfzle2 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
114	113	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
115	108, 109, 110, 110, 112, 114	le2addd 8671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
116	63	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
117	116	2timesd 9315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
118	115, 117	breqtrrd 4087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
119	104	ltp1d 9038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
120	119, 66	breqtrrd 4087	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
121	120	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
122	100, 105, 107, 118, 121	lelttrd 8232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
123		zltnle 9453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
130		nn0abscl 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
131	94, 130	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
132	131	nn0red 9384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
133	132	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
134	128	zred 9530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
135	131	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
136	135	nn0zd 9528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
137	94	zcnd 9531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
138	137	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
139	87, 88	subeq0ad 8428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
140	139	necon3bid 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
141	140	biimpar 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
142		0zd 9419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
143		zapne 9482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ #
144	94, 142, 143	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ #
145	141, 144	mpbird 167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ #
146	138, 145	absrpclapd 11614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
147	146	rpgt0d 9856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
148		elnnz 9417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
149	136, 147, 148	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
150	149	nnge1d 9114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
151		0cnd 8100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
152	87, 88, 151	abs3difd 11626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
153	87	subid1d 8407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
154	153	fveq2d 5603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
155		elfzle1 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
156	155	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
157	108, 156	absidd 11593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
158	154, 157	eqtrd 2240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
159		0cn 8099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
160		abssub 11527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
161	159, 88, 160	sylancr 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
162	88	subid1d 8407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
163	162	fveq2d 5603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
164		elfzle1 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
165	164	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
166	109, 165	absidd 11593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
167	161, 163, 166	3eqtrd 2244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
168	158, 167	oveq12d 5985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
169	152, 168	breqtrd 4085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
170	169	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
171	129, 133, 134, 150, 170	letrd 8231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
172		elnnz1 9430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
173	128, 171, 172	sylanbrc 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
174		dvdsle 12270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
175	127, 173, 174	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
176	126, 175	mtod 665	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
177	176	ex 115	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
178	177	a1d 22	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ DECID
179	178	necon4addc 2448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ DECID
180	99, 179	mpd 13	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
181		dvdsabsb 12236	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
182	106, 94, 181	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
183		letr 8190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
184	107, 132, 100, 183	syl3anc 1250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
185	169, 184	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
186	125, 185	mtod 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
187	186	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
188		dvdsle 12270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
189	106, 149, 188	syl2an2r 595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
190	187, 189	mtod 665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
191	190	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
192	191	a1d 22	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ DECID
193	192	necon4addc 2448	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ DECID
194	99, 193	mpd 13	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
195	182, 194	sylbid 150	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
196	180, 195	jaod 719	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$
197	97, 196	sylbid 150	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
198		oveq1 5974	. . . . . . . . . . . . . . . . . . . 20
199	198	oveq1d 5982	. . . . . . . . . . . . . . . . . . 19
200	197, 199	impbid1 142	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
201	200	ex 115	. . . . . . . . . . . . . . . . 17 $/\$
202	77, 201	dom2lem 6886	. . . . . . . . . . . . . . . 16
203		f1f1orn 5555	. . . . . . . . . . . . . . . 16
204	202, 203	syl 14	. . . . . . . . . . . . . . 15
205		eqid 2207	. . . . . . . . . . . . . . . . . 18
206	205	rnmpt 4945	. . . . . . . . . . . . . . . . 17
207	5, 206	eqtr4i 2231	. . . . . . . . . . . . . . . 16
208		f1oeq3 5534	. . . . . . . . . . . . . . . 16
209	207, 208	ax-mp 5	. . . . . . . . . . . . . . 15
210	204, 209	sylibr 134	. . . . . . . . . . . . . 14
211		f1oeng 6871	. . . . . . . . . . . . . 14 $/\$
212	76, 210, 211	syl2anc 411	. . . . . . . . . . . . 13
213	212	ensymd 6898	. . . . . . . . . . . 12
214		ax-1cn 8053	. . . . . . . . . . . . . . 15
215		pncan 8313	. . . . . . . . . . . . . . 15 $/\$
216	63, 214, 215	sylancl 413	. . . . . . . . . . . . . 14
217	216	oveq2d 5983	. . . . . . . . . . . . 13
218	1	nnnn0d 9383	. . . . . . . . . . . . . . . 16
219		peano2nn0 9370	. . . . . . . . . . . . . . . 16
220	218, 219	syl 14	. . . . . . . . . . . . . . 15
221	220	nn0zd 9528	. . . . . . . . . . . . . 14
222		fz01en 10210	. . . . . . . . . . . . . 14
223	221, 222	syl 14	. . . . . . . . . . . . 13
224	217, 223	eqbrtrrd 4083	. . . . . . . . . . . 12
225		entr 6899	. . . . . . . . . . . 12 $/\$
226	213, 224, 225	syl2anc 411	. . . . . . . . . . 11
227	50, 221	fzfigd 10613	. . . . . . . . . . . 12
228		hashen 10966	. . . . . . . . . . . 12 $/\$ ♯ ♯
229	6, 227, 228	syl2anc 411	. . . . . . . . . . 11 ♯ ♯
230	226, 229	mpbird 167	. . . . . . . . . 10 ♯ ♯
231		hashfz1 10965	. . . . . . . . . . 11 ♯
232	220, 231	syl 14	. . . . . . . . . 10 ♯
233	230, 232	eqtrd 2240	. . . . . . . . 9 ♯
234	39	ex 115	. . . . . . . . . . . . . 14
235	32	adantr 276	. . . . . . . . . . . . . . . 16 $/\$ $/\$
236		fzssuz 10222	. . . . . . . . . . . . . . . . . . . 20
237		uzssz 9703	. . . . . . . . . . . . . . . . . . . . 21
238		zsscn 9415	. . . . . . . . . . . . . . . . . . . . 21
239	237, 238	sstri 3210	. . . . . . . . . . . . . . . . . . . 20
240	236, 239	sstri 3210	. . . . . . . . . . . . . . . . . . 19
241	31, 240	sstrdi 3213	. . . . . . . . . . . . . . . . . 18
242	241	sselda 3201	. . . . . . . . . . . . . . . . 17 $/\$
243	242	adantrr 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$
244	241	sselda 3201	. . . . . . . . . . . . . . . . 17 $/\$
245	244	adantrl 478	. . . . . . . . . . . . . . . 16 $/\$ $/\$
246	235, 243, 245	subcanad 8461	. . . . . . . . . . . . . . 15 $/\$ $/\$
247	246	ex 115	. . . . . . . . . . . . . 14 $/\$
248	234, 247	dom2lem 6886	. . . . . . . . . . . . 13
249		f1eq1 5498	. . . . . . . . . . . . . 14
250	7, 249	ax-mp 5	. . . . . . . . . . . . 13
251	248, 250	sylibr 134	. . . . . . . . . . . 12
252		f1f1orn 5555	. . . . . . . . . . . 12
253	251, 252	syl 14	. . . . . . . . . . 11
254	6, 253	fihasheqf1od 10971	. . . . . . . . . 10 ♯ ♯
255	254, 233	eqtr3d 2242	. . . . . . . . 9 ♯
256	233, 255	oveq12d 5985	. . . . . . . 8 ♯ ♯
257	65, 74, 256	3eqtr4d 2250	. . . . . . 7 ♯ ♯
258	257	adantr 276	. . . . . 6 $/\$ ♯ ♯
259	6	adantr 276	. . . . . . 7 $/\$
260	8	adantr 276	. . . . . . 7 $/\$
261		simpr 110	. . . . . . 7 $/\$
262		hashun 10987	. . . . . . 7 $/\$ $/\$ ♯ ♯ ♯
263	259, 260, 261, 262	syl3anc 1250	. . . . . 6 $/\$ ♯ ♯ ♯
264	258, 263	eqtr4d 2243	. . . . 5 $/\$ ♯
265	62, 264	breqtrd 4085	. . . 4 $/\$ ♯
266	265	ex 115	. . 3 ♯
267	266	necon3bd 2421	. 2 ♯
268	60, 267	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710 DECID wdc 836

wceq 1373

wcel 2178

cab 2193

wne 2378

wrex 2487

cun 3172

cin 3173

wss 3174

c0 3468 class class class wbr 4059

cmpt 4121

crn 4694

wf1 5287

wf1o 5289

cfv 5290 (class class class)co 5967

cen 6848

cdom 6849

cfn 6850

cc 7958

cr 7959

cc0 7960

c1 7961

caddc 7963

cmul 7965

clt 8142

cle 8143

cmin 8278 # cap 8689

cn 9071

c2 9122

cn0 9330

cz 9407

cuz 9683

cfz 10165

cmo 10504

cexp 10720 ♯chash 10957

cabs 11423

cdvds 12213

cprime 12544

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 2180 ax-14 2181 ax-ext 2189 ax-coll 4175 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-iinf 4654 ax-cnex 8051 ax-resscn 8052 ax-1cn 8053 ax-1re 8054 ax-icn 8055 ax-addcl 8056 ax-addrcl 8057 ax-mulcl 8058 ax-mulrcl 8059 ax-addcom 8060 ax-mulcom 8061 ax-addass 8062 ax-mulass 8063 ax-distr 8064 ax-i2m1 8065 ax-0lt1 8066 ax-1rid 8067 ax-0id 8068 ax-rnegex 8069 ax-precex 8070 ax-cnre 8071 ax-pre-ltirr 8072 ax-pre-ltwlin 8073 ax-pre-lttrn 8074 ax-pre-apti 8075 ax-pre-ltadd 8076 ax-pre-mulgt0 8077 ax-pre-mulext 8078 ax-arch 8079 ax-caucvg 8080

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-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rmo 2494 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-if 3580 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-po 4361 df-iso 4362 df-iord 4431 df-on 4433 df-ilim 4434 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-f1 5295 df-fo 5296 df-f1o 5297 df-fv 5298 df-riota 5922 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1st 6249 df-2nd 6250 df-recs 6414 df-irdg 6479 df-frec 6500 df-1o 6525 df-2o 6526 df-oadd 6529 df-er 6643 df-en 6851 df-dom 6852 df-fin 6853 df-sup 7112 df-pnf 8144 df-mnf 8145 df-xr 8146 df-ltxr 8147 df-le 8148 df-sub 8280 df-neg 8281 df-reap 8683 df-ap 8690 df-div 8781 df-inn 9072 df-2 9130 df-3 9131 df-4 9132 df-n0 9331 df-z 9408 df-uz 9684 df-q 9776 df-rp 9811 df-fz 10166 df-fzo 10300 df-fl 10450 df-mod 10505 df-seqfrec 10630 df-exp 10721 df-ihash 10958 df-cj 11268 df-re 11269 df-im 11270 df-rsqrt 11424 df-abs 11425 df-dvds 12214 df-gcd 12390 df-prm 12545

This theorem is referenced by: 4sqlem12 12840

W3C validator