Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nn0cn | GIF version |
Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
nn0cn | ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0sscn 8982 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | 1 | sseli 3093 | 1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 ℂcc 7618 ℕ0cn0 8977 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-cnex 7711 ax-resscn 7712 ax-1re 7714 ax-addrcl 7717 ax-rnegex 7729 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-sn 3533 df-int 3772 df-inn 8721 df-n0 8978 |
This theorem is referenced by: nn0nnaddcl 9008 elnn0nn 9019 nn0n0n1ge2 9121 uzaddcl 9381 fzctr 9910 nn0split 9913 zpnn0elfzo1 9985 ubmelm1fzo 10003 subfzo0 10019 modqmuladdnn0 10141 addmodidr 10146 modfzo0difsn 10168 nn0ennn 10206 expadd 10335 expmul 10338 bernneq 10412 bernneq2 10413 faclbnd 10487 faclbnd6 10490 bccmpl 10500 bcn0 10501 bcnn 10503 bcnp1n 10505 bcn2 10510 bcp1m1 10511 bcpasc 10512 bcn2p1 10516 hashfzo0 10569 hashfz0 10571 fisum0diag2 11216 hashiun 11247 binom1dif 11256 bcxmas 11258 geolim 11280 efaddlem 11380 efexp 11388 eftlub 11396 demoivreALT 11480 nn0ob 11605 modremain 11626 mulgcdr 11706 nn0seqcvgd 11722 znnen 11911 ennnfonelemp1 11919 |
Copyright terms: Public domain | W3C validator |