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

Theorem recni 9608
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1  |-  A  e.  RR
Assertion
Ref Expression
recni  |-  A  e.  CC

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 9549 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3501 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   CCcc 9490   RRcr 9491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9549
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  renegcli  9880  resubcli  9881  recgt0ii  10451  ledivp1i  10471  ltdivp1i  10472  nncni  10546  2cn  10606  3cn  10610  4cn  10613  5cn  10615  6cn  10617  7cn  10619  8cn  10621  9cn  10623  8th4div3  10759  nn0cni  10807  numltc  10996  sqge0i  12223  lt2sqi  12224  le2sqi  12225  sq11i  12226  crreczi  12259  faclbnd4lem1  12339  sqrtmsq2i  13183  abs3lemi  13205  0.999...  13653  ef01bndlem  13780  sin4lt0  13791  eirrlem  13798  rpnnen2lem3  13811  rpnnen2lem9  13817  rpnnen2lem11  13819  dvdslelem  13889  divalglem1  13911  divalglem2  13912  divalglem5  13914  divalglem6  13915  divalglem9  13918  prmreclem6  14298  modsubi  14417  pcoass  21287  aaliou3lem7  22507  picn  22614  sinhalfpilem  22617  cosneghalfpi  22624  sincosq1sgn  22652  sincosq2sgn  22653  sincosq3sgn  22654  sincosq4sgn  22655  sincos4thpi  22667  tan4thpi  22668  sincos6thpi  22669  pige3  22671  cosne0  22678  sinord  22682  resinf1o  22684  efif1olem2  22691  efif1olem4  22693  efifo  22695  logimul  22755  ecxp  22810  cxpsqrtlem  22839  ang180lem1  22897  ang180lem2  22898  1cubrlem  22928  quartlem3  22946  asinsin  22979  acoscos  22980  asin1  22981  reasinsin  22983  acosbnd  22987  atanlogsublem  23002  atanbnd  23013  atan1  23015  log2tlbnd  23032  log2ublem1  23033  birthday  23040  basellem8  23117  basellem9  23118  cht2  23202  mumullem2  23210  chtublem  23242  chtub  23243  bposlem6  23320  bposlem7  23321  bposlem8  23322  bposlem9  23323  chebbnd1lem3  23412  chebbnd1  23413  chto1ub  23417  mulogsumlem  23472  mulog2sumlem1  23475  mulog2sumlem2  23476  mulog2sumlem3  23477  pntibndlem3  23533  nmblolbii  25418  ip0i  25444  ip1ilem  25445  ipasslem10  25458  siilem1  25470  siii  25472  normlem1  25731  normlem3  25733  normlem5  25735  normlem6  25736  norm-ii-i  25758  normsubi  25762  norm3adifii  25769  norm3lem  25770  normpar2i  25777  bcsiALT  25800  pjneli  26345  lnophmlem2  26640  nmbdoplbi  26647  nmcoplbi  26651  nmophmi  26654  nmbdfnlbi  26672  nmcfnlbi  26675  cnlnadjlem2  26691  cnlnadjlem7  26696  nmopadjlem  26712  nmopcoi  26718  nmopcoadji  26724  nmopcoadj0i  26726  unierri  26727  opsqrlem1  26763  log2le1  27691  subfaclim  28300  subfacval3  28301  problem2  28523  problem3  28524  problem4  28525  problem5  28526  circum  28543  bpoly4  29426  cos2h  29651  tan2h  29652  dvtanlem  29669  dvacos  29709  areacirc  29717  fdc  29869  rmspecsqrtnq  30474  proot1ex  30794  arearect  30816  areaquad  30817  coseq0  31227  sinaover2ne0  31232  itgsinexplem1  31299  wallispilem2  31394  wallispilem4  31396  wallispi  31398  stirlinglem3  31404  stirlinglem4  31405  stirlinglem13  31414  stirlinglem15  31416  dirker2re  31420  dirkerdenne0  31421  dirkerval2  31422  dirkerper  31424  dirkertrigeqlem1  31426  dirkertrigeqlem2  31427  dirkertrigeqlem3  31428  dirkertrigeq  31429  dirkeritg  31430  dirkercncflem1  31431  fourierdlem24  31459  fourierdlem66  31501  fourierdlem95  31530  fourierdlem103  31538  fourierdlem104  31539  sqwvfoura  31557  sqwvfourb  31558  fourierswlem  31559  fouriersw  31560  dpfrac1  32265  elogb  32268  sineq0ALT  32835  taupilem1  36785
  Copyright terms: Public domain W3C validator