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

Theorem recni 9905
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 9846 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3561 1 𝐴 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  cc 9787  cr 9788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-resscn 9846
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-in 3543  df-ss 3550
This theorem is referenced by:  renegcli  10190  resubcli  10191  recgt0ii  10775  ledivp1i  10795  ltdivp1i  10796  nncni  10874  2cn  10935  3cn  10939  4cn  10942  5cn  10944  6cn  10946  7cn  10948  8cn  10950  9cn  10952  8th4div3  11096  nn0cni  11148  numltc  11357  sqge0i  12765  lt2sqi  12766  le2sqi  12767  sq11i  12768  crreczi  12803  faclbnd4lem1  12894  sqrtmsq2i  13918  abs3lemi  13940  0.999...  14394  0.999...OLD  14395  bpoly4  14572  ef01bndlem  14696  sin4lt0  14707  eirrlem  14714  rpnnen2lem3  14727  rpnnen2lem9  14733  rpnnen2lem11  14735  dvdslelem  14812  divalglem1  14898  divalglem2  14899  divalglem5  14901  divalglem6  14902  divalglem9  14905  prmreclem6  15406  modsubi  15557  pcoass  22560  aaliou3lem7  23822  picn  23929  sinhalfpilem  23933  cosneghalfpi  23940  sincosq1sgn  23968  sincosq2sgn  23969  sincosq3sgn  23970  sincosq4sgn  23971  sincos4thpi  23983  tan4thpi  23984  sincos6thpi  23985  pige3  23987  cosne0  23994  sinord  23998  resinf1o  24000  efif1olem2  24007  efif1olem4  24009  efifo  24011  logimul  24078  ecxp  24133  cxpsqrtlem  24162  elogb  24222  logblog  24244  ang180lem1  24253  ang180lem2  24254  1cubrlem  24282  quartlem3  24300  asinsin  24333  acoscos  24334  asin1  24335  reasinsin  24337  acosbnd  24341  atanlogsublem  24356  atanbnd  24367  atan1  24369  log2tlbnd  24386  log2ublem1  24387  log2le1  24391  birthday  24395  basellem8  24528  basellem9  24529  cht2  24612  mumullem2  24620  chtublem  24650  chtub  24651  bposlem6  24728  bposlem7  24729  bposlem8  24730  bposlem9  24731  chebbnd1lem3  24874  chebbnd1  24875  chto1ub  24879  mulogsumlem  24934  mulog2sumlem1  24937  mulog2sumlem2  24938  mulog2sumlem3  24939  pntibndlem3  24995  ex-ceil  26460  nmblolbii  26841  ip0i  26867  ip1ilem  26868  ipasslem10  26881  siilem1  26893  siii  26895  normlem1  27154  normlem3  27156  normlem5  27158  normlem6  27159  norm-ii-i  27181  normsubi  27185  norm3adifii  27192  norm3lem  27193  normpar2i  27200  bcsiALT  27223  pjneli  27769  lnophmlem2  28063  nmbdoplbi  28070  nmcoplbi  28074  nmophmi  28077  nmbdfnlbi  28095  nmcfnlbi  28098  cnlnadjlem2  28114  cnlnadjlem7  28119  nmopadjlem  28135  nmopcoi  28141  nmopcoadji  28147  nmopcoadj0i  28149  unierri  28150  opsqrlem1  28186  subfaclim  30227  subfacval3  30228  problem2  30616  problem2OLD  30617  problem3  30618  problem4  30619  problem5  30620  circum  30625  logi  30676  iexpire  30677  taupilem1  32144  dvacos  32467  fdc  32511  rmspecsqrtnqOLD  36289  arearect  36620  areaquad  36621  sineq0ALT  37995  wallispilem2  38760  stirlinglem3  38770  stirlinglem4  38771  stirlinglem13  38780  stirlinglem15  38782  dirkerper  38790  fourierdlem24  38825  fourierdlem103  38903  fourierdlem104  38904  sqwvfoura  38922  sqwvfourb  38923  fourierswlem  38924  fouriersw  38925  etransclem18  38946  etransclem23  38951  etransclem46  38974  etransclem47  38975  etransclem48  38976  etransc  38977  tgoldbach  40034  tgoldbachOLD  40041  dpfrac1  42272  dpfrac1OLD  42273
  Copyright terms: Public domain W3C validator