![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nncn | GIF version |
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
Ref | Expression |
---|---|
nncn | ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn 8954 | . 2 ⊢ ℕ ⊆ ℂ | |
2 | 1 | sseli 3166 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ℂcc 7839 ℕcn 8949 |
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 4136 ax-cnex 7932 ax-resscn 7933 ax-1re 7935 ax-addrcl 7938 |
This theorem depends on definitions: df-bi 117 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-v 2754 df-in 3150 df-ss 3157 df-int 3860 df-inn 8950 |
This theorem is referenced by: nn1m1nn 8967 nn1suc 8968 nnaddcl 8969 nnmulcl 8970 nnsub 8988 nndiv 8990 nndivtr 8991 nnnn0addcl 9236 nn0nnaddcl 9237 elnnnn0 9249 nnnegz 9286 zaddcllempos 9320 zaddcllemneg 9322 nnaddm1cl 9344 elz2 9354 zdiv 9371 zdivadd 9372 zdivmul 9373 nneoor 9385 nneo 9386 divfnzn 9651 qmulz 9653 qaddcl 9665 qnegcl 9666 qmulcl 9667 qreccl 9672 nnledivrp 9796 nn0ledivnn 9797 fseq1m1p1 10125 nnsplit 10167 ubmelm1fzo 10256 subfzo0 10272 flqdiv 10352 addmodidr 10404 modfzo0difsn 10426 nn0ennn 10464 expnegap0 10559 expm1t 10579 nnsqcl 10621 nnlesq 10655 facdiv 10750 facndiv 10751 faclbnd 10753 bcn1 10770 bcn2m1 10781 arisum 11538 arisum2 11539 expcnvap0 11542 mertenslem2 11576 ef0lem 11700 efexp 11722 nndivides 11836 modmulconst 11862 dvdsflip 11889 nn0enne 11939 nno 11943 divalgmod 11964 ndvdsadd 11968 modgcd 12024 gcddiv 12052 gcdmultiple 12053 gcdmultiplez 12054 rpmulgcd 12059 rplpwr 12060 sqgcd 12062 lcmgcdlem 12109 qredeq 12128 qredeu 12129 divgcdcoprm0 12133 cncongrcoprm 12138 prmind2 12152 isprm6 12179 sqrt2irr 12194 oddpwdclemodd 12204 divnumden 12228 divdenle 12229 nn0gcdsq 12232 hashgcdlem 12270 pythagtriplem1 12297 pythagtriplem2 12298 pythagtriplem6 12302 pythagtriplem7 12303 pythagtriplem12 12307 pythagtriplem14 12309 pythagtriplem15 12310 pythagtriplem16 12311 pythagtriplem17 12312 pythagtriplem19 12314 pcqcl 12338 pcexp 12341 pcneg 12357 fldivp1 12380 oddprmdvds 12386 prmpwdvds 12387 infpnlem2 12392 4sqlem19 12441 mulgnegnn 13072 mulgnnass 13097 mulgmodid 13101 cnfldmulg 13879 dvexp 14632 rpcxproot 14791 logbgcd1irr 14842 lgssq2 14900 2sqlem6 14925 2sqlem10 14930 |
Copyright terms: Public domain | W3C validator |