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

Theorem recn 8823
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 8790 . 2  |-  RR  C_  CC
21sseli 3177 1  |-  ( A  e.  RR  ->  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:  mulid1  8831  recnd  8857  pnfnre  8870  mnfnre  8871  mul02  8986  renegcli  9104  resubcl  9107  ltaddsub2  9245  leaddsub2  9247  leltadd  9254  ltaddpos  9260  ltaddpos2  9261  posdif  9263  lenegcon1  9274  lenegcon2  9275  addge01  9280  addge02  9281  mullt0  9289  recex  9396  ltm1  9592  prodgt02  9598  prodge02  9600  ltmul2  9603  lemul1  9604  lemul2  9605  lemul1a  9606  lemul2a  9607  ltmulgt12  9613  lemulge12  9615  gt0div  9618  ge0div  9619  ltmuldiv2  9623  ltdivmul  9624  ledivmul  9625  ledivmulOLD  9626  ltdivmul2  9627  lt2mul2div  9628  ledivmul2  9629  ledivmul2OLD  9630  lemuldiv2  9632  ltdiv2  9637  ltrec1  9639  lerec2  9640  ledivdiv  9641  lediv2  9642  ltdiv23  9643  lediv23  9644  lediv12a  9645  recp1lt1  9650  ledivp1  9654  infm3lem  9708  supmul  9718  riotaneg  9725  negiso  9726  cju  9738  nnge1  9768  halfpos  9938  lt2halves  9942  addltmul  9943  avgle1  9947  avgle2  9948  avgle  9949  nnrecl  9959  elznn0  10034  elznn  10035  elz2  10036  zmulcl  10062  gtndiv  10085  zeo  10093  uzindOLD  10102  eqreznegel  10299  negn0  10300  supminf  10301  rebtwnz  10311  irradd  10336  irrmul  10337  max0sub  10519  xnegneg  10537  rexsub  10556  xnegid  10559  xaddcom  10561  xaddid1  10562  xnegdi  10564  xaddass  10565  rexmul  10587  xmulasslem3  10602  xadddilem  10610  flzadd  10947  intfrac2  10958  fldiv2  10961  mod0  10974  negmod0  10975  modlt  10977  modfrac  10980  flmod  10981  intfrac  10982  modmulnn  10984  modid  10989  modcyc  10995  modcyc2  10996  modadd1  10997  modmul1  10998  moddi  11003  modsubdir  11004  modirr  11005  expgt1  11136  mulexpz  11138  leexp1a  11156  expubnd  11158  sqgt0  11168  lt2sq  11173  le2sq  11174  sqge0  11176  sumsqeq0  11178  sqlecan  11205  bernneq  11223  bernneq2  11224  expnbnd  11226  digit2  11230  digit1  11231  crre  11595  crim  11596  reim0  11599  mulre  11602  rere  11603  remul2  11611  rediv  11612  immul2  11618  imdiv  11619  cjre  11620  cjreim  11641  rennim  11720  resqrex  11732  resqreu  11734  resqrcl  11735  resqrthlem  11736  sqrneglem  11748  sqrneg  11749  absreimsq  11773  absreim  11774  absnid  11779  leabs  11780  absre  11782  absresq  11783  sqabs  11788  max0add  11791  absz  11792  absdiflt  11797  absdifle  11798  lenegsq  11800  abssuble0  11808  absmax  11809  rddif  11820  absrdbnd  11821  o1rlimmul  12088  caurcvg2  12146  reefcl  12364  efgt0  12379  reeftlcl  12384  resinval  12411  recosval  12412  resin4p  12414  recos4p  12415  resincl  12416  recoscl  12417  retancl  12418  resinhcl  12432  rpcoshcl  12433  retanhcl  12435  tanhlt1  12436  tanhbnd  12437  efieq  12439  sinbnd  12456  cosbnd  12457  absefi  12472  odd2np1  12583  bezoutlem1  12713  xrsdsreclb  16414  resubdrg  16419  remetdval  18291  bl2ioo  18294  ioo2bl  18295  cnperf  18321  icccvx  18444  tchcph  18663  shft2rab  18863  volsup2  18956  volcn  18957  c1lip1  19340  plyreres  19659  aalioulem3  19710  taylthlem2  19749  reeff1o  19819  reefgim  19822  sincosq1sgn  19862  sincosq2sgn  19863  sincosq3sgn  19864  sincosq4sgn  19865  sinq12gt0  19871  pige3  19881  efif1olem4  19903  efifo  19905  relogrn  19915  logrnaddcl  19927  relogoprlem  19940  advlog  19997  advlogexp  19998  logtayl  20003  recxpcl  20018  rpcxpcl  20019  cxpge0  20026  dvcxp1  20078  logreclem  20112  angpieqvd  20124  atanre  20177  basellem9  20322  log2sumbnd  20689  readdsubgo  21014  nvsge0  21223  nmoub3i  21345  nmlnoubi  21368  isblo3i  21373  ipasslem3  21405  ipasslem9  21410  ipasslem11  21412  hmopm  22597  riesz1  22641  leopmuli  22709  leopmul  22710  leopmul2i  22711  leopnmid  22714  nmopleid  22715  cdj1i  23009  cdj3lem1  23010  cdj3i  23017  addltmulALT  23022  modaddabs  23418  lediv2aALT  23420  divelunit  23486  mulge0b  23492  mulle0b  23493  brbtwn2  23943  colinearalglem4  23947  colinearalg  23948  nndivlub  24307  dvreasin  24333  areacirclem2  24335  areacirclem3  24336  areacirclem4  24337  areacirclem5  24339  areacirclem6  24340  areacirc  24341  truni1  24916  dmse1  25014  mslb1  25018  2wsms  25019  iintlem1  25021  trran  25025  trnij  25026  cnvtr  25027  lvsovso  25037  clsmulrv  25094  divclrvd  25106  rdr  25846  expmordi  26443  lhe4.4ex1a  26957  expgrowthi  26961  mulltgt0  27104  refsum2cnlem1  27119  fmul01  27121  fmul01lt1lem1  27125  fmul01lt1lem2  27126  eluzelcn  27135  dvcosre  27152  itgsin0pilem1  27155  itgsinexplem1  27159  stoweidlem7  27167  stoweidlem10  27170  stoweidlem11  27171  stoweidlem13  27173  stoweidlem19  27179  stoweidlem20  27180  stoweidlem22  27182  stoweidlem23  27183  stoweidlem24  27184  stoweidlem26  27186  stoweidlem32  27192  stoweidlem34  27194  stoweidlem36  27196  stoweidlem44  27204  stoweid  27223  reseccl  27495  recsccl  27496  recotcl  27497  dpfrac1  27514
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