| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 7nn0 | Structured version Visualization version GIF version | ||
| Description: 7 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| Ref | Expression |
|---|---|
| 7nn0 | ⊢ 7 ∈ ℕ0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 7nn 12237 | . 2 ⊢ 7 ∈ ℕ | |
| 2 | 1 | nnnn0i 12409 | 1 ⊢ 7 ∈ ℕ0 |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2113 7c7 12205 ℕ0cn0 12401 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 ax-un 7680 ax-1cn 11084 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-om 7809 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-n0 12402 |
| This theorem is referenced by: 7p4e11 12683 7p5e12 12684 7p6e13 12685 7p7e14 12686 8p8e16 12693 9p8e17 12700 9p9e18 12701 7t3e21 12717 7t4e28 12718 7t5e35 12719 7t6e42 12720 7t7e49 12721 8t8e64 12728 9t3e27 12730 9t4e36 12731 9t8e72 12735 9t9e81 12736 s7f1o 14889 7prm 17038 17prm 17044 23prm 17046 prmlem2 17047 37prm 17048 83prm 17050 139prm 17051 163prm 17052 317prm 17053 631prm 17054 1259lem1 17058 1259lem2 17059 1259lem3 17060 1259lem4 17061 1259lem5 17062 1259prm 17063 2503lem1 17064 2503lem2 17065 2503lem3 17066 2503prm 17067 4001lem1 17068 4001lem2 17069 4001lem3 17070 4001lem4 17071 4001prm 17072 quartlem1 26823 quartlem2 26824 log2ublem1 26912 log2ublem3 26914 log2ub 26915 bclbnd 27247 bpos1 27250 slotslnbpsd 28514 ex-prmo 30534 hgt750lemd 34805 hgt750lem 34808 hgt750lem2 34809 hgt750leme 34815 tgoldbachgnn 34816 tgoldbachgtde 34817 tgoldbachgt 34820 60lcm7e420 42264 3exp7 42307 3lexlogpow5ineq1 42308 3lexlogpow5ineq2 42309 3lexlogpow2ineq1 42312 3lexlogpow5ineq5 42314 aks4d1p1 42330 235t711 42560 ex-decpmul 42561 3cubeslem3l 42928 3cubeslem3r 42929 expdiophlem2 43264 resqrtvalex 43886 imsqrtvalex 43887 fmtno5lem2 47800 fmtno5lem4 47802 fmtno5 47803 257prm 47807 fmtno4nprmfac193 47820 fmtno5faclem1 47825 fmtno5faclem2 47826 fmtno5fac 47828 fmtno5nprm 47829 139prmALT 47842 127prm 47845 m11nprm 47847 2exp340mod341 47979 tgoldbach 48063 ackval2012 48937 |
| Copyright terms: Public domain | W3C validator |