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

Theorem recn 9571
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn  |-  ( A  e.  RR  ->  A  e.  CC )

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 9538 . 2  |-  RR  C_  CC
21sseli 3485 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   CCcc 9479   RRcr 9480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  mulid1  9582  recnd  9611  pnfnre  9624  mnfnre  9625  mul02  9747  renegcli  9871  resubcl  9874  ltaddsub2  10023  leaddsub2  10025  leltadd  10032  ltaddpos  10038  ltaddpos2  10039  posdif  10041  lenegcon1  10052  lenegcon2  10053  addge01  10058  addge02  10059  leaddle0  10063  mullt0  10068  recex  10177  ltm1  10378  prodgt02  10384  prodge02  10386  ltmul2  10389  lemul1  10390  lemul2  10391  lemul1a  10392  lemul2a  10393  ltmulgt12  10399  lemulge12  10401  gt0div  10404  ge0div  10405  mulge0b  10408  mulle0b  10409  ltmuldiv2  10412  ltdivmul  10413  ledivmul  10414  ltdivmul2  10415  lt2mul2div  10416  ledivmul2  10417  ledivmul2OLD  10418  lemuldiv2  10420  ltdiv2  10425  ltrec1  10427  lerec2  10428  ledivdiv  10429  lediv2  10430  ltdiv23  10431  lediv23  10432  lediv12a  10433  recp1lt1  10438  ledivp1  10442  infm3lem  10496  supmul  10506  riotaneg  10513  negiso  10514  cju  10527  nnge1  10557  halfpos  10765  lt2halves  10769  addltmul  10770  avgle1  10774  avgle2  10775  avgle  10776  nnrecl  10789  elznn0  10875  elznn  10876  elz2  10877  zmulcl  10908  gtndiv  10936  zeo  10944  uzindOLD  10953  eqreznegel  11168  negn0  11169  supminf  11170  rebtwnz  11182  irradd  11207  irrmul  11208  max0sub  11398  xnegneg  11416  rexsub  11435  xnegid  11438  xaddcom  11440  xaddid1  11441  xnegdi  11443  xaddass  11444  rexmul  11466  xmulasslem3  11481  xadddilem  11489  divelunit  11665  fzonmapblen  11845  ico01fl0  11935  flzadd  11941  ltdifltdiv  11948  dfceil2  11950  intfrac2  11967  fldiv2  11970  flpmodeq  11983  mod0  11985  negmod0  11986  modlt  11988  modfrac  11991  flmod  11992  intfrac  11993  modmulnn  11995  modvalp1  11996  modid  12002  modcyc  12013  modcyc2  12014  modadd1  12015  modaddabs  12016  modadd2mod  12019  modmul1  12022  modaddmulmod  12035  moddi  12036  modsubdir  12037  modirr  12039  expgt1  12186  mulexpz  12188  leexp1a  12206  expubnd  12208  sqgt0  12218  lt2sq  12223  le2sq  12224  sqge0  12226  sumsqeq0  12228  sqlecan  12256  bernneq  12274  bernneq2  12275  expnbnd  12277  digit2  12281  digit1  12282  swrdccatin2  12703  swrdccat3blem  12711  cshweqrep  12780  crre  13029  crim  13030  reim0  13033  mulre  13036  rere  13037  remul2  13045  rediv  13046  immul2  13052  imdiv  13053  cjre  13054  cjreim  13075  rennim  13154  resqrex  13166  resqreu  13168  resqrtcl  13169  resqrtthlem  13170  sqrtneglem  13182  sqrtneg  13183  absreimsq  13207  absreim  13208  absnid  13213  leabs  13214  absre  13216  absresq  13217  sqabs  13222  max0add  13225  absz  13226  absdiflt  13232  absdifle  13233  lenegsq  13235  abssuble0  13243  absmax  13244  rddif  13255  absrdbnd  13256  o1rlimmul  13523  caurcvg2  13582  reefcl  13904  efgt0  13920  reeftlcl  13925  resinval  13952  recosval  13953  resin4p  13955  recos4p  13956  resincl  13957  recoscl  13958  retancl  13959  resinhcl  13973  rpcoshcl  13974  retanhcl  13976  tanhlt1  13977  tanhbnd  13978  efieq  13980  sinbnd  13997  cosbnd  13998  absefi  14013  odd2np1  14130  bezoutlem1  14260  xrsdsreclb  18660  remulg  18816  resubdrg  18817  remetdval  21460  bl2ioo  21463  ioo2bl  21464  cnperf  21491  icccvx  21616  tchcph  21846  shft2rab  22085  volsup2  22180  volcn  22181  c1lip1  22564  plyreres  22845  aalioulem3  22896  taylthlem2  22935  reeff1o  23008  reefgim  23011  sincosq1sgn  23057  sincosq2sgn  23058  sincosq3sgn  23059  sincosq4sgn  23060  sinq12gt0  23066  pige3  23076  efif1olem4  23098  efifo  23100  relogrn  23115  logrnaddcl  23128  relogoprlem  23144  advlog  23203  advlogexp  23204  logtayl  23209  recxpcl  23224  rpcxpcl  23225  cxpge0  23232  dvcxp1  23284  logreclem  23301  relogbreexp  23314  relogbcxp  23324  angpieqvd  23359  atanre  23413  basellem9  23560  log2sumbnd  23927  brbtwn2  24410  colinearalglem4  24414  colinearalg  24415  readdsubgo  25553  nvsge0  25764  nmoub3i  25886  nmlnoubi  25909  isblo3i  25914  ipasslem3  25946  ipasslem9  25951  ipasslem11  25953  hmopm  27138  riesz1  27182  leopmuli  27250  leopmul  27251  leopmul2i  27252  leopnmid  27255  nmopleid  27256  cdj1i  27550  cdj3lem1  27551  cdj3i  27558  addltmulALT  27563  rexdiv  27856  xdivid  27858  xdiv0  27859  rmulccn  28145  sgnneg  28743  lediv2aALT  29307  nndivlub  30151  cos2h  30286  tan2h  30287  mblfinlem2  30292  mblfinlem4  30294  dvtanlem  30304  itg2addnclem  30306  itg2addnclem2  30307  dvasin  30343  areacirclem1  30347  areacirclem2  30348  areacirclem4  30350  areacirclem5  30351  areacirc  30352  expmordi  31122  areaquad  31425  radcnvrat  31436  lhe4.4ex1a  31475  expgrowthi  31479  mulltgt0  31637  refsum2cnlem1  31652  dstregt0  31703  ltaddneg  31724  fmul01lt1lem1  31817  lptre2pt  31885  dvcosre  31945  itgsin0pilem1  31987  itgsinexplem1  31991  volioc  32010  stoweidlem7  32028  stoweidlem10  32031  stoweidlem19  32040  stoweidlem34  32055  stoweid  32084  dirker2re  32113  dirkerdenne0  32114  dirkerper  32117  dirkertrigeq  32122  dirkeritg  32123  fourierdlem39  32167  fourierdlem42  32170  fourierdlem47  32175  fourierdlem56  32184  fourierdlem57  32185  fourierdlem58  32186  fourierdlem60  32188  fourierdlem61  32189  fourierdlem73  32201  fourierdlem76  32204  fourierdlem77  32205  fourierdlem92  32220  fourierdlem97  32225  etransclem46  32302  m1mod0mod1  32533  2leaddle2  32694  ltsubsubaddltsub  32698  divlt1lt  33372  flsubz  33384  rege1logbrege0  33433  nn0digval  33475  reseccl  33537  recsccl  33538  recotcl  33539  dpfrac1  33556
  Copyright terms: Public domain W3C validator