Theorem zcnd 9379

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7812   ZZcz 9256

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7906

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5881  df-neg 8134  df-z 9257

This theorem is referenced by:  qapne  9642  fzm1  10103  fzrevral  10108  fzshftral  10111  nn0disj  10141  fzoss2  10175  fzosubel  10197  fzosubel3  10199  fzocatel  10202  fzosplitsnm1  10212  qtri3or  10246  exbtwnzlemstep  10251  exbtwnzlemex  10253  rebtwn2zlemstep  10256  rebtwn2z  10258  flqaddz  10300  flqzadd  10301  2tnp1ge0ge0  10304  ceiqm1l  10314  intqfrac2  10322  intfracq  10323  flqdiv  10324  modqvalr  10328  flqpmodeq  10330  modq0  10332  mulqmod0  10333  modqlt  10336  modqdiffl  10338  modqfrac  10340  flqmod  10341  intqfrac  10342  modqmulnn  10345  modqvalp1  10346  modqcyc  10362  modqcyc2  10363  modqadd1  10364  mulqaddmodid  10367  mulp1mod1  10368  modqmul1  10380  modqmul12d  10381  modqnegd  10382  modqmulmodr  10393  modqdi  10395  modqsubdir  10396  modfzo0difsn  10398  modsumfzodifsn  10399  addmodlteq  10401  frecfzen2  10430  uzennn  10439  uzsinds  10445  seq3shft2  10476  monoord2  10480  iseqf1olemab  10492  seq3f1olemqsumkj  10501  seq3f1olemqsum  10503  expaddzaplem  10566  modqexp  10650  sqoddm1div8  10677  bcm1k  10743  bcp1nk  10745  bcpasc  10749  hashfz  10804  hashfzo  10805  hashfzp1  10807  seq3coll  10825  seq3shft  10850  fzomaxdif  11125  climshft2  11317  iserex  11350  iser3shft  11357  serf0  11363  fsumm1  11427  fsumsplitsnun  11430  fsump1  11431  fsumshftm  11456  fisumrev2  11457  telfsumo  11477  fsumparts  11481  binomlem  11494  isumshft  11501  isumsplit  11502  isum1p  11503  divcnv  11508  arisum  11509  trireciplem  11511  cvgratnnlemmn  11536  cvgratnnlemsumlt  11539  mertenslemi1  11546  ntrivcvgap  11559  fprodm1  11609  fprodp1  11611  fprodfac  11626  fprodrev  11630  fprodmodd  11652  eirraplem  11787  moddvds  11809  dvdscmulr  11830  dvdsmulcr  11831  dvds2ln  11834  dvdsadd2b  11850  dvdsaddre2b  11851  fzocongeq  11867  addmodlteqALT  11868  dvdsexp  11870  dvdsmod  11871  mulmoddvds  11872  odd2np1  11881  oddm1even  11883  oexpneg  11885  mulsucdiv2z  11893  zob  11899  ltoddhalfle  11901  divalglemnn  11926  divalglemqt  11927  divalglemex  11930  divalglemeuneg  11931  divalgb  11933  divalgmod  11935  modremain  11937  flodddiv4  11942  infssuzex  11953  zsupssdc  11958  dvdsbnd  11960  gcdaddm  11988  modgcd  11995  gcdmultipled  11997  dvdsgcdidd  11998  bezoutlemnewy  12000  bezoutlemaz  12007  bezoutlembz  12008  dvdsmulgcd  12029  rplpwr  12031  uzwodc  12041  lcmval  12066  lcmcllem  12070  lcmid  12083  mulgcddvds  12097  divgcdcoprm0  12104  cncongr1  12106  cncongr2  12107  rpexp  12156  sqrt2irrlem  12164  sqrt2irrap  12183  qmuldeneqnum  12198  numdensq  12205  qden1elz  12208  hashdvds  12224  phiprm  12226  eulerthlema  12233  eulerthlemh  12234  eulerthlemth  12235  fermltl  12237  prmdiv  12238  prmdiveq  12239  hashgcdlem  12241  odzdvds  12248  modprm0  12257  modprmn0modprm0  12259  pythagtriplem6  12273  pythagtriplem7  12274  pythagtriplem15  12281  pcpremul  12296  pceulem  12297  pceu  12298  pczpre  12300  pcdiv  12305  pcqmul  12306  pcqdiv  12310  pcexp  12312  pcaddlem  12341  pcadd  12342  fldivp1  12349  pcfac  12351  pcbc  12352  prmpwdvds  12356  4sqlem5  12383  4sqlem8  12386  4sqlem9  12387  4sqlem10  12388  znnen  12402  mulgsubcl  13003  mulgdirlem  13020  mulgdir  13021  mulgass  13026  mulgmodid  13028  mulgsubdir  13029  zringmulg  13628  relogbexpap  14516  logbgcd1irraplemap  14527  lgslem1  14541  lgsval2lem  14551  lgsval4a  14563  lgsneg  14565  lgsneg1  14566  lgsmod  14567  lgsdirprm  14575  lgsdir  14576  lgsdilem2  14577  lgsdi  14578  lgsne0  14579  lgsabs1  14580  lgssq  14581  lgssq2  14582  lgsmulsqcoprm  14587  lgsdirnn0  14588  lgsdinn0  14589  lgseisenlem1  14590  lgseisenlem2  14591  2lgsoddprmlem2  14594  2sqlem3  14604  2sqlem4  14605  2sqlem8a  14609  2sqlem8  14610  iswomni0  14940