MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zcnd Structured version   Unicode version

Theorem zcnd 10849
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
StepHypRef Expression
1 zred.1 . . 3  |-  ( ph  ->  A  e.  ZZ )
21zred 10848 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9513 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   CCcc 9381   ZZcz 10747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-resscn 9440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-neg 9699  df-z 10748
This theorem is referenced by:  uzp1  10995  peano2uzr  11011  uzaddcl  11012  zsupss  11045  rpnnen1lem5  11084  fzm1  11641  fzrevral  11645  fzshftral  11648  fzoss2  11678  fzosubel  11700  fzosubel3  11702  fzocatel  11703  fzosplitsnm1  11709  quoremz  11795  intfrac2  11798  intfracq  11799  flpmodeq  11814  moddiffl  11820  modmul1  11853  modmul12d  11854  uzrdgxfr  11890  fzen2  11892  seqm1  11924  monoord2  11938  seqf1olem1  11946  seqf1olem2  11947  seqz  11955  expaddzlem  12008  modexp  12100  bcm1k  12192  bcp1nk  12194  bcval5  12195  bcpasc  12198  hashfz  12290  hashfzo  12292  hashbclem  12307  seqcoll  12318  ccatval3  12380  ccatlid  12386  ccatass  12388  swrd0val  12419  swrdid  12423  swrd0fv  12437  swrdspsleq  12444  swrds1  12447  ccatswrd  12452  swrdswrd0  12458  spllen  12498  splfv1  12499  splfv2a  12500  revccat  12508  revrev  12509  cshwidxmod  12542  cshwidxm1  12545  shftuz  12660  seqshft  12676  fzomaxdif  12933  climshftlem  13154  climshft  13156  climshft2  13162  iserex  13236  isercoll2  13248  serf0  13260  iseraltlem2  13262  iseraltlem3  13263  iseralt  13264  sumrblem  13290  fsumm1  13322  fsump1  13325  fsumshftm  13350  fsumrev2  13351  fsumtscopo  13367  fsumparts  13371  binomlem  13394  isumshft  13404  isumsplit  13405  isum1p  13406  arisum  13424  cvgrat  13445  mertenslem1  13446  eirrlem  13588  sqr2irrlem  13632  dvds2ln  13665  dvdsadd2b  13677  fsumdvds  13678  fzocongeq  13689  dvdsexp  13691  dvdsmod  13692  oddm1even  13695  oexpneg  13697  3dvds  13698  divalglem0  13699  divalglem4  13702  divalglem8  13706  divalgb  13710  divalgmod  13712  bitsp1  13729  bitsfzo  13733  bitsmod  13734  bitsinv1lem  13739  bitsf1  13744  sadaddlem  13764  bitsres  13771  bitsuz  13772  bitsshft  13773  smumullem  13790  modgcd  13822  bezoutlem1  13824  bezoutlem2  13825  bezoutlem3  13826  bezoutlem4  13827  dvdsmulgcd  13840  rplpwr  13842  mulgcddvds  13892  rpexp  13908  qmuldeneqnum  13927  numdensq  13934  qden1elz  13937  hashdvds  13952  phiprm  13954  eulerthlem2  13959  fermltl  13961  prmdiv  13962  prmdiveq  13963  odzdvds  13969  modprm0  13975  modprmn0modprm0  13977  pythagtriplem6  13990  pythagtriplem7  13991  pythagtriplem15  13998  pclem  14007  pcpremul  14012  pceulem  14014  pczpre  14016  pcdiv  14021  pcqmul  14022  pcqdiv  14026  pcexp  14028  pcaddlem  14052  pcadd  14053  fldivp1  14061  pcfac  14063  pcbc  14064  prmpwdvds  14067  prmreclem4  14082  4sqlem5  14105  4sqlem8  14108  4sqlem9  14109  4sqlem10  14110  4sqlem11  14118  4sqlem14  14121  4sqlem16  14123  4sqlem17  14124  vdwapun  14137  vdwnnlem2  14159  prmlem0  14235  mulgsubcl  15743  mulgdirlem  15753  mulgdir  15754  mulgass  15759  mulgsubdir  15760  psgnunilem5  16102  psgnunilem2  16103  psgnunilem4  16105  m1expaddsub  16106  psgnuni  16107  odnncl  16152  odmulg  16161  odbezout  16163  sylow1lem1  16201  sylow2alem2  16221  efgtlen  16327  efgsres  16339  efgredleme  16344  efgredlemc  16346  odadd1  16434  odadd2  16435  cyggeninv  16464  gsummptshft  16534  ablfacrp  16672  pgpfac1lem3  16683  srgbinomlem3  16746  srgbinomlem4  16747  zringmulg  18000  zrngmulg  18006  zringlpirlem1  18012  zringlpirlem3  18014  zlpirlem1  18017  zlpirlem3  18019  prmirredlem  18026  prmirredlemOLD  18029  zndvds0  18092  znf1o  18093  znunit  18105  tgpmulg  19780  zdis  20509  uniioombllem3  21181  mbfi1fseqlem4  21312  dvexp3  21566  aareccl  21908  aalioulem1  21914  geolim3  21921  aaliou3lem2  21925  aaliou3lem6  21930  ulmshft  21971  dvradcnv  22002  sineq0  22099  efif1olem2  22115  wilthlem1  22522  wilthlem2  22523  basellem3  22536  mumul  22635  musum  22647  musumsum  22648  muinv  22649  ppiub  22659  chtub  22667  logfac2  22672  chpchtsum  22674  dchrptlem1  22719  pcbcctr  22731  bcmono  22732  bposlem5  22743  bposlem6  22744  lgslem1  22751  lgsval2lem  22761  lgsval4a  22773  lgsneg  22774  lgsneg1  22775  lgsmod  22776  lgsdirprm  22784  lgsdir  22785  lgsdilem2  22786  lgsdi  22787  lgsne0  22788  lgsabs1  22789  lgssq  22790  lgssq2  22791  lgsdirnn0  22794  lgsdinn0  22795  lgsqrlem1  22796  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgseisenlem4  22807  lgsquadlem1  22809  lgsquad2lem1  22813  lgsquad3  22816  2sqlem3  22821  2sqlem4  22822  2sqlem8a  22826  2sqlem8  22827  2sqlem11  22830  2sqblem  22832  dchrisumlem1  22854  dchrmusum2  22859  dchrvmasumlem1  22860  dchrvmasum2lem  22861  mudivsum  22895  mulogsum  22897  mulog2sumlem2  22900  selberglem1  22910  selberglem3  22912  selberg  22913  pntpbnd2  22952  pntlemf  22970  padicabvcxp  22997  axlowdimlem14  23336  axlowdimlem16  23338  wlkdvspthlem  23641  fargshiftf1  23658  fargshiftfo  23659  eupatrl  23724  gxmodid  23901  fzspl  26211  bcm1n  26213  numdenneg  26220  divnumden2  26221  ltesubnnd  26225  archiabllem1  26344  archiabllem2c  26346  zrhnm  26532  qqhval2lem  26544  qqhghm  26551  qqhrhm  26552  qqhnm  26553  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemic  27023  ballotlem1c  27024  ballotlemsgt1  27027  ballotlemsdom  27028  ballotlemsel1i  27029  ballotlemsf1o  27030  ballotlemsima  27032  ballotlemfrceq  27045  ballotlemfrcn0  27046  ballotlem1ri  27051  signsplypnf  27085  igamz  27168  divcnvlin  27533  ntrivcvg  27546  ntrivcvgtail  27549  prodrblem  27576  fprodser  27596  fprodm1  27611  fprodp1  27613  fprodshft  27621  fprodrev  27622  fallfacval3  27649  fallfacfwd  27673  0fallfac  27674  binomfallfaclem2  27677  fallfacval4  27680  predfz  27798  fsumkthpow  28333  ltflcei  28557  fdc  28779  mettrifi  28791  caushft  28795  cntotbnd  28833  mzpsubmpt  29217  lzenom  29246  diophun  29250  eqrabdioph  29254  irrapxlem2  29302  irrapxlem3  29303  pellexlem6  29313  pell1234qrreccl  29333  pellfund14  29377  rmspecsqrnq  29385  rmxyneg  29399  rmxyadd  29400  rmxp1  29411  rmxm1  29413  rmym1  29414  rmxluc  29415  rmyluc  29416  rmyluc2  29417  rmxdbl  29418  rmydbl  29419  jm2.17a  29441  congadd  29447  congsub  29451  congabseq  29455  acongrep  29461  acongeq  29464  jm2.18  29475  jm2.19lem1  29476  jm2.19lem2  29477  jm2.19lem3  29478  jm2.22  29482  jm2.23  29483  jm2.20nn  29484  jm2.25  29486  jm2.26lem3  29488  jm2.27c  29494  hashgcdlem  29703  fmul01lt1lem2  29904  clim1fr1  29912  stoweidlem11  29944  stoweidlem26  29959  wallispilem5  30002  2elfz2melfz  30340  fsumsplitsndif  30376  fsumsplitsnun  30380  clwwisshclww  30609  cshwlemma1  30627  nn0disj  30876  ztprmneprm  30877  altgsumbcALT  30888  cayhamlem1  31320  sineq0ALT  31973
  Copyright terms: Public domain W3C validator