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

Theorem recni 9535
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 9476 . 2
2 recni.1 . 2
31, 2sselii 3467 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1758   cc 9417   cr 9418
This theorem is referenced by:  renegcli  9807  resubcli  9808  recgt0ii  10375  ledivp1i  10395  ltdivp1i  10396  nncni  10470  2cn  10530  3cn  10534  4cn  10537  5cn  10539  6cn  10541  7cn  10543  8cn  10545  9cn  10547  8th4div3  10683  nn0cni  10729  numltc  10914  sqge0i  12110  lt2sqi  12111  le2sqi  12112  sq11i  12113  crreczi  12146  faclbnd4lem1  12226  sqrmsq2i  13033  abs3lemi  13055  0.999...  13499  ef01bndlem  13626  sin4lt0  13637  eirrlem  13644  rpnnen2lem3  13657  rpnnen2lem9  13663  rpnnen2lem11  13665  dvdslelem  13735  divalglem1  13756  divalglem2  13757  divalglem5  13759  divalglem6  13760  divalglem9  13763  prmreclem6  14140  modsubi  14259  pcoass  20995  aaliou3lem7  22215  picn  22322  sinhalfpilem  22325  cosneghalfpi  22332  sincosq1sgn  22360  sincosq2sgn  22361  sincosq3sgn  22362  sincosq4sgn  22363  sincos4thpi  22375  tan4thpi  22376  sincos6thpi  22377  pige3  22379  cosne0  22386  sinord  22390  resinf1o  22392  efif1olem2  22399  efif1olem4  22401  efifo  22403  logimul  22463  ecxp  22518  cxpsqrlem  22547  ang180lem1  22605  ang180lem2  22606  1cubrlem  22636  quartlem3  22654  asinsin  22687  acoscos  22688  asin1  22689  reasinsin  22691  acosbnd  22695  atanlogsublem  22710  atanbnd  22721  atan1  22723  log2tlbnd  22740  log2ublem1  22741  birthday  22748  basellem8  22825  basellem9  22826  cht2  22910  mumullem2  22918  chtublem  22950  chtub  22951  bposlem6  23028  bposlem7  23029  bposlem8  23030  bposlem9  23031  chebbnd1lem3  23120  chebbnd1  23121  chto1ub  23125  mulogsumlem  23180  mulog2sumlem1  23183  mulog2sumlem2  23184  mulog2sumlem3  23185  pntibndlem3  23241  nmblolbii  24668  ip0i  24694  ip1ilem  24695  ipasslem10  24708  siilem1  24720  siii  24722  normlem1  24981  normlem3  24983  normlem5  24985  normlem6  24986  norm-ii-i  25008  normsubi  25012  norm3adifii  25019  norm3lem  25020  normpar2i  25027  bcsiALT  25050  pjneli  25595  lnophmlem2  25890  nmbdoplbi  25897  nmcoplbi  25901  nmophmi  25904  nmbdfnlbi  25922  nmcfnlbi  25925  cnlnadjlem2  25941  cnlnadjlem7  25946  nmopadjlem  25962  nmopcoi  25968  nmopcoadji  25974  nmopcoadj0i  25976  unierri  25977  opsqrlem1  26013  log2le1  26923  subfaclim  27532  subfacval3  27533  problem2  27755  problem3  27756  problem4  27757  problem5  27758  circum  27775  bpoly4  28658  cos2h  28883  tan2h  28884  dvtanlem  28901  dvacos  28941  areacirc  28949  fdc  29101  rmspecsqrnq  29707  proot1ex  30029  arearect  30051  areaquad  30052  coseq0  30428  sinaover2ne0  30433  itgsinexplem1  30500  wallispilem2  30595  wallispilem4  30597  wallispi  30599  stirlinglem3  30605  stirlinglem4  30606  stirlinglem13  30615  stirlinglem15  30617  dirker2re  30621  dirkerdenne0  30622  dirkerval2  30623  dirkerper  30625  dirkertrigeqlem1  30627  dirkertrigeqlem2  30628  dirkertrigeqlem3  30629  dirkertrigeq  30630  dirkeritg  30631  dirkercncflem1  30632  fourierdlem24  30660  fourierdlem66  30702  fourierdlem95  30731  fourierdlem103  30739  fourierdlem104  30740  sqwvfoura  30758  sqwvfourb  30759  fourierswlem  30760  fouriersw  30761  dpfrac1  31946  elogb  31949  sineq0ALT  32516  taupilem1  36466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-resscn 9476
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3449  df-ss 3456
  Copyright terms: Public domain W3C validator