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

Theorem recni 9611
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 9552 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3486 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   CCcc 9493   RRcr 9494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-resscn 9552
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  renegcli  9885  resubcli  9886  recgt0ii  10458  ledivp1i  10478  ltdivp1i  10479  nncni  10553  2cn  10613  3cn  10617  4cn  10620  5cn  10622  6cn  10624  7cn  10626  8cn  10628  9cn  10630  8th4div3  10766  nn0cni  10814  numltc  11006  sqge0i  12237  lt2sqi  12238  le2sqi  12239  sq11i  12240  crreczi  12273  faclbnd4lem1  12353  sqrtmsq2i  13202  abs3lemi  13224  0.999...  13672  ef01bndlem  13901  sin4lt0  13912  eirrlem  13919  rpnnen2lem3  13932  rpnnen2lem9  13938  rpnnen2lem11  13940  dvdslelem  14012  divalglem1  14034  divalglem2  14035  divalglem5  14037  divalglem6  14038  divalglem9  14041  prmreclem6  14421  modsubi  14540  pcoass  21502  aaliou3lem7  22723  picn  22830  sinhalfpilem  22834  cosneghalfpi  22841  sincosq1sgn  22869  sincosq2sgn  22870  sincosq3sgn  22871  sincosq4sgn  22872  sincos4thpi  22884  tan4thpi  22885  sincos6thpi  22886  pige3  22888  cosne0  22895  sinord  22899  resinf1o  22901  efif1olem2  22908  efif1olem4  22910  efifo  22912  logimul  22977  ecxp  23032  cxpsqrtlem  23061  ang180lem1  23119  ang180lem2  23120  1cubrlem  23150  quartlem3  23168  asinsin  23201  acoscos  23202  asin1  23203  reasinsin  23205  acosbnd  23209  atanlogsublem  23224  atanbnd  23235  atan1  23237  log2tlbnd  23254  log2ublem1  23255  birthday  23262  basellem8  23339  basellem9  23340  cht2  23424  mumullem2  23432  chtublem  23464  chtub  23465  bposlem6  23542  bposlem7  23543  bposlem8  23544  bposlem9  23545  chebbnd1lem3  23634  chebbnd1  23635  chto1ub  23639  mulogsumlem  23694  mulog2sumlem1  23697  mulog2sumlem2  23698  mulog2sumlem3  23699  pntibndlem3  23755  nmblolbii  25692  ip0i  25718  ip1ilem  25719  ipasslem10  25732  siilem1  25744  siii  25746  normlem1  26005  normlem3  26007  normlem5  26009  normlem6  26010  norm-ii-i  26032  normsubi  26036  norm3adifii  26043  norm3lem  26044  normpar2i  26051  bcsiALT  26074  pjneli  26619  lnophmlem2  26914  nmbdoplbi  26921  nmcoplbi  26925  nmophmi  26928  nmbdfnlbi  26946  nmcfnlbi  26949  cnlnadjlem2  26965  cnlnadjlem7  26970  nmopadjlem  26986  nmopcoi  26992  nmopcoadji  26998  nmopcoadj0i  27000  unierri  27001  opsqrlem1  27037  log2le1  28001  subfaclim  28610  subfacval3  28611  problem2  28998  problem3  28999  problem4  29000  problem5  29001  circum  29018  bpoly4  29797  dvtanlem  30040  dvacos  30080  fdc  30214  rmspecsqrtnq  30818  arearect  31159  areaquad  31160  wallispilem2  31802  stirlinglem3  31812  stirlinglem4  31813  stirlinglem13  31822  stirlinglem15  31824  dirkerper  31832  fourierdlem24  31867  fourierdlem103  31946  fourierdlem104  31947  sqwvfoura  31965  sqwvfourb  31966  fourierswlem  31967  fouriersw  31968  etransclem18  31989  etransclem23  31994  etransclem46  32017  etransclem47  32018  etransclem48  32019  etransc  32020  dpfrac1  33036  elogb  33039  sineq0ALT  33605  taupilem1  37571
  Copyright terms: Public domain W3C validator