MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recn Structured version   Visualization version   GIF version

Theorem recn 10064
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 10031 . 2 ℝ ⊆ ℂ
21sseli 3632 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cc 9972  cr 9973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  mulid1  10075  recnd  10106  pnfnre  10119  mnfnre  10120  mul02  10252  ltaddneg  10289  ltaddnegr  10290  renegcli  10380  resubcl  10383  negn0  10497  negf1o  10498  ltaddsub2  10541  leaddsub2  10543  leltadd  10550  ltaddpos  10556  ltaddpos2  10557  posdif  10559  lenegcon1  10570  lenegcon2  10571  addge01  10576  addge02  10577  leaddle0  10581  mullt0  10585  recex  10697  ltm1  10901  prodgt02  10907  prodge02  10909  ltmul2  10912  lemul1  10913  lemul2  10914  lemul1a  10915  lemul2a  10916  ltmulgt12  10922  lemulge12  10924  gt0div  10927  ge0div  10928  mulge0b  10931  mulle0b  10932  ltmuldiv2  10935  ltdivmul  10936  ledivmul  10937  ltdivmul2  10938  lt2mul2div  10939  ledivmul2  10940  lemuldiv2  10942  ltdiv2  10947  ltrec1  10948  lerec2  10949  ledivdiv  10950  lediv2  10951  ltdiv23  10952  lediv23  10953  lediv12a  10954  recp1lt1  10959  ledivp1  10963  negfi  11009  fiminre  11010  infm3lem  11019  supmul  11033  riotaneg  11040  negiso  11041  cju  11054  nnge1  11084  halfpos  11300  lt2halves  11305  addltmul  11306  avgle1  11310  avgle2  11311  avgle  11312  div4p1lem1div2  11325  nnrecl  11328  difgtsumgt  11384  elznn0  11430  elznn  11431  elz2  11432  nzadd  11463  zmulcl  11464  gtndiv  11492  zeo  11501  eqreznegel  11812  supminf  11813  rebtwnz  11825  irradd  11850  irrmul  11851  divlt1lt  11937  divle1le  11938  max0sub  12065  xnegneg  12083  rexsub  12102  xnegid  12107  xaddcom  12109  xaddid1  12110  xnegdi  12116  xaddass  12117  rexmul  12139  xmulasslem3  12154  xadddilem  12162  divelunit  12352  fzonmapblen  12553  ico01fl0  12660  flzadd  12667  ltdifltdiv  12675  dfceil2  12680  intfrac2  12697  fldiv2  12700  flpmodeq  12713  mod0  12715  negmod0  12717  modlt  12719  modfrac  12723  flmod  12724  intfrac  12725  modmulnn  12728  modvalp1  12729  modid  12735  modcyc  12745  modcyc2  12746  modadd1  12747  modaddabs  12748  muladdmodid  12750  negmod  12755  modadd2mod  12760  modmul1  12763  modmulmodr  12776  modaddmulmod  12777  moddi  12778  modsubdir  12779  modirr  12781  addmodlteq  12785  expgt1  12938  mulexpz  12940  leexp1a  12959  expubnd  12961  sqgt0  12972  lt2sq  12977  le2sq  12978  sqge0  12980  sumsqeq0  12982  sqlecan  13011  bernneq  13030  bernneq2  13031  expnbnd  13033  digit2  13037  digit1  13038  swrdccatin2  13533  swrdccat3blem  13541  cshweqrep  13613  crre  13898  crim  13899  reim0  13902  mulre  13905  rere  13906  remul2  13914  rediv  13915  immul2  13921  imdiv  13922  cjre  13923  cjreim  13944  rennim  14023  resqrex  14035  resqreu  14037  resqrtcl  14038  resqrtthlem  14039  sqrtneglem  14051  sqrtneg  14052  absreimsq  14076  absreim  14077  absnid  14082  leabs  14083  absre  14085  absresq  14086  sqabs  14091  max0add  14094  absz  14095  absdiflt  14101  absdifle  14102  lenegsq  14104  abssuble0  14112  absmax  14113  rddif  14124  absrdbnd  14125  o1rlimmul  14393  caurcvg2  14452  reefcl  14861  efgt0  14877  reeftlcl  14882  resinval  14909  recosval  14910  resin4p  14912  recos4p  14913  resincl  14914  recoscl  14915  retancl  14916  resinhcl  14930  rpcoshcl  14931  retanhcl  14933  tanhlt1  14934  tanhbnd  14935  efieq  14937  sinbnd  14954  cosbnd  14955  absefi  14970  dvdsaddre2b  15076  odd2np1  15112  bezoutlem1  15303  xrsdsreclb  19841  remulg  20001  resubdrg  20002  remetdval  22639  bl2ioo  22642  ioo2bl  22643  cnperf  22670  icccvx  22796  tchcph  23082  shft2rab  23322  volsup2  23419  volcn  23420  c1lip1  23805  plyreres  24083  aalioulem3  24134  taylthlem2  24173  reeff1o  24246  reefgim  24249  sincosq1sgn  24295  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  sinq12gt0  24304  pige3  24314  efif1olem4  24336  efifo  24338  relogrn  24353  logrnaddcl  24366  relogoprlem  24382  advlog  24445  advlogexp  24446  logtayl  24451  recxpcl  24466  rpcxpcl  24467  cxpge0  24474  dvcxp1  24526  logreclem  24545  relogbreexp  24558  relogbcxp  24568  angpieqvd  24603  atanre  24657  basellem9  24860  gausslemma2dlem1a  25135  log2sumbnd  25278  brbtwn2  25830  colinearalglem4  25834  colinearalg  25835  crctcshwlkn0lem1  26758  nvsge0  27647  nmoub3i  27756  nmlnoubi  27779  isblo3i  27784  ipasslem3  27816  ipasslem9  27821  ipasslem11  27823  hmopm  29008  riesz1  29052  leopmuli  29120  leopmul  29121  leopmul2i  29122  leopnmid  29125  nmopleid  29126  cdj1i  29420  cdj3lem1  29421  cdj3i  29428  addltmulALT  29433  dpfrac1  29727  dpfrac1OLD  29728  rexdiv  29762  xdivid  29764  xdiv0  29765  rmulccn  30102  sgnneg  30730  lediv2aALT  31697  nndivlub  32582  cos2h  33530  tan2h  33531  poimir  33572  mblfinlem2  33577  mblfinlem4  33579  itg2addnclem  33591  itg2addnclem2  33592  dvasin  33626  areacirclem1  33630  areacirclem2  33631  areacirclem4  33633  areacirclem5  33634  areacirc  33635  expmordi  37829  areaquad  38119  radcnvrat  38830  lhe4.4ex1a  38845  expgrowthi  38849  mulltgt0  39495  refsum2cnlem1  39510  infnsuprnmpt  39779  dstregt0  39807  suplesup  39868  infleinflem1  39899  infleinflem2  39900  ltdiv23neg  39930  rexabslelem  39958  supminfrnmpt  39985  supminfxr  40007  fmul01lt1lem1  40134  lptre2pt  40190  cnrefiisplem  40373  dvcosre  40444  itgsin0pilem1  40483  itgsinexplem1  40487  volioc  40506  volico  40518  stoweidlem7  40542  stoweidlem10  40545  stoweidlem19  40554  stoweidlem34  40569  stoweid  40598  dirker2re  40627  dirkerdenne0  40628  dirkerper  40631  dirkertrigeq  40636  dirkeritg  40637  fourierdlem39  40681  fourierdlem42  40684  fourierdlem47  40688  fourierdlem56  40697  fourierdlem57  40698  fourierdlem58  40699  fourierdlem60  40701  fourierdlem61  40702  fourierdlem73  40714  fourierdlem76  40717  fourierdlem77  40718  fourierdlem92  40733  fourierdlem97  40738  etransclem46  40815  volico2  41176  smflimlem4  41303  smfinflem  41344  2leaddle2  41637  ltsubsubaddltsub  41640  m1mod0mod1  41664  bgoldbtbndlem2  42019  flsubz  42637  rege1logbrege0  42677  nn0digval  42719  reseccl  42822  recsccl  42823  recotcl  42824
  Copyright terms: Public domain W3C validator