![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2nn | GIF version |
Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.) |
Ref | Expression |
---|---|
2nn | ⊢ 2 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 9013 | . 2 ⊢ 2 = (1 + 1) | |
2 | 1nn 8965 | . . 3 ⊢ 1 ∈ ℕ | |
3 | peano2nn 8966 | . . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ (1 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2262 | 1 ⊢ 2 ∈ ℕ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 (class class class)co 5900 1c1 7847 + caddc 7849 ℕcn 8954 2c2 9005 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-sep 4139 ax-cnex 7937 ax-resscn 7938 ax-1re 7940 ax-addrcl 7943 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-sn 3616 df-pr 3617 df-op 3619 df-uni 3828 df-int 3863 df-br 4022 df-iota 5199 df-fv 5246 df-ov 5903 df-inn 8955 df-2 9013 |
This theorem is referenced by: 3nn 9116 2nn0 9228 2z 9316 uz3m2nn 9609 ige2m1fz1 10145 qbtwnre 10293 flhalf 10339 sqeq0 10623 sqeq0d 10693 facavg 10767 bcn2 10785 resqrexlemnm 11068 abs00ap 11112 geo2sum 11563 geo2lim 11565 ege2le3 11720 ef01bndlem 11805 mod2eq0even 11924 mod2eq1n2dvds 11925 sqgcd 12071 3lcm2e6woprm 12129 prm2orodd 12169 3prm 12171 4nprm 12172 isprm5lem 12184 divgcdodd 12186 isevengcd2 12201 3lcm2e6 12203 pw2dvdslemn 12208 pw2dvds 12209 pw2dvdseulemle 12210 oddpwdclemxy 12212 oddpwdclemodd 12215 oddpwdclemdc 12216 oddpwdc 12217 sqpweven 12218 2sqpwodd 12219 pythagtriplem4 12311 oddprmdvds 12397 4sqlem5 12425 4sqlem6 12426 4sqlem10 12430 4sqlem12 12445 evenennn 12455 exmidunben 12488 plusgndx 12632 plusgid 12633 plusgndxnn 12634 plusgslid 12635 grpstrg 12648 grpbaseg 12649 grpplusgg 12650 rngstrg 12657 lmodstrd 12686 topgrpstrd 12718 dsndx 12733 dsid 12734 dsslid 12735 dsndxnn 12736 slotsdifdsndx 12743 slotsdifunifndx 12750 dveflem 14672 lgsval 14891 lgsfvalg 14892 lgsfcl2 14893 lgsval2lem 14897 lgsdir2lem2 14916 lgsdir2 14920 lgseisenlem1 14936 lgseisenlem2 14937 m1lgs 14938 2sqlem3 14950 2sqlem8 14956 ex-fl 14963 ex-ceil 14964 redcwlpolemeq1 15290 nconstwlpolem0 15299 |
Copyright terms: Public domain | W3C validator |