![]() |
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 8579 | . 2 ⊢ 2 = (1 + 1) | |
2 | 1nn 8531 | . . 3 ⊢ 1 ∈ ℕ | |
3 | peano2nn 8532 | . . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ) | |
4 | 2, 3 | ax-mp 7 | . 2 ⊢ (1 + 1) ∈ ℕ |
5 | 1, 4 | eqeltri 2167 | 1 ⊢ 2 ∈ ℕ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1445 (class class class)co 5690 1c1 7448 + caddc 7450 ℕcn 8520 2c2 8571 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-cnex 7533 ax-resscn 7534 ax-1re 7536 ax-addrcl 7539 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-rex 2376 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 df-inn 8521 df-2 8579 |
This theorem is referenced by: 3nn 8676 2nn0 8788 2z 8876 uz3m2nn 9160 ige2m1fz1 9672 qbtwnre 9817 flhalf 9858 sqeq0 10149 sqeq0d 10216 facavg 10285 bcn2 10303 resqrexlemnm 10582 abs00ap 10626 geo2sum 11072 geo2lim 11074 ege2le3 11125 ef01bndlem 11211 mod2eq0even 11320 mod2eq1n2dvds 11321 sqgcd 11460 3lcm2e6woprm 11510 prm2orodd 11550 3prm 11552 4nprm 11553 divgcdodd 11564 isevengcd2 11579 3lcm2e6 11581 pw2dvdslemn 11585 pw2dvds 11586 pw2dvdseulemle 11587 oddpwdclemxy 11589 oddpwdclemodd 11592 oddpwdclemdc 11593 oddpwdc 11594 sqpweven 11595 2sqpwodd 11596 evenennn 11648 plusgndx 11751 plusgid 11752 plusgslid 11753 grpstrg 11765 grpbaseg 11766 grpplusgg 11767 rngstrg 11773 lmodstrd 11791 topgrpstrd 11809 dsndx 11816 dsid 11817 dsslid 11818 ex-fl 12364 ex-ceil 12365 |
Copyright terms: Public domain | W3C validator |