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

Theorem recni 10037
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1 𝐴 ∈ ℝ
Assertion
Ref Expression
recni 𝐴 ∈ ℂ

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 9978 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3592 1 𝐴 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  cc 9919  cr 9920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  renegcli  10327  resubcli  10328  recgt0ii  10914  ledivp1i  10934  ltdivp1i  10935  nncni  11015  2cn  11076  3cn  11080  4cn  11083  5cn  11085  6cn  11087  7cn  11089  8cn  11091  9cn  11093  8th4div3  11237  nn0cni  11289  numltc  11513  sqge0i  12934  lt2sqi  12935  le2sqi  12936  sq11i  12937  crreczi  12972  faclbnd4lem1  13063  sqrtmsq2i  14108  abs3lemi  14130  0.999...  14593  0.999...OLD  14594  bpoly4  14771  ef01bndlem  14895  sin4lt0  14906  eirrlem  14913  rpnnen2lem3  14926  rpnnen2lem9  14932  rpnnen2lem11  14934  dvdslelem  15012  divalglem1  15098  divalglem2  15099  divalglem5  15101  divalglem6  15102  divalglem9  15105  prmreclem6  15606  modsubi  15757  pcoass  22805  aaliou3lem7  24085  picn  24192  sinhalfpilem  24196  cosneghalfpi  24203  sincosq1sgn  24231  sincosq2sgn  24232  sincosq3sgn  24233  sincosq4sgn  24234  sincos4thpi  24246  tan4thpi  24247  sincos6thpi  24248  pige3  24250  cosne0  24257  sinord  24261  resinf1o  24263  efif1olem2  24270  efif1olem4  24272  efifo  24274  logimul  24341  ecxp  24400  cxpsqrtlem  24429  elogb  24489  logblog  24511  ang180lem1  24520  ang180lem2  24521  1cubrlem  24549  quartlem3  24567  asinsin  24600  acoscos  24601  asin1  24602  reasinsin  24604  acosbnd  24608  atanlogsublem  24623  atanbnd  24634  atan1  24636  log2tlbnd  24653  log2ublem1  24654  log2le1  24658  birthday  24662  basellem8  24795  basellem9  24796  cht2  24879  mumullem2  24887  chtublem  24917  chtub  24918  bposlem6  24995  bposlem7  24996  bposlem8  24997  bposlem9  24998  chebbnd1lem3  25141  chebbnd1  25142  chto1ub  25146  mulogsumlem  25201  mulog2sumlem1  25204  mulog2sumlem2  25205  mulog2sumlem3  25206  pntibndlem3  25262  ex-ceil  27275  nmblolbii  27624  ip0i  27650  ip1ilem  27651  ipasslem10  27664  siilem1  27676  siii  27678  normlem1  27937  normlem3  27939  normlem5  27941  normlem6  27942  norm-ii-i  27964  normsubi  27968  norm3adifii  27975  norm3lem  27976  normpar2i  27983  bcsiALT  28006  pjneli  28552  lnophmlem2  28846  nmbdoplbi  28853  nmcoplbi  28857  nmophmi  28860  nmbdfnlbi  28878  nmcfnlbi  28881  cnlnadjlem2  28897  cnlnadjlem7  28902  nmopadjlem  28918  nmopcoi  28924  nmopcoadji  28930  nmopcoadj0i  28932  unierri  28933  opsqrlem1  28969  dfdec100  29550  dp20u  29559  dp2ltsuc  29567  dpfrac1  29573  dpfrac1OLD  29574  dpmul10  29577  decdiv10  29578  dpmul100  29579  dp3mul10  29580  dpmul1000  29581  dpexpp1  29590  dpadd2  29592  dpadd3  29594  dpmul  29595  dpmul4  29596  threehalves  29597  hgt750lemd  30700  hgt750lem  30703  hgt750lem2  30704  subfaclim  31144  subfacval3  31145  problem2  31533  problem2OLD  31534  problem3  31535  problem4  31536  problem5  31537  circum  31542  logi  31595  iexpire  31596  taupilem1  33138  dvacos  33468  fdc  33512  rmspecsqrtnqOLD  37290  arearect  37620  areaquad  37621  sineq0ALT  38993  wallispilem2  40046  stirlinglem3  40056  stirlinglem4  40057  stirlinglem13  40066  stirlinglem15  40068  dirkerper  40076  fourierdlem24  40111  fourierdlem103  40189  fourierdlem104  40190  sqwvfoura  40208  sqwvfourb  40209  fourierswlem  40210  fouriersw  40211  etransclem18  40232  etransclem23  40237  etransclem46  40260  etransclem47  40261  etransclem48  40262  etransc  40263  tgoldbach  41470  tgoldbachOLD  41477
  Copyright terms: Public domain W3C validator