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

Theorem recni 8865
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1  |-  A  e.  RR
Assertion
Ref Expression
recni  |-  A  e.  CC

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 8810 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3190 1  |-  A  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   CCcc 8751   RRcr 8752
This theorem is referenced by:  renegcli  9124  resubcli  9125  recgt0ii  9678  ledivp1i  9698  ltdivp1i  9699  nncni  9772  2cn  9832  3cn  9834  4cn  9836  5p2e7  9876  5p3e8  9877  5p4e9  9878  5p5e10  9879  6p2e8  9880  6p3e9  9881  6p4e10  9882  7p2e9  9883  7p3e10  9884  8p2e10  9885  5t2e10  9891  8th4div3  9951  halfpm6th  9952  nn0cni  9993  numltc  10160  sqge0i  11207  lt2sqi  11208  le2sqi  11209  sq11i  11210  crreczi  11242  faclbnd4lem1  11322  rddif  11840  sqrmsq2i  11887  abs3lemi  11909  geo2sum  12345  geo2lim  12347  0.999...  12353  efcllem  12375  efi4p  12433  ef01bndlem  12480  cos2bnd  12484  sin4lt0  12491  eirrlem  12498  rpnnen2lem3  12511  rpnnen2lem9  12517  rpnnen2lem11  12519  dvdslelem  12589  divalglem1  12609  divalglem2  12610  divalglem5  12612  divalglem6  12613  divalglem9  12616  prmreclem6  12984  modsubi  13103  prmlem1  13125  pcoass  18538  iscmet3lem3  18732  mbfi1fseqlem6  19091  aaliou3lem2  19739  aaliou3lem7  19745  sinhalfpilem  19850  cosneghalfpi  19854  efhalfpi  19855  cospi  19856  efipi  19857  sin2pi  19859  cos2pi  19860  ef2pi  19861  ef2kpi  19862  efper  19863  sinperlem  19864  sin2kpi  19867  cos2kpi  19868  sin2pim  19869  cos2pim  19870  sinmpi  19871  cosmpi  19872  sinppi  19873  cosppi  19874  efimpi  19875  sinhalfpip  19876  sinhalfpim  19877  coshalfpip  19878  coshalfpim  19879  ptolemy  19880  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  sinq12gt0  19891  sinq34lt0t  19893  cosq14gt0  19894  cosq14ge0  19895  sincosq1eq  19896  sincos4thpi  19897  tan4thpi  19898  sincos6thpi  19899  sincos3rdpi  19900  pige3  19901  abssinper  19902  sinkpi  19903  coskpi  19904  sineq0  19905  coseq1  19906  efeq1  19907  cosne0  19908  sinord  19912  resinf1o  19914  efif1olem2  19921  efif1olem4  19923  efifo  19925  eff1o  19927  logneg  19957  logm1  19958  eflogeq  19971  argimgt0  19982  logimul  19984  logneg2  19985  logf1o2  20013  ecxp  20036  cxpsqrlem  20065  cxpsqr  20066  abscxpbnd  20109  root1eq1  20111  cxpeq  20113  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  pythag  20131  1cubrlem  20153  quartlem3  20171  acosf  20186  acosneg  20199  asinsin  20204  acoscos  20205  asin1  20206  acos1  20207  reasinsin  20208  acosbnd  20212  sinacos  20217  atanlogsublem  20227  atanlogsub  20228  atantan  20235  atanbndlem  20237  atanbnd  20238  atan1  20240  log2tlbnd  20257  log2ublem1  20258  birthday  20265  basellem1  20334  basellem8  20341  basellem9  20342  cht2  20426  mumullem2  20434  chtublem  20466  chtub  20467  bposlem6  20544  bposlem7  20545  bposlem8  20546  bposlem9  20547  lgsdir2lem1  20578  lgsdir2lem5  20582  chebbnd1lem3  20636  chebbnd1  20637  chto1ub  20641  mulogsumlem  20696  mulog2sumlem1  20699  mulog2sumlem2  20700  mulog2sumlem3  20701  pntibndlem3  20757  nmblolbii  21393  ip0i  21419  ip1ilem  21420  ipasslem10  21433  siilem1  21445  siii  21447  normlem1  21705  normlem3  21707  normlem5  21709  normlem6  21710  norm-ii-i  21732  normsubi  21736  norm3adifii  21743  norm3lem  21744  normpar2i  21751  bcsiALT  21774  pjneli  22318  lnophmlem2  22613  nmbdoplbi  22620  nmcoplbi  22624  nmophmi  22627  nmbdfnlbi  22645  nmcfnlbi  22648  cnlnadjlem2  22664  cnlnadjlem7  22669  nmopadjlem  22685  nmopcoi  22691  nmopcoadji  22697  nmopcoadj0i  22699  unierri  22700  opsqrlem1  22736  ballotlem2  23063  log2le1  23424  subfaclim  23734  subfacval3  23735  circum  24022  faclimlem8  24124  bpoly2  24864  bpoly3  24865  bpoly4  24866  dvreacos  25027  areacirc  25034  cntrset  25705  fdc  26558  cntotbnd  26623  rmspecsqrnq  27094  proot1ex  27623  itgsinexplem1  27851  stoweidlem13  27865  wallispilem4  27920  stirlinglem3  27928  stirlinglem4  27929  stirlinglem13  27938  stirlinglem15  27940  dpfrac1  28496  elogb  28513
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator