ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zcnd Unicode version

Theorem zcnd 9194
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 9193 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 7814 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1481   CCcc 7638   ZZcz 9074
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7732
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-rab 2426  df-v 2689  df-un 3076  df-in 3078  df-ss 3085  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-br 3934  df-iota 5092  df-fv 5135  df-ov 5781  df-neg 7956  df-z 9075
This theorem is referenced by:  qapne  9454  fzm1  9907  fzrevral  9912  fzshftral  9915  nn0disj  9942  fzoss2  9976  fzosubel  9998  fzosubel3  10000  fzocatel  10003  fzosplitsnm1  10013  qtri3or  10047  exbtwnzlemstep  10052  exbtwnzlemex  10054  rebtwn2zlemstep  10057  rebtwn2z  10059  flqaddz  10097  flqzadd  10098  2tnp1ge0ge0  10101  ceiqm1l  10111  intqfrac2  10119  intfracq  10120  flqdiv  10121  modqvalr  10125  flqpmodeq  10127  modq0  10129  mulqmod0  10130  modqlt  10133  modqdiffl  10135  modqfrac  10137  flqmod  10138  intqfrac  10139  modqmulnn  10142  modqvalp1  10143  modqcyc  10159  modqcyc2  10160  modqadd1  10161  mulqaddmodid  10164  mulp1mod1  10165  modqmul1  10177  modqmul12d  10178  modqnegd  10179  modqmulmodr  10190  modqdi  10192  modqsubdir  10193  modfzo0difsn  10195  modsumfzodifsn  10196  addmodlteq  10198  frecfzen2  10227  uzennn  10236  uzsinds  10242  seq3shft2  10273  monoord2  10277  iseqf1olemab  10289  seq3f1olemqsumkj  10298  seq3f1olemqsum  10300  expaddzaplem  10363  sqoddm1div8  10471  bcm1k  10534  bcp1nk  10536  bcpasc  10540  hashfz  10595  hashfzo  10596  hashfzp1  10598  seq3coll  10613  seq3shft  10638  fzomaxdif  10913  climshft2  11103  iserex  11136  iser3shft  11143  serf0  11149  fsumm1  11213  fsumsplitsnun  11216  fsump1  11217  fsumshftm  11242  fisumrev2  11243  telfsumo  11263  fsumparts  11267  binomlem  11280  isumshft  11287  isumsplit  11288  isum1p  11289  divcnv  11294  arisum  11295  trireciplem  11297  cvgratnnlemmn  11322  cvgratnnlemsumlt  11325  mertenslemi1  11332  ntrivcvgap  11345  eirraplem  11510  moddvds  11529  dvdscmulr  11549  dvdsmulcr  11550  dvds2ln  11553  dvdsadd2b  11567  fzocongeq  11583  addmodlteqALT  11584  dvdsexp  11586  dvdsmod  11587  mulmoddvds  11588  odd2np1  11597  oddm1even  11599  oexpneg  11601  mulsucdiv2z  11609  zob  11615  ltoddhalfle  11617  divalglemnn  11642  divalglemqt  11643  divalglemex  11646  divalglemeuneg  11647  divalgb  11649  divalgmod  11651  modremain  11653  flodddiv4  11658  infssuzex  11669  dvdsbnd  11672  gcdaddm  11699  modgcd  11706  gcdmultipled  11708  dvdsgcdidd  11709  bezoutlemnewy  11711  bezoutlemaz  11718  bezoutlembz  11719  dvdsmulgcd  11740  rplpwr  11742  lcmval  11771  lcmcllem  11775  lcmid  11788  mulgcddvds  11802  divgcdcoprm0  11809  cncongr1  11811  cncongr2  11812  rpexp  11858  sqrt2irrlem  11866  sqrt2irrap  11885  qmuldeneqnum  11900  numdensq  11907  qden1elz  11910  hashdvds  11924  phiprm  11926  hashgcdlem  11930  znnen  11938  relogbexpap  13074  logbgcd1irraplemap  13085
  Copyright terms: Public domain W3C validator