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

Theorem recni 9629
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 9570 . 2
2 recni.1 . 2
31, 2sselii 3500 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cc 9511   cr 9512
This theorem is referenced by:  renegcli  9903  resubcli  9904  recgt0ii  10476  ledivp1i  10496  ltdivp1i  10497  nncni  10571  2cn  10631  3cn  10635  4cn  10638  5cn  10640  6cn  10642  7cn  10644  8cn  10646  9cn  10648  8th4div3  10784  nn0cni  10832  numltc  11024  sqge0i  12255  lt2sqi  12256  le2sqi  12257  sq11i  12258  crreczi  12291  faclbnd4lem1  12371  sqrtmsq2i  13220  abs3lemi  13242  0.999...  13690  ef01bndlem  13919  sin4lt0  13930  eirrlem  13937  rpnnen2lem3  13950  rpnnen2lem9  13956  rpnnen2lem11  13958  dvdslelem  14030  divalglem1  14052  divalglem2  14053  divalglem5  14055  divalglem6  14056  divalglem9  14059  prmreclem6  14439  modsubi  14558  pcoass  21524  aaliou3lem7  22745  picn  22852  sinhalfpilem  22856  cosneghalfpi  22863  sincosq1sgn  22891  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  sincos4thpi  22906  tan4thpi  22907  sincos6thpi  22908  pige3  22910  cosne0  22917  sinord  22921  resinf1o  22923  efif1olem2  22930  efif1olem4  22932  efifo  22934  logimul  22999  ecxp  23054  cxpsqrtlem  23083  ang180lem1  23141  ang180lem2  23142  1cubrlem  23172  quartlem3  23190  asinsin  23223  acoscos  23224  asin1  23225  reasinsin  23227  acosbnd  23231  atanlogsublem  23246  atanbnd  23257  atan1  23259  log2tlbnd  23276  log2ublem1  23277  birthday  23284  basellem8  23361  basellem9  23362  cht2  23446  mumullem2  23454  chtublem  23486  chtub  23487  bposlem6  23564  bposlem7  23565  bposlem8  23566  bposlem9  23567  chebbnd1lem3  23656  chebbnd1  23657  chto1ub  23661  mulogsumlem  23716  mulog2sumlem1  23719  mulog2sumlem2  23720  mulog2sumlem3  23721  pntibndlem3  23777  nmblolbii  25714  ip0i  25740  ip1ilem  25741  ipasslem10  25754  siilem1  25766  siii  25768  normlem1  26027  normlem3  26029  normlem5  26031  normlem6  26032  norm-ii-i  26054  normsubi  26058  norm3adifii  26065  norm3lem  26066  normpar2i  26073  bcsiALT  26096  pjneli  26641  lnophmlem2  26936  nmbdoplbi  26943  nmcoplbi  26947  nmophmi  26950  nmbdfnlbi  26968  nmcfnlbi  26971  cnlnadjlem2  26987  cnlnadjlem7  26992  nmopadjlem  27008  nmopcoi  27014  nmopcoadji  27020  nmopcoadj0i  27022  unierri  27023  opsqrlem1  27059  log2le1  28023  subfaclim  28632  subfacval3  28633  problem2  29020  problem3  29021  problem4  29022  problem5  29023  circum  29040  logi  29121  iexpire  29122  bpoly4  29821  dvtanlem  30064  dvacos  30104  fdc  30238  rmspecsqrtnq  30842  arearect  31183  areaquad  31184  wallispilem2  31848  stirlinglem3  31858  stirlinglem4  31859  stirlinglem13  31868  stirlinglem15  31870  dirkerper  31878  fourierdlem24  31913  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem18  32035  etransclem23  32040  etransclem46  32063  etransclem47  32064  etransclem48  32065  etransc  32066  dpfrac1  33166  elogb  33169  sineq0ALT  33737  taupilem1  37696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator