Theorem recni 11272

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

Syntax hints:   ∈ wcel 2105  ℂcc 11150  ℝcr 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979

This theorem is referenced by:  0cnALT  11493  renegcli  11567  resubcli  11568  recgt0ii  12171  ledivp1i  12190  ltdivp1i  12191  2cnALT  12339  8th4div3  12483  numltc  12756  sqge0i  14223  lt2sqi  14224  le2sqi  14225  sq11i  14226  crreczi  14263  faclbnd4lem1  14328  sqrtmsq2i  15422  abs3lemi  15445  0.999...  15913  bpoly4  16091  ef01bndlem  16216  sin4lt0  16227  eirrlem  16236  rpnnen2lem3  16248  rpnnen2lem9  16254  rpnnen2lem11  16256  dvdslelem  16342  divalglem1  16427  divalglem2  16428  divalglem5  16430  divalglem6  16431  divalglem9  16434  prmreclem6  16954  modsubi  17105  pcoass  25070  aaliou3lem7  26405  picn  26515  sinhalfpilem  26519  cosneghalfpi  26526  sinhalfpip  26548  sinhalfpim  26549  coshalfpip  26550  coshalfpim  26551  sincosq1sgn  26554  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  sincos4thpi  26569  tan4thpi  26570  tan4thpiOLD  26571  sincos6thpi  26572  pige3ALT  26576  cosne0  26585  sinord  26590  resinf1o  26592  efif1olem2  26599  efif1olem4  26601  efifo  26603  logi  26643  logimul  26670  ecxp  26729  cxpsqrtlem  26758  2irrexpq  26787  elogb  26827  logblog  26849  sqrt2cxp2logb9e3  26856  ang180lem1  26866  ang180lem2  26867  1cubrlem  26898  quartlem3  26916  asinsin  26949  acoscos  26950  asin1  26951  reasinsin  26953  acosbnd  26957  atanlogsublem  26972  atanbnd  26983  atan1  26985  log2tlbnd  27002  log2ublem1  27003  log2le1  27007  birthday  27011  basellem8  27145  basellem9  27146  cht2  27229  mumullem2  27237  chtublem  27269  chtub  27270  bposlem6  27347  bposlem7  27348  bposlem8  27349  bposlem9  27350  chebbnd1lem3  27529  chebbnd1  27530  chto1ub  27534  mulogsumlem  27589  mulog2sumlem1  27592  mulog2sumlem2  27593  mulog2sumlem3  27594  pntibndlem3  27650  ex-ceil  30476  nmblolbii  30827  ip0i  30853  ip1ilem  30854  ipasslem10  30867  siilem1  30879  siii  30881  normlem1  31138  normlem3  31140  normlem5  31142  normlem6  31143  norm-ii-i  31165  normsubi  31169  norm3adifii  31176  norm3lem  31177  normpar2i  31184  bcsiALT  31207  pjneli  31751  lnophmlem2  32045  nmbdoplbi  32052  nmcoplbi  32056  nmophmi  32059  nmbdfnlbi  32077  nmcfnlbi  32080  cnlnadjlem2  32096  cnlnadjlem7  32101  nmopadjlem  32117  nmopcoi  32123  nmopcoadji  32129  nmopcoadj0i  32131  unierri  32132  opsqrlem1  32168  dfdec100  32836  dp20u  32844  dp2ltsuc  32852  dpfrac1  32858  dpmul10  32861  decdiv10  32862  dpmul100  32863  dp3mul10  32864  dpmul1000  32865  dpexpp1  32874  dpadd2  32876  dpadd3  32878  dpmul  32879  dpmul4  32880  threehalves  32881  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  subfaclim  35172  subfacval3  35173  problem2  35650  problem3  35651  problem4  35652  problem5  35653  circum  35658  iexpire  35714  taupilem1  37303  dvacos  37691  fdc  37731  lcmineqlem23  42032  aks4d1p1p4  42052  aks4d1p1p7  42055  0cnALT3  42272  acos1half  42366  re1m1e0m0  42403  ipiiie0  42443  arearect  43203  areaquad  43204  sineq0ALT  44934  wallispilem2  46021  stirlinglem3  46031  stirlinglem4  46032  stirlinglem13  46041  stirlinglem15  46043  dirkerper  46051  fourierdlem24  46086  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem18  46207  etransclem23  46212  etransclem46  46235  etransclem47  46236  etransclem48  46237  etransc  46238  tgoldbach  47741