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

Theorem recni 10648
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 10587 . 2 ℝ ⊆ ℂ
2 recni.1 . 2 𝐴 ∈ ℝ
31, 2sselii 3915 1 𝐴 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  cc 10528  cr 10529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-resscn 10587
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  0cnALT  10867  renegcli  10940  resubcli  10941  recgt0ii  11539  ledivp1i  11558  ltdivp1i  11559  2cnALT  11705  8th4div3  11849  numltc  12116  sqge0i  13551  lt2sqi  13552  le2sqi  13553  sq11i  13554  crreczi  13589  faclbnd4lem1  13653  sqrtmsq2i  14743  abs3lemi  14766  0.999...  15233  bpoly4  15409  ef01bndlem  15533  sin4lt0  15544  eirrlem  15553  rpnnen2lem3  15565  rpnnen2lem9  15571  rpnnen2lem11  15573  dvdslelem  15655  divalglem1  15739  divalglem2  15740  divalglem5  15742  divalglem6  15743  divalglem9  15746  prmreclem6  16251  modsubi  16402  pcoass  23633  aaliou3lem7  24949  picn  25056  sinhalfpilem  25060  cosneghalfpi  25067  sinhalfpip  25089  sinhalfpim  25090  coshalfpip  25091  coshalfpim  25092  sincosq1sgn  25095  sincosq2sgn  25096  sincosq3sgn  25097  sincosq4sgn  25098  sincos4thpi  25110  tan4thpi  25111  sincos6thpi  25112  pige3ALT  25116  cosne0  25125  sinord  25130  resinf1o  25132  efif1olem2  25139  efif1olem4  25141  efifo  25143  logimul  25209  ecxp  25268  cxpsqrtlem  25297  2irrexpq  25325  elogb  25360  logblog  25382  sqrt2cxp2logb9e3  25389  ang180lem1  25399  ang180lem2  25400  1cubrlem  25431  quartlem3  25449  asinsin  25482  acoscos  25483  asin1  25484  reasinsin  25486  acosbnd  25490  atanlogsublem  25505  atanbnd  25516  atan1  25518  log2tlbnd  25535  log2ublem1  25536  log2le1  25540  birthday  25544  basellem8  25677  basellem9  25678  cht2  25761  mumullem2  25769  chtublem  25799  chtub  25800  bposlem6  25877  bposlem7  25878  bposlem8  25879  bposlem9  25880  chebbnd1lem3  26059  chebbnd1  26060  chto1ub  26064  mulogsumlem  26119  mulog2sumlem1  26122  mulog2sumlem2  26123  mulog2sumlem3  26124  pntibndlem3  26180  ex-ceil  28237  nmblolbii  28586  ip0i  28612  ip1ilem  28613  ipasslem10  28626  siilem1  28638  siii  28640  normlem1  28897  normlem3  28899  normlem5  28901  normlem6  28902  norm-ii-i  28924  normsubi  28928  norm3adifii  28935  norm3lem  28936  normpar2i  28943  bcsiALT  28966  pjneli  29510  lnophmlem2  29804  nmbdoplbi  29811  nmcoplbi  29815  nmophmi  29818  nmbdfnlbi  29836  nmcfnlbi  29839  cnlnadjlem2  29855  cnlnadjlem7  29860  nmopadjlem  29876  nmopcoi  29882  nmopcoadji  29888  nmopcoadj0i  29890  unierri  29891  opsqrlem1  29927  dfdec100  30576  dp20u  30584  dp2ltsuc  30592  dpfrac1  30598  dpmul10  30601  decdiv10  30602  dpmul100  30603  dp3mul10  30604  dpmul1000  30605  dpexpp1  30614  dpadd2  30616  dpadd3  30618  dpmul  30619  dpmul4  30620  threehalves  30621  hgt750lemd  32033  hgt750lem  32036  hgt750lem2  32037  subfaclim  32549  subfacval3  32550  problem2  33023  problem3  33024  problem4  33025  problem5  33026  circum  33031  logi  33080  iexpire  33081  taupilem1  34736  dvacos  35141  fdc  35182  lcmineqlem23  39338  3lexlogpow5ineq1  39340  0cnALT3  39454  re1m1e0m0  39528  ipiiie0  39567  arearect  40158  areaquad  40159  sineq0ALT  41636  wallispilem2  42701  stirlinglem3  42711  stirlinglem4  42712  stirlinglem13  42721  stirlinglem15  42723  dirkerper  42731  fourierdlem24  42766  fourierdlem103  42844  fourierdlem104  42845  sqwvfoura  42863  sqwvfourb  42864  fourierswlem  42865  fouriersw  42866  etransclem18  42887  etransclem23  42892  etransclem46  42915  etransclem47  42916  etransclem48  42917  etransc  42918  tgoldbach  44328
  Copyright terms: Public domain W3C validator