| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 4nn0 | GIF version | ||
| Description: 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| Ref | Expression |
|---|---|
| 4nn0 | ⊢ 4 ∈ ℕ0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 4nn 9182 | . 2 ⊢ 4 ∈ ℕ | |
| 2 | 1 | nnnn0i 9285 | 1 ⊢ 4 ∈ ℕ0 |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2175 4c4 9071 ℕ0cn0 9277 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 ax-sep 4161 ax-cnex 7998 ax-resscn 7999 ax-1re 8001 ax-addrcl 8004 |
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ral 2488 df-rex 2489 df-v 2773 df-un 3169 df-in 3171 df-ss 3178 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-br 4044 df-iota 5229 df-fv 5276 df-ov 5937 df-inn 9019 df-2 9077 df-3 9078 df-4 9079 df-n0 9278 |
| This theorem is referenced by: 6p5e11 9558 7p5e12 9562 8p5e13 9568 8p7e15 9570 9p5e14 9575 9p6e15 9576 4t3e12 9583 4t4e16 9584 5t5e25 9588 6t4e24 9591 6t5e30 9592 7t3e21 9595 7t5e35 9597 7t7e49 9599 8t3e24 9601 8t4e32 9602 8t5e40 9603 8t6e48 9604 8t7e56 9605 8t8e64 9606 9t5e45 9610 9t6e54 9611 9t7e63 9612 decbin3 9627 fzo0to42pr 10330 4bc3eq4 10899 resin4p 11948 recos4p 11949 ef01bndlem 11986 sin01bnd 11987 cos01bnd 11988 prm23lt5 12505 2exp7 12676 2exp8 12677 2exp11 12678 2exp16 12679 2expltfac 12681 slotsdifdsndx 12975 slotsdifunifndx 12982 prdsvalstrd 13021 binom4 15369 2lgslem3a 15488 2lgslem3b 15489 2lgslem3c 15490 2lgslem3d 15491 ex-exp 15527 ex-fac 15528 ex-bc 15529 |
| Copyright terms: Public domain | W3C validator |