Theorem zcnd 9779

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

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

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 8277

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 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9654

This theorem is used by:  qapne  10054  ltesubnnd  10186  fzsplit3  10474  fzspl  10492  fzm1  10523  fzrevral  10528  fzshftral  10531  nn0disj  10561  fzoss2  10597  fzo0addelr  10623  elfzoext  10626  fzosubel  10628  fzosubel3  10630  fzocatel  10633  fzosplitsnm1  10643  infssuzex  10682  zsupssdc  10689  qtri3or  10691  exbtwnzlemstep  10698  exbtwnzlemex  10700  rebtwn2zlemstep  10703  rebtwn2z  10705  flqaddz  10752  flqzadd  10753  2tnp1ge0ge0  10756  ceiqm1l  10768  intqfrac2  10776  intfracq  10777  flqdiv  10778  modqvalr  10782  flqpmodeq  10784  modq0  10786  mulqmod0  10787  modqlt  10790  modqdiffl  10792  modqfrac  10794  flqmod  10795  intqfrac  10796  modqmulnn  10799  modqvalp1  10800  modqcyc  10816  modqcyc2  10817  modqadd1  10818  mulqaddmodid  10821  mulp1mod1  10822  modqmul1  10834  modqmul12d  10835  modqnegd  10836  modqmulmodr  10847  modqdi  10849  modqsubdir  10850  modfzo0difsn  10852  modsumfzodifsn  10853  addmodlteq  10855  frecfzen2  10884  uzennn  10893  uzsinds  10901  seq3shft2  10938  monoord2  10943  iseqf1olemab  10959  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seqf1oglem1  10976  seqf1oglem2  10977  expaddzaplem  11039  modqexp  11124  sqoddm1div8  11151  bcm1k  11219  bcp1nk  11221  bcpasc  11225  bcm1n  11228  hashfz  11283  hashfzo  11284  hashfzp1  11286  hashfibclem  11303  seq3coll  11315  ccatval3  11388  ccatlid  11395  ccatass  11397  ccatalpha  11402  swrdfv0  11447  swrdfv2  11456  swrds1  11461  ccatswrd  11463  pfxfv  11477  ccatpfx  11494  swrdpfx  11500  pfxccatin12lem2  11524  seq3shft  11624  fzomaxdif  11901  climshft2  12096  iserex  12129  iser3shft  12136  serf0  12142  fsumm1  12207  fsumsplitsnun  12210  fsump1  12211  fsumshftm  12236  fisumrev2  12237  telfsumo  12257  fsumparts  12261  binomlem  12274  isumshft  12281  isumsplit  12282  isum1p  12283  divcnv  12288  arisum  12289  trireciplem  12291  cvgratnnlemmn  12316  cvgratnnlemsumlt  12319  mertenslemi1  12326  ntrivcvgap  12339  fprodm1  12389  fprodp1  12391  fprodfac  12406  fprodrev  12410  fprodmodd  12432  eirraplem  12568  moddvds  12590  dvdscmulr  12611  dvdsmulcr  12612  dvds2ln  12615  dvdsadd2b  12631  dvdsaddre2b  12632  fsumdvds  12633  fzocongeq  12649  addmodlteqALT  12650  dvdsexp  12652  dvdsmod  12653  mulmoddvds  12654  3dvds  12655  odd2np1  12664  oddm1even  12666  oexpneg  12668  mulsucdiv2z  12676  zob  12682  ltoddhalfle  12684  divalglemnn  12709  divalglemqt  12710  divalglemex  12713  divalglemeuneg  12714  divalgb  12716  divalgmod  12718  modremain  12720  flodddiv4  12727  bitsp1  12742  bitsfzo  12746  bitsmod  12747  bitsinv1lem  12752  dvdsbnd  12757  gcdaddm  12785  modgcd  12792  gcdmultipled  12794  dvdsgcdidd  12795  bezoutlemnewy  12797  bezoutlemaz  12804  bezoutlembz  12805  dvdsmulgcd  12826  rplpwr  12828  uzwodc  12838  lcmval  12865  lcmcllem  12869  lcmid  12882  mulgcddvds  12896  divgcdcoprm0  12903  cncongr1  12905  cncongr2  12906  rpexp  12956  sqrt2irrlem  12964  sqrt2irrap  12984  qmuldeneqnum  12999  numdensq  13006  qden1elz  13009  hashdvds  13027  phiprm  13029  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  fermltl  13040  prmdiv  13041  prmdiveq  13042  hashgcdlem  13044  odzdvds  13052  modprm0  13061  modprmn0modprm0  13063  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem15  13085  pcpremul  13100  pceulem  13101  pceu  13102  pczpre  13104  pcdiv  13109  pcqmul  13110  pcqdiv  13114  pcexp  13116  pcaddlem  13146  pcadd  13147  fldivp1  13155  pcfac  13157  pcbc  13158  prmpwdvds  13162  4sqlem5  13189  4sqlem8  13192  4sqlem9  13193  4sqlem10  13194  4sqlemffi  13203  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  4sqlem14  13211  4sqlem16  13213  4sqlem17  13214  prmlem0  13248  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsgt1  13311  ballotfilemsdom  13312  ballotfilemsel1i  13313  ballotfilemsf1o  13314  ballotfilemsima  13316  ballotfilemfrceq  13329  ballotfilemfrcn0  13330  ballotfilem1ri  13335  znnen  13346  mulgsubcl  13997  mulgdirlem  14014  mulgdir  14015  mulgass  14020  mulgmodid  14022  mulgsubdir  14023  gzsumconst  14232  gzsumsnfd  14236  gzsumsplit0  14237  gzsumshift  14238  gzsumgsum  14244  zringmulg  15041  zndvds0  15093  znf1o  15094  znunit  15102  logfac  16143  relogbexpap  16211  logbgcd1irraplemap  16222  wilthlem1  16249  ppiqub  16310  chtqub  16313  pcbcctr  16320  bcmono  16321  bposlem5  16332  bposlem6  16333  lgslem1  16341  lgsval2lem  16351  lgsval4a  16363  lgsneg  16365  lgsneg1  16366  lgsmod  16367  lgsdirprm  16375  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsabs1  16380  lgssq  16381  lgssq2  16382  lgsmulsqcoprm  16387  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem1  16402  gausslemma2dlem4  16405  gausslemma2dlem5a  16406  gausslemma2dlem5  16407  gausslemma2dlem6  16408  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquad2lem1  16422  lgsquad3  16425  2lgslem1b  16430  2lgsoddprmlem2  16447  2sqlem3  16458  2sqlem4  16459  2sqlem8a  16463  2sqlem8  16464  clwwlkccatlem  16863  iswomni0  17325