Theorem recni 11146

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

Syntax hints:   ∈ wcel 2113  ℂcc 11024  ℝcr 11025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ss 3918

This theorem is referenced by:  0cnALT  11368  renegcli  11442  resubcli  11443  recgt0ii  12048  ledivp1i  12067  ltdivp1i  12068  2cnALT  12221  8th4div3  12361  numltc  12633  sqge0i  14111  lt2sqi  14112  le2sqi  14113  sq11i  14114  crreczi  14151  faclbnd4lem1  14216  sqrtmsq2i  15311  abs3lemi  15334  0.999...  15804  bpoly4  15982  ef01bndlem  16109  sin4lt0  16120  eirrlem  16129  rpnnen2lem3  16141  rpnnen2lem9  16147  rpnnen2lem11  16149  dvdslelem  16236  divalglem1  16321  divalglem2  16322  divalglem5  16324  divalglem6  16325  divalglem9  16328  prmreclem6  16849  modsubi  17000  pcoass  24980  aaliou3lem7  26313  picn  26423  sinhalfpilem  26428  cosneghalfpi  26435  sinhalfpip  26457  sinhalfpim  26458  coshalfpip  26459  coshalfpim  26460  sincosq1sgn  26463  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  sincos4thpi  26478  tan4thpi  26479  tan4thpiOLD  26480  sincos6thpi  26481  pige3ALT  26485  cosne0  26494  sinord  26499  resinf1o  26501  efif1olem2  26508  efif1olem4  26510  efifo  26512  logi  26552  logimul  26579  ecxp  26638  cxpsqrtlem  26667  2irrexpq  26696  elogb  26736  logblog  26758  sqrt2cxp2logb9e3  26765  ang180lem1  26775  ang180lem2  26776  1cubrlem  26807  quartlem3  26825  asinsin  26858  acoscos  26859  asin1  26860  reasinsin  26862  acosbnd  26866  atanlogsublem  26881  atanbnd  26892  atan1  26894  log2tlbnd  26911  log2ublem1  26912  log2le1  26916  birthday  26920  basellem8  27054  basellem9  27055  cht2  27138  mumullem2  27146  chtublem  27178  chtub  27179  bposlem6  27256  bposlem7  27257  bposlem8  27258  bposlem9  27259  chebbnd1lem3  27438  chebbnd1  27439  chto1ub  27443  mulogsumlem  27498  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  pntibndlem3  27559  ex-ceil  30523  nmblolbii  30874  ip0i  30900  ip1ilem  30901  ipasslem10  30914  siilem1  30926  siii  30928  normlem1  31185  normlem3  31187  normlem5  31189  normlem6  31190  norm-ii-i  31212  normsubi  31216  norm3adifii  31223  norm3lem  31224  normpar2i  31231  bcsiALT  31254  pjneli  31798  lnophmlem2  32092  nmbdoplbi  32099  nmcoplbi  32103  nmophmi  32106  nmbdfnlbi  32124  nmcfnlbi  32127  cnlnadjlem2  32143  cnlnadjlem7  32148  nmopadjlem  32164  nmopcoi  32170  nmopcoadji  32176  nmopcoadj0i  32178  unierri  32179  opsqrlem1  32215  dfdec100  32911  dp20u  32959  dp2ltsuc  32967  dpfrac1  32973  dpmul10  32976  decdiv10  32977  dpmul100  32978  dp3mul10  32979  dpmul1000  32980  dpexpp1  32989  dpadd2  32991  dpadd3  32993  dpmul  32994  dpmul4  32995  threehalves  32996  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  subfaclim  35382  subfacval3  35383  problem2  35860  problem3  35861  problem4  35862  problem5  35863  circum  35868  iexpire  35929  taupilem1  37522  dvacos  37902  fdc  37942  lcmineqlem23  42301  aks4d1p1p4  42321  aks4d1p1p7  42324  0cnALT3  42504  acos1half  42609  re1m1e0m0  42648  ipiiie0  42689  arearect  43453  areaquad  43454  sineq0ALT  45173  wallispilem2  46306  stirlinglem3  46316  stirlinglem4  46317  stirlinglem13  46326  stirlinglem15  46328  dirkerper  46336  fourierdlem24  46371  fourierdlem103  46449  fourierdlem104  46450  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  etransclem18  46492  etransclem23  46497  etransclem46  46520  etransclem47  46521  etransclem48  46522  etransc  46523  tgoldbach  48059