Theorem recni 11148

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 11085	. 2 ⊢ ℝ ⊆ ℂ
2		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
3	1, 2	sselii 3934	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2109  ℂcc 11026  ℝcr 11027

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3922

This theorem is referenced by:  0cnALT  11369  renegcli  11443  resubcli  11444  recgt0ii  12049  ledivp1i  12068  ltdivp1i  12069  2cnALT  12222  8th4div3  12362  numltc  12635  sqge0i  14113  lt2sqi  14114  le2sqi  14115  sq11i  14116  crreczi  14153  faclbnd4lem1  14218  sqrtmsq2i  15313  abs3lemi  15336  0.999...  15806  bpoly4  15984  ef01bndlem  16111  sin4lt0  16122  eirrlem  16131  rpnnen2lem3  16143  rpnnen2lem9  16149  rpnnen2lem11  16151  dvdslelem  16238  divalglem1  16323  divalglem2  16324  divalglem5  16326  divalglem6  16327  divalglem9  16330  prmreclem6  16851  modsubi  17002  pcoass  24940  aaliou3lem7  26273  picn  26383  sinhalfpilem  26388  cosneghalfpi  26395  sinhalfpip  26417  sinhalfpim  26418  coshalfpip  26419  coshalfpim  26420  sincosq1sgn  26423  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  sincos4thpi  26438  tan4thpi  26439  tan4thpiOLD  26440  sincos6thpi  26441  pige3ALT  26445  cosne0  26454  sinord  26459  resinf1o  26461  efif1olem2  26468  efif1olem4  26470  efifo  26472  logi  26512  logimul  26539  ecxp  26598  cxpsqrtlem  26627  2irrexpq  26656  elogb  26696  logblog  26718  sqrt2cxp2logb9e3  26725  ang180lem1  26735  ang180lem2  26736  1cubrlem  26767  quartlem3  26785  asinsin  26818  acoscos  26819  asin1  26820  reasinsin  26822  acosbnd  26826  atanlogsublem  26841  atanbnd  26852  atan1  26854  log2tlbnd  26871  log2ublem1  26872  log2le1  26876  birthday  26880  basellem8  27014  basellem9  27015  cht2  27098  mumullem2  27106  chtublem  27138  chtub  27139  bposlem6  27216  bposlem7  27217  bposlem8  27218  bposlem9  27219  chebbnd1lem3  27398  chebbnd1  27399  chto1ub  27403  mulogsumlem  27458  mulog2sumlem1  27461  mulog2sumlem2  27462  mulog2sumlem3  27463  pntibndlem3  27519  ex-ceil  30410  nmblolbii  30761  ip0i  30787  ip1ilem  30788  ipasslem10  30801  siilem1  30813  siii  30815  normlem1  31072  normlem3  31074  normlem5  31076  normlem6  31077  norm-ii-i  31099  normsubi  31103  norm3adifii  31110  norm3lem  31111  normpar2i  31118  bcsiALT  31141  pjneli  31685  lnophmlem2  31979  nmbdoplbi  31986  nmcoplbi  31990  nmophmi  31993  nmbdfnlbi  32011  nmcfnlbi  32014  cnlnadjlem2  32030  cnlnadjlem7  32035  nmopadjlem  32051  nmopcoi  32057  nmopcoadji  32063  nmopcoadj0i  32065  unierri  32066  opsqrlem1  32102  dfdec100  32788  dp20u  32831  dp2ltsuc  32839  dpfrac1  32845  dpmul10  32848  decdiv10  32849  dpmul100  32850  dp3mul10  32851  dpmul1000  32852  dpexpp1  32861  dpadd2  32863  dpadd3  32865  dpmul  32866  dpmul4  32867  threehalves  32868  hgt750lemd  34615  hgt750lem  34618  hgt750lem2  34619  subfaclim  35160  subfacval3  35161  problem2  35638  problem3  35639  problem4  35640  problem5  35641  circum  35646  iexpire  35707  taupilem1  37294  dvacos  37684  fdc  37724  lcmineqlem23  42024  aks4d1p1p4  42044  aks4d1p1p7  42047  0cnALT3  42226  acos1half  42331  re1m1e0m0  42370  ipiiie0  42411  arearect  43188  areaquad  43189  sineq0ALT  44910  wallispilem2  46048  stirlinglem3  46058  stirlinglem4  46059  stirlinglem13  46068  stirlinglem15  46070  dirkerper  46078  fourierdlem24  46113  fourierdlem103  46191  fourierdlem104  46192  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  etransclem18  46234  etransclem23  46239  etransclem46  46262  etransclem47  46263  etransclem48  46264  etransc  46265  tgoldbach  47802