![]() |
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 11378 | . 2 ⊢ 7 ∈ ℕ | |
2 | 1 | nnnn0i 11488 | 1 ⊢ 7 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2135 7c7 11263 ℕ0cn0 11480 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110 ax-1cn 10182 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-ral 3051 df-rex 3052 df-reu 3053 df-rab 3055 df-v 3338 df-sbc 3573 df-csb 3671 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-pss 3727 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4585 df-iun 4670 df-br 4801 df-opab 4861 df-mpt 4878 df-tr 4901 df-id 5170 df-eprel 5175 df-po 5183 df-so 5184 df-fr 5221 df-we 5223 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-pred 5837 df-ord 5883 df-on 5884 df-lim 5885 df-suc 5886 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-f1 6050 df-fo 6051 df-f1o 6052 df-fv 6053 df-ov 6812 df-om 7227 df-wrecs 7572 df-recs 7633 df-rdg 7671 df-nn 11209 df-2 11267 df-3 11268 df-4 11269 df-5 11270 df-6 11271 df-7 11272 df-n0 11481 |
This theorem is referenced by: 7p4e11 11793 7p4e11OLD 11794 7p5e12 11795 7p6e13 11796 7p7e14 11797 8p8e16 11806 9p8e17 11814 9p9e18 11815 7t3e21 11837 7t4e28 11838 7t5e35 11839 7t6e42 11840 7t7e49 11841 8t8e64 11850 9t3e27 11852 9t4e36 11853 9t8e72 11857 9t9e81 11858 7prm 16015 17prm 16022 23prm 16024 prmlem2 16025 37prm 16026 83prm 16028 139prm 16029 163prm 16030 317prm 16031 631prm 16032 1259lem1 16036 1259lem2 16037 1259lem3 16038 1259lem4 16039 1259lem5 16040 1259prm 16041 2503lem1 16042 2503lem2 16043 2503lem3 16044 2503prm 16045 4001lem1 16046 4001lem2 16047 4001lem3 16048 4001lem4 16049 4001prm 16050 quartlem1 24779 quartlem2 24780 log2ublem1 24868 log2ublem3 24870 log2ub 24871 bclbnd 25200 bpos1 25203 ex-prmo 27623 hgt750lemd 31031 hgt750lem 31034 hgt750lem2 31035 hgt750leme 31041 tgoldbachgnn 31042 tgoldbachgtde 31043 tgoldbachgt 31046 expdiophlem2 38087 fmtno5lem2 41972 fmtno5lem4 41974 fmtno5 41975 257prm 41979 fmtno4nprmfac193 41992 fmtno5faclem1 41997 fmtno5faclem2 41998 fmtno5fac 42000 fmtno5nprm 42001 139prmALT 42017 127prm 42021 m11nprm 42024 tgoldbach 42211 tgoldbachOLD 42218 |
Copyright terms: Public domain | W3C validator |