Theorem recni 9931

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

Syntax hints:   ∈ wcel 1977  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  renegcli  10221  resubcli  10222  recgt0ii  10808  ledivp1i  10828  ltdivp1i  10829  nncni  10907  2cn  10968  3cn  10972  4cn  10975  5cn  10977  6cn  10979  7cn  10981  8cn  10983  9cn  10985  8th4div3  11129  nn0cni  11181  numltc  11404  sqge0i  12813  lt2sqi  12814  le2sqi  12815  sq11i  12816  crreczi  12851  faclbnd4lem1  12942  sqrtmsq2i  13975  abs3lemi  13997  0.999...  14451  0.999...OLD  14452  bpoly4  14629  ef01bndlem  14753  sin4lt0  14764  eirrlem  14771  rpnnen2lem3  14784  rpnnen2lem9  14790  rpnnen2lem11  14792  dvdslelem  14869  divalglem1  14955  divalglem2  14956  divalglem5  14958  divalglem6  14959  divalglem9  14962  prmreclem6  15463  modsubi  15614  pcoass  22632  aaliou3lem7  23908  picn  24015  sinhalfpilem  24019  cosneghalfpi  24026  sincosq1sgn  24054  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  sincos4thpi  24069  tan4thpi  24070  sincos6thpi  24071  pige3  24073  cosne0  24080  sinord  24084  resinf1o  24086  efif1olem2  24093  efif1olem4  24095  efifo  24097  logimul  24164  ecxp  24219  cxpsqrtlem  24248  elogb  24308  logblog  24330  ang180lem1  24339  ang180lem2  24340  1cubrlem  24368  quartlem3  24386  asinsin  24419  acoscos  24420  asin1  24421  reasinsin  24423  acosbnd  24427  atanlogsublem  24442  atanbnd  24453  atan1  24455  log2tlbnd  24472  log2ublem1  24473  log2le1  24477  birthday  24481  basellem8  24614  basellem9  24615  cht2  24698  mumullem2  24706  chtublem  24736  chtub  24737  bposlem6  24814  bposlem7  24815  bposlem8  24816  bposlem9  24817  chebbnd1lem3  24960  chebbnd1  24961  chto1ub  24965  mulogsumlem  25020  mulog2sumlem1  25023  mulog2sumlem2  25024  mulog2sumlem3  25025  pntibndlem3  25081  ex-ceil  26697  nmblolbii  27038  ip0i  27064  ip1ilem  27065  ipasslem10  27078  siilem1  27090  siii  27092  normlem1  27351  normlem3  27353  normlem5  27355  normlem6  27356  norm-ii-i  27378  normsubi  27382  norm3adifii  27389  norm3lem  27390  normpar2i  27397  bcsiALT  27420  pjneli  27966  lnophmlem2  28260  nmbdoplbi  28267  nmcoplbi  28271  nmophmi  28274  nmbdfnlbi  28292  nmcfnlbi  28295  cnlnadjlem2  28311  cnlnadjlem7  28316  nmopadjlem  28332  nmopcoi  28338  nmopcoadji  28344  nmopcoadj0i  28346  unierri  28347  opsqrlem1  28383  subfaclim  30424  subfacval3  30425  problem2  30813  problem2OLD  30814  problem3  30815  problem4  30816  problem5  30817  circum  30822  logi  30873  iexpire  30874  taupilem1  32344  dvacos  32667  fdc  32711  rmspecsqrtnqOLD  36489  arearect  36820  areaquad  36821  sineq0ALT  38195  wallispilem2  38959  stirlinglem3  38969  stirlinglem4  38970  stirlinglem13  38979  stirlinglem15  38981  dirkerper  38989  fourierdlem24  39024  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem18  39145  etransclem23  39150  etransclem46  39173  etransclem47  39174  etransclem48  39175  etransc  39176  tgoldbach  40232  tgoldbachOLD  40239  dpfrac1  42312  dpfrac1OLD  42313