Theorem recni 11350

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

This proof depends on syntax axioms:   ∈ wcel 2147  ℂcc 11225  ℝcr 11226

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-resscn 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901

This theorem is used by:  0cnALT  11572  renegcli  11646  resubcli  11647  recgt0ii  12250  ledivp1i  12269  ltdivp1i  12270  2cnALT  12446  numltc  12872  sqge0i  14358  lt2sqi  14359  le2sqi  14360  sq11i  14361  crreczi  14399  faclbnd4lem1  14464  sqrtmsq2i  15584  abs3lemi  15607  0.999...  16079  bpoly4  16254  ef01bndlem  16381  sin4lt0  16392  eirrlem  16401  rpnnen2lem3  16413  rpnnen2lem9  16419  rpnnen2lem11  16421  dvdslelem  16508  divalglem1  16593  divalglem2  16594  divalglem5  16596  divalglem6  16597  divalglem9  16600  prmreclem6  17128  modsubi  17279  pcoass  25375  aaliou3lem7  26706  picn  26815  sinhalfpilem  26822  cosneghalfpi  26829  sinhalfpip  26851  sinhalfpim  26852  coshalfpip  26853  coshalfpim  26854  sincosq1sgn  26857  sincosq2sgn  26858  sincosq3sgn  26859  sincosq4sgn  26860  sincos4thpi  26872  tan4thpi  26873  sincos6thpi  26874  pige3ALT  26878  cosne0  26887  sinord  26892  resinf1o  26894  efif1olem2  26901  efifo  26905  logi  26945  logimul  26972  ecxp  27031  cxpsqrtlem  27060  2irrexpq  27089  elogb  27128  logblog  27150  sqrt2cxp2logb9e3  27157  ang180lem1  27167  ang180lem2  27168  1cubrlem  27199  quartlem3  27217  asinsin  27250  acoscos  27251  asin1  27252  reasinsin  27254  acosbnd  27258  atanlogsublem  27273  atanbnd  27284  atan1  27286  log2tlbnd  27303  log2ublem1  27304  log2le1  27308  birthday  27312  basellem8  27445  basellem9  27446  cht2  27529  mumullem2  27537  chtublem  27568  chtub  27569  bposlem6  27646  bposlem7  27647  bposlem8  27648  bposlem9  27649  chebbnd1lem3  27828  chebbnd1  27829  chto1ub  27833  mulogsumlem  27888  mulog2sumlem1  27891  mulog2sumlem2  27892  mulog2sumlem3  27893  pntibndlem3  27949  ex-ceil  31079  nmblolbii  31431  ip0i  31457  ip1ilem  31458  ipasslem10  31471  siilem1  31483  siii  31485  normlem1  31742  normlem3  31744  normlem5  31746  normlem6  31747  norm-ii-i  31769  normsubi  31773  norm3adifii  31780  norm3lem  31781  normpar2i  31788  bcsiALT  31811  pjneli  32355  lnophmlem2  32649  nmbdoplbi  32656  nmcoplbi  32660  nmophmi  32663  nmbdfnlbi  32681  nmcfnlbi  32684  cnlnadjlem2  32700  cnlnadjlem7  32705  nmopadjlem  32721  nmopcoi  32727  nmopcoadji  32733  nmopcoadj0i  32735  unierri  32736  opsqrlem1  32772  dfdec100  33491  dp20u  33514  dp2ltsuc  33522  dpfrac1  33528  dpmul10  33531  decdiv10  33532  dpmul100  33533  dp3mul10  33534  dpmul1000  33535  dpexpp1  33544  dpadd2  33546  dpadd3  33548  dpmul  33549  dpmul4  33550  threehalves  33551  hgt750lemd  35347  hgt750lem  35350  hgt750lem2  35351  subfaclim  36120  subfacval3  36121  problem2  36598  problem3  36599  problem4  36600  problem5  36601  circum  36606  iexpire  36678  taupilem1  38434  dvacos  38815  fdc  38871  lcmineqlem23  43293  aks4d1p1p4  43313  aks4d1p1p7  43316  0cnALT3  43497  acos1half  43602  re1m1e0m0  43641  ipiiie0  43682  arearect  44409  areaquad  44410  sineq0ALT  46110  wallispilem2  47281  stirlinglem3  47291  stirlinglem4  47292  stirlinglem13  47301  stirlinglem15  47303  dirkerper  47311  fourierdlem24  47346  fourierdlem103  47424  fourierdlem104  47425  sqwvfoura  47443  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  etransclem18  47467  etransclem23  47472  etransclem46  47495  etransclem47  47496  etransclem48  47497  etransc  47498  goldrasin  48134  goldratmolem2  48138  goldratmolem3  48139  goldratmolem4  48140  goldratval  48141  tgoldbach  49120