Theorem recni 10052

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

Syntax hints:   ∈ wcel 1990  ℂcc 9934  ℝcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  renegcli  10342  resubcli  10343  recgt0ii  10929  ledivp1i  10949  ltdivp1i  10950  nncni  11030  2cn  11091  3cn  11095  4cn  11098  5cn  11100  6cn  11102  7cn  11104  8cn  11106  9cn  11108  8th4div3  11252  nn0cni  11304  numltc  11528  sqge0i  12951  lt2sqi  12952  le2sqi  12953  sq11i  12954  crreczi  12989  faclbnd4lem1  13080  sqrtmsq2i  14127  abs3lemi  14149  0.999...  14612  0.999...OLD  14613  bpoly4  14790  ef01bndlem  14914  sin4lt0  14925  eirrlem  14932  rpnnen2lem3  14945  rpnnen2lem9  14951  rpnnen2lem11  14953  dvdslelem  15031  divalglem1  15117  divalglem2  15118  divalglem5  15120  divalglem6  15121  divalglem9  15124  prmreclem6  15625  modsubi  15776  pcoass  22824  aaliou3lem7  24104  picn  24211  sinhalfpilem  24215  cosneghalfpi  24222  sincosq1sgn  24250  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  sincos4thpi  24265  tan4thpi  24266  sincos6thpi  24267  pige3  24269  cosne0  24276  sinord  24280  resinf1o  24282  efif1olem2  24289  efif1olem4  24291  efifo  24293  logimul  24360  ecxp  24419  cxpsqrtlem  24448  elogb  24508  logblog  24530  ang180lem1  24539  ang180lem2  24540  1cubrlem  24568  quartlem3  24586  asinsin  24619  acoscos  24620  asin1  24621  reasinsin  24623  acosbnd  24627  atanlogsublem  24642  atanbnd  24653  atan1  24655  log2tlbnd  24672  log2ublem1  24673  log2le1  24677  birthday  24681  basellem8  24814  basellem9  24815  cht2  24898  mumullem2  24906  chtublem  24936  chtub  24937  bposlem6  25014  bposlem7  25015  bposlem8  25016  bposlem9  25017  chebbnd1lem3  25160  chebbnd1  25161  chto1ub  25165  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  pntibndlem3  25281  ex-ceil  27305  nmblolbii  27654  ip0i  27680  ip1ilem  27681  ipasslem10  27694  siilem1  27706  siii  27708  normlem1  27967  normlem3  27969  normlem5  27971  normlem6  27972  norm-ii-i  27994  normsubi  27998  norm3adifii  28005  norm3lem  28006  normpar2i  28013  bcsiALT  28036  pjneli  28582  lnophmlem2  28876  nmbdoplbi  28883  nmcoplbi  28887  nmophmi  28890  nmbdfnlbi  28908  nmcfnlbi  28911  cnlnadjlem2  28927  cnlnadjlem7  28932  nmopadjlem  28948  nmopcoi  28954  nmopcoadji  28960  nmopcoadj0i  28962  unierri  28963  opsqrlem1  28999  dfdec100  29576  dp20u  29585  dp2ltsuc  29593  dpfrac1  29599  dpfrac1OLD  29600  dpmul10  29603  decdiv10  29604  dpmul100  29605  dp3mul10  29606  dpmul1000  29607  dpexpp1  29616  dpadd2  29618  dpadd3  29620  dpmul  29621  dpmul4  29622  threehalves  29623  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  subfaclim  31170  subfacval3  31171  problem2  31559  problem2OLD  31560  problem3  31561  problem4  31562  problem5  31563  circum  31568  logi  31620  iexpire  31621  taupilem1  33167  dvacos  33497  fdc  33541  rmspecsqrtnqOLD  37471  arearect  37801  areaquad  37802  sineq0ALT  39173  wallispilem2  40283  stirlinglem3  40293  stirlinglem4  40294  stirlinglem13  40303  stirlinglem15  40305  dirkerper  40313  fourierdlem24  40348  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem18  40469  etransclem23  40474  etransclem46  40497  etransclem47  40498  etransclem48  40499  etransc  40500  tgoldbach  41705  tgoldbachOLD  41712