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

Theorem recni 10090
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 10031 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3633 1 𝐴 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  cc 9972  cr 9973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  renegcli  10380  resubcli  10381  recgt0ii  10967  ledivp1i  10987  ltdivp1i  10988  nncni  11068  2cn  11129  3cn  11133  4cn  11136  5cn  11138  6cn  11140  7cn  11142  8cn  11144  9cn  11146  8th4div3  11290  nn0cni  11342  numltc  11566  sqge0i  12991  lt2sqi  12992  le2sqi  12993  sq11i  12994  crreczi  13029  faclbnd4lem1  13120  sqrtmsq2i  14171  abs3lemi  14193  0.999...  14656  0.999...OLD  14657  bpoly4  14834  ef01bndlem  14958  sin4lt0  14969  eirrlem  14976  rpnnen2lem3  14989  rpnnen2lem9  14995  rpnnen2lem11  14997  dvdslelem  15078  divalglem1  15164  divalglem2  15165  divalglem5  15167  divalglem6  15168  divalglem9  15171  prmreclem6  15672  modsubi  15823  pcoass  22870  aaliou3lem7  24149  picn  24256  sinhalfpilem  24260  cosneghalfpi  24267  sincosq1sgn  24295  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  sincos4thpi  24310  tan4thpi  24311  sincos6thpi  24312  pige3  24314  cosne0  24321  sinord  24325  resinf1o  24327  efif1olem2  24334  efif1olem4  24336  efifo  24338  logimul  24405  ecxp  24464  cxpsqrtlem  24493  elogb  24553  logblog  24575  ang180lem1  24584  ang180lem2  24585  1cubrlem  24613  quartlem3  24631  asinsin  24664  acoscos  24665  asin1  24666  reasinsin  24668  acosbnd  24672  atanlogsublem  24687  atanbnd  24698  atan1  24700  log2tlbnd  24717  log2ublem1  24718  log2le1  24722  birthday  24726  basellem8  24859  basellem9  24860  cht2  24943  mumullem2  24951  chtublem  24981  chtub  24982  bposlem6  25059  bposlem7  25060  bposlem8  25061  bposlem9  25062  chebbnd1lem3  25205  chebbnd1  25206  chto1ub  25210  mulogsumlem  25265  mulog2sumlem1  25268  mulog2sumlem2  25269  mulog2sumlem3  25270  pntibndlem3  25326  ex-ceil  27435  nmblolbii  27782  ip0i  27808  ip1ilem  27809  ipasslem10  27822  siilem1  27834  siii  27836  normlem1  28095  normlem3  28097  normlem5  28099  normlem6  28100  norm-ii-i  28122  normsubi  28126  norm3adifii  28133  norm3lem  28134  normpar2i  28141  bcsiALT  28164  pjneli  28710  lnophmlem2  29004  nmbdoplbi  29011  nmcoplbi  29015  nmophmi  29018  nmbdfnlbi  29036  nmcfnlbi  29039  cnlnadjlem2  29055  cnlnadjlem7  29060  nmopadjlem  29076  nmopcoi  29082  nmopcoadji  29088  nmopcoadj0i  29090  unierri  29091  opsqrlem1  29127  dfdec100  29704  dp20u  29713  dp2ltsuc  29721  dpfrac1  29727  dpfrac1OLD  29728  dpmul10  29731  decdiv10  29732  dpmul100  29733  dp3mul10  29734  dpmul1000  29735  dpexpp1  29744  dpadd2  29746  dpadd3  29748  dpmul  29749  dpmul4  29750  threehalves  29751  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  subfaclim  31296  subfacval3  31297  problem2  31685  problem2OLD  31686  problem3  31687  problem4  31688  problem5  31689  circum  31694  logi  31746  iexpire  31747  taupilem1  33297  dvacos  33627  fdc  33671  rmspecsqrtnqOLD  37788  arearect  38118  areaquad  38119  sineq0ALT  39487  wallispilem2  40601  stirlinglem3  40611  stirlinglem4  40612  stirlinglem13  40621  stirlinglem15  40623  dirkerper  40631  fourierdlem24  40666  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  etransclem18  40787  etransclem23  40792  etransclem46  40815  etransclem47  40816  etransclem48  40817  etransc  40818  tgoldbach  42030  tgoldbachOLD  42037
  Copyright terms: Public domain W3C validator