![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 4nn0 | Structured version Visualization version GIF version |
Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Ref | Expression |
---|---|
4nn0 | ⊢ 4 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4nn 11459 | . 2 ⊢ 4 ∈ ℕ | |
2 | 1 | nnnn0i 11651 | 1 ⊢ 4 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 4c4 11432 ℕ0cn0 11642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-1cn 10330 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4672 df-iun 4755 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-ov 6925 df-om 7344 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-nn 11375 df-2 11438 df-3 11439 df-4 11440 df-n0 11643 |
This theorem is referenced by: 6p5e11 11920 7p5e12 11924 8p5e13 11930 8p7e15 11932 9p5e14 11937 9p6e15 11938 4t3e12 11945 4t4e16 11946 5t5e25 11950 6t4e24 11953 6t5e30 11954 7t3e21 11957 7t5e35 11959 7t7e49 11961 8t3e24 11963 8t4e32 11964 8t5e40 11965 8t6e48 11966 8t7e56 11967 8t8e64 11968 9t5e45 11972 9t6e54 11973 9t7e63 11974 decbin3 11989 fzo0to42pr 12874 4bc3eq4 13433 bpoly4 15192 fsumcube 15193 resin4p 15270 recos4p 15271 ef01bndlem 15316 sin01bnd 15317 cos01bnd 15318 prm23lt5 15923 decexp2 16183 2exp8 16195 2exp16 16196 2expltfac 16198 13prm 16221 19prm 16223 prmlem2 16225 37prm 16226 43prm 16227 83prm 16228 139prm 16229 163prm 16230 317prm 16231 631prm 16232 1259lem1 16236 1259lem2 16237 1259lem3 16238 1259lem4 16239 1259lem5 16240 1259prm 16241 2503lem1 16242 2503lem2 16243 2503lem3 16244 2503prm 16245 4001lem1 16246 4001lem2 16247 4001lem3 16248 4001lem4 16249 4001prm 16250 resshom 16464 slotsbhcdif 16466 prdsvalstr 16499 oppchomfval 16759 oppcbas 16763 rescbas 16874 rescco 16877 rescabs 16878 catstr 17002 lt6abl 18682 cnfldfun 20154 binom4 25028 dquart 25031 quart1cl 25032 quart1lem 25033 quart1 25034 log2ublem3 25127 log2ub 25128 ppiublem2 25380 bclbnd 25457 bpos1 25460 bposlem8 25468 bposlem9 25469 bpos 25470 2lgslem3a 25573 2lgslem3b 25574 2lgslem3c 25575 2lgslem3d 25576 usgrexmplef 26606 upgr4cycl4dv4e 27588 ex-exp 27882 ex-fac 27883 ex-bc 27884 ex-ind-dvds 27893 hgt750lemd 31328 hgt750lem 31331 hgt750lem2 31332 hgt750leme 31338 tgoldbachgtde 31340 kur14lem9 31795 235t711 38159 ex-decpmul 38160 rmxdioph 38546 inductionexd 39413 amgm4d 39463 wallispi2lem1 41219 wallispi2lem2 41220 wallispi2 41221 stirlinglem3 41224 stirlinglem8 41229 stirlinglem15 41236 smfmullem2 41930 fmtno4 42489 fmtno5lem4 42493 fmtno5 42494 257prm 42498 fmtno4prmfac 42509 fmtno4prmfac193 42510 fmtno4nprmfac193 42511 fmtno4prm 42512 fmtnofz04prm 42514 fmtnole4prm 42515 fmtno5faclem1 42516 fmtno5faclem2 42517 fmtno5faclem3 42518 fmtno5fac 42519 fmtno5nprm 42520 139prmALT 42536 2exp7 42539 127prm 42540 2exp11 42542 m11nprm 42543 3exp4mod41 42558 41prothprmlem2 42560 |
Copyright terms: Public domain | W3C validator |