Theorem zcnd 9769

Description: An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	|- ( ph -> A e. ZZ )

Assertion

Ref	Expression
zcnd	|- ( ph -> A e. CC )

Proof of Theorem zcnd

Step	Hyp	Ref	Expression
1		zred.1	. . 3 |- ( ph -> A e. ZZ )
2	1	zred 9768	. 2 |- ( ph -> A e. RR )
3	2	recnd 8354	1 |- ( ph -> A e. CC )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   ZZcz 9644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8500  df-z 9645

This theorem is used by:  qapne  10039  ltesubnnd  10170  fzsplit3  10458  fzspl  10476  fzm1  10507  fzrevral  10512  fzshftral  10515  nn0disj  10545  fzoss2  10581  fzo0addelr  10607  elfzoext  10610  fzosubel  10612  fzosubel3  10614  fzocatel  10617  fzosplitsnm1  10627  infssuzex  10666  zsupssdc  10673  qtri3or  10675  exbtwnzlemstep  10682  exbtwnzlemex  10684  rebtwn2zlemstep  10687  rebtwn2z  10689  flqaddz  10732  flqzadd  10733  2tnp1ge0ge0  10736  ceiqm1l  10748  intqfrac2  10756  intfracq  10757  flqdiv  10758  modqvalr  10762  flqpmodeq  10764  modq0  10766  mulqmod0  10767  modqlt  10770  modqdiffl  10772  modqfrac  10774  flqmod  10775  intqfrac  10776  modqmulnn  10779  modqvalp1  10780  modqcyc  10796  modqcyc2  10797  modqadd1  10798  mulqaddmodid  10801  mulp1mod1  10802  modqmul1  10814  modqmul12d  10815  modqnegd  10816  modqmulmodr  10827  modqdi  10829  modqsubdir  10830  modfzo0difsn  10832  modsumfzodifsn  10833  addmodlteq  10835  frecfzen2  10864  uzennn  10873  uzsinds  10881  seq3shft2  10918  monoord2  10923  iseqf1olemab  10939  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seqf1oglem1  10956  seqf1oglem2  10957  expaddzaplem  11019  modqexp  11104  sqoddm1div8  11131  bcm1k  11198  bcp1nk  11200  bcpasc  11204  bcm1n  11207  hashfz  11262  hashfzo  11263  hashfzp1  11265  hashfibclem  11282  seq3coll  11294  ccatval3  11367  ccatlid  11374  ccatass  11376  ccatalpha  11381  swrdfv0  11426  swrdfv2  11435  swrds1  11440  ccatswrd  11442  pfxfv  11456  ccatpfx  11473  swrdpfx  11479  pfxccatin12lem2  11503  seq3shft  11603  fzomaxdif  11879  climshft2  12072  iserex  12105  iser3shft  12112  serf0  12118  fsumm1  12183  fsumsplitsnun  12186  fsump1  12187  fsumshftm  12212  fisumrev2  12213  telfsumo  12233  fsumparts  12237  binomlem  12250  isumshft  12257  isumsplit  12258  isum1p  12259  divcnv  12264  arisum  12265  trireciplem  12267  cvgratnnlemmn  12292  cvgratnnlemsumlt  12295  mertenslemi1  12302  ntrivcvgap  12315  fprodm1  12365  fprodp1  12367  fprodfac  12382  fprodrev  12386  fprodmodd  12408  eirraplem  12544  moddvds  12566  dvdscmulr  12587  dvdsmulcr  12588  dvds2ln  12591  dvdsadd2b  12607  dvdsaddre2b  12608  fsumdvds  12609  fzocongeq  12625  addmodlteqALT  12626  dvdsexp  12628  dvdsmod  12629  mulmoddvds  12630  3dvds  12631  odd2np1  12640  oddm1even  12642  oexpneg  12644  mulsucdiv2z  12652  zob  12658  ltoddhalfle  12660  divalglemnn  12685  divalglemqt  12686  divalglemex  12689  divalglemeuneg  12690  divalgb  12692  divalgmod  12694  modremain  12696  flodddiv4  12703  bitsp1  12718  bitsfzo  12722  bitsmod  12723  bitsinv1lem  12728  dvdsbnd  12733  gcdaddm  12761  modgcd  12768  gcdmultipled  12770  dvdsgcdidd  12771  bezoutlemnewy  12773  bezoutlemaz  12780  bezoutlembz  12781  dvdsmulgcd  12802  rplpwr  12804  uzwodc  12814  lcmval  12841  lcmcllem  12845  lcmid  12858  mulgcddvds  12872  divgcdcoprm0  12879  cncongr1  12881  cncongr2  12882  rpexp  12931  sqrt2irrlem  12939  sqrt2irrap  12958  qmuldeneqnum  12973  numdensq  12980  qden1elz  12983  hashdvds  12999  phiprm  13001  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  fermltl  13012  prmdiv  13013  prmdiveq  13014  hashgcdlem  13016  odzdvds  13024  modprm0  13033  modprmn0modprm0  13035  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem15  13057  pcpremul  13072  pceulem  13073  pceu  13074  pczpre  13076  pcdiv  13081  pcqmul  13082  pcqdiv  13086  pcexp  13088  pcaddlem  13118  pcadd  13119  fldivp1  13127  pcfac  13129  pcbc  13130  prmpwdvds  13134  4sqlem5  13161  4sqlem8  13164  4sqlem9  13165  4sqlem10  13166  4sqlemffi  13175  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  4sqlem14  13183  4sqlem16  13185  4sqlem17  13186  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsgt1  13254  ballotfilemsdom  13255  ballotfilemsel1i  13256  ballotfilemsf1o  13257  ballotfilemsima  13259  ballotfilemfrceq  13272  ballotfilemfrcn0  13273  ballotfilem1ri  13278  znnen  13289  mulgsubcl  13939  mulgdirlem  13956  mulgdir  13957  mulgass  13962  mulgmodid  13964  mulgsubdir  13965  gzsumconst  14143  gzsumsnfd  14147  gzsumsplit0  14148  gzsumshift  14149  gzsumgsum  14155  zringmulg  14933  zndvds0  14985  znf1o  14986  znunit  14994  logfac  15995  relogbexpap  16060  logbgcd1irraplemap  16071  wilthlem1  16094  lgslem1  16119  lgsval2lem  16129  lgsval4a  16141  lgsneg  16143  lgsneg1  16144  lgsmod  16145  lgsdirprm  16153  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsabs1  16158  lgssq  16159  lgssq2  16160  lgsmulsqcoprm  16165  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem1  16180  gausslemma2dlem4  16183  gausslemma2dlem5a  16184  gausslemma2dlem5  16185  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquad2lem1  16200  lgsquad3  16203  2lgslem1b  16208  2lgsoddprmlem2  16225  2sqlem3  16236  2sqlem4  16237  2sqlem8a  16241  2sqlem8  16242  clwwlkccatlem  16641  iswomni0  17101