Theorem zcnd 9376

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7809  ℤcz 9253

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-neg 8131  df-z 9254

This theorem is referenced by:  qapne  9639  fzm1  10100  fzrevral  10105  fzshftral  10108  nn0disj  10138  fzoss2  10172  fzosubel  10194  fzosubel3  10196  fzocatel  10199  fzosplitsnm1  10209  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemex  10250  rebtwn2zlemstep  10253  rebtwn2z  10255  flqaddz  10297  flqzadd  10298  2tnp1ge0ge0  10301  ceiqm1l  10311  intqfrac2  10319  intfracq  10320  flqdiv  10321  modqvalr  10325  flqpmodeq  10327  modq0  10329  mulqmod0  10330  modqlt  10333  modqdiffl  10335  modqfrac  10337  flqmod  10338  intqfrac  10339  modqmulnn  10342  modqvalp1  10343  modqcyc  10359  modqcyc2  10360  modqadd1  10361  mulqaddmodid  10364  mulp1mod1  10365  modqmul1  10377  modqmul12d  10378  modqnegd  10379  modqmulmodr  10390  modqdi  10392  modqsubdir  10393  modfzo0difsn  10395  modsumfzodifsn  10396  addmodlteq  10398  frecfzen2  10427  uzennn  10436  uzsinds  10442  seq3shft2  10473  monoord2  10477  iseqf1olemab  10489  seq3f1olemqsumkj  10498  seq3f1olemqsum  10500  expaddzaplem  10563  modqexp  10647  sqoddm1div8  10674  bcm1k  10740  bcp1nk  10742  bcpasc  10746  hashfz  10801  hashfzo  10802  hashfzp1  10804  seq3coll  10822  seq3shft  10847  fzomaxdif  11122  climshft2  11314  iserex  11347  iser3shft  11354  serf0  11360  fsumm1  11424  fsumsplitsnun  11427  fsump1  11428  fsumshftm  11453  fisumrev2  11454  telfsumo  11474  fsumparts  11478  binomlem  11491  isumshft  11498  isumsplit  11499  isum1p  11500  divcnv  11505  arisum  11506  trireciplem  11508  cvgratnnlemmn  11533  cvgratnnlemsumlt  11536  mertenslemi1  11543  ntrivcvgap  11556  fprodm1  11606  fprodp1  11608  fprodfac  11623  fprodrev  11627  fprodmodd  11649  eirraplem  11784  moddvds  11806  dvdscmulr  11827  dvdsmulcr  11828  dvds2ln  11831  dvdsadd2b  11847  dvdsaddre2b  11848  fzocongeq  11864  addmodlteqALT  11865  dvdsexp  11867  dvdsmod  11868  mulmoddvds  11869  odd2np1  11878  oddm1even  11880  oexpneg  11882  mulsucdiv2z  11890  zob  11896  ltoddhalfle  11898  divalglemnn  11923  divalglemqt  11924  divalglemex  11927  divalglemeuneg  11928  divalgb  11930  divalgmod  11932  modremain  11934  flodddiv4  11939  infssuzex  11950  zsupssdc  11955  dvdsbnd  11957  gcdaddm  11985  modgcd  11992  gcdmultipled  11994  dvdsgcdidd  11995  bezoutlemnewy  11997  bezoutlemaz  12004  bezoutlembz  12005  dvdsmulgcd  12026  rplpwr  12028  uzwodc  12038  lcmval  12063  lcmcllem  12067  lcmid  12080  mulgcddvds  12094  divgcdcoprm0  12101  cncongr1  12103  cncongr2  12104  rpexp  12153  sqrt2irrlem  12161  sqrt2irrap  12180  qmuldeneqnum  12195  numdensq  12202  qden1elz  12205  hashdvds  12221  phiprm  12223  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  fermltl  12234  prmdiv  12235  prmdiveq  12236  hashgcdlem  12238  odzdvds  12245  modprm0  12254  modprmn0modprm0  12256  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem15  12278  pcpremul  12293  pceulem  12294  pceu  12295  pczpre  12297  pcdiv  12302  pcqmul  12303  pcqdiv  12307  pcexp  12309  pcaddlem  12338  pcadd  12339  fldivp1  12346  pcfac  12348  pcbc  12349  prmpwdvds  12353  4sqlem5  12380  4sqlem8  12383  4sqlem9  12384  4sqlem10  12385  znnen  12399  mulgsubcl  12997  mulgdirlem  13014  mulgdir  13015  mulgass  13020  mulgmodid  13022  mulgsubdir  13023  zringmulg  13491  relogbexpap  14379  logbgcd1irraplemap  14390  lgslem1  14404  lgsval2lem  14414  lgsval4a  14426  lgsneg  14428  lgsneg1  14429  lgsmod  14430  lgsdirprm  14438  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgsabs1  14443  lgssq  14444  lgssq2  14445  lgsmulsqcoprm  14450  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem1  14453  lgseisenlem2  14454  2lgsoddprmlem2  14457  2sqlem3  14467  2sqlem4  14468  2sqlem8a  14472  2sqlem8  14473  iswomni0  14802