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

Theorem recni 9344
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 9285 . 2
2 recni.1 . 2
31, 2sselii 3330 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1749   cc 9226   cr 9227
This theorem is referenced by:  renegcli  9616  resubcli  9617  recgt0ii  10184  ledivp1i  10204  ltdivp1i  10205  nncni  10278  2cn  10338  3cn  10342  4cn  10345  5cn  10347  6cn  10349  7cn  10351  8cn  10353  9cn  10355  8th4div3  10491  nn0cni  10537  numltc  10720  sqge0i  11894  lt2sqi  11895  le2sqi  11896  sq11i  11897  crreczi  11930  faclbnd4lem1  12010  sqrmsq2i  12816  abs3lemi  12838  0.999...  13281  ef01bndlem  13408  sin4lt0  13419  eirrlem  13426  rpnnen2lem3  13439  rpnnen2lem9  13445  rpnnen2lem11  13447  dvdslelem  13517  divalglem1  13538  divalglem2  13539  divalglem5  13541  divalglem6  13542  divalglem9  13545  prmreclem6  13922  modsubi  14041  pcoass  20296  aaliou3lem7  21556  picn  21663  sinhalfpilem  21666  cosneghalfpi  21673  sincosq1sgn  21701  sincosq2sgn  21702  sincosq3sgn  21703  sincosq4sgn  21704  sincos4thpi  21716  tan4thpi  21717  sincos6thpi  21718  pige3  21720  cosne0  21727  sinord  21731  resinf1o  21733  efif1olem2  21740  efif1olem4  21742  efifo  21744  logimul  21804  ecxp  21859  cxpsqrlem  21888  ang180lem1  21946  ang180lem2  21947  1cubrlem  21977  quartlem3  21995  asinsin  22028  acoscos  22029  asin1  22030  reasinsin  22032  acosbnd  22036  atanlogsublem  22051  atanbnd  22062  atan1  22064  log2tlbnd  22081  log2ublem1  22082  birthday  22089  basellem8  22166  basellem9  22167  cht2  22251  mumullem2  22259  chtublem  22291  chtub  22292  bposlem6  22369  bposlem7  22370  bposlem8  22371  bposlem9  22372  chebbnd1lem3  22461  chebbnd1  22462  chto1ub  22466  mulogsumlem  22521  mulog2sumlem1  22524  mulog2sumlem2  22525  mulog2sumlem3  22526  pntibndlem3  22582  nmblolbii  23878  ip0i  23904  ip1ilem  23905  ipasslem10  23918  siilem1  23930  siii  23932  normlem1  24191  normlem3  24193  normlem5  24195  normlem6  24196  norm-ii-i  24218  normsubi  24222  norm3adifii  24229  norm3lem  24230  normpar2i  24237  bcsiALT  24260  pjneli  24805  lnophmlem2  25100  nmbdoplbi  25107  nmcoplbi  25111  nmophmi  25114  nmbdfnlbi  25132  nmcfnlbi  25135  cnlnadjlem2  25151  cnlnadjlem7  25156  nmopadjlem  25172  nmopcoi  25178  nmopcoadji  25184  nmopcoadj0i  25186  unierri  25187  opsqrlem1  25223  log2le1  26175  subfaclim  26779  subfacval3  26780  problem2  27002  problem3  27003  problem4  27004  problem5  27005  circum  27021  bpoly4  27904  cos2h  28094  tan2h  28095  dvtanlem  28112  dvacos  28152  areacirc  28160  fdc  28312  rmspecsqrnq  28920  proot1ex  29242  arearect  29264  areaquad  29265  itgsinexplem1  29468  wallispilem2  29535  wallispilem4  29537  wallispi  29539  stirlinglem3  29545  stirlinglem4  29546  stirlinglem13  29555  stirlinglem15  29557  dpfrac1  30691  elogb  30694  sineq0ALT  31251  taupilem1  35052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-resscn 9285
This theorem depends on definitions:  df-bi 179  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3312  df-ss 3319
  Copyright terms: Public domain W3C validator