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

Theorem recnd 8857
Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
recnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem recnd
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 recn 8823 . 2  |-  ( A  e.  RR  ->  A  e.  CC )
31, 2syl 15 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1685   CCcc 8731   RRcr 8732
This theorem is referenced by:  00id  8983  mul02lem1  8984  addid1  8988  cnegex  8989  ltadd1  9237  leadd2  9239  ltsubadd  9240  ltsubadd2  9241  lesubadd  9242  lesubadd2  9243  lesub1  9264  lesub2  9265  ltnegcon1  9271  ltnegcon2  9272  add20  9282  subge0  9283  suble0  9284  lesub0  9286  mulge0  9287  eqord2  9300  rereccl  9474  redivcl  9475  recgt0  9596  prodgt0  9597  prodge0  9599  ltmul1a  9601  ltdiv1  9616  ltmuldiv  9622  ltrec  9633  recp1lt1  9650  recreclt  9651  ledivp1  9654  infmsup  9728  infmrcl  9729  rimul  9733  cru  9734  avglt1  9945  avglt2  9946  nn0cnd  10016  zcn  10025  zeo  10093  zcnd  10114  cnref1o  10345  rpcn  10358  rpcnd  10388  ltaddrp2d  10416  qbtwnre  10522  xralrple  10528  xpncan  10567  xmulcom  10582  xmulneg1  10585  xlemul1  10606  icoshftf1o  10755  lincmb01cmp  10773  iccf1o  10774  fladdz  10946  flzadd  10947  flhalf  10950  ceim1l  10953  intfracq  10959  fldiv  10960  mod0  10974  modlt  10977  moddiffl  10978  modfrac  10980  flmod  10981  intfrac  10982  modmulnn  10984  modid  10989  modcyc  10995  modadd1  10997  modnegd  11000  modadd12d  11001  modsub12d  11002  moddi  11003  modsubdir  11004  modirr  11005  seqf1olem1  11081  serle  11097  expcl2lem  11111  expnegz  11132  expaddzlem  11141  expaddz  11142  expmulz  11144  ltexp2a  11149  leexp2a  11153  leexp2r  11155  exple1  11157  expubnd  11158  sq11  11172  bernneq2  11224  expmulnbnd  11229  discr1  11233  discr  11234  faclbnd  11299  bcp1nk  11325  remim  11598  reim0b  11600  rereb  11601  mulre  11602  cjreb  11604  recj  11605  reneg  11606  readd  11607  resub  11608  remullem  11609  remul2  11611  rediv  11612  imcj  11613  imneg  11614  imadd  11615  imsub  11616  immul2  11618  imdiv  11619  cjcj  11621  cjadd  11622  ipcnval  11624  cjmulval  11626  cjneg  11628  imval2  11632  cjreim2  11642  sqr0lem  11722  sqrlem5  11728  sqrlem7  11730  resqrthlem  11736  remsqsqr  11738  sqrmul  11741  sqrdiv  11747  sqrneg  11749  sqrmsq  11752  absdiv  11776  absid  11777  absexp  11785  absexpz  11786  absimle  11790  abslt  11794  absle  11795  abssubne0  11796  releabs  11801  recval  11802  abstri  11810  abs2difabs  11814  abs1m  11815  abslem2  11819  absrdbnd  11821  sqreulem  11839  sqreu  11840  amgm2  11849  lo1bddrp  11995  o1lo1  12007  rlimrecl  12050  rlimge0  12051  climrecl  12053  climge0  12054  climabs0  12055  reccn2  12066  o1rlimmul  12088  lo1mul2  12098  lo1sub  12100  climle  12109  climsqz  12110  climsqz2  12111  rlimsqz  12119  rlimsqz2  12120  rlimno1  12123  climlec2  12128  isercolllem1  12134  climsup  12139  caucvgrlem  12141  caurcvgr  12142  caucvgrlem2  12143  iseraltlem1  12150  iseraltlem2  12151  iseraltlem3  12152  iseralt  12153  isumrecl  12224  isumge0  12225  fsumless  12250  fsumge1  12251  fsum00  12252  fsumle  12253  fsumlt  12254  fsumabs  12255  o1fsum  12267  seqabs  12268  cvgcmp  12270  cvgcmpce  12272  abscvgcvg  12273  isumrpcl  12298  isumle  12299  isumless  12300  isumsup  12302  climcndslem1  12304  climcndslem2  12305  climcnds  12306  flo1  12309  supcvg  12310  trireciplem  12316  trirecip  12317  explecnv  12319  geo2sum  12325  geo2lim  12327  geomulcvg  12328  cvgrat  12335  mertenslem1  12336  mertenslem2  12337  efcllem  12355  ege2le3  12367  efaddlem  12370  efgt0  12379  eftlub  12385  effsumlt  12387  eflt  12393  eflegeo  12397  resin4p  12414  recos4p  12415  retanhcl  12435  tanhlt1  12436  efeul  12438  ef01bndlem  12460  sin01bnd  12461  cos01bnd  12462  sin01gt0  12466  cos01gt0  12467  sin02gt0  12468  absefi  12472  absef  12473  absefib  12474  efieq1re  12475  eirrlem  12478  rpnnen2lem5  12493  rpnnen2lem8  12496  rpnnen2lem9  12497  rpnnen2lem11  12499  rpnnen2  12500  moddvds  12534  odd2np1  12583  divalglem5  12592  bitsp1  12618  bitsp1o  12620  bitsfzo  12622  bitscmp  12625  sadcaddlem  12644  nn0seqcvgd  12736  sqnprm  12773  isprm5  12787  nonsq  12826  eulerthlem2  12846  prmdiveq  12850  odzdvds  12856  pythagtriplem14  12877  pcid  12921  fldivp1  12941  pcfac  12943  pockthlem  12948  prmreclem3  12961  prmreclem4  12962  prmreclem5  12963  prmrec  12965  4sqlem5  12985  4sqlem10  12990  mul4sqlem  12996  4sqlem15  13002  4sqlem16  13003  mulgneg  14581  ghmmulg  14691  odmodnn0  14851  mndodconglem  14852  pgpfaclem2  15313  isabvd  15581  abv1z  15593  abvneg  15595  abvrec  15597  abvdiv  15598  abvdom  15599  rege0subm  16424  cnsubrg  16428  gzrngunitlem  16432  prmirredlem  16442  bl2in  17953  blhalf  17956  blss  17968  methaus  18062  nrmmetd  18093  nm2dif  18142  nminvr  18176  nmdvr  18177  nlmmul0or  18190  nrginvrcnlem  18197  nmolb2d  18223  nmoi2  18235  nmoleub  18236  nmo0  18240  nmoeq0  18241  nmoco  18242  nmotri  18244  nmoid  18247  blcvx  18300  xrsxmet  18311  recld2  18316  reconnlem2  18328  opnreen  18332  metdstri  18351  metnrmlem3  18361  iihalf2cn  18428  icchmeo  18435  icopnfcnv  18436  icopnfhmeo  18437  iccpnfhmeo  18439  xrhmeo  18440  icccvx  18444  cnheiborlem  18448  evth  18453  lebnumii  18460  pcoass  18518  pcorevlem  18520  pcorev2  18522  pi1xfrcnv  18551  nmoleub2lem  18591  nmoleub2lem3  18592  nmoleub3  18596  cphsqrcl2  18618  ipcau2  18660  tchcphlem1  18661  tchcphlem2  18662  tchcph  18663  iscau3  18700  minveclem2  18786  minveclem3b  18788  minveclem4  18792  minveclem6  18794  minveclem7  18795  pjthlem1  18797  ivthlem2  18808  ivthlem3  18809  ivth2  18811  ovolfsval  18826  ovollb2lem  18843  ovolctb  18845  ovolunlem1a  18851  ovolunnul  18855  ovolfiniun  18856  ovoliunlem1  18857  ovoliun2  18861  shft2rab  18863  ovolshftlem1  18864  sca2rab  18867  ovolscalem1  18868  ovolsca  18870  ovolicc1  18871  ovolicc2lem4  18875  ovolicopnf  18879  cmmbl  18888  nulmbl  18889  nulmbl2  18890  unmbl  18891  volinun  18899  volfiniun  18900  voliunlem1  18903  voliunlem3  18905  ioombl1lem3  18913  ioombl1lem4  18914  ovolioo  18921  ioorcl2  18923  uniioovol  18930  uniioombllem3  18936  uniioombllem4  18937  uniioombllem5  18938  uniioombllem6  18939  dyadovol  18944  dyaddisjlem  18946  opnmbllem  18952  vitalilem1  18959  vitalilem2  18960  vitalilem3  18961  vitalilem4  18962  ismbf  18981  mbfmulc2lem  18998  mbfmulc2re  18999  mbfpos  19002  mbfmulc2  19014  mbfinf  19016  itg1val2  19035  itg11  19042  i1fmullem  19045  i1fadd  19046  itg1addlem4  19050  itg1addlem5  19051  i1fmulclem  19053  i1fmulc  19054  itg1mulc  19055  itg1sub  19060  itg10a  19061  itg1ge0a  19062  itg1climres  19065  mbfi1fseqlem3  19068  mbfi1fseqlem4  19069  mbfi1fseqlem5  19070  mbfi1fseqlem6  19071  mbfi1flimlem  19073  mbfmullem2  19075  itg2const  19091  itg2const2  19092  itg2mulclem  19097  itg2mulc  19098  itg2splitlem  19099  itg2split  19100  itg2monolem1  19101  itg2monolem3  19103  itg2addlem  19109  itgcl  19134  itgcnlem  19140  itgrevallem1  19145  itgposval  19146  iblneg  19153  itgneg  19154  i1fibl  19158  itgitg1  19159  itgconst  19169  ibladd  19171  itgaddlem2  19174  iblabslem  19178  iblabs  19179  iblabsr  19180  iblmulc2  19181  itgmulc2lem2  19183  itgmulc2  19184  itgabs  19185  itgsplit  19186  bddmulibl  19189  dvcjbr  19294  dvfre  19296  dvexp3  19321  dveflem  19322  dvferm1lem  19327  dvferm2lem  19329  rolle  19333  cmvth  19334  mvth  19335  dvlip  19336  dvlipcn  19337  c1liplem1  19339  c1lip1  19340  dveq0  19343  dv11cn  19344  dvlt0  19348  dvle  19350  dvivthlem1  19351  dvivth  19353  lhop1lem  19356  lhop1  19357  lhop2  19358  lhop  19359  dvcvx  19363  dvfsumle  19364  dvfsumge  19365  dvfsumabs  19366  dvfsumlem1  19369  dvfsumlem2  19370  dvfsumlem4  19372  dvfsumrlimge0  19373  dvfsumrlim2  19375  dvfsum2  19377  ftc1a  19380  ftc1lem4  19382  ftc1lem5  19383  plyeq0lem  19588  coemulhi  19631  plyrecj  19656  plydivlem3  19671  aalioulem2  19709  aalioulem3  19710  aalioulem4  19711  aalioulem5  19712  aalioulem6  19713  aaliou  19714  aaliou2  19716  aaliou2b  19717  aaliou3lem3  19720  aaliou3lem7  19725  aaliou3lem9  19726  taylthlem2  19749  ulmcn  19772  ulmdvlem1  19773  mtest  19777  itgulm  19780  radcnvlem1  19785  radcnvlem2  19786  radcnvlt1  19790  radcnvle  19792  dvradcnv  19793  pserulm  19794  abelthlem2  19804  abelthlem5  19807  abelthlem7  19810  abelth2  19814  reeff1olem  19818  efcvx  19821  pilem2  19824  pilem3  19825  sincosq2sgn  19863  sincosq3sgn  19864  sincosq4sgn  19865  coseq0negpitopi  19867  tanrpcl  19868  tangtx  19869  tanabsge  19870  sinq12gt0  19871  sinq34lt0t  19873  cosq14gt0  19874  cosq14ge0  19875  pige3  19881  coskpi  19884  sineq0  19885  cosordlem  19889  sinord  19892  tanord1  19895  tanord  19896  tanregt0  19897  efif1olem2  19901  efif1olem4  19903  eff1olem  19906  logrnaddcl  19927  logneg  19937  lognegb  19939  reexplog  19944  relogexp  19945  logfac  19950  efiarg  19957  cosargd  19958  cosarg0d  19959  argregt0  19960  argrege0  19961  argimgt0  19962  logneg2  19965  tanarg  19966  logdivlti  19967  divlogrlim  19978  logcnlem2  19986  logcnlem3  19987  logcnlem4  19988  logcn  19990  logf1o2  19993  advlog  19997  advlogexp  19998  efopnlem1  19999  logtayllem  20002  logtayl  20003  logccv  20006  logcxp  20012  mulcxp  20028  divcxp  20030  cxpmul  20031  cxproot  20033  cxpmul2z  20034  abscxp  20035  abscxp2  20036  cxplt  20037  cxplea  20039  cxple2  20040  cxple2a  20042  cxplt3  20043  cxpsqrlem  20045  cxpsqr  20046  logsqr  20047  dvcxp2  20079  cxpcn3lem  20083  resqrcn  20085  cxpaddlelem  20087  cxpaddle  20088  abscxpbnd  20089  root1id  20090  root1eq1  20091  root1cj  20092  cxpeq  20093  loglesqr  20094  cosangneg2d  20101  angrtmuld  20102  ang180lem2  20104  lawcoslem1  20109  lawcos  20110  pythag  20111  isosctrlem1  20114  isosctrlem2  20115  isosctrlem3  20116  ssscongptld  20118  chordthmlem  20125  chordthmlem2  20126  chordthmlem3  20127  chordthmlem4  20128  chordthmlem5  20129  asinsinlem  20183  reasinsin  20188  acosrecl  20195  atancj  20202  atanrecl  20203  atanlogaddlem  20205  atanlogsublem  20207  atanbndlem  20217  atans2  20223  ressatans  20226  atantayl  20229  leibpilem2  20233  leibpi  20234  leibpisum  20235  log2tlbnd  20237  log2ublem2  20239  birthdaylem2  20243  birthdaylem3  20244  cxp2limlem  20266  cxp2lim  20267  cxploglim  20268  cxploglim2  20269  divsqrsumo1  20274  cvxcl  20275  scvxcvx  20276  jensenlem2  20278  jensen  20279  amgmlem  20280  emcllem2  20286  emcllem3  20287  emcllem5  20289  emcllem6  20290  emcllem7  20291  harmonicbnd4  20300  fsumharmonic  20301  ftalem1  20306  ftalem2  20307  ftalem4  20309  ftalem5  20310  basellem3  20316  basellem4  20317  basellem5  20318  basellem6  20319  basellem7  20320  basellem8  20321  basellem9  20322  efnnfsumcl  20336  chtprm  20387  chpp1  20389  chtdif  20392  efchtdvds  20393  prmorcht  20412  mumullem2  20414  fsumfldivdiaglem  20425  ppiub  20439  chtleppi  20445  chtublem  20446  chtub  20447  pclogsum  20450  vmasum  20451  logfac2  20452  chpval2  20453  chpchtsum  20454  chpub  20455  logfaclbnd  20457  logfacbnd3  20458  logfacrlim  20459  logexprlim  20460  logfacrlim2  20461  mersenne  20462  dchrabs  20495  dchrptlem1  20499  dchrptlem2  20500  bcmax  20513  bcp1ctr  20514  bposlem1  20519  bposlem9  20527  lgsvalmod  20550  lgsdilem  20557  lgsne0  20568  lgsqrlem2  20577  lgseisenlem1  20584  lgseisenlem2  20585  lgseisen  20588  lgsquadlem1  20589  lgsquadlem2  20590  mul2sq  20600  2sqlem3  20601  2sqlem8  20607  chebbnd1lem1  20614  chebbnd1lem2  20615  chebbnd1lem3  20616  chtppilimlem1  20618  chtppilimlem2  20619  chtppilim  20620  chto1ub  20621  chto1lb  20623  chpchtlim  20624  chpo1ub  20625  vmadivsum  20627  vmadivsumb  20628  rplogsumlem1  20629  rplogsumlem2  20630  rpvmasumlem  20632  dchrisumlema  20633  dchrisumlem1  20634  dchrisumlem2  20635  dchrisumlem3  20636  dchrmusumlema  20638  dchrmusum2  20639  dchrvmasumlem1  20640  dchrvmasum2lem  20641  dchrvmasum2if  20642  dchrvmasumlem2  20643  dchrvmasumlem3  20644  dchrvmasumiflem1  20646  dchrvmasumiflem2  20647  dchrisum0flblem1  20653  dchrisum0fno1  20656  rpvmasum2  20657  dchrisum0re  20658  dchrisum0lema  20659  dchrisum0lem1b  20660  dchrisum0lem1  20661  dchrisum0lem2a  20662  dchrisum0lem2  20663  dchrisum0lem3  20664  dchrmusumlem  20667  dchrvmasumlem  20668  rpvmasum  20671  rplogsum  20672  dirith2  20673  mudivsum  20675  mulogsumlem  20676  mulogsum  20677  logdivsum  20678  mulog2sumlem1  20679  mulog2sumlem2  20680  mulog2sumlem3  20681  vmalogdivsum2  20683  vmalogdivsum  20684  2vmadivsumlem  20685  logsqvma  20687  logsqvma2  20688  log2sumbnd  20689  selberglem1  20690  selberglem2  20691  selberglem3  20692  selberg  20693  selbergb  20694  selberg2lem  20695  selberg2  20696  selberg2b  20697  chpdifbndlem1  20698  logdivbnd  20701  selberg3lem1  20702  selberg3lem2  20703  selberg3  20704  selberg4lem1  20705  selberg4  20706  pntrmax  20709  pntrsumo1  20710  pntrsumbnd  20711  pntrsumbnd2  20712  selbergr  20713  selberg3r  20714  selberg4r  20715  selberg34r  20716  pntsval2  20721  pntrlog2bndlem1  20722  pntrlog2bndlem2  20723  pntrlog2bndlem3  20724  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  pntrlog2bndlem6a  20727  pntrlog2bndlem6  20728  pntrlog2bnd  20729  pntpbnd1a  20730  pntpbnd1  20731  pntpbnd2  20732  pntibndlem2  20736  pntibndlem3  20737  pntlemb  20742  pntlemg  20743  pntlemh  20744  pntlemn  20745  pntlemr  20747  pntlemj  20748  pntlemf  20750  pntlemk  20751  pntlemo  20752  pntlem3  20754  pntleml  20756  pnt2  20758  pnt  20759  abvcxp  20760  ostth2lem1  20763  qabvexp  20771  padicabv  20775  padicabvcxp  20777  ostth2lem2  20779  ostth2lem3  20780  ostth2lem4  20781  ostth2  20782  ostth3  20783  nvm1  21224  nvpi  21226  nvz0  21228  nvmtri  21231  nvabs  21233  nvge0  21234  nv1  21236  smcnlem  21264  ipval2lem4  21273  ipval2  21274  4ipval2  21275  4ipval3  21279  ipidsq  21280  dipcj  21284  dip0r  21287  ipz  21289  nmoub3i  21345  nmlno0lem  21365  nmblolbii  21371  blocnilem  21376  cncph  21391  ipasslem4  21406  ipasslem5  21407  ipblnfi  21428  minvecolem2  21448  minvecolem4  21453  minvecolem6  21455  minvecolem7  21456  htthlem  21491  normpyc  21721  hhph  21753  bcs2  21757  norm1  21824  norm1exi  21825  pjhthlem1  21966  eigvalcl  22537  eighmorth  22540  nmlnop0iALT  22571  nmbdoplbi  22600  nmcexi  22602  nmcoplbi  22604  nmbdfnlbi  22625  nmcfnlbi  22628  riesz4i  22639  cnlnadjlem2  22644  cnlnadjlem7  22649  nmopcoi  22671  nmopcoadji  22677  branmfn  22681  leopnmid  22714  opsqrlem1  22716  hst1h  22803  hstle  22806  hstoh  22808  sto2i  22813  stadd3i  22824  strlem1  22826  golem1  22847  stcltrlem1  22852  cdj1i  23009  cdj3lem1  23010  cdj3lem3b  23016  cdj3i  23017  fzsplit3  23027  bcm1n  23028  ballotlemfc0  23047  ballotlemfcc  23048  ballotlemsgt1  23065  ballotlemsel1i  23067  ballotlemsi  23069  zetacvg  23096  subfacval2  23125  subfaclim  23126  subfacval3  23127  rescon  23184  eupap1  23307  sinccvglem  23412  circum  23414  modaddabs  23418  fveecn  23940  eqeelen  23942  brbtwn2  23943  colinearalglem4  23947  colinearalg  23948  axsegconlem9  23963  axsegconlem10  23964  ax5seglem1  23966  ax5seglem2  23967  ax5seglem3  23969  ax5seglem5  23971  ax5seglem6  23972  ax5seglem9  23975  ax5seg  23976  axbtwnid  23977  axpaschlem  23978  axpasch  23979  axeuclidlem  24000  axcontlem2  24003  axcontlem4  24005  axcontlem7  24008  axcontlem8  24009  bpolydiflem  24199  bpoly4  24204  dvreasin  24333  dvreacos  24334  areacirclem2  24335  areacirclem3  24336  areacirclem6  24340  areacirc  24341  cntrset  25013  dmse1  25014  msr3  25016  msr4  25017  mslb1  25018  2wsms  25019  msra3  25020  iintlem1  25021  lvsovso  25037  rnegvex2  25072  nn0prpwlem  25649  csbrn  25873  trirn  25874  mettrifi  25884  lmclim2  25885  geomcau  25886  isbnd3  25919  ssbnd  25923  cntotbnd  25931  bfplem1  25957  bfplem2  25958  bfp  25959  rrnmet  25964  rrndstprj1  25965  rrndstprj2  25966  rrncmslem  25967  rrnequiv  25970  rrntotbnd  25971  ismrer1  25973  eldioph2lem1  26250  lzenom  26260  rencldnfilem  26314  icodiamlt  26316  irrapxlem1  26318  irrapxlem2  26319  irrapxlem3  26320  irrapxlem4  26321  irrapxlem5  26322  pellexlem2  26326  pellexlem6  26330  pell1234qrreccl  26350  pell14qrgt0  26355  pell14qrdivcl  26361  pell14qrexpclnn0  26362  pell14qrexpcl  26363  pell14qrdich  26365  pell1qrgaplem  26369  pellfundex  26382  reglogmul  26389  reglogexp  26390  reglogbas  26391  reglog1  26392  pellfund14  26394  rmspecsqrnq  26402  rmspecfund  26405  rmym1  26431  rmyluc  26433  monotoddzzfi  26438  expmordi  26443  jm2.24nn  26457  jm2.17a  26458  jm2.17b  26459  jm2.17c  26460  jm2.24  26461  acongrep  26478  fzmaxdif  26479  acongeq  26481  modabsdifz  26489  jm2.19lem4  26496  jm2.19  26497  jm2.26lem3  26505  jm3.1lem1  26521  jm3.1lem2  26522  dvconstbi  26962  climinf  27143  stoweidlem13  27173  stoweidlem17  27177  stoweidlem21  27181  stoweidlem47  27207  stoweidlem59  27219  wallispilem3  27227  wallispilem5  27229  wallispi2lem1  27231  stirlinglem1  27234  stirlinglem5  27238  stirlinglem11  27244  stirlinglem12  27245  stirlinglem14  27247
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-resscn 8790
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator