Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nncn | Unicode version |
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) |
Ref | Expression |
---|---|
nncn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn 8876 | . 2 | |
2 | 1 | sseli 3143 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2141 cc 7765 cn 8871 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-sep 4105 ax-cnex 7858 ax-resscn 7859 ax-1re 7861 ax-addrcl 7864 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-v 2732 df-in 3127 df-ss 3134 df-int 3830 df-inn 8872 |
This theorem is referenced by: nn1m1nn 8889 nn1suc 8890 nnaddcl 8891 nnmulcl 8892 nnsub 8910 nndiv 8912 nndivtr 8913 nnnn0addcl 9158 nn0nnaddcl 9159 elnnnn0 9171 nnnegz 9208 zaddcllempos 9242 zaddcllemneg 9244 nnaddm1cl 9266 elz2 9276 zdiv 9293 zdivadd 9294 zdivmul 9295 nneoor 9307 nneo 9308 divfnzn 9573 qmulz 9575 qaddcl 9587 qnegcl 9588 qmulcl 9589 qreccl 9594 nnledivrp 9716 nn0ledivnn 9717 fseq1m1p1 10044 nnsplit 10086 ubmelm1fzo 10175 subfzo0 10191 flqdiv 10270 addmodidr 10322 modfzo0difsn 10344 nn0ennn 10382 expnegap0 10477 expm1t 10497 nnsqcl 10538 nnlesq 10572 facdiv 10665 facndiv 10666 faclbnd 10668 bcn1 10685 bcn2m1 10696 arisum 11454 arisum2 11455 expcnvap0 11458 mertenslem2 11492 ef0lem 11616 efexp 11638 nndivides 11752 modmulconst 11778 dvdsflip 11804 nn0enne 11854 nno 11858 divalgmod 11879 ndvdsadd 11883 modgcd 11939 gcddiv 11967 gcdmultiple 11968 gcdmultiplez 11969 rpmulgcd 11974 rplpwr 11975 sqgcd 11977 lcmgcdlem 12024 qredeq 12043 qredeu 12044 divgcdcoprm0 12048 cncongrcoprm 12053 prmind2 12067 isprm6 12094 sqrt2irr 12109 oddpwdclemodd 12119 divnumden 12143 divdenle 12144 nn0gcdsq 12147 hashgcdlem 12185 pythagtriplem1 12212 pythagtriplem2 12213 pythagtriplem6 12217 pythagtriplem7 12218 pythagtriplem12 12222 pythagtriplem14 12224 pythagtriplem15 12225 pythagtriplem16 12226 pythagtriplem17 12227 pythagtriplem19 12229 pcqcl 12253 pcexp 12256 pcneg 12271 fldivp1 12293 oddprmdvds 12299 prmpwdvds 12300 infpnlem2 12305 dvexp 13434 rpcxproot 13593 logbgcd1irr 13644 lgssq2 13701 2sqlem6 13715 2sqlem10 13720 |
Copyright terms: Public domain | W3C validator |