![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnnn0d | GIF version |
Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnnn0d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
Ref | Expression |
---|---|
nnnn0d | ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssnn0 9004 | . 2 ⊢ ℕ ⊆ ℕ0 | |
2 | nnnn0d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
3 | 1, 2 | sseldi 3100 | 1 ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1481 ℕcn 8744 ℕ0cn0 9001 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-un 3080 df-in 3082 df-ss 3089 df-n0 9002 |
This theorem is referenced by: nn0ge2m1nn0 9062 nnzd 9196 eluzge2nn0 9391 modsumfzodifsn 10200 addmodlteq 10202 expnnval 10327 expgt1 10362 expaddzaplem 10367 expaddzap 10368 expmulzap 10370 expnbnd 10446 facwordi 10518 faclbnd 10519 facavg 10524 bcm1k 10538 bcval5 10541 1elfz0hash 10584 resqrexlemnm 10822 resqrexlemcvg 10823 summodc 11184 zsumdc 11185 bcxmas 11290 geo2sum 11315 geo2lim 11317 geoisum1 11320 geoisum1c 11321 cvgratnnlembern 11324 cvgratnnlemsumlt 11329 cvgratnnlemfm 11330 mertenslemi1 11336 prodmodclem3 11376 prodmodclem2a 11377 zproddc 11380 fprodseq 11384 eftabs 11399 efcllemp 11401 eftlub 11433 eirraplem 11519 dvdsfac 11594 divalglemnqt 11653 divalglemeunn 11654 gcdval 11684 gcdcl 11691 dvdsgcdidd 11718 mulgcd 11740 rplpwr 11751 rppwr 11752 lcmcl 11789 lcmgcdnn 11799 nprmdvds1 11856 rpexp 11867 pw2dvdslemn 11879 sqpweven 11889 2sqpwodd 11890 nn0sqrtelqelz 11920 phiprmpw 11934 crth 11936 logbgcd1irraplemexp 13093 cvgcmp2nlemabs 13402 trilpolemlt1 13409 redcwlpolemeq1 13421 |
Copyright terms: Public domain | W3C validator |