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 8853 | . 2 ⊢ ℕ ⊆ ℂ | |
2 | 1 | sseli 3133 | 1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 ℂcc 7742 ℕcn 8848 |
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 |
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-v 2723 df-in 3117 df-ss 3124 df-int 3819 df-inn 8849 |
This theorem is referenced by: nn1m1nn 8866 nn1suc 8867 nnaddcl 8868 nnmulcl 8869 nnsub 8887 nndiv 8889 nndivtr 8890 nnnn0addcl 9135 nn0nnaddcl 9136 elnnnn0 9148 nnnegz 9185 zaddcllempos 9219 zaddcllemneg 9221 nnaddm1cl 9243 elz2 9253 zdiv 9270 zdivadd 9271 zdivmul 9272 nneoor 9284 nneo 9285 divfnzn 9550 qmulz 9552 qaddcl 9564 qnegcl 9565 qmulcl 9566 qreccl 9571 nnledivrp 9693 nn0ledivnn 9694 fseq1m1p1 10020 nnsplit 10062 ubmelm1fzo 10151 subfzo0 10167 flqdiv 10246 addmodidr 10298 modfzo0difsn 10320 nn0ennn 10358 expnegap0 10453 expm1t 10473 nnsqcl 10514 nnlesq 10548 facdiv 10640 facndiv 10641 faclbnd 10643 bcn1 10660 bcn2m1 10671 arisum 11425 arisum2 11426 expcnvap0 11429 mertenslem2 11463 ef0lem 11587 efexp 11609 nndivides 11723 modmulconst 11749 dvdsflip 11774 nn0enne 11824 nno 11828 divalgmod 11849 ndvdsadd 11853 modgcd 11909 gcddiv 11937 gcdmultiple 11938 gcdmultiplez 11939 rpmulgcd 11944 rplpwr 11945 sqgcd 11947 lcmgcdlem 11988 qredeq 12007 qredeu 12008 divgcdcoprm0 12012 cncongrcoprm 12017 prmind2 12031 isprm6 12056 sqrt2irr 12071 oddpwdclemodd 12081 divnumden 12105 divdenle 12106 nn0gcdsq 12109 hashgcdlem 12147 pythagtriplem1 12174 pythagtriplem2 12175 pythagtriplem6 12179 pythagtriplem7 12180 pythagtriplem12 12184 pythagtriplem14 12186 pythagtriplem15 12187 pythagtriplem16 12188 pythagtriplem17 12189 pythagtriplem19 12191 pcqcl 12215 pcexp 12218 pcneg 12233 fldivp1 12255 oddprmdvds 12261 dvexp 13216 rpcxproot 13375 logbgcd1irr 13426 |
Copyright terms: Public domain | W3C validator |