Theorem zcnd 9773

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 9772	. 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 9648

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 8501  df-z 9649

This theorem is used by:  qapne  10048  ltesubnnd  10180  fzsplit3  10468  fzspl  10486  fzm1  10517  fzrevral  10522  fzshftral  10525  nn0disj  10555  fzoss2  10591  fzo0addelr  10617  elfzoext  10620  fzosubel  10622  fzosubel3  10624  fzocatel  10627  fzosplitsnm1  10637  infssuzex  10676  zsupssdc  10683  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemex  10694  rebtwn2zlemstep  10697  rebtwn2z  10699  flqaddz  10745  flqzadd  10746  2tnp1ge0ge0  10749  ceiqm1l  10761  intqfrac2  10769  intfracq  10770  flqdiv  10771  modqvalr  10775  flqpmodeq  10777  modq0  10779  mulqmod0  10780  modqlt  10783  modqdiffl  10785  modqfrac  10787  flqmod  10788  intqfrac  10789  modqmulnn  10792  modqvalp1  10793  modqcyc  10809  modqcyc2  10810  modqadd1  10811  mulqaddmodid  10814  mulp1mod1  10815  modqmul1  10827  modqmul12d  10828  modqnegd  10829  modqmulmodr  10840  modqdi  10842  modqsubdir  10843  modfzo0difsn  10845  modsumfzodifsn  10846  addmodlteq  10848  frecfzen2  10877  uzennn  10886  uzsinds  10894  seq3shft2  10931  monoord2  10936  iseqf1olemab  10952  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seqf1oglem1  10969  seqf1oglem2  10970  expaddzaplem  11032  modqexp  11117  sqoddm1div8  11144  bcm1k  11212  bcp1nk  11214  bcpasc  11218  bcm1n  11221  hashfz  11276  hashfzo  11277  hashfzp1  11279  hashfibclem  11296  seq3coll  11308  ccatval3  11381  ccatlid  11388  ccatass  11390  ccatalpha  11395  swrdfv0  11440  swrdfv2  11449  swrds1  11454  ccatswrd  11456  pfxfv  11470  ccatpfx  11487  swrdpfx  11493  pfxccatin12lem2  11517  seq3shft  11617  fzomaxdif  11894  climshft2  12088  iserex  12121  iser3shft  12128  serf0  12134  fsumm1  12199  fsumsplitsnun  12202  fsump1  12203  fsumshftm  12228  fisumrev2  12229  telfsumo  12249  fsumparts  12253  binomlem  12266  isumshft  12273  isumsplit  12274  isum1p  12275  divcnv  12280  arisum  12281  trireciplem  12283  cvgratnnlemmn  12308  cvgratnnlemsumlt  12311  mertenslemi1  12318  ntrivcvgap  12331  fprodm1  12381  fprodp1  12383  fprodfac  12398  fprodrev  12402  fprodmodd  12424  eirraplem  12560  moddvds  12582  dvdscmulr  12603  dvdsmulcr  12604  dvds2ln  12607  dvdsadd2b  12623  dvdsaddre2b  12624  fsumdvds  12625  fzocongeq  12641  addmodlteqALT  12642  dvdsexp  12644  dvdsmod  12645  mulmoddvds  12646  3dvds  12647  odd2np1  12656  oddm1even  12658  oexpneg  12660  mulsucdiv2z  12668  zob  12674  ltoddhalfle  12676  divalglemnn  12701  divalglemqt  12702  divalglemex  12705  divalglemeuneg  12706  divalgb  12708  divalgmod  12710  modremain  12712  flodddiv4  12719  bitsp1  12734  bitsfzo  12738  bitsmod  12739  bitsinv1lem  12744  dvdsbnd  12749  gcdaddm  12777  modgcd  12784  gcdmultipled  12786  dvdsgcdidd  12787  bezoutlemnewy  12789  bezoutlemaz  12796  bezoutlembz  12797  dvdsmulgcd  12818  rplpwr  12820  uzwodc  12830  lcmval  12857  lcmcllem  12861  lcmid  12874  mulgcddvds  12888  divgcdcoprm0  12895  cncongr1  12897  cncongr2  12898  rpexp  12948  sqrt2irrlem  12956  sqrt2irrap  12976  qmuldeneqnum  12991  numdensq  12998  qden1elz  13001  hashdvds  13019  phiprm  13021  eulerthlema  13028  eulerthlemh  13029  eulerthlemth  13030  fermltl  13032  prmdiv  13033  prmdiveq  13034  hashgcdlem  13036  odzdvds  13044  modprm0  13053  modprmn0modprm0  13055  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem15  13077  pcpremul  13092  pceulem  13093  pceu  13094  pczpre  13096  pcdiv  13101  pcqmul  13102  pcqdiv  13106  pcexp  13108  pcaddlem  13138  pcadd  13139  fldivp1  13147  pcfac  13149  pcbc  13150  prmpwdvds  13154  4sqlem5  13181  4sqlem8  13184  4sqlem9  13185  4sqlem10  13186  4sqlemffi  13195  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  4sqlem14  13203  4sqlem16  13205  4sqlem17  13206  prmlem0  13240  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsgt1  13303  ballotfilemsdom  13304  ballotfilemsel1i  13305  ballotfilemsf1o  13306  ballotfilemsima  13308  ballotfilemfrceq  13321  ballotfilemfrcn0  13322  ballotfilem1ri  13327  znnen  13338  mulgsubcl  13988  mulgdirlem  14005  mulgdir  14006  mulgass  14011  mulgmodid  14013  mulgsubdir  14014  gzsumconst  14192  gzsumsnfd  14196  gzsumsplit0  14197  gzsumshift  14198  gzsumgsum  14204  zringmulg  14982  zndvds0  15034  znf1o  15035  znunit  15043  logfac  16048  relogbexpap  16113  logbgcd1irraplemap  16124  wilthlem1  16151  ppiqub  16194  pcbcctr  16201  bcmono  16202  bposlem5  16213  lgslem1  16217  lgsval2lem  16227  lgsval4a  16239  lgsneg  16241  lgsneg1  16242  lgsmod  16243  lgsdirprm  16251  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsabs1  16256  lgssq  16257  lgssq2  16258  lgsmulsqcoprm  16263  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem1  16278  gausslemma2dlem4  16281  gausslemma2dlem5a  16282  gausslemma2dlem5  16283  gausslemma2dlem6  16284  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquad2lem1  16298  lgsquad3  16301  2lgslem1b  16306  2lgsoddprmlem2  16323  2sqlem3  16334  2sqlem4  16335  2sqlem8a  16339  2sqlem8  16340  clwwlkccatlem  16739  iswomni0  17199