![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > hashnncl | Structured version Visualization version Unicode version |
Description: Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Ref | Expression |
---|---|
hashnncl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnne0 10642 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | hashcl 12538 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elnn0 10871 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylib 200 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | ord 379 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | necon1ad 2641 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 6 | impbid2 208 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | hasheq0 12544 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 8 | necon3bid 2668 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 7, 9 | bitrd 257 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-card 8373 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-n0 10870 df-z 10938 df-uz 11160 df-fz 11785 df-hash 12516 |
This theorem is referenced by: hashge1 12568 lennncl 12688 lswlgt0cl 12716 wrdind 12833 wrd2ind 12834 incexc 13895 incexc2 13896 ramub1 14986 gsumwmhm 16629 psgnunilem5 17135 psgnunilem4 17138 gexcl2 17241 sylow1lem3 17252 sylow1lem5 17254 pgpfi 17257 pgpfi2 17258 sylow2alem2 17270 sylow2blem3 17274 slwhash 17276 fislw 17277 sylow3lem3 17281 sylow3lem4 17282 efgsp1 17387 efgsres 17388 efgredlem 17397 lt6abl 17529 ablfacrp2 17700 ablfac1lem 17701 ablfac1b 17703 ablfac1c 17704 ablfac1eu 17706 pgpfac1lem2 17708 pgpfac1lem3a 17709 pgpfaclem2 17715 ablfaclem3 17720 lebnumlem3 21991 lebnumlem3OLD 21994 birthdaylem3 23879 birthday 23880 amgmlem 23915 amgm 23916 musum 24120 dchrabs 24188 dchrisum0flblem1 24346 cusgraisrusgra 25666 frghash2spot 25791 derangfmla 29913 erdszelem2 29915 rrndstprj2 32163 rrncmslem 32164 rrnequiv 32167 isnumbasgrplem3 35964 fzisoeu 37518 fourierdlem54 38024 fourierdlem103 38073 fourierdlem104 38074 qndenserrnbllem 38163 ovnhoilem1 38423 hoiqssbllem1 38444 hoiqssbllem2 38445 hoiqssbllem3 38446 cusgrrusgr 39597 |
Copyright terms: Public domain | W3C validator |