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 9110 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | 1 | sseli 3133 | 1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 ℂcc 7742 ℕ0cn0 9105 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-sep 4094 ax-cnex 7835 ax-resscn 7836 ax-1re 7838 ax-addrcl 7841 ax-rnegex 7853 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rex 2448 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 df-sn 3576 df-int 3819 df-inn 8849 df-n0 9106 |
This theorem is referenced by: nn0nnaddcl 9136 elnn0nn 9147 difgtsumgt 9251 nn0n0n1ge2 9252 uzaddcl 9515 fzctr 10058 nn0split 10061 zpnn0elfzo1 10133 ubmelm1fzo 10151 subfzo0 10167 modqmuladdnn0 10293 addmodidr 10298 modfzo0difsn 10320 nn0ennn 10358 expadd 10487 expmul 10490 bernneq 10564 bernneq2 10565 faclbnd 10643 faclbnd6 10646 bccmpl 10656 bcn0 10657 bcnn 10659 bcnp1n 10661 bcn2 10666 bcp1m1 10667 bcpasc 10668 bcn2p1 10672 hashfzo0 10725 hashfz0 10727 fisum0diag2 11374 hashiun 11405 binom1dif 11414 bcxmas 11416 geolim 11438 efaddlem 11601 efexp 11609 eftlub 11617 demoivreALT 11700 nn0ob 11830 modremain 11851 mulgcdr 11936 nn0seqcvgd 11952 modprmn0modprm0 12167 coprimeprodsq 12168 coprimeprodsq2 12169 pcexp 12220 dvdsprmpweqle 12247 difsqpwdvds 12248 znnen 12274 ennnfonelemp1 12282 |
Copyright terms: Public domain | W3C validator |