Theorem zcnd 9451

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7879   ZZcz 9328

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7973

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5926  df-neg 8202  df-z 9329

This theorem is referenced by:  qapne  9715  fzm1  10177  fzrevral  10182  fzshftral  10185  nn0disj  10215  fzoss2  10250  fzosubel  10272  fzosubel3  10274  fzocatel  10277  fzosplitsnm1  10287  infssuzex  10325  zsupssdc  10330  qtri3or  10332  exbtwnzlemstep  10339  exbtwnzlemex  10341  rebtwn2zlemstep  10344  rebtwn2z  10346  flqaddz  10389  flqzadd  10390  2tnp1ge0ge0  10393  ceiqm1l  10405  intqfrac2  10413  intfracq  10414  flqdiv  10415  modqvalr  10419  flqpmodeq  10421  modq0  10423  mulqmod0  10424  modqlt  10427  modqdiffl  10429  modqfrac  10431  flqmod  10432  intqfrac  10433  modqmulnn  10436  modqvalp1  10437  modqcyc  10453  modqcyc2  10454  modqadd1  10455  mulqaddmodid  10458  mulp1mod1  10459  modqmul1  10471  modqmul12d  10472  modqnegd  10473  modqmulmodr  10484  modqdi  10486  modqsubdir  10487  modfzo0difsn  10489  modsumfzodifsn  10490  addmodlteq  10492  frecfzen2  10521  uzennn  10530  uzsinds  10538  seq3shft2  10575  monoord2  10580  iseqf1olemab  10596  seq3f1olemqsumkj  10605  seq3f1olemqsum  10607  seqf1oglem1  10613  seqf1oglem2  10614  expaddzaplem  10676  modqexp  10760  sqoddm1div8  10787  bcm1k  10854  bcp1nk  10856  bcpasc  10860  hashfz  10915  hashfzo  10916  hashfzp1  10918  seq3coll  10936  seq3shft  11005  fzomaxdif  11280  climshft2  11473  iserex  11506  iser3shft  11513  serf0  11519  fsumm1  11583  fsumsplitsnun  11586  fsump1  11587  fsumshftm  11612  fisumrev2  11613  telfsumo  11633  fsumparts  11637  binomlem  11650  isumshft  11657  isumsplit  11658  isum1p  11659  divcnv  11664  arisum  11665  trireciplem  11667  cvgratnnlemmn  11692  cvgratnnlemsumlt  11695  mertenslemi1  11702  ntrivcvgap  11715  fprodm1  11765  fprodp1  11767  fprodfac  11782  fprodrev  11786  fprodmodd  11808  eirraplem  11944  moddvds  11966  dvdscmulr  11987  dvdsmulcr  11988  dvds2ln  11991  dvdsadd2b  12007  dvdsaddre2b  12008  fsumdvds  12009  fzocongeq  12025  addmodlteqALT  12026  dvdsexp  12028  dvdsmod  12029  mulmoddvds  12030  3dvds  12031  odd2np1  12040  oddm1even  12042  oexpneg  12044  mulsucdiv2z  12052  zob  12058  ltoddhalfle  12060  divalglemnn  12085  divalglemqt  12086  divalglemex  12089  divalglemeuneg  12090  divalgb  12092  divalgmod  12094  modremain  12096  flodddiv4  12103  bitsp1  12118  bitsfzo  12122  bitsmod  12123  bitsinv1lem  12128  dvdsbnd  12133  gcdaddm  12161  modgcd  12168  gcdmultipled  12170  dvdsgcdidd  12171  bezoutlemnewy  12173  bezoutlemaz  12180  bezoutlembz  12181  dvdsmulgcd  12202  rplpwr  12204  uzwodc  12214  lcmval  12241  lcmcllem  12245  lcmid  12258  mulgcddvds  12272  divgcdcoprm0  12279  cncongr1  12281  cncongr2  12282  rpexp  12331  sqrt2irrlem  12339  sqrt2irrap  12358  qmuldeneqnum  12373  numdensq  12380  qden1elz  12383  hashdvds  12399  phiprm  12401  eulerthlema  12408  eulerthlemh  12409  eulerthlemth  12410  fermltl  12412  prmdiv  12413  prmdiveq  12414  hashgcdlem  12416  odzdvds  12424  modprm0  12433  modprmn0modprm0  12435  pythagtriplem6  12449  pythagtriplem7  12450  pythagtriplem15  12457  pcpremul  12472  pceulem  12473  pceu  12474  pczpre  12476  pcdiv  12481  pcqmul  12482  pcqdiv  12486  pcexp  12488  pcaddlem  12518  pcadd  12519  fldivp1  12527  pcfac  12529  pcbc  12530  prmpwdvds  12534  4sqlem5  12561  4sqlem8  12564  4sqlem9  12565  4sqlem10  12566  4sqlemffi  12575  4sqexercise2  12578  4sqlemsdc  12579  4sqlem11  12580  4sqlem14  12583  4sqlem16  12585  4sqlem17  12586  znnen  12625  mulgsubcl  13276  mulgdirlem  13293  mulgdir  13294  mulgass  13299  mulgmodid  13301  mulgsubdir  13302  gsumfzconst  13481  gsumfzsnfd  13485  zringmulg  14164  zndvds0  14216  znf1o  14217  znunit  14225  relogbexpap  15204  logbgcd1irraplemap  15215  wilthlem1  15226  lgslem1  15251  lgsval2lem  15261  lgsval4a  15273  lgsneg  15275  lgsneg1  15276  lgsmod  15277  lgsdirprm  15285  lgsdir  15286  lgsdilem2  15287  lgsdi  15288  lgsne0  15289  lgsabs1  15290  lgssq  15291  lgssq2  15292  lgsmulsqcoprm  15297  lgsdirnn0  15298  lgsdinn0  15299  gausslemma2dlem1a  15309  gausslemma2dlem1f1o  15311  gausslemma2dlem1  15312  gausslemma2dlem4  15315  gausslemma2dlem5a  15316  gausslemma2dlem5  15317  gausslemma2dlem6  15318  gausslemma2d  15320  lgseisenlem1  15321  lgseisenlem2  15322  lgseisenlem3  15323  lgseisenlem4  15324  lgsquadlem1  15328  lgsquad2lem1  15332  lgsquad3  15335  2lgslem1b  15340  2lgsoddprmlem2  15357  2sqlem3  15368  2sqlem4  15369  2sqlem8a  15373  2sqlem8  15374  iswomni0  15705