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

Theorem recn 11220
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 11187 . 2 ℝ ⊆ ℂ
21sseli 3974 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099  cc 11128  cr 11129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-resscn 11187
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961
This theorem is referenced by:  mulrid  11234  recnd  11264  pnfnre  11277  mnfnre  11279  mul02  11414  ltaddneg  11451  ltaddnegr  11452  renegcli  11543  resubcl  11546  negn0  11665  negf1o  11666  ltaddsub2  11711  leaddsub2  11713  leltadd  11720  ltaddpos  11726  ltaddpos2  11727  posdif  11729  lenegcon1  11740  lenegcon2  11741  addge01  11746  addge02  11747  leaddle0  11751  mullt0  11755  recex  11868  ltm1  12078  prodgt02  12084  ltmul2  12087  lemul1  12088  lemul2  12089  lemul1a  12090  lemul2a  12091  ltmulgt12  12097  lemulge12  12099  gt0div  12102  ge0div  12103  mulge0b  12106  mulle0b  12107  ltmuldiv2  12110  ltdivmul  12111  ledivmul  12112  ltdivmul2  12113  lt2mul2div  12114  ledivmul2  12115  lemuldiv2  12117  ltdiv2  12122  ltrec1  12123  lerec2  12124  ledivdiv  12125  lediv2  12126  ltdiv23  12127  lediv23  12128  lediv12a  12129  recp1lt1  12134  ledivp1  12138  negfi  12185  infm3lem  12194  supmul  12208  riotaneg  12215  negiso  12216  cju  12230  nnge1  12262  halfpos  12464  lt2halves  12469  addltmul  12470  avgle1  12474  avgle2  12475  avgle  12476  div4p1lem1div2  12489  nnrecl  12492  difgtsumgt  12547  elznn0  12595  elznn  12596  elz2  12598  nzadd  12632  zmulcl  12633  gtndiv  12661  zeo  12670  eqreznegel  12940  supminf  12941  rebtwnz  12953  irradd  12979  irrmul  12980  divlt1lt  13067  divle1le  13068  max0sub  13199  xnegneg  13217  rexsub  13236  xnegid  13241  xaddcom  13243  xaddrid  13244  xnegdi  13251  xaddass  13252  rexmul  13274  xmulasslem3  13289  xadddilem  13297  divelunit  13495  fzonmapblen  13702  ico01fl0  13808  flzadd  13815  ltdifltdiv  13823  dfceil2  13828  intfrac2  13847  fldiv2  13850  flpmodeq  13863  mod0  13865  negmod0  13867  modlt  13869  modfrac  13873  flmod  13874  intfrac  13875  modmulnn  13878  modvalp1  13879  modid  13885  modcyc  13895  modcyc2  13896  modadd1  13897  modaddabs  13898  muladdmodid  13900  negmod  13905  modadd2mod  13910  modmul1  13913  modmulmodr  13926  modaddmulmod  13927  moddi  13928  modsubdir  13929  modirr  13931  addmodlteq  13935  expgt1  14089  mulexpz  14091  sqgt0  14114  lt2sq  14121  le2sq  14122  sqge0  14124  expmordi  14155  leexp1a  14163  expubnd  14165  sumsqeq0  14166  sqlecan  14196  bernneq  14215  bernneq2  14216  expnbnd  14218  digit2  14222  digit1  14223  expnngt1  14227  swrdccatin2  14703  swrdccat3blem  14713  cshweqrep  14795  crre  15085  crim  15086  reim0  15089  mulre  15092  rere  15093  remul2  15101  rediv  15102  immul2  15108  imdiv  15109  cjre  15110  cjreim  15131  rennim  15210  resqrex  15221  resqreu  15223  resqrtcl  15224  resqrtthlem  15225  sqrtneglem  15237  sqrtneg  15238  absreimsq  15263  absreim  15264  absnid  15269  leabs  15270  absre  15272  absresq  15273  sqabs  15278  max0add  15281  absz  15282  absdiflt  15288  absdifle  15289  lenegsq  15291  abssuble0  15299  absmax  15300  rddif  15311  absrdbnd  15312  o1rlimmul  15587  caurcvg2  15648  reefcl  16055  efgt0  16071  reeftlcl  16076  resinval  16103  recosval  16104  resin4p  16106  recos4p  16107  resincl  16108  recoscl  16109  retancl  16110  resinhcl  16124  rpcoshcl  16125  retanhcl  16127  tanhlt1  16128  tanhbnd  16129  efieq  16131  sinbnd  16148  cosbnd  16149  absefi  16164  dvdsaddre2b  16275  odd2np1  16309  bezoutlem1  16506  xrsdsreclb  21333  remulg  21526  resubdrg  21527  remetdval  24692  bl2ioo  24695  ioo2bl  24696  cnperf  24723  icccvx  24862  tcphcph  25152  shft2rab  25424  volsup2  25521  volcn  25522  c1lip1  25917  plyreres  26204  aalioulem3  26256  taylthlem2  26296  taylthlem2OLD  26297  reeff1o  26371  reefgim  26374  sincosq1sgn  26420  sincosq2sgn  26421  sincosq3sgn  26422  sincosq4sgn  26423  sinq12gt0  26429  pige3ALT  26441  efif1olem4  26466  efifo  26468  relogrn  26482  logrnaddcl  26495  relogoprlem  26512  advlog  26575  advlogexp  26576  logtayl  26581  recxpcl  26596  rpcxpcl  26597  cxpge0  26604  cxpcom  26660  dvcxp1  26661  logreclem  26681  relogbreexp  26694  relogbcxp  26704  angpieqvd  26750  atanre  26804  basellem9  27008  gausslemma2dlem1a  27285  2sqnn0  27358  log2sumbnd  27464  brbtwn2  28703  colinearalglem4  28707  colinearalg  28708  crctcshwlkn0lem1  29608  nvsge0  30461  nmoub3i  30570  nmlnoubi  30593  isblo3i  30598  ipasslem3  30630  ipasslem9  30635  ipasslem11  30637  hmopm  31818  riesz1  31862  leopmuli  31930  leopmul  31931  leopmul2i  31932  leopnmid  31935  nmopleid  31936  cdj1i  32230  cdj3lem1  32231  cdj3i  32238  addltmulALT  32243  dpfrac1  32597  rexdiv  32631  xdivid  32633  xdiv0  32634  sgnneg  34096  lediv2aALT  35217  nndivlub  35878  irrdiff  36741  cos2h  37019  tan2h  37020  poimir  37061  mblfinlem2  37066  mblfinlem4  37068  itg2addnclem  37079  itg2addnclem2  37080  dvasin  37112  areacirclem1  37116  areacirclem2  37117  areacirclem4  37119  areacirclem5  37120  areacirc  37121  lcmineqlem12  41448  dvrelog2b  41474  aks4d1p1p6  41481  2xp3dxp2ge1d  41613  retire  41802  resubeulem2  41853  renegneg  41888  renegid2  41890  sn-it0e0  41892  sn-negex12  41893  resubeqsub  41906  sn-mullid  41912  sn-mul02  41917  areaquad  42567  reabssgn  42989  radcnvrat  43674  lhe4.4ex1a  43689  expgrowthi  43693  mulltgt0  44307  refsum2cnlem1  44322  infnsuprnmpt  44549  dstregt0  44586  suplesup  44644  infleinflem1  44675  infleinflem2  44676  ltdiv23neg  44699  rexabslelem  44723  supminfrnmpt  44750  supminfxr  44769  fmul01lt1lem1  44895  lptre2pt  44951  cnrefiisplem  45140  dvcosre  45223  itgsin0pilem1  45261  itgsinexplem1  45265  volioc  45283  volico  45294  stoweidlem7  45318  stoweidlem10  45321  stoweidlem19  45330  stoweidlem34  45345  stoweid  45374  dirker2re  45403  dirkerdenne0  45404  dirkerper  45407  dirkertrigeq  45412  dirkeritg  45413  fourierdlem39  45457  fourierdlem42  45460  fourierdlem47  45464  fourierdlem56  45473  fourierdlem57  45474  fourierdlem58  45475  fourierdlem60  45477  fourierdlem61  45478  fourierdlem73  45490  fourierdlem76  45493  fourierdlem77  45494  fourierdlem92  45509  fourierdlem97  45514  etransclem46  45591  volico2  45952  smflimlem4  46085  smfinflem  46128  et-sqrtnegnre  46184  2leaddle2  46601  ltsubsubaddltsub  46604  sqrtnegnre  46610  m1mod0mod1  46632  requad01  46884  requad1  46885  bgoldbtbndlem2  47069  flsubz  47513  rege1logbrege0  47554  nn0digval  47596  rrx2vlinest  47737  line2  47748  line2xlem  47749  line2x  47750  itscnhlc0yqe  47755  itsclc0yqsollem2  47759  itsclc0yqsol  47760  itscnhlc0xyqsol  47761  itschlc0xyqsol1  47762  itsclc0xyqsolr  47765  itsclquadb  47772  reseccl  48107  recsccl  48108  recotcl  48109
  Copyright terms: Public domain W3C validator