Theorem zcnd 9449

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 9448	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8055	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7877  ℤcz 9326

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 7971

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 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-neg 8200  df-z 9327

This theorem is referenced by:  qapne  9713  fzm1  10175  fzrevral  10180  fzshftral  10183  nn0disj  10213  fzoss2  10248  fzosubel  10270  fzosubel3  10272  fzocatel  10275  fzosplitsnm1  10285  infssuzex  10323  zsupssdc  10328  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemex  10339  rebtwn2zlemstep  10342  rebtwn2z  10344  flqaddz  10387  flqzadd  10388  2tnp1ge0ge0  10391  ceiqm1l  10403  intqfrac2  10411  intfracq  10412  flqdiv  10413  modqvalr  10417  flqpmodeq  10419  modq0  10421  mulqmod0  10422  modqlt  10425  modqdiffl  10427  modqfrac  10429  flqmod  10430  intqfrac  10431  modqmulnn  10434  modqvalp1  10435  modqcyc  10451  modqcyc2  10452  modqadd1  10453  mulqaddmodid  10456  mulp1mod1  10457  modqmul1  10469  modqmul12d  10470  modqnegd  10471  modqmulmodr  10482  modqdi  10484  modqsubdir  10485  modfzo0difsn  10487  modsumfzodifsn  10488  addmodlteq  10490  frecfzen2  10519  uzennn  10528  uzsinds  10536  seq3shft2  10573  monoord2  10578  iseqf1olemab  10594  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seqf1oglem1  10611  seqf1oglem2  10612  expaddzaplem  10674  modqexp  10758  sqoddm1div8  10785  bcm1k  10852  bcp1nk  10854  bcpasc  10858  hashfz  10913  hashfzo  10914  hashfzp1  10916  seq3coll  10934  seq3shft  11003  fzomaxdif  11278  climshft2  11471  iserex  11504  iser3shft  11511  serf0  11517  fsumm1  11581  fsumsplitsnun  11584  fsump1  11585  fsumshftm  11610  fisumrev2  11611  telfsumo  11631  fsumparts  11635  binomlem  11648  isumshft  11655  isumsplit  11656  isum1p  11657  divcnv  11662  arisum  11663  trireciplem  11665  cvgratnnlemmn  11690  cvgratnnlemsumlt  11693  mertenslemi1  11700  ntrivcvgap  11713  fprodm1  11763  fprodp1  11765  fprodfac  11780  fprodrev  11784  fprodmodd  11806  eirraplem  11942  moddvds  11964  dvdscmulr  11985  dvdsmulcr  11986  dvds2ln  11989  dvdsadd2b  12005  dvdsaddre2b  12006  fsumdvds  12007  fzocongeq  12023  addmodlteqALT  12024  dvdsexp  12026  dvdsmod  12027  mulmoddvds  12028  3dvds  12029  odd2np1  12038  oddm1even  12040  oexpneg  12042  mulsucdiv2z  12050  zob  12056  ltoddhalfle  12058  divalglemnn  12083  divalglemqt  12084  divalglemex  12087  divalglemeuneg  12088  divalgb  12090  divalgmod  12092  modremain  12094  flodddiv4  12101  bitsp1  12115  bitsfzo  12119  dvdsbnd  12123  gcdaddm  12151  modgcd  12158  gcdmultipled  12160  dvdsgcdidd  12161  bezoutlemnewy  12163  bezoutlemaz  12170  bezoutlembz  12171  dvdsmulgcd  12192  rplpwr  12194  uzwodc  12204  lcmval  12231  lcmcllem  12235  lcmid  12248  mulgcddvds  12262  divgcdcoprm0  12269  cncongr1  12271  cncongr2  12272  rpexp  12321  sqrt2irrlem  12329  sqrt2irrap  12348  qmuldeneqnum  12363  numdensq  12370  qden1elz  12373  hashdvds  12389  phiprm  12391  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  fermltl  12402  prmdiv  12403  prmdiveq  12404  hashgcdlem  12406  odzdvds  12414  modprm0  12423  modprmn0modprm0  12425  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem15  12447  pcpremul  12462  pceulem  12463  pceu  12464  pczpre  12466  pcdiv  12471  pcqmul  12472  pcqdiv  12476  pcexp  12478  pcaddlem  12508  pcadd  12509  fldivp1  12517  pcfac  12519  pcbc  12520  prmpwdvds  12524  4sqlem5  12551  4sqlem8  12554  4sqlem9  12555  4sqlem10  12556  4sqlemffi  12565  4sqexercise2  12568  4sqlemsdc  12569  4sqlem11  12570  4sqlem14  12573  4sqlem16  12575  4sqlem17  12576  znnen  12615  mulgsubcl  13266  mulgdirlem  13283  mulgdir  13284  mulgass  13289  mulgmodid  13291  mulgsubdir  13292  gsumfzconst  13471  gsumfzsnfd  13475  zringmulg  14154  zndvds0  14206  znf1o  14207  znunit  14215  relogbexpap  15194  logbgcd1irraplemap  15205  wilthlem1  15216  lgslem1  15241  lgsval2lem  15251  lgsval4a  15263  lgsneg  15265  lgsneg1  15266  lgsmod  15267  lgsdirprm  15275  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsabs1  15280  lgssq  15281  lgssq2  15282  lgsmulsqcoprm  15287  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem1  15302  gausslemma2dlem4  15305  gausslemma2dlem5a  15306  gausslemma2dlem5  15307  gausslemma2dlem6  15308  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquad2lem1  15322  lgsquad3  15325  2lgslem1b  15330  2lgsoddprmlem2  15347  2sqlem3  15358  2sqlem4  15359  2sqlem8a  15363  2sqlem8  15364  iswomni0  15695