Theorem zcnd 9440

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

Syntax hints:   -> wi 4   e. wcel 2164   CCcc 7870   ZZcz 9317

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-rab 2481  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318

This theorem is referenced by:  qapne  9704  fzm1  10166  fzrevral  10171  fzshftral  10174  nn0disj  10204  fzoss2  10239  fzosubel  10261  fzosubel3  10263  fzocatel  10266  fzosplitsnm1  10276  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemex  10318  rebtwn2zlemstep  10321  rebtwn2z  10323  flqaddz  10366  flqzadd  10367  2tnp1ge0ge0  10370  ceiqm1l  10382  intqfrac2  10390  intfracq  10391  flqdiv  10392  modqvalr  10396  flqpmodeq  10398  modq0  10400  mulqmod0  10401  modqlt  10404  modqdiffl  10406  modqfrac  10408  flqmod  10409  intqfrac  10410  modqmulnn  10413  modqvalp1  10414  modqcyc  10430  modqcyc2  10431  modqadd1  10432  mulqaddmodid  10435  mulp1mod1  10436  modqmul1  10448  modqmul12d  10449  modqnegd  10450  modqmulmodr  10461  modqdi  10463  modqsubdir  10464  modfzo0difsn  10466  modsumfzodifsn  10467  addmodlteq  10469  frecfzen2  10498  uzennn  10507  uzsinds  10515  seq3shft2  10552  monoord2  10557  iseqf1olemab  10573  seq3f1olemqsumkj  10582  seq3f1olemqsum  10584  seqf1oglem1  10590  seqf1oglem2  10591  expaddzaplem  10653  modqexp  10737  sqoddm1div8  10764  bcm1k  10831  bcp1nk  10833  bcpasc  10837  hashfz  10892  hashfzo  10893  hashfzp1  10895  seq3coll  10913  seq3shft  10982  fzomaxdif  11257  climshft2  11449  iserex  11482  iser3shft  11489  serf0  11495  fsumm1  11559  fsumsplitsnun  11562  fsump1  11563  fsumshftm  11588  fisumrev2  11589  telfsumo  11609  fsumparts  11613  binomlem  11626  isumshft  11633  isumsplit  11634  isum1p  11635  divcnv  11640  arisum  11641  trireciplem  11643  cvgratnnlemmn  11668  cvgratnnlemsumlt  11671  mertenslemi1  11678  ntrivcvgap  11691  fprodm1  11741  fprodp1  11743  fprodfac  11758  fprodrev  11762  fprodmodd  11784  eirraplem  11920  moddvds  11942  dvdscmulr  11963  dvdsmulcr  11964  dvds2ln  11967  dvdsadd2b  11983  dvdsaddre2b  11984  fzocongeq  12000  addmodlteqALT  12001  dvdsexp  12003  dvdsmod  12004  mulmoddvds  12005  odd2np1  12014  oddm1even  12016  oexpneg  12018  mulsucdiv2z  12026  zob  12032  ltoddhalfle  12034  divalglemnn  12059  divalglemqt  12060  divalglemex  12063  divalglemeuneg  12064  divalgb  12066  divalgmod  12068  modremain  12070  flodddiv4  12075  infssuzex  12086  zsupssdc  12091  dvdsbnd  12093  gcdaddm  12121  modgcd  12128  gcdmultipled  12130  dvdsgcdidd  12131  bezoutlemnewy  12133  bezoutlemaz  12140  bezoutlembz  12141  dvdsmulgcd  12162  rplpwr  12164  uzwodc  12174  lcmval  12201  lcmcllem  12205  lcmid  12218  mulgcddvds  12232  divgcdcoprm0  12239  cncongr1  12241  cncongr2  12242  rpexp  12291  sqrt2irrlem  12299  sqrt2irrap  12318  qmuldeneqnum  12333  numdensq  12340  qden1elz  12343  hashdvds  12359  phiprm  12361  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  fermltl  12372  prmdiv  12373  prmdiveq  12374  hashgcdlem  12376  odzdvds  12383  modprm0  12392  modprmn0modprm0  12394  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem15  12416  pcpremul  12431  pceulem  12432  pceu  12433  pczpre  12435  pcdiv  12440  pcqmul  12441  pcqdiv  12445  pcexp  12447  pcaddlem  12477  pcadd  12478  fldivp1  12486  pcfac  12488  pcbc  12489  prmpwdvds  12493  4sqlem5  12520  4sqlem8  12523  4sqlem9  12524  4sqlem10  12525  4sqlemffi  12534  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  4sqlem14  12542  4sqlem16  12544  4sqlem17  12545  znnen  12555  mulgsubcl  13206  mulgdirlem  13223  mulgdir  13224  mulgass  13229  mulgmodid  13231  mulgsubdir  13232  gsumfzconst  13411  gsumfzsnfd  13415  zringmulg  14086  zndvds0  14138  znf1o  14139  znunit  14147  relogbexpap  15090  logbgcd1irraplemap  15101  wilthlem1  15112  lgslem1  15116  lgsval2lem  15126  lgsval4a  15138  lgsneg  15140  lgsneg1  15141  lgsmod  15142  lgsdirprm  15150  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsabs1  15155  lgssq  15156  lgssq2  15157  lgsmulsqcoprm  15162  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem1  15177  gausslemma2dlem4  15180  gausslemma2dlem5a  15181  gausslemma2dlem5  15182  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  2lgsoddprmlem2  15194  2sqlem3  15204  2sqlem4  15205  2sqlem8a  15209  2sqlem8  15210  iswomni0  15541