Theorem recni 11304

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

Syntax hints:   ∈ wcel 2108  ℂcc 11182  ℝcr 11183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  0cnALT  11524  renegcli  11597  resubcli  11598  recgt0ii  12201  ledivp1i  12220  ltdivp1i  12221  2cnALT  12369  8th4div3  12513  numltc  12784  sqge0i  14237  lt2sqi  14238  le2sqi  14239  sq11i  14240  crreczi  14277  faclbnd4lem1  14342  sqrtmsq2i  15436  abs3lemi  15459  0.999...  15929  bpoly4  16107  ef01bndlem  16232  sin4lt0  16243  eirrlem  16252  rpnnen2lem3  16264  rpnnen2lem9  16270  rpnnen2lem11  16272  dvdslelem  16357  divalglem1  16442  divalglem2  16443  divalglem5  16445  divalglem6  16446  divalglem9  16449  prmreclem6  16968  modsubi  17119  pcoass  25076  aaliou3lem7  26409  picn  26519  sinhalfpilem  26523  cosneghalfpi  26530  sinhalfpip  26552  sinhalfpim  26553  coshalfpip  26554  coshalfpim  26555  sincosq1sgn  26558  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  sincos4thpi  26573  tan4thpi  26574  tan4thpiOLD  26575  sincos6thpi  26576  pige3ALT  26580  cosne0  26589  sinord  26594  resinf1o  26596  efif1olem2  26603  efif1olem4  26605  efifo  26607  logi  26647  logimul  26674  ecxp  26733  cxpsqrtlem  26762  2irrexpq  26791  elogb  26831  logblog  26853  sqrt2cxp2logb9e3  26860  ang180lem1  26870  ang180lem2  26871  1cubrlem  26902  quartlem3  26920  asinsin  26953  acoscos  26954  asin1  26955  reasinsin  26957  acosbnd  26961  atanlogsublem  26976  atanbnd  26987  atan1  26989  log2tlbnd  27006  log2ublem1  27007  log2le1  27011  birthday  27015  basellem8  27149  basellem9  27150  cht2  27233  mumullem2  27241  chtublem  27273  chtub  27274  bposlem6  27351  bposlem7  27352  bposlem8  27353  bposlem9  27354  chebbnd1lem3  27533  chebbnd1  27534  chto1ub  27538  mulogsumlem  27593  mulog2sumlem1  27596  mulog2sumlem2  27597  mulog2sumlem3  27598  pntibndlem3  27654  ex-ceil  30480  nmblolbii  30831  ip0i  30857  ip1ilem  30858  ipasslem10  30871  siilem1  30883  siii  30885  normlem1  31142  normlem3  31144  normlem5  31146  normlem6  31147  norm-ii-i  31169  normsubi  31173  norm3adifii  31180  norm3lem  31181  normpar2i  31188  bcsiALT  31211  pjneli  31755  lnophmlem2  32049  nmbdoplbi  32056  nmcoplbi  32060  nmophmi  32063  nmbdfnlbi  32081  nmcfnlbi  32084  cnlnadjlem2  32100  cnlnadjlem7  32105  nmopadjlem  32121  nmopcoi  32127  nmopcoadji  32133  nmopcoadj0i  32135  unierri  32136  opsqrlem1  32172  dfdec100  32834  dp20u  32842  dp2ltsuc  32850  dpfrac1  32856  dpmul10  32859  decdiv10  32860  dpmul100  32861  dp3mul10  32862  dpmul1000  32863  dpexpp1  32872  dpadd2  32874  dpadd3  32876  dpmul  32877  dpmul4  32878  threehalves  32879  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  subfaclim  35156  subfacval3  35157  problem2  35634  problem3  35635  problem4  35636  problem5  35637  circum  35642  iexpire  35697  taupilem1  37287  dvacos  37665  fdc  37705  lcmineqlem23  42008  aks4d1p1p4  42028  aks4d1p1p7  42031  0cnALT3  42248  acos1half  42340  re1m1e0m0  42373  ipiiie0  42413  arearect  43176  areaquad  43177  sineq0ALT  44908  wallispilem2  45987  stirlinglem3  45997  stirlinglem4  45998  stirlinglem13  46007  stirlinglem15  46009  dirkerper  46017  fourierdlem24  46052  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem18  46173  etransclem23  46178  etransclem46  46201  etransclem47  46202  etransclem48  46203  etransc  46204  tgoldbach  47691