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

Theorem recni 11035
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 10974 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3923 1 𝐴 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2104  cc 10915  cr 10916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-resscn 10974
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909
This theorem is referenced by:  0cnALT  11255  renegcli  11328  resubcli  11329  recgt0ii  11927  ledivp1i  11946  ltdivp1i  11947  2cnALT  12095  8th4div3  12239  numltc  12509  sqge0i  13951  lt2sqi  13952  le2sqi  13953  sq11i  13954  crreczi  13989  faclbnd4lem1  14053  sqrtmsq2i  15144  abs3lemi  15167  0.999...  15638  bpoly4  15814  ef01bndlem  15938  sin4lt0  15949  eirrlem  15958  rpnnen2lem3  15970  rpnnen2lem9  15976  rpnnen2lem11  15978  dvdslelem  16063  divalglem1  16148  divalglem2  16149  divalglem5  16151  divalglem6  16152  divalglem9  16155  prmreclem6  16667  modsubi  16818  pcoass  24232  aaliou3lem7  25554  picn  25661  sinhalfpilem  25665  cosneghalfpi  25672  sinhalfpip  25694  sinhalfpim  25695  coshalfpip  25696  coshalfpim  25697  sincosq1sgn  25700  sincosq2sgn  25701  sincosq3sgn  25702  sincosq4sgn  25703  sincos4thpi  25715  tan4thpi  25716  sincos6thpi  25717  pige3ALT  25721  cosne0  25730  sinord  25735  resinf1o  25737  efif1olem2  25744  efif1olem4  25746  efifo  25748  logimul  25814  ecxp  25873  cxpsqrtlem  25902  2irrexpq  25930  elogb  25965  logblog  25987  sqrt2cxp2logb9e3  25994  ang180lem1  26004  ang180lem2  26005  1cubrlem  26036  quartlem3  26054  asinsin  26087  acoscos  26088  asin1  26089  reasinsin  26091  acosbnd  26095  atanlogsublem  26110  atanbnd  26121  atan1  26123  log2tlbnd  26140  log2ublem1  26141  log2le1  26145  birthday  26149  basellem8  26282  basellem9  26283  cht2  26366  mumullem2  26374  chtublem  26404  chtub  26405  bposlem6  26482  bposlem7  26483  bposlem8  26484  bposlem9  26485  chebbnd1lem3  26664  chebbnd1  26665  chto1ub  26669  mulogsumlem  26724  mulog2sumlem1  26727  mulog2sumlem2  26728  mulog2sumlem3  26729  pntibndlem3  26785  ex-ceil  28857  nmblolbii  29206  ip0i  29232  ip1ilem  29233  ipasslem10  29246  siilem1  29258  siii  29260  normlem1  29517  normlem3  29519  normlem5  29521  normlem6  29522  norm-ii-i  29544  normsubi  29548  norm3adifii  29555  norm3lem  29556  normpar2i  29563  bcsiALT  29586  pjneli  30130  lnophmlem2  30424  nmbdoplbi  30431  nmcoplbi  30435  nmophmi  30438  nmbdfnlbi  30456  nmcfnlbi  30459  cnlnadjlem2  30475  cnlnadjlem7  30480  nmopadjlem  30496  nmopcoi  30502  nmopcoadji  30508  nmopcoadj0i  30510  unierri  30511  opsqrlem1  30547  dfdec100  31189  dp20u  31197  dp2ltsuc  31205  dpfrac1  31211  dpmul10  31214  decdiv10  31215  dpmul100  31216  dp3mul10  31217  dpmul1000  31218  dpexpp1  31227  dpadd2  31229  dpadd3  31231  dpmul  31232  dpmul4  31233  threehalves  31234  hgt750lemd  32673  hgt750lem  32676  hgt750lem2  32677  subfaclim  33195  subfacval3  33196  problem2  33669  problem3  33670  problem4  33671  problem5  33672  circum  33677  logi  33745  iexpire  33746  taupilem1  35536  dvacos  35906  fdc  35947  lcmineqlem23  40101  aks4d1p1p4  40121  aks4d1p1p7  40124  acos1half  40212  0cnALT3  40327  re1m1e0m0  40417  ipiiie0  40456  arearect  41084  areaquad  41085  sineq0ALT  42595  wallispilem2  43656  stirlinglem3  43666  stirlinglem4  43667  stirlinglem13  43676  stirlinglem15  43678  dirkerper  43686  fourierdlem24  43721  fourierdlem103  43799  fourierdlem104  43800  sqwvfoura  43818  sqwvfourb  43819  fourierswlem  43820  fouriersw  43821  etransclem18  43842  etransclem23  43847  etransclem46  43870  etransclem47  43871  etransclem48  43872  etransc  43873  tgoldbach  45327
  Copyright terms: Public domain W3C validator