| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 6nn0 | Structured version Visualization version GIF version | ||
| Description: 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| Ref | Expression |
|---|---|
| 6nn0 | ⊢ 6 ∈ ℕ0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 6nn 12301 | . 2 ⊢ 6 ∈ ℕ | |
| 2 | 1 | nnnn0i 12483 | 1 ⊢ 6 ∈ ℕ0 |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2141 6c6 12270 ℕ0cn0 12475 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pr 5387 ax-un 7713 ax-1cn 11125 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-ov 7394 df-om 7842 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-n0 12476 |
| This theorem is referenced by: 16nn0 12700 6p5e11 12760 6p6e12 12761 7p7e14 12766 8p7e15 12772 9p7e16 12779 9p8e17 12780 6t3e18 12792 6t4e24 12793 6t5e30 12794 6t6e36 12795 7t7e49 12801 8t3e24 12803 8t7e56 12807 8t8e64 12808 9t4e36 12811 9t5e45 12812 9t7e63 12814 9t8e72 12815 6lt10 12822 6lcm4e12 16641 2exp7 17114 2exp8 17115 2exp11 17116 2exp16 17117 2expltfac 17119 19prm 17145 prmlem2 17147 37prm 17148 43prm 17149 139prm 17151 163prm 17152 317prm 17153 631prm 17154 1259lem1 17158 1259lem2 17159 1259lem3 17160 1259lem4 17161 1259lem5 17162 2503lem1 17164 2503lem2 17165 2503lem3 17166 2503prm 17167 4001lem1 17168 4001lem2 17169 4001lem3 17170 4001lem4 17171 4001prm 17172 slotsdnscsi 17412 log2ublem2 27000 log2ublem3 27001 log2ub 27002 log2le1 27003 birthday 27007 bclbnd 27332 bpos1 27335 bposlem8 27343 bposlem9 27344 bpos 27345 slotsinbpsd 28598 slotslnbpsd 28599 lngndxnitvndx 28600 eengstr 29138 ex-exp 30609 cos9thpiminplylem5 34044 hgt750lemd 34903 hgt750lem 34906 hgt750lem2 34907 kur14lem8 35524 420gcd8e4 42584 12lcm5e60 42586 60lcm7e420 42588 lcmineqlem 42630 3exp7 42631 3lexlogpow5ineq1 42632 3lexlogpow5ineq5 42638 aks4d1p1p7 42652 aks4d1p1p5 42653 aks4d1p1 42654 235t711 42875 ex-decpmul 42876 3cubeslem3l 43228 3cubeslem3r 43229 expdiophlem2 43560 resqrtvalex 44182 imsqrtvalex 44183 wallispi2lem2 46607 sin5tlem4 47431 goldratmolem2 47441 fmtno2 48120 fmtno3 48121 fmtno4 48122 fmtno5lem1 48123 fmtno5lem2 48124 fmtno5lem3 48125 fmtno5lem4 48126 fmtno5 48127 257prm 48131 fmtno4prmfac 48142 fmtno4nprmfac193 48144 fmtno5faclem1 48149 fmtno5faclem2 48150 fmtno5faclem3 48151 fmtno5fac 48152 fmtno5nprm 48153 139prmALT 48166 127prm 48169 m11nprm 48171 2exp340mod341 48316 8exp8mod9 48319 ackval41 49278 ackval42 49279 |
| Copyright terms: Public domain | W3C validator |