Theorem recni 10391

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

Step	Hyp	Ref	Expression
1		ax-resscn 10329	. 2 ⊢ ℝ ⊆ ℂ
2		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
3	1, 2	sselii 3818	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2107  ℂcc 10270  ℝcr 10271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-resscn 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  0cnALT  10610  renegcli  10684  resubcli  10685  recgt0ii  11283  ledivp1i  11303  ltdivp1i  11304  nncniOLD  11386  2cnALT  11451  3cnOLD  11457  4cnOLD  11462  5cnOLD  11466  6cnOLD  11470  7cnOLD  11474  8cnOLD  11478  9cnOLD  11482  8th4div3  11602  nn0cniOLD  11656  numltc  11872  sqge0i  13270  lt2sqi  13271  le2sqi  13272  sq11i  13273  crreczi  13308  faclbnd4lem1  13398  sqrtmsq2i  14534  abs3lemi  14557  0.999...  15016  bpoly4  15192  ef01bndlem  15316  sin4lt0  15327  eirrlem  15336  rpnnen2lem3  15349  rpnnen2lem9  15355  rpnnen2lem11  15357  dvdslelem  15438  divalglem1  15524  divalglem2  15525  divalglem5  15527  divalglem6  15528  divalglem9  15531  prmreclem6  16029  modsubi  16180  pcoass  23231  aaliou3lem7  24541  picn  24649  sinhalfpilem  24653  cosneghalfpi  24660  sincosq1sgn  24688  sincosq2sgn  24689  sincosq3sgn  24690  sincosq4sgn  24691  sincos4thpi  24703  tan4thpi  24704  sincos6thpi  24705  pige3  24707  cosne0  24714  sinord  24718  resinf1o  24720  efif1olem2  24727  efif1olem4  24729  efifo  24731  logimul  24797  ecxp  24856  cxpsqrtlem  24885  2irrexpq  24913  elogb  24948  logblog  24970  sqrt2cxp2logb9e3  24977  ang180lem1  24987  ang180lem2  24988  1cubrlem  25019  quartlem3  25037  asinsin  25070  acoscos  25071  asin1  25072  reasinsin  25074  acosbnd  25078  atanlogsublem  25093  atanbnd  25104  atan1  25106  log2tlbnd  25124  log2ublem1  25125  log2le1  25129  birthday  25133  basellem8  25266  basellem9  25267  cht2  25350  mumullem2  25358  chtublem  25388  chtub  25389  bposlem6  25466  bposlem7  25467  bposlem8  25468  bposlem9  25469  chebbnd1lem3  25612  chebbnd1  25613  chto1ub  25617  mulogsumlem  25672  mulog2sumlem1  25675  mulog2sumlem2  25676  mulog2sumlem3  25677  pntibndlem3  25733  ex-ceil  27880  nmblolbii  28226  ip0i  28252  ip1ilem  28253  ipasslem10  28266  siilem1  28278  siii  28280  normlem1  28539  normlem3  28541  normlem5  28543  normlem6  28544  norm-ii-i  28566  normsubi  28570  norm3adifii  28577  norm3lem  28578  normpar2i  28585  bcsiALT  28608  pjneli  29154  lnophmlem2  29448  nmbdoplbi  29455  nmcoplbi  29459  nmophmi  29462  nmbdfnlbi  29480  nmcfnlbi  29483  cnlnadjlem2  29499  cnlnadjlem7  29504  nmopadjlem  29520  nmopcoi  29526  nmopcoadji  29532  nmopcoadj0i  29534  unierri  29535  opsqrlem1  29571  dfdec100  30140  dp20u  30148  dp2ltsuc  30156  dpfrac1  30162  dpmul10  30165  decdiv10  30166  dpmul100  30167  dp3mul10  30168  dpmul1000  30169  dpexpp1  30178  dpadd2  30180  dpadd3  30182  dpmul  30183  dpmul4  30184  threehalves  30185  hgt750lemd  31328  hgt750lem  31331  hgt750lem2  31332  subfaclim  31769  subfacval3  31770  problem2  32157  problem3  32158  problem4  32159  problem5  32160  circum  32165  logi  32214  iexpire  32215  taupilem1  33763  dvacos  34122  fdc  34165  0cnALT3  38140  arearect  38759  areaquad  38760  sineq0ALT  40106  wallispilem2  41210  stirlinglem3  41220  stirlinglem4  41221  stirlinglem13  41230  stirlinglem15  41232  dirkerper  41240  fourierdlem24  41275  fourierdlem103  41353  fourierdlem104  41354  sqwvfoura  41372  sqwvfourb  41373  fourierswlem  41374  fouriersw  41375  etransclem18  41396  etransclem23  41401  etransclem46  41424  etransclem47  41425  etransclem48  41426  etransc  41427  tgoldbach  42730