![]() |
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 11583 | . 2 ⊢ 7 ∈ ℕ | |
2 | 1 | nnnn0i 11759 | 1 ⊢ 7 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2083 7c7 11551 ℕ0cn0 11751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-1cn 10448 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-om 7444 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-nn 11493 df-2 11554 df-3 11555 df-4 11556 df-5 11557 df-6 11558 df-7 11559 df-n0 11752 |
This theorem is referenced by: 7p4e11 12028 7p5e12 12029 7p6e13 12030 7p7e14 12031 8p8e16 12038 9p8e17 12045 9p9e18 12046 7t3e21 12062 7t4e28 12063 7t5e35 12064 7t6e42 12065 7t7e49 12066 8t8e64 12073 9t3e27 12075 9t4e36 12076 9t8e72 12080 9t9e81 12081 7prm 16277 17prm 16283 23prm 16285 prmlem2 16286 37prm 16287 83prm 16289 139prm 16290 163prm 16291 317prm 16292 631prm 16293 1259lem1 16297 1259lem2 16298 1259lem3 16299 1259lem4 16300 1259lem5 16301 1259prm 16302 2503lem1 16303 2503lem2 16304 2503lem3 16305 2503prm 16306 4001lem1 16307 4001lem2 16308 4001lem3 16309 4001lem4 16310 4001prm 16311 quartlem1 25120 quartlem2 25121 log2ublem1 25210 log2ublem3 25212 log2ub 25213 bclbnd 25542 bpos1 25545 ex-prmo 27926 hgt750lemd 31532 hgt750lem 31535 hgt750lem2 31536 hgt750leme 31542 tgoldbachgnn 31543 tgoldbachgtde 31544 tgoldbachgt 31547 235t711 38720 ex-decpmul 38721 expdiophlem2 39125 fmtno5lem2 43220 fmtno5lem4 43222 fmtno5 43223 257prm 43227 fmtno4nprmfac193 43240 fmtno5faclem1 43245 fmtno5faclem2 43246 fmtno5fac 43248 fmtno5nprm 43249 139prmALT 43263 127prm 43267 m11nprm 43270 2exp340mod341 43402 tgoldbach 43486 |
Copyright terms: Public domain | W3C validator |