![]() |
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 12244 | . 2 ⊢ 7 ∈ ℕ | |
2 | 1 | nnnn0i 12420 | 1 ⊢ 7 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 7c7 12212 ℕ0cn0 12412 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7671 ax-1cn 11108 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7359 df-om 7802 df-2nd 7921 df-frecs 8211 df-wrecs 8242 df-recs 8316 df-rdg 8355 df-nn 12153 df-2 12215 df-3 12216 df-4 12217 df-5 12218 df-6 12219 df-7 12220 df-n0 12413 |
This theorem is referenced by: 7p4e11 12693 7p5e12 12694 7p6e13 12695 7p7e14 12696 8p8e16 12703 9p8e17 12710 9p9e18 12711 7t3e21 12727 7t4e28 12728 7t5e35 12729 7t6e42 12730 7t7e49 12731 8t8e64 12738 9t3e27 12740 9t4e36 12741 9t8e72 12745 9t9e81 12746 7prm 16982 17prm 16988 23prm 16990 prmlem2 16991 37prm 16992 83prm 16994 139prm 16995 163prm 16996 317prm 16997 631prm 16998 1259lem1 17002 1259lem2 17003 1259lem3 17004 1259lem4 17005 1259lem5 17006 1259prm 17007 2503lem1 17008 2503lem2 17009 2503lem3 17010 2503prm 17011 4001lem1 17012 4001lem2 17013 4001lem3 17014 4001lem4 17015 4001prm 17016 quartlem1 26205 quartlem2 26206 log2ublem1 26294 log2ublem3 26296 log2ub 26297 bclbnd 26626 bpos1 26629 slotslnbpsd 27382 ex-prmo 29401 hgt750lemd 33252 hgt750lem 33255 hgt750lem2 33256 hgt750leme 33262 tgoldbachgnn 33263 tgoldbachgtde 33264 tgoldbachgt 33267 60lcm7e420 40458 3exp7 40501 3lexlogpow5ineq1 40502 3lexlogpow5ineq2 40503 3lexlogpow2ineq1 40506 3lexlogpow5ineq5 40508 aks4d1p1 40524 235t711 40783 ex-decpmul 40784 3cubeslem3l 40987 3cubeslem3r 40988 expdiophlem2 41324 resqrtvalex 41899 imsqrtvalex 41900 fmtno5lem2 45718 fmtno5lem4 45720 fmtno5 45721 257prm 45725 fmtno4nprmfac193 45738 fmtno5faclem1 45743 fmtno5faclem2 45744 fmtno5fac 45746 fmtno5nprm 45747 139prmALT 45760 127prm 45763 m11nprm 45765 2exp340mod341 45897 tgoldbach 45981 ackval2012 46749 |
Copyright terms: Public domain | W3C validator |