![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 5nn0 | Structured version Visualization version GIF version |
Description: 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
5nn0 | ⊢ 5 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 5nn 12322 | . 2 ⊢ 5 ∈ ℕ | |
2 | 1 | nnnn0i 12504 | 1 ⊢ 5 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 5c5 12294 ℕ0cn0 12496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pr 5423 ax-un 7734 ax-1cn 11190 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-ral 3058 df-rex 3067 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7417 df-om 7865 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-nn 12237 df-2 12299 df-3 12300 df-4 12301 df-5 12302 df-n0 12497 |
This theorem is referenced by: 6p6e12 12775 7p6e13 12779 8p6e14 12785 8p8e16 12787 9p6e15 12792 9p7e16 12793 5t2e10 12801 5t3e15 12802 5t4e20 12803 5t5e25 12804 6t6e36 12809 7t5e35 12813 7t6e42 12814 8t6e48 12820 8t8e64 12822 9t5e45 12826 9t6e54 12827 9t7e63 12828 dec2dvds 17025 dec5dvds2 17027 2exp8 17051 2exp11 17052 2exp16 17053 prmlem1 17070 5prm 17071 7prm 17073 11prm 17077 13prm 17078 17prm 17079 19prm 17080 prmlem2 17082 37prm 17083 139prm 17086 163prm 17087 317prm 17088 631prm 17089 1259lem1 17093 1259lem2 17094 1259lem3 17095 1259lem4 17096 1259lem5 17097 1259prm 17098 2503lem1 17099 2503lem2 17100 2503lem3 17101 2503prm 17102 4001lem1 17103 4001lem2 17104 4001lem3 17105 4001lem4 17106 4001prm 17107 slotsdnscsi 17366 slotsbhcdif 17389 slotsbhcdifOLD 17390 quart1cl 26779 quart1lem 26780 quart1 26781 log2ublem1 26871 log2ublem3 26873 log2ub 26874 log2le1 26875 birthday 26879 ppiublem2 27129 bpos1 27209 bposlem8 27217 ex-fac 30254 threehalves 32632 zlmdsOLD 33558 hgt750lemd 34274 hgt750lem2 34278 hgt750leme 34284 kur14lem8 34817 420gcd8e4 41471 12lcm5e60 41473 lcmineqlem 41517 3lexlogpow5ineq1 41519 3lexlogpow5ineq2 41520 3lexlogpow5ineq4 41521 3lexlogpow5ineq3 41522 3lexlogpow2ineq2 41524 3lexlogpow5ineq5 41525 aks4d1lem1 41527 aks4d1p1p3 41534 aks4d1p1p2 41535 aks4d1p1p4 41536 aks4d1p1p6 41538 aks4d1p1p7 41539 aks4d1p1p5 41540 aks4d1p1 41541 aks4d1p2 41542 aks4d1p3 41543 aks4d1p5 41545 aks4d1p6 41546 aks4d1p7d1 41547 aks4d1p7 41548 aks4d1p8 41552 sqn5i 41853 235t711 41861 ex-decpmul 41862 sq45 42089 sum9cubes 42090 3cubeslem3l 42100 3cubeslem3r 42101 resqrtvalex 43069 imsqrtvalex 43070 inductionexd 43579 fmtno3 46885 fmtno4 46886 fmtno5lem1 46887 fmtno5lem2 46888 fmtno5lem3 46889 fmtno5lem4 46890 fmtno5 46891 257prm 46895 fmtno4prmfac 46906 fmtno4prmfac193 46907 fmtno4nprmfac193 46908 fmtno5faclem3 46915 flsqrt5 46928 139prmALT 46930 31prm 46931 127prm 46933 41prothprmlem2 46952 2exp340mod341 47067 linevalexample 47457 ackval2012 47758 ackval3012 47759 ackval41 47762 |
Copyright terms: Public domain | W3C validator |