Theorem zcnd 9498

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 9497	. 2 |- ( ph -> A e. RR )
3	2	recnd 8103	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   ZZcz 9374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8019

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949  df-neg 8248  df-z 9375

This theorem is referenced by:  qapne  9762  fzm1  10224  fzrevral  10229  fzshftral  10232  nn0disj  10262  fzoss2  10298  fzo0addelr  10320  elfzoext  10323  fzosubel  10325  fzosubel3  10327  fzocatel  10330  fzosplitsnm1  10340  infssuzex  10378  zsupssdc  10383  qtri3or  10385  exbtwnzlemstep  10392  exbtwnzlemex  10394  rebtwn2zlemstep  10397  rebtwn2z  10399  flqaddz  10442  flqzadd  10443  2tnp1ge0ge0  10446  ceiqm1l  10458  intqfrac2  10466  intfracq  10467  flqdiv  10468  modqvalr  10472  flqpmodeq  10474  modq0  10476  mulqmod0  10477  modqlt  10480  modqdiffl  10482  modqfrac  10484  flqmod  10485  intqfrac  10486  modqmulnn  10489  modqvalp1  10490  modqcyc  10506  modqcyc2  10507  modqadd1  10508  mulqaddmodid  10511  mulp1mod1  10512  modqmul1  10524  modqmul12d  10525  modqnegd  10526  modqmulmodr  10537  modqdi  10539  modqsubdir  10540  modfzo0difsn  10542  modsumfzodifsn  10543  addmodlteq  10545  frecfzen2  10574  uzennn  10583  uzsinds  10591  seq3shft2  10628  monoord2  10633  iseqf1olemab  10649  seq3f1olemqsumkj  10658  seq3f1olemqsum  10660  seqf1oglem1  10666  seqf1oglem2  10667  expaddzaplem  10729  modqexp  10813  sqoddm1div8  10840  bcm1k  10907  bcp1nk  10909  bcpasc  10913  hashfz  10968  hashfzo  10969  hashfzp1  10971  seq3coll  10989  ccatval3  11058  ccatlid  11065  ccatass  11067  swrdfv0  11110  swrdfv2  11119  swrds1  11124  ccatswrd  11126  pfxfv  11138  ccatpfx  11155  seq3shft  11182  fzomaxdif  11457  climshft2  11650  iserex  11683  iser3shft  11690  serf0  11696  fsumm1  11760  fsumsplitsnun  11763  fsump1  11764  fsumshftm  11789  fisumrev2  11790  telfsumo  11810  fsumparts  11814  binomlem  11827  isumshft  11834  isumsplit  11835  isum1p  11836  divcnv  11841  arisum  11842  trireciplem  11844  cvgratnnlemmn  11869  cvgratnnlemsumlt  11872  mertenslemi1  11879  ntrivcvgap  11892  fprodm1  11942  fprodp1  11944  fprodfac  11959  fprodrev  11963  fprodmodd  11985  eirraplem  12121  moddvds  12143  dvdscmulr  12164  dvdsmulcr  12165  dvds2ln  12168  dvdsadd2b  12184  dvdsaddre2b  12185  fsumdvds  12186  fzocongeq  12202  addmodlteqALT  12203  dvdsexp  12205  dvdsmod  12206  mulmoddvds  12207  3dvds  12208  odd2np1  12217  oddm1even  12219  oexpneg  12221  mulsucdiv2z  12229  zob  12235  ltoddhalfle  12237  divalglemnn  12262  divalglemqt  12263  divalglemex  12266  divalglemeuneg  12267  divalgb  12269  divalgmod  12271  modremain  12273  flodddiv4  12280  bitsp1  12295  bitsfzo  12299  bitsmod  12300  bitsinv1lem  12305  dvdsbnd  12310  gcdaddm  12338  modgcd  12345  gcdmultipled  12347  dvdsgcdidd  12348  bezoutlemnewy  12350  bezoutlemaz  12357  bezoutlembz  12358  dvdsmulgcd  12379  rplpwr  12381  uzwodc  12391  lcmval  12418  lcmcllem  12422  lcmid  12435  mulgcddvds  12449  divgcdcoprm0  12456  cncongr1  12458  cncongr2  12459  rpexp  12508  sqrt2irrlem  12516  sqrt2irrap  12535  qmuldeneqnum  12550  numdensq  12557  qden1elz  12560  hashdvds  12576  phiprm  12578  eulerthlema  12585  eulerthlemh  12586  eulerthlemth  12587  fermltl  12589  prmdiv  12590  prmdiveq  12591  hashgcdlem  12593  odzdvds  12601  modprm0  12610  modprmn0modprm0  12612  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem15  12634  pcpremul  12649  pceulem  12650  pceu  12651  pczpre  12653  pcdiv  12658  pcqmul  12659  pcqdiv  12663  pcexp  12665  pcaddlem  12695  pcadd  12696  fldivp1  12704  pcfac  12706  pcbc  12707  prmpwdvds  12711  4sqlem5  12738  4sqlem8  12741  4sqlem9  12742  4sqlem10  12743  4sqlemffi  12752  4sqexercise2  12755  4sqlemsdc  12756  4sqlem11  12757  4sqlem14  12760  4sqlem16  12762  4sqlem17  12763  znnen  12802  mulgsubcl  13505  mulgdirlem  13522  mulgdir  13523  mulgass  13528  mulgmodid  13530  mulgsubdir  13531  gsumfzconst  13710  gsumfzsnfd  13714  zringmulg  14393  zndvds0  14445  znf1o  14446  znunit  14454  relogbexpap  15463  logbgcd1irraplemap  15474  wilthlem1  15485  lgslem1  15510  lgsval2lem  15520  lgsval4a  15532  lgsneg  15534  lgsneg1  15535  lgsmod  15536  lgsdirprm  15544  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsabs1  15549  lgssq  15550  lgssq2  15551  lgsmulsqcoprm  15556  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem1  15571  gausslemma2dlem4  15574  gausslemma2dlem5a  15575  gausslemma2dlem5  15576  gausslemma2dlem6  15577  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlem1  15587  lgsquad2lem1  15591  lgsquad3  15594  2lgslem1b  15599  2lgsoddprmlem2  15616  2sqlem3  15627  2sqlem4  15628  2sqlem8a  15632  2sqlem8  15633  iswomni0  16027