![]() |
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 8583 | . 2 ⊢ ℕ ⊆ ℂ | |
2 | 1 | sseli 3043 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1448 ℂcc 7498 ℕcn 8578 |
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 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-cnex 7586 ax-resscn 7587 ax-1re 7589 ax-addrcl 7592 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 df-v 2643 df-in 3027 df-ss 3034 df-int 3719 df-inn 8579 |
This theorem is referenced by: nn1m1nn 8596 nn1suc 8597 nnaddcl 8598 nnmulcl 8599 nnsub 8617 nndiv 8619 nndivtr 8620 nnnn0addcl 8859 nn0nnaddcl 8860 elnnnn0 8872 nnnegz 8909 zaddcllempos 8943 zaddcllemneg 8945 nnaddm1cl 8967 elz2 8974 zdiv 8991 zdivadd 8992 zdivmul 8993 nneoor 9005 nneo 9006 divfnzn 9263 qmulz 9265 qaddcl 9277 qnegcl 9278 qmulcl 9279 qreccl 9284 nnledivrp 9394 nn0ledivnn 9395 fseq1m1p1 9716 nnsplit 9755 ubmelm1fzo 9844 subfzo0 9860 flqdiv 9935 addmodidr 9987 modfzo0difsn 10009 nn0ennn 10047 expnegap0 10142 expm1t 10162 nnsqcl 10203 nnlesq 10237 facdiv 10325 facndiv 10326 faclbnd 10328 bcn1 10345 bcn2m1 10356 arisum 11106 arisum2 11107 expcnvap0 11110 mertenslem2 11144 ef0lem 11164 efexp 11186 nndivides 11295 modmulconst 11320 dvdsflip 11344 nn0enne 11394 nno 11398 divalgmod 11419 ndvdsadd 11423 modgcd 11474 gcddiv 11500 gcdmultiple 11501 gcdmultiplez 11502 rpmulgcd 11507 rplpwr 11508 sqgcd 11510 lcmgcdlem 11551 qredeq 11570 qredeu 11571 divgcdcoprm0 11575 cncongrcoprm 11580 prmind2 11594 isprm6 11618 sqrt2irr 11633 oddpwdclemodd 11642 divnumden 11666 divdenle 11667 nn0gcdsq 11670 hashgcdlem 11695 |
Copyright terms: Public domain | W3C validator |