ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zcn Unicode version

Theorem zcn 9190
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
zcn  |-  ( N  e.  ZZ  ->  N  e.  CC )

Proof of Theorem zcn
StepHypRef Expression
1 zre 9189 . 2  |-  ( N  e.  ZZ  ->  N  e.  RR )
21recnd 7921 1  |-  ( N  e.  ZZ  ->  N  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2135   CCcc 7745   ZZcz 9185
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-resscn 7839
This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-rab 2451  df-v 2726  df-un 3118  df-in 3120  df-ss 3127  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-br 3980  df-iota 5150  df-fv 5193  df-ov 5842  df-neg 8066  df-z 9186
This theorem is referenced by:  zsscn  9193  zaddcllempos  9222  peano2zm  9223  zaddcllemneg  9224  zaddcl  9225  zsubcl  9226  zrevaddcl  9235  nzadd  9237  zlem1lt  9241  zltlem1  9242  zapne  9259  zdiv  9273  zdivadd  9274  zdivmul  9275  zextlt  9277  zneo  9286  zeo2  9291  peano5uzti  9293  zindd  9303  divfnzn  9553  qmulz  9555  zq  9558  qaddcl  9567  qnegcl  9568  qmulcl  9569  qreccl  9574  fzen  9972  uzsubsubfz  9976  fz01en  9982  fzmmmeqm  9987  fzsubel  9989  fztp  10007  fzsuc2  10008  fzrev2  10014  fzrev3  10016  elfzp1b  10026  fzrevral  10034  fzrevral2  10035  fzrevral3  10036  fzshftral  10037  fzoaddel2  10122  fzosubel2  10124  eluzgtdifelfzo  10126  fzocatel  10128  elfzom1elp1fzo  10131  fzval3  10133  zpnn0elfzo1  10137  fzosplitprm1  10163  fzoshftral  10167  flqzadd  10227  2tnp1ge0ge0  10230  ceilid  10244  intfracq  10249  zmod10  10269  modqmuladdnn0  10297  addmodlteq  10327  frecfzen2  10356  ser3mono  10407  m1expeven  10496  expsubap  10497  zesq  10567  sqoddm1div8  10602  bccmpl  10661  shftuz  10753  nnabscl  11036  climshftlemg  11237  climshft  11239  mptfzshft  11377  fsumrev  11378  fisum0diag2  11382  efexp  11617  efzval  11618  demoivre  11707  dvdsval2  11724  iddvds  11738  1dvds  11739  dvds0  11740  negdvdsb  11741  dvdsnegb  11742  0dvds  11745  dvdsmul1  11747  iddvdsexp  11749  muldvds1  11750  muldvds2  11751  dvdscmul  11752  dvdsmulc  11753  summodnegmod  11756  modmulconst  11757  dvds2ln  11758  dvds2add  11759  dvds2sub  11760  dvdstr  11762  dvdssub2  11769  dvdsadd  11770  dvdsaddr  11771  dvdssub  11772  dvdssubr  11773  dvdsadd2b  11774  dvdsabseq  11779  divconjdvds  11781  alzdvds  11786  addmodlteqALT  11791  zeo3  11799  odd2np1lem  11803  odd2np1  11804  even2n  11805  oddp1even  11807  mulsucdiv2z  11816  zob  11822  ltoddhalfle  11824  halfleoddlt  11825  opoe  11826  omoe  11827  opeo  11828  omeo  11829  m1exp1  11832  divalgb  11856  divalgmod  11858  modremain  11860  ndvdssub  11861  ndvdsadd  11862  flodddiv4  11865  flodddiv4t2lthalf  11868  gcdneg  11909  gcdadd  11912  gcdid  11913  modgcd  11918  dvdsgcd  11939  mulgcd  11943  absmulgcd  11944  mulgcdr  11945  gcddiv  11946  gcdmultiplez  11948  dvdssqim  11951  dvdssq  11958  bezoutr1  11960  lcmneg  12000  lcmgcdlem  12003  lcmgcd  12004  lcmid  12006  lcm1  12007  coprmdvds  12018  coprmdvds2  12019  qredeq  12022  qredeu  12023  divgcdcoprmex  12028  cncongr1  12029  cncongr2  12030  prmdvdsexp  12074  rpexp1i  12080  sqrt2irr  12088  divnumden  12122  phiprmpw  12148  nnnn0modprm0  12181  modprmn0modprm0  12182  coprimeprodsq2  12184  pclemub  12213  pcprendvds2  12217  pcmul  12227  pcneg  12250  fldivp1  12272  prmpwdvds  12279  zgz  12297  ef2kpi  13325  efper  13326  sinperlem  13327  sin2kpi  13330  cos2kpi  13331  abssinper  13365  sinkpi  13366  coskpi  13367  cxpexprp  13414
  Copyright terms: Public domain W3C validator