Theorem zcnd 8968

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

Syntax hints:   -> wi 4   e. wcel 1445   CCcc 7445   ZZcz 8848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-resscn 7534

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-rab 2379  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693  df-neg 7753  df-z 8849

This theorem is referenced by:  qapne  9223  fzm1  9663  fzrevral  9668  fzshftral  9671  nn0disj  9698  fzoss2  9732  fzosubel  9754  fzosubel3  9756  fzocatel  9759  fzosplitsnm1  9769  qtri3or  9803  exbtwnzlemstep  9808  exbtwnzlemex  9810  rebtwn2zlemstep  9813  rebtwn2z  9815  flqaddz  9853  flqzadd  9854  2tnp1ge0ge0  9857  ceiqm1l  9867  intqfrac2  9875  intfracq  9876  flqdiv  9877  modqvalr  9881  flqpmodeq  9883  modq0  9885  mulqmod0  9886  modqlt  9889  modqdiffl  9891  modqfrac  9893  flqmod  9894  intqfrac  9895  modqmulnn  9898  modqvalp1  9899  modqcyc  9915  modqcyc2  9916  modqadd1  9917  mulqaddmodid  9920  mulp1mod1  9921  modqmul1  9933  modqmul12d  9934  modqnegd  9935  modqmulmodr  9946  modqdi  9948  modqsubdir  9949  modfzo0difsn  9951  modsumfzodifsn  9952  addmodlteq  9954  frecfzen2  9983  uzsinds  9997  seq3shft2  10023  monoord2  10027  iseqf1olemab  10039  seq3f1olemqsumkj  10048  seq3f1olemqsum  10050  expaddzaplem  10113  sqoddm1div8  10221  bcm1k  10283  bcp1nk  10285  bcpasc  10289  hashfz  10344  hashfzo  10345  hashfzp1  10347  seq3coll  10362  seq3shft  10387  fzomaxdif  10661  climshft2  10849  iserex  10882  iser3shft  10889  serf0  10895  fsumm1  10959  fsumsplitsnun  10962  fsump1  10963  fsumshftm  10988  fisumrev2  10989  telfsumo  11009  fsumparts  11013  binomlem  11026  isumshft  11033  isumsplit  11034  isum1p  11035  divcnv  11040  arisum  11041  trireciplem  11043  cvgratnnlemmn  11068  cvgratnnlemsumlt  11071  mertenslemi1  11078  eirraplem  11213  moddvds  11232  dvdscmulr  11252  dvdsmulcr  11253  dvds2ln  11256  dvdsadd2b  11270  fzocongeq  11286  addmodlteqALT  11287  dvdsexp  11289  dvdsmod  11290  mulmoddvds  11291  odd2np1  11300  oddm1even  11302  oexpneg  11304  mulsucdiv2z  11312  zob  11318  ltoddhalfle  11320  divalglemnn  11345  divalglemqt  11346  divalglemex  11349  divalglemeuneg  11350  divalgb  11352  divalgmod  11354  modremain  11356  flodddiv4  11361  infssuzex  11372  dvdsbnd  11375  gcdaddm  11402  modgcd  11409  bezoutlemnewy  11412  bezoutlemaz  11419  bezoutlembz  11420  dvdsmulgcd  11441  rplpwr  11443  lcmval  11472  lcmcllem  11476  lcmid  11489  mulgcddvds  11503  divgcdcoprm0  11510  cncongr1  11512  cncongr2  11513  rpexp  11559  sqrt2irrlem  11567  sqrt2irrap  11585  qmuldeneqnum  11600  numdensq  11607  qden1elz  11610  hashdvds  11624  phiprm  11626  hashgcdlem  11630  znnen  11638