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

Theorem recni 9104
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 9049 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3347 1  |-  A  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   CCcc 8990   RRcr 8991
This theorem is referenced by:  renegcli  9364  resubcli  9365  recgt0ii  9918  ledivp1i  9938  ltdivp1i  9939  nncni  10012  2cn  10072  3cn  10074  4cn  10076  5p2e7  10118  5p3e8  10119  5p4e9  10120  5p5e10  10121  6p2e8  10122  6p3e9  10123  6p4e10  10124  7p2e9  10125  7p3e10  10126  8p2e10  10127  5t2e10  10133  8th4div3  10193  halfpm6th  10194  nn0cni  10235  numltc  10404  sqge0i  11471  lt2sqi  11472  le2sqi  11473  sq11i  11474  crreczi  11506  faclbnd4lem1  11586  rddif  12146  sqrmsq2i  12193  abs3lemi  12215  geo2sum  12652  geo2lim  12654  0.999...  12660  efcllem  12682  efi4p  12740  ef01bndlem  12787  cos2bnd  12791  sin4lt0  12798  eirrlem  12805  rpnnen2lem3  12818  rpnnen2lem9  12824  rpnnen2lem11  12826  dvdslelem  12896  divalglem1  12916  divalglem2  12917  divalglem5  12919  divalglem6  12920  divalglem9  12923  prmreclem6  13291  modsubi  13410  prmlem1  13432  pcoass  19051  iscmet3lem3  19245  mbfi1fseqlem6  19614  aaliou3lem2  20262  aaliou3lem7  20268  sinhalfpilem  20376  cosneghalfpi  20380  efhalfpi  20381  cospi  20382  efipi  20383  sin2pi  20385  cos2pi  20386  ef2pi  20387  ef2kpi  20388  efper  20389  sinperlem  20390  sin2kpi  20393  cos2kpi  20394  sin2pim  20395  cos2pim  20396  sinmpi  20397  cosmpi  20398  sinppi  20399  cosppi  20400  efimpi  20401  sinhalfpip  20402  sinhalfpim  20403  coshalfpip  20404  coshalfpim  20405  ptolemy  20406  sincosq1sgn  20408  sincosq2sgn  20409  sincosq3sgn  20410  sincosq4sgn  20411  sinq12gt0  20417  sinq34lt0t  20419  cosq14gt0  20420  cosq14ge0  20421  sincosq1eq  20422  sincos4thpi  20423  tan4thpi  20424  sincos6thpi  20425  sincos3rdpi  20426  pige3  20427  abssinper  20428  sinkpi  20429  coskpi  20430  sineq0  20431  coseq1  20432  efeq1  20433  cosne0  20434  sinord  20438  resinf1o  20440  efif1olem2  20447  efif1olem4  20449  efifo  20451  eff1o  20453  logneg  20484  logm1  20485  eflogeq  20498  argimgt0  20509  logimul  20511  logneg2  20512  logf1o2  20543  ecxp  20566  cxpsqrlem  20595  cxpsqr  20596  abscxpbnd  20639  root1eq1  20641  cxpeq  20643  ang180lem1  20653  ang180lem2  20654  ang180lem3  20655  ang180lem4  20656  1cubrlem  20683  quartlem3  20701  acosf  20716  acosneg  20729  asinsin  20734  acoscos  20735  asin1  20736  acos1  20737  reasinsin  20738  acosbnd  20742  sinacos  20747  atanlogsublem  20757  atanlogsub  20758  atantan  20765  atanbndlem  20767  atanbnd  20768  atan1  20770  log2tlbnd  20787  log2ublem1  20788  birthday  20795  basellem1  20865  basellem8  20872  basellem9  20873  cht2  20957  mumullem2  20965  chtublem  20997  chtub  20998  bposlem6  21075  bposlem7  21076  bposlem8  21077  bposlem9  21078  lgsdir2lem1  21109  lgsdir2lem5  21113  chebbnd1lem3  21167  chebbnd1  21168  chto1ub  21172  mulogsumlem  21227  mulog2sumlem1  21230  mulog2sumlem2  21231  mulog2sumlem3  21232  pntibndlem3  21288  nmblolbii  22302  ip0i  22328  ip1ilem  22329  ipasslem10  22342  siilem1  22354  siii  22356  normlem1  22614  normlem3  22616  normlem5  22618  normlem6  22619  norm-ii-i  22641  normsubi  22645  norm3adifii  22652  norm3lem  22653  normpar2i  22660  bcsiALT  22683  pjneli  23227  lnophmlem2  23522  nmbdoplbi  23529  nmcoplbi  23533  nmophmi  23536  nmbdfnlbi  23554  nmcfnlbi  23557  cnlnadjlem2  23573  cnlnadjlem7  23578  nmopadjlem  23594  nmopcoi  23600  nmopcoadji  23606  nmopcoadj0i  23608  unierri  23609  opsqrlem1  23645  log2le1  24409  subfaclim  24876  subfacval3  24877  circum  25113  bpoly2  26105  bpoly3  26106  bpoly4  26107  dvreacos  26293  areacirc  26299  fdc  26451  cntotbnd  26507  rmspecsqrnq  26971  proot1ex  27499  itgsinexplem1  27726  wallispilem2  27793  wallispilem4  27795  wallispi  27797  stirlinglem3  27803  stirlinglem4  27804  stirlinglem13  27813  stirlinglem15  27815  dpfrac1  28517  elogb  28534  sineq0ALT  29051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9049
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator