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

Theorem recn 9655
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 9622 . 2  |-  RR  C_  CC
21sseli 3440 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   CCcc 9563   RRcr 9564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-resscn 9622
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  mulid1  9666  recnd  9695  pnfnre  9708  mnfnre  9709  mul02  9837  renegcli  9961  resubcl  9964  negn0  10076  negf1o  10077  ltaddsub2  10117  leaddsub2  10119  leltadd  10126  ltaddpos  10132  ltaddpos2  10133  posdif  10135  lenegcon1  10146  lenegcon2  10147  addge01  10152  addge02  10153  leaddle0  10157  mullt0  10161  recex  10272  ltm1  10473  prodgt02  10479  prodge02  10481  ltmul2  10484  lemul1  10485  lemul2  10486  lemul1a  10487  lemul2a  10488  ltmulgt12  10494  lemulge12  10496  gt0div  10499  ge0div  10500  mulge0b  10503  mulle0b  10504  ltmuldiv2  10507  ltdivmul  10508  ledivmul  10509  ltdivmul2  10510  lt2mul2div  10511  ledivmul2  10512  ledivmul2OLD  10513  lemuldiv2  10515  ltdiv2  10520  ltrec1  10521  lerec2  10522  ledivdiv  10523  lediv2  10524  ltdiv23  10525  lediv23  10526  lediv12a  10527  recp1lt1  10532  ledivp1  10536  negfi  10582  fiminre  10583  infm3lem  10595  supmul  10607  riotaneg  10614  negiso  10615  cju  10633  nnge1  10663  halfpos  10872  lt2halves  10876  addltmul  10877  avgle1  10881  avgle2  10882  avgle  10883  nnrecl  10896  elznn0  10981  elznn  10982  elz2  10983  zmulcl  11014  gtndiv  11042  zeo  11050  eqreznegel  11278  supminf  11279  supminfOLD  11280  rebtwnz  11292  irradd  11317  irrmul  11318  max0sub  11518  xnegneg  11536  rexsub  11555  xnegid  11558  xaddcom  11560  xaddid1  11561  xnegdi  11563  xaddass  11564  rexmul  11586  xmulasslem3  11601  xadddilem  11609  divelunit  11803  fzonmapblen  11992  ico01fl0  12085  flzadd  12091  ltdifltdiv  12098  dfceil2  12100  intfrac2  12117  fldiv2  12120  flpmodeq  12133  mod0  12135  negmod0  12137  modlt  12139  modfrac  12142  flmod  12143  intfrac  12144  modmulnn  12146  modvalp1  12147  modid  12153  modcyc  12164  modcyc2  12165  modadd1  12166  modaddabs  12167  muladdmodid  12169  negmod  12170  modadd2mod  12172  modmul1  12175  modaddmulmod  12188  moddi  12189  modsubdir  12190  modirr  12192  expgt1  12342  mulexpz  12344  leexp1a  12363  expubnd  12365  sqgt0  12375  lt2sq  12380  le2sq  12381  sqge0  12383  sumsqeq0  12385  sqlecan  12413  bernneq  12430  bernneq2  12431  expnbnd  12433  digit2  12437  digit1  12438  swrdccatin2  12880  swrdccat3blem  12888  cshweqrep  12957  crre  13226  crim  13227  reim0  13230  mulre  13233  rere  13234  remul2  13242  rediv  13243  immul2  13249  imdiv  13250  cjre  13251  cjreim  13272  rennim  13351  resqrex  13363  resqreu  13365  resqrtcl  13366  resqrtthlem  13367  sqrtneglem  13379  sqrtneg  13380  absreimsq  13404  absreim  13405  absnid  13410  leabs  13411  absre  13413  absresq  13414  sqabs  13419  max0add  13422  absz  13423  absdiflt  13429  absdifle  13430  lenegsq  13432  abssuble0  13440  absmax  13441  rddif  13452  absrdbnd  13453  o1rlimmul  13731  caurcvg2  13793  reefcl  14190  efgt0  14206  reeftlcl  14211  resinval  14238  recosval  14239  resin4p  14241  recos4p  14242  resincl  14243  recoscl  14244  retancl  14245  resinhcl  14259  rpcoshcl  14260  retanhcl  14262  tanhlt1  14263  tanhbnd  14264  efieq  14266  sinbnd  14283  cosbnd  14284  absefi  14299  odd2np1  14414  bezoutlem1  14552  xrsdsreclb  19064  remulg  19224  resubdrg  19225  remetdval  21856  bl2ioo  21859  ioo2bl  21860  cnperf  21887  icccvx  22027  tchcph  22260  shft2rab  22510  volsup2  22612  volcn  22613  c1lip1  22998  plyreres  23285  aalioulem3  23339  taylthlem2  23378  reeff1o  23451  reefgim  23454  sincosq1sgn  23502  sincosq2sgn  23503  sincosq3sgn  23504  sincosq4sgn  23505  sinq12gt0  23511  pige3  23521  efif1olem4  23543  efifo  23545  relogrn  23560  logrnaddcl  23573  relogoprlem  23589  advlog  23648  advlogexp  23649  logtayl  23654  recxpcl  23669  rpcxpcl  23670  cxpge0  23677  dvcxp1  23729  logreclem  23748  relogbreexp  23761  relogbcxp  23771  angpieqvd  23806  atanre  23860  basellem9  24064  log2sumbnd  24431  brbtwn2  24984  colinearalglem4  24988  colinearalg  24989  readdsubgo  26130  nvsge0  26341  nmoub3i  26463  nmlnoubi  26486  isblo3i  26491  ipasslem3  26523  ipasslem9  26528  ipasslem11  26530  hmopm  27723  riesz1  27767  leopmuli  27835  leopmul  27836  leopmul2i  27837  leopnmid  27840  nmopleid  27841  cdj1i  28135  cdj3lem1  28136  cdj3i  28143  addltmulALT  28148  rexdiv  28444  xdivid  28446  xdiv0  28447  rmulccn  28783  sgnneg  29460  lediv2aALT  30370  nndivlub  31167  cos2h  31981  tan2h  31982  poimir  32018  mblfinlem2  32023  mblfinlem4  32025  dvtanlemOLD  32036  itg2addnclem  32038  itg2addnclem2  32039  dvasin  32073  areacirclem1  32077  areacirclem2  32078  areacirclem4  32080  areacirclem5  32081  areacirc  32082  expmordi  35840  areaquad  36146  radcnvrat  36707  lhe4.4ex1a  36722  expgrowthi  36726  mulltgt0  37383  refsum2cnlem1  37398  dstregt0  37529  ltaddneg  37546  suplesup  37600  fmul01lt1lem1  37700  lptre2pt  37758  dvcosre  37819  itgsin0pilem1  37864  itgsinexplem1  37868  volioc  37887  stoweidlem7  37905  stoweidlem10  37908  stoweidlem19  37917  stoweidlem34  37933  stoweid  37963  dirker2re  37992  dirkerdenne0  37993  dirkerper  37996  dirkertrigeq  38001  dirkeritg  38002  fourierdlem39  38047  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem47  38055  fourierdlem56  38064  fourierdlem57  38065  fourierdlem58  38066  fourierdlem60  38068  fourierdlem61  38069  fourierdlem73  38081  fourierdlem76  38084  fourierdlem77  38085  fourierdlem92  38100  fourierdlem97  38105  etransclem46  38183  volico  38401  m1mod0mod1  38761  bgoldbtbndlem2  38939  2leaddle2  39086  ltsubsubaddltsub  39090  divlt1lt  40583  flsubz  40593  rege1logbrege0  40642  nn0digval  40684  reseccl  40746  recsccl  40747  recotcl  40748  dpfrac1  40765
  Copyright terms: Public domain W3C validator