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 11919 | . 2 ⊢ 7 ∈ ℕ | |
2 | 1 | nnnn0i 12095 | 1 ⊢ 7 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 7c7 11887 ℕ0cn0 12087 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 ax-un 7520 ax-1cn 10784 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2940 df-ral 3063 df-rex 3064 df-reu 3065 df-rab 3067 df-v 3407 df-sbc 3692 df-csb 3809 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-pss 3882 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-tp 4543 df-op 4545 df-uni 4817 df-iun 4903 df-br 5051 df-opab 5113 df-mpt 5133 df-tr 5159 df-id 5452 df-eprel 5457 df-po 5465 df-so 5466 df-fr 5506 df-we 5508 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6157 df-ord 6213 df-on 6214 df-lim 6215 df-suc 6216 df-iota 6335 df-fun 6379 df-fn 6380 df-f 6381 df-f1 6382 df-fo 6383 df-f1o 6384 df-fv 6385 df-ov 7213 df-om 7642 df-wrecs 8044 df-recs 8105 df-rdg 8143 df-nn 11828 df-2 11890 df-3 11891 df-4 11892 df-5 11893 df-6 11894 df-7 11895 df-n0 12088 |
This theorem is referenced by: 7p4e11 12366 7p5e12 12367 7p6e13 12368 7p7e14 12369 8p8e16 12376 9p8e17 12383 9p9e18 12384 7t3e21 12400 7t4e28 12401 7t5e35 12402 7t6e42 12403 7t7e49 12404 8t8e64 12411 9t3e27 12413 9t4e36 12414 9t8e72 12418 9t9e81 12419 7prm 16661 17prm 16667 23prm 16669 prmlem2 16670 37prm 16671 83prm 16673 139prm 16674 163prm 16675 317prm 16676 631prm 16677 1259lem1 16681 1259lem2 16682 1259lem3 16683 1259lem4 16684 1259lem5 16685 1259prm 16686 2503lem1 16687 2503lem2 16688 2503lem3 16689 2503prm 16690 4001lem1 16691 4001lem2 16692 4001lem3 16693 4001lem4 16694 4001prm 16695 quartlem1 25737 quartlem2 25738 log2ublem1 25826 log2ublem3 25828 log2ub 25829 bclbnd 26158 bpos1 26161 ex-prmo 28539 hgt750lemd 32337 hgt750lem 32340 hgt750lem2 32341 hgt750leme 32347 tgoldbachgnn 32348 tgoldbachgtde 32349 tgoldbachgt 32352 60lcm7e420 39750 3exp7 39793 3lexlogpow5ineq1 39794 3lexlogpow5ineq2 39795 3lexlogpow2ineq1 39798 3lexlogpow5ineq5 39800 aks4d1p1 39815 235t711 40024 ex-decpmul 40025 3cubeslem3l 40209 3cubeslem3r 40210 expdiophlem2 40545 resqrtvalex 40927 imsqrtvalex 40928 fmtno5lem2 44677 fmtno5lem4 44679 fmtno5 44680 257prm 44684 fmtno4nprmfac193 44697 fmtno5faclem1 44702 fmtno5faclem2 44703 fmtno5fac 44705 fmtno5nprm 44706 139prmALT 44719 127prm 44722 m11nprm 44724 2exp340mod341 44856 tgoldbach 44940 ackval2012 45708 |
Copyright terms: Public domain | W3C validator |