Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > hashnncl | Structured version Visualization version GIF version |
Description: Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Ref | Expression |
---|---|
hashnncl | ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnne0 11659 | . . 3 ⊢ ((♯‘𝐴) ∈ ℕ → (♯‘𝐴) ≠ 0) | |
2 | hashcl 13705 | . . . . . 6 ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0) | |
3 | elnn0 11887 | . . . . . 6 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ ((♯‘𝐴) ∈ ℕ ∨ (♯‘𝐴) = 0)) | |
4 | 2, 3 | sylib 219 | . . . . 5 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ∨ (♯‘𝐴) = 0)) |
5 | 4 | ord 858 | . . . 4 ⊢ (𝐴 ∈ Fin → (¬ (♯‘𝐴) ∈ ℕ → (♯‘𝐴) = 0)) |
6 | 5 | necon1ad 3030 | . . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ≠ 0 → (♯‘𝐴) ∈ ℕ)) |
7 | 1, 6 | impbid2 227 | . 2 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ (♯‘𝐴) ≠ 0)) |
8 | hasheq0 13712 | . . 3 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) | |
9 | 8 | necon3bid 3057 | . 2 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ≠ 0 ↔ 𝐴 ≠ ∅)) |
10 | 7, 9 | bitrd 280 | 1 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∨ wo 841 = wceq 1528 ∈ wcel 2105 ≠ wne 3013 ∅c0 4288 ‘cfv 6348 Fincfn 8497 0cc0 10525 ℕcn 11626 ℕ0cn0 11885 ♯chash 13678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 ax-cnex 10581 ax-resscn 10582 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-addrcl 10586 ax-mulcl 10587 ax-mulrcl 10588 ax-mulcom 10589 ax-addass 10590 ax-mulass 10591 ax-distr 10592 ax-i2m1 10593 ax-1ne0 10594 ax-1rid 10595 ax-rnegex 10596 ax-rrecex 10597 ax-cnre 10598 ax-pre-lttri 10599 ax-pre-lttrn 10600 ax-pre-ltadd 10601 ax-pre-mulgt0 10602 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-nel 3121 df-ral 3140 df-rex 3141 df-reu 3142 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-pss 3951 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4831 df-int 4868 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-riota 7103 df-ov 7148 df-oprab 7149 df-mpo 7150 df-om 7570 df-1st 7678 df-2nd 7679 df-wrecs 7936 df-recs 7997 df-rdg 8035 df-1o 8091 df-er 8278 df-en 8498 df-dom 8499 df-sdom 8500 df-fin 8501 df-card 9356 df-pnf 10665 df-mnf 10666 df-xr 10667 df-ltxr 10668 df-le 10669 df-sub 10860 df-neg 10861 df-nn 11627 df-n0 11886 df-z 11970 df-uz 12232 df-fz 12881 df-hash 13679 |
This theorem is referenced by: hashge1 13738 lennncl 13872 lswlgt0cl 13909 wrdind 14072 wrd2ind 14073 incexc 15180 incexc2 15181 ramub1 16352 gsumwmhm 17998 psgnunilem5 18551 psgnunilem4 18554 gexcl2 18643 sylow1lem3 18654 sylow1lem5 18656 pgpfi 18659 pgpfi2 18660 sylow2alem2 18672 sylow2blem3 18676 slwhash 18678 fislw 18679 sylow3lem3 18683 sylow3lem4 18684 efgsres 18793 efgredlem 18802 lt6abl 18944 ablfacrp2 19118 ablfac1lem 19119 ablfac1b 19121 ablfac1c 19122 ablfac1eu 19124 pgpfac1lem2 19126 pgpfac1lem3a 19127 pgpfaclem2 19133 ablfaclem3 19138 lebnumlem3 23494 birthdaylem3 25458 birthday 25459 amgmlem 25494 amgm 25495 musum 25695 dchrabs 25763 dchrisum0flblem1 26011 cusgrrusgr 27290 frgrreg 28100 tgoldbachgtda 31831 derangfmla 32334 erdszelem2 32336 rrndstprj2 34990 rrncmslem 34991 rrnequiv 34994 isnumbasgrplem3 39583 fzisoeu 41443 fourierdlem54 42322 fourierdlem103 42371 fourierdlem104 42372 qndenserrnbllem 42456 ovnhoilem1 42760 hoiqssbllem1 42781 hoiqssbllem2 42782 hoiqssbllem3 42783 vonsn 42850 amgmlemALT 44832 |
Copyright terms: Public domain | W3C validator |