Theorem zcnd 9719

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   ZZcz 9594

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595

This theorem is referenced by:  qapne  9989  ltesubnnd  10120  fzsplit3  10407  fzspl  10425  fzm1  10456  fzrevral  10461  fzshftral  10464  nn0disj  10494  fzoss2  10530  fzo0addelr  10556  elfzoext  10559  fzosubel  10561  fzosubel3  10563  fzocatel  10566  fzosplitsnm1  10576  infssuzex  10615  zsupssdc  10622  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemex  10633  rebtwn2zlemstep  10636  rebtwn2z  10638  flqaddz  10681  flqzadd  10682  2tnp1ge0ge0  10685  ceiqm1l  10697  intqfrac2  10705  intfracq  10706  flqdiv  10707  modqvalr  10711  flqpmodeq  10713  modq0  10715  mulqmod0  10716  modqlt  10719  modqdiffl  10721  modqfrac  10723  flqmod  10724  intqfrac  10725  modqmulnn  10728  modqvalp1  10729  modqcyc  10745  modqcyc2  10746  modqadd1  10747  mulqaddmodid  10750  mulp1mod1  10751  modqmul1  10763  modqmul12d  10764  modqnegd  10765  modqmulmodr  10776  modqdi  10778  modqsubdir  10779  modfzo0difsn  10781  modsumfzodifsn  10782  addmodlteq  10784  frecfzen2  10813  uzennn  10822  uzsinds  10830  seq3shft2  10867  monoord2  10872  iseqf1olemab  10888  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seqf1oglem1  10905  seqf1oglem2  10906  expaddzaplem  10968  modqexp  11053  sqoddm1div8  11080  bcm1k  11147  bcp1nk  11149  bcpasc  11153  bcm1n  11156  hashfz  11211  hashfzo  11212  hashfzp1  11214  hashfibclem  11231  seq3coll  11239  ccatval3  11312  ccatlid  11319  ccatass  11321  ccatalpha  11326  swrdfv0  11371  swrdfv2  11380  swrds1  11385  ccatswrd  11387  pfxfv  11401  ccatpfx  11418  swrdpfx  11424  pfxccatin12lem2  11448  seq3shft  11548  fzomaxdif  11823  climshft2  12016  iserex  12049  iser3shft  12056  serf0  12062  fsumm1  12127  fsumsplitsnun  12130  fsump1  12131  fsumshftm  12156  fisumrev2  12157  telfsumo  12177  fsumparts  12181  binomlem  12194  isumshft  12201  isumsplit  12202  isum1p  12203  divcnv  12208  arisum  12209  trireciplem  12211  cvgratnnlemmn  12236  cvgratnnlemsumlt  12239  mertenslemi1  12246  ntrivcvgap  12259  fprodm1  12309  fprodp1  12311  fprodfac  12326  fprodrev  12330  fprodmodd  12352  eirraplem  12488  moddvds  12510  dvdscmulr  12531  dvdsmulcr  12532  dvds2ln  12535  dvdsadd2b  12551  dvdsaddre2b  12552  fsumdvds  12553  fzocongeq  12569  addmodlteqALT  12570  dvdsexp  12572  dvdsmod  12573  mulmoddvds  12574  3dvds  12575  odd2np1  12584  oddm1even  12586  oexpneg  12588  mulsucdiv2z  12596  zob  12602  ltoddhalfle  12604  divalglemnn  12629  divalglemqt  12630  divalglemex  12633  divalglemeuneg  12634  divalgb  12636  divalgmod  12638  modremain  12640  flodddiv4  12647  bitsp1  12662  bitsfzo  12666  bitsmod  12667  bitsinv1lem  12672  dvdsbnd  12677  gcdaddm  12705  modgcd  12712  gcdmultipled  12714  dvdsgcdidd  12715  bezoutlemnewy  12717  bezoutlemaz  12724  bezoutlembz  12725  dvdsmulgcd  12746  rplpwr  12748  uzwodc  12758  lcmval  12785  lcmcllem  12789  lcmid  12802  mulgcddvds  12816  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  rpexp  12875  sqrt2irrlem  12883  sqrt2irrap  12902  qmuldeneqnum  12917  numdensq  12924  qden1elz  12927  hashdvds  12943  phiprm  12945  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  fermltl  12956  prmdiv  12957  prmdiveq  12958  hashgcdlem  12960  odzdvds  12968  modprm0  12977  modprmn0modprm0  12979  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem15  13001  pcpremul  13016  pceulem  13017  pceu  13018  pczpre  13020  pcdiv  13025  pcqmul  13026  pcqdiv  13030  pcexp  13032  pcaddlem  13062  pcadd  13063  fldivp1  13071  pcfac  13073  pcbc  13074  prmpwdvds  13078  4sqlem5  13105  4sqlem8  13108  4sqlem9  13109  4sqlem10  13110  4sqlemffi  13119  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem14  13127  4sqlem16  13129  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsgt1  13198  ballotfilemsdom  13199  ballotfilemsel1i  13200  ballotfilemsf1o  13201  ballotfilemsima  13203  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilem1ri  13222  znnen  13233  mulgsubcl  13889  mulgdirlem  13906  mulgdir  13907  mulgass  13912  mulgmodid  13914  mulgsubdir  13915  gsumfzconst  14094  gsumfzsnfd  14098  gsumsplit0  14099  gsumshift  14105  gsumgfsum  14106  zringmulg  14872  zndvds0  14924  znf1o  14925  znunit  14933  relogbexpap  15949  logbgcd1irraplemap  15960  wilthlem1  15974  lgslem1  15999  lgsval2lem  16009  lgsval4a  16021  lgsneg  16023  lgsneg1  16024  lgsmod  16025  lgsdirprm  16033  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsabs1  16038  lgssq  16039  lgssq2  16040  lgsmulsqcoprm  16045  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem1  16060  gausslemma2dlem4  16063  gausslemma2dlem5a  16064  gausslemma2dlem5  16065  gausslemma2dlem6  16066  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquad2lem1  16080  lgsquad3  16083  2lgslem1b  16088  2lgsoddprmlem2  16105  2sqlem3  16116  2sqlem4  16117  2sqlem8a  16121  2sqlem8  16122  clwwlkccatlem  16521  iswomni0  16962