MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashf1 Unicode version

Theorem hashf1 12506
Description: The permutation number |A| (| | |A|)= | | (| | |A|) counts the number of injections from to . (Contributed by Mario Carneiro, 21-Jan-2015.)
Assertion
Ref Expression
hashf1
Distinct variable groups:   ,   ,

Proof of Theorem hashf1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1eq2 5782 . . . . . . . . 9
2 f1fn 5787 . . . . . . . . . . . 12
3 fn0 5705 . . . . . . . . . . . 12
42, 3sylib 196 . . . . . . . . . . 11
5 f10 5852 . . . . . . . . . . . 12
6 f1eq1 5781 . . . . . . . . . . . 12
75, 6mpbiri 233 . . . . . . . . . . 11
84, 7impbii 188 . . . . . . . . . 10
9 elsn 4043 . . . . . . . . . 10
108, 9bitr4i 252 . . . . . . . . 9
111, 10syl6bb 261 . . . . . . . 8
1211abbi1dv 2595 . . . . . . 7
1312fveq2d 5875 . . . . . 6
14 0ex 4582 . . . . . . 7
15 hashsng 12438 . . . . . . 7
1614, 15ax-mp 5 . . . . . 6
1713, 16syl6eq 2514 . . . . 5
18 fveq2 5871 . . . . . . . . 9
19 hash0 12437 . . . . . . . . 9
2018, 19syl6eq 2514 . . . . . . . 8
2120fveq2d 5875 . . . . . . 7
22 fac0 12356 . . . . . . 7
2321, 22syl6eq 2514 . . . . . 6
2420oveq2d 6312 . . . . . 6
2523, 24oveq12d 6314 . . . . 5
2617, 25eqeq12d 2479 . . . 4
2726imbi2d 316 . . 3
28 f1eq2 5782 . . . . . . 7
2928abbidv 2593 . . . . . 6
3029fveq2d 5875 . . . . 5
31 fveq2 5871 . . . . . . 7
3231fveq2d 5875 . . . . . 6
3331oveq2d 6312 . . . . . 6
3432, 33oveq12d 6314 . . . . 5
3530, 34eqeq12d 2479 . . . 4
3635imbi2d 316 . . 3
37 f1eq2 5782 . . . . . . 7
3837abbidv 2593 . . . . . 6
3938fveq2d 5875 . . . . 5
40 fveq2 5871 . . . . . . 7
4140fveq2d 5875 . . . . . 6
4240oveq2d 6312 . . . . . 6
4341, 42oveq12d 6314 . . . . 5
4439, 43eqeq12d 2479 . . . 4
4544imbi2d 316 . . 3
46 f1eq2 5782 . . . . . . 7
4746abbidv 2593 . . . . . 6
4847fveq2d 5875 . . . . 5
49 fveq2 5871 . . . . . . 7
5049fveq2d 5875 . . . . . 6
5149oveq2d 6312 . . . . . 6
5250, 51oveq12d 6314 . . . . 5
5348, 52eqeq12d 2479 . . . 4
5453imbi2d 316 . . 3
55 hashcl 12428 . . . . . 6
56 bcn0 12388 . . . . . 6
5755, 56syl 16 . . . . 5
5857oveq2d 6312 . . . 4
59 1t1e1 10708 . . . 4
6058, 59syl6req 2515 . . 3
61 abn0 3804 . . . . . . . . . . . . 13
62 f1domg 7555 . . . . . . . . . . . . . . . 16
6362adantr 465 . . . . . . . . . . . . . . 15
64 vex 3112 . . . . . . . . . . . . . . . . . . 19
65 hashunsng 12459 . . . . . . . . . . . . . . . . . . 19
6664, 65ax-mp 5 . . . . . . . . . . . . . . . . . 18
6766adantl 466 . . . . . . . . . . . . . . . . 17
6867breq1d 4462 . . . . . . . . . . . . . . . 16
69 simprl 756 . . . . . . . . . . . . . . . . . 18
70 snfi 7616 . . . . . . . . . . . . . . . . . 18
71 unfi 7807 . . . . . . . . . . . . . . . . . 18
7269, 70, 71sylancl 662 . . . . . . . . . . . . . . . . 17
73 simpl 457 . . . . . . . . . . . . . . . . 17
74 hashdom 12447 . . . . . . . . . . . . . . . . 17
7572, 73, 74syl2anc 661 . . . . . . . . . . . . . . . 16
76 hashcl 12428 . . . . . . . . . . . . . . . . . . . 20
7776ad2antrl 727 . . . . . . . . . . . . . . . . . . 19
78 nn0p1nn 10860 . . . . . . . . . . . . . . . . . . 19
7977, 78syl 16 . . . . . . . . . . . . . . . . . 18
8079nnred 10576 . . . . . . . . . . . . . . . . 17
8155adantr 465 . . . . . . . . . . . . . . . . . 18
8281nn0red 10878 . . . . . . . . . . . . . . . . 17
8380, 82lenltd 9752 . . . . . . . . . . . . . . . 16
8468, 75, 833bitr3d 283 . . . . . . . . . . . . . . 15
8563, 84sylibd 214 . . . . . . . . . . . . . 14
8685exlimdv 1724 . . . . . . . . . . . . 13
8761, 86syl5bi 217 . . . . . . . . . . . 12
8887necon4ad 2677 . . . . . . . . . . 11
8988imp 429 . . . . . . . . . 10
9089fveq2d 5875 . . . . . . . . 9
91 hashcl 12428 . . . . . . . . . . . . . 14
9272, 91syl 16 . . . . . . . . . . . . 13
93 faccl 12363 . . . . . . . . . . . . 13
9492, 93syl 16 . . . . . . . . . . . 12
9594nncnd 10577 . . . . . . . . . . 11
9695adantr 465 . . . . . . . . . 10
9796mul01d 9800 . . . . . . . . 9
9819, 90, 973eqtr4a 2524 . . . . . . . 8
9967adantr 465 . . . . . . . . . . 11
10099oveq2d 6312 . . . . . . . . . 10
10181adantr 465 . . . . . . . . . . 11
10279adantr 465 . . . . . . . . . . . 12
103102nnzd 10993 . . . . . . . . . . 11
104 simpr 461 . . . . . . . . . . . 12
105104olcd 393 . . . . . . . . . . 11
106 bcval4 12385 . . . . . . . . . . 11
107101, 103, 105, 106syl3anc 1228 . . . . . . . . . 10
108100, 107eqtrd 2498 . . . . . . . . 9
109108oveq2d 6312 . . . . . . . 8
11098, 109eqtr4d 2501 . . . . . . 7
111110a1d 25 . . . . . 6
112 oveq2 6304 . . . . . . 7
11369adantr 465 . . . . . . . . 9
11473adantr 465 . . . . . . . . 9
115 simplrr 762 . . . . . . . . 9
116 simpr 461 . . . . . . . . 9
117113, 114, 115, 116hashf1lem2 12505 . . . . . . . 8
11881adantr 465 . . . . . . . . . . . . . 14
119 faccl 12363 . . . . . . . . . . . . . 14
120118, 119syl 16 . . . . . . . . . . . . 13
121120nncnd 10577 . . . . . . . . . . . 12
12277adantr 465 . . . . . . . . . . . . . . . 16
123 peano2nn0 10861 . . . . . . . . . . . . . . . 16
124122, 123syl 16 . . . . . . . . . . . . . . 15
125 nn0sub2 10949 . . . . . . . . . . . . . . 15
126124, 118, 116, 125syl3anc 1228 . . . . . . . . . . . . . 14
127 faccl 12363 . . . . . . . . . . . . . 14
128126, 127syl 16 . . . . . . . . . . . . 13
129128nncnd 10577 . . . . . . . . . . . 12
130128nnne0d 10605 . . . . . . . . . . . 12
131121, 129, 130divcld 10345 . . . . . . . . . . 11
132 faccl 12363 . . . . . . . . . . . . 13
133124, 132syl 16 . . . . . . . . . . . 12
134133nncnd 10577 . . . . . . . . . . 11
135133nnne0d 10605 . . . . . . . . . . 11
136131, 134, 135divcan2d 10347 . . . . . . . . . 10
137118nn0cnd 10879 . . . . . . . . . . . 12
138122nn0cnd 10879 . . . . . . . . . . . 12
139137, 138subcld 9954 . . . . . . . . . . 11
140 ax-1cn 9571 . . . . . . . . . . . . . 14
141 npcan 9852 . . . . . . . . . . . . . 14
142139, 140, 141sylancl 662 . . . . . . . . . . . . 13
143 1cnd 9633 . . . . . . . . . . . . . . . 16
144137, 138, 143subsub4d 9985 . . . . . . . . . . . . . . 15
145144, 126eqeltrd 2545 . . . . . . . . . . . . . 14
146 nn0p1nn 10860 . . . . . . . . . . . . . 14
147145, 146syl 16 . . . . . . . . . . . . 13
148142, 147eqeltrrd 2546 . . . . . . . . . . . 12
149148nnne0d 10605 . . . . . . . . . . 11
150131, 139, 149divcan2d 10347 . . . . . . . . . 10
151136, 150eqtr4d 2501 . . . . . . . . 9
15267adantr 465 . . . . . . . . . . 11
153152fveq2d 5875 . . . . . . . . . 10
154 nn0uz 11144 . . . . . . . . . . . . . . 15
155124, 154syl6eleq 2555 . . . . . . . . . . . . . 14
156118nn0zd 10992 . . . . . . . . . . . . . 14
157 elfz5 11709 . . . . . . . . . . . . . 14
158155, 156, 157syl2anc 661 . . . . . . . . . . . . 13
159116, 158mpbird 232 . . . . . . . . . . . 12
160 bcval2 12383 . . . . . . . . . . . 12
161159, 160syl 16 . . . . . . . . . . 11
162152oveq2d 6312 . . . . . . . . . . 11
163121, 129, 134, 130, 135divdiv1d 10376 . . . . . . . . . . 11
164161, 162, 1633eqtr4d 2508 . . . . . . . . . 10
165153, 164oveq12d 6314 . . . . . . . . 9
166122, 154syl6eleq 2555 . . . . . . . . . . . . . . 15
167 peano2fzr 11728 . . . . . . . . . . . . . . 15
168166, 159, 167syl2anc 661 . . . . . . . . . . . . . 14
169 bcval2 12383 . . . . . . . . . . . . . 14
170168, 169syl 16 . . . . . . . . . . . . 13
171 elfzle2 11719 . . . . . . . . . . . . . . . . . 18
172168, 171syl 16 . . . . . . . . . . . . . . . . 17
173 nn0sub2 10949 . . . . . . . . . . . . . . . . 17
174122, 118, 172, 173syl3anc 1228 . . . . . . . . . . . . . . . 16
175 faccl 12363 . . . . . . . . . . . . . . . 16
176174, 175syl 16 . . . . . . . . . . . . . . 15
177176nncnd 10577 . . . . . . . . . . . . . 14
178 faccl 12363 . . . . . . . . . . . . . . . 16
179122, 178syl 16 . . . . . . . . . . . . . . 15
180179nncnd 10577 . . . . . . . . . . . . . 14
181176nnne0d 10605 . . . . . . . . . . . . . 14
182179nnne0d 10605 . . . . . . . . . . . . . 14
183121, 177, 180, 181, 182divdiv1d 10376 . . . . . . . . . . . . 13