Theorem zcnd 9335

Description: An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zcnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem zcnd

Step	Hyp	Ref	Expression
1		zred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2	1	zred 9334	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 7948	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  ℤcz 9212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7866

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856  df-neg 8093  df-z 9213

This theorem is referenced by:  qapne  9598  fzm1  10056  fzrevral  10061  fzshftral  10064  nn0disj  10094  fzoss2  10128  fzosubel  10150  fzosubel3  10152  fzocatel  10155  fzosplitsnm1  10165  qtri3or  10199  exbtwnzlemstep  10204  exbtwnzlemex  10206  rebtwn2zlemstep  10209  rebtwn2z  10211  flqaddz  10253  flqzadd  10254  2tnp1ge0ge0  10257  ceiqm1l  10267  intqfrac2  10275  intfracq  10276  flqdiv  10277  modqvalr  10281  flqpmodeq  10283  modq0  10285  mulqmod0  10286  modqlt  10289  modqdiffl  10291  modqfrac  10293  flqmod  10294  intqfrac  10295  modqmulnn  10298  modqvalp1  10299  modqcyc  10315  modqcyc2  10316  modqadd1  10317  mulqaddmodid  10320  mulp1mod1  10321  modqmul1  10333  modqmul12d  10334  modqnegd  10335  modqmulmodr  10346  modqdi  10348  modqsubdir  10349  modfzo0difsn  10351  modsumfzodifsn  10352  addmodlteq  10354  frecfzen2  10383  uzennn  10392  uzsinds  10398  seq3shft2  10429  monoord2  10433  iseqf1olemab  10445  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  expaddzaplem  10519  modqexp  10602  sqoddm1div8  10629  bcm1k  10694  bcp1nk  10696  bcpasc  10700  hashfz  10756  hashfzo  10757  hashfzp1  10759  seq3coll  10777  seq3shft  10802  fzomaxdif  11077  climshft2  11269  iserex  11302  iser3shft  11309  serf0  11315  fsumm1  11379  fsumsplitsnun  11382  fsump1  11383  fsumshftm  11408  fisumrev2  11409  telfsumo  11429  fsumparts  11433  binomlem  11446  isumshft  11453  isumsplit  11454  isum1p  11455  divcnv  11460  arisum  11461  trireciplem  11463  cvgratnnlemmn  11488  cvgratnnlemsumlt  11491  mertenslemi1  11498  ntrivcvgap  11511  fprodm1  11561  fprodp1  11563  fprodfac  11578  fprodrev  11582  fprodmodd  11604  eirraplem  11739  moddvds  11761  dvdscmulr  11782  dvdsmulcr  11783  dvds2ln  11786  dvdsadd2b  11802  fzocongeq  11818  addmodlteqALT  11819  dvdsexp  11821  dvdsmod  11822  mulmoddvds  11823  odd2np1  11832  oddm1even  11834  oexpneg  11836  mulsucdiv2z  11844  zob  11850  ltoddhalfle  11852  divalglemnn  11877  divalglemqt  11878  divalglemex  11881  divalglemeuneg  11882  divalgb  11884  divalgmod  11886  modremain  11888  flodddiv4  11893  infssuzex  11904  zsupssdc  11909  dvdsbnd  11911  gcdaddm  11939  modgcd  11946  gcdmultipled  11948  dvdsgcdidd  11949  bezoutlemnewy  11951  bezoutlemaz  11958  bezoutlembz  11959  dvdsmulgcd  11980  rplpwr  11982  uzwodc  11992  lcmval  12017  lcmcllem  12021  lcmid  12034  mulgcddvds  12048  divgcdcoprm0  12055  cncongr1  12057  cncongr2  12058  rpexp  12107  sqrt2irrlem  12115  sqrt2irrap  12134  qmuldeneqnum  12149  numdensq  12156  qden1elz  12159  hashdvds  12175  phiprm  12177  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  fermltl  12188  prmdiv  12189  prmdiveq  12190  hashgcdlem  12192  odzdvds  12199  modprm0  12208  modprmn0modprm0  12210  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem15  12232  pcpremul  12247  pceulem  12248  pceu  12249  pczpre  12251  pcdiv  12256  pcqmul  12257  pcqdiv  12261  pcexp  12263  pcaddlem  12292  pcadd  12293  fldivp1  12300  pcfac  12302  pcbc  12303  prmpwdvds  12307  4sqlem5  12334  4sqlem8  12337  4sqlem9  12338  4sqlem10  12339  znnen  12353  relogbexpap  13670  logbgcd1irraplemap  13681  lgslem1  13695  lgsval2lem  13705  lgsval4a  13717  lgsneg  13719  lgsneg1  13720  lgsmod  13721  lgsdirprm  13729  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsabs1  13734  lgssq  13735  lgssq2  13736  lgsmulsqcoprm  13741  lgsdirnn0  13742  lgsdinn0  13743  2sqlem3  13747  2sqlem4  13748  2sqlem8a  13752  2sqlem8  13753  iswomni0  14083