Theorem recn 10616

Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)

Assertion

Ref	Expression
recn	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn

Step	Hyp	Ref	Expression
1		ax-resscn 10583	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 3911	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 10524  ℝcr 10525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  mulid1  10628  recnd  10658  pnfnre  10671  mnfnre  10673  mul02  10807  ltaddneg  10844  ltaddnegr  10845  renegcli  10936  resubcl  10939  negn0  11058  negf1o  11059  ltaddsub2  11104  leaddsub2  11106  leltadd  11113  ltaddpos  11119  ltaddpos2  11120  posdif  11122  lenegcon1  11133  lenegcon2  11134  addge01  11139  addge02  11140  leaddle0  11144  mullt0  11148  recex  11261  ltm1  11471  prodgt02  11477  ltmul2  11480  lemul1  11481  lemul2  11482  lemul1a  11483  lemul2a  11484  ltmulgt12  11490  lemulge12  11492  gt0div  11495  ge0div  11496  mulge0b  11499  mulle0b  11500  ltmuldiv2  11503  ltdivmul  11504  ledivmul  11505  ltdivmul2  11506  lt2mul2div  11507  ledivmul2  11508  lemuldiv2  11510  ltdiv2  11515  ltrec1  11516  lerec2  11517  ledivdiv  11518  lediv2  11519  ltdiv23  11520  lediv23  11521  lediv12a  11522  recp1lt1  11527  ledivp1  11531  negfi  11577  infm3lem  11586  supmul  11600  riotaneg  11607  negiso  11608  cju  11621  nnge1  11653  halfpos  11855  lt2halves  11860  addltmul  11861  avgle1  11865  avgle2  11866  avgle  11867  div4p1lem1div2  11880  nnrecl  11883  difgtsumgt  11938  elznn0  11984  elznn  11985  elz2  11987  nzadd  12018  zmulcl  12019  gtndiv  12047  zeo  12056  eqreznegel  12322  supminf  12323  rebtwnz  12335  irradd  12360  irrmul  12361  divlt1lt  12446  divle1le  12447  max0sub  12577  xnegneg  12595  rexsub  12614  xnegid  12619  xaddcom  12621  xaddid1  12622  xnegdi  12629  xaddass  12630  rexmul  12652  xmulasslem3  12667  xadddilem  12675  divelunit  12872  fzonmapblen  13078  ico01fl0  13184  flzadd  13191  ltdifltdiv  13199  dfceil2  13204  intfrac2  13221  fldiv2  13224  flpmodeq  13237  mod0  13239  negmod0  13241  modlt  13243  modfrac  13247  flmod  13248  intfrac  13249  modmulnn  13252  modvalp1  13253  modid  13259  modcyc  13269  modcyc2  13270  modadd1  13271  modaddabs  13272  muladdmodid  13274  negmod  13279  modadd2mod  13284  modmul1  13287  modmulmodr  13300  modaddmulmod  13301  moddi  13302  modsubdir  13303  modirr  13305  addmodlteq  13309  expgt1  13463  mulexpz  13465  sqgt0  13487  lt2sq  13494  le2sq  13495  sqge0  13497  expmordi  13527  leexp1a  13535  expubnd  13537  sumsqeq0  13538  sqlecan  13567  bernneq  13586  bernneq2  13587  expnbnd  13589  digit2  13593  digit1  13594  expnngt1  13598  swrdccatin2  14082  swrdccat3blem  14092  cshweqrep  14174  crre  14465  crim  14466  reim0  14469  mulre  14472  rere  14473  remul2  14481  rediv  14482  immul2  14488  imdiv  14489  cjre  14490  cjreim  14511  rennim  14590  resqrex  14602  resqreu  14604  resqrtcl  14605  resqrtthlem  14606  sqrtneglem  14618  sqrtneg  14619  absreimsq  14644  absreim  14645  absnid  14650  leabs  14651  absre  14653  absresq  14654  sqabs  14659  max0add  14662  absz  14663  absdiflt  14669  absdifle  14670  lenegsq  14672  abssuble0  14680  absmax  14681  rddif  14692  absrdbnd  14693  o1rlimmul  14967  caurcvg2  15026  reefcl  15432  efgt0  15448  reeftlcl  15453  resinval  15480  recosval  15481  resin4p  15483  recos4p  15484  resincl  15485  recoscl  15486  retancl  15487  resinhcl  15501  rpcoshcl  15502  retanhcl  15504  tanhlt1  15505  tanhbnd  15506  efieq  15508  sinbnd  15525  cosbnd  15526  absefi  15541  dvdsaddre2b  15649  odd2np1  15682  bezoutlem1  15877  xrsdsreclb  20138  remulg  20296  resubdrg  20297  remetdval  23394  bl2ioo  23397  ioo2bl  23398  cnperf  23425  icccvx  23555  tcphcph  23841  shft2rab  24112  volsup2  24209  volcn  24210  c1lip1  24600  plyreres  24879  aalioulem3  24930  taylthlem2  24969  reeff1o  25042  reefgim  25045  sincosq1sgn  25091  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  sinq12gt0  25100  pige3ALT  25112  efif1olem4  25137  efifo  25139  relogrn  25153  logrnaddcl  25166  relogoprlem  25182  advlog  25245  advlogexp  25246  logtayl  25251  recxpcl  25266  rpcxpcl  25267  cxpge0  25274  cxpcom  25328  dvcxp1  25329  logreclem  25348  relogbreexp  25361  relogbcxp  25371  angpieqvd  25417  atanre  25471  basellem9  25674  gausslemma2dlem1a  25949  2sqnn0  26022  log2sumbnd  26128  brbtwn2  26699  colinearalglem4  26703  colinearalg  26704  crctcshwlkn0lem1  27596  nvsge0  28447  nmoub3i  28556  nmlnoubi  28579  isblo3i  28584  ipasslem3  28616  ipasslem9  28621  ipasslem11  28623  hmopm  29804  riesz1  29848  leopmuli  29916  leopmul  29917  leopmul2i  29918  leopnmid  29921  nmopleid  29922  cdj1i  30216  cdj3lem1  30217  cdj3i  30224  addltmulALT  30229  dpfrac1  30594  rexdiv  30628  xdivid  30630  xdiv0  30631  rmulccn  31281  sgnneg  31908  lediv2aALT  33033  nndivlub  33919  irrdiff  34740  cos2h  35048  tan2h  35049  poimir  35090  mblfinlem2  35095  mblfinlem4  35097  itg2addnclem  35108  itg2addnclem2  35109  dvasin  35141  areacirclem1  35145  areacirclem2  35146  areacirclem4  35148  areacirclem5  35149  areacirc  35150  lcmineqlem12  39328  2xp3dxp2ge1d  39387  resubeulem2  39514  renegneg  39549  renegid2  39551  sn-it0e0  39552  sn-negex12  39553  resubeqsub  39566  sn-mulid2  39572  sn-mul02  39577  areaquad  40166  reabssgn  40336  radcnvrat  41018  lhe4.4ex1a  41033  expgrowthi  41037  mulltgt0  41651  refsum2cnlem1  41666  infnsuprnmpt  41888  dstregt0  41912  suplesup  41971  infleinflem1  42002  infleinflem2  42003  ltdiv23neg  42030  rexabslelem  42055  supminfrnmpt  42082  supminfxr  42103  fmul01lt1lem1  42226  lptre2pt  42282  cnrefiisplem  42471  dvcosre  42554  itgsin0pilem1  42592  itgsinexplem1  42596  volioc  42614  volico  42625  stoweidlem7  42649  stoweidlem10  42652  stoweidlem19  42661  stoweidlem34  42676  stoweid  42705  dirker2re  42734  dirkerdenne0  42735  dirkerper  42738  dirkertrigeq  42743  dirkeritg  42744  fourierdlem39  42788  fourierdlem42  42791  fourierdlem47  42795  fourierdlem56  42804  fourierdlem57  42805  fourierdlem58  42806  fourierdlem60  42808  fourierdlem61  42809  fourierdlem73  42821  fourierdlem76  42824  fourierdlem77  42825  fourierdlem92  42840  fourierdlem97  42845  etransclem46  42922  volico2  43280  smflimlem4  43407  smfinflem  43448  2leaddle2  43855  ltsubsubaddltsub  43858  sqrtnegnre  43864  m1mod0mod1  43886  requad01  44139  requad1  44140  bgoldbtbndlem2  44324  flsubz  44931  rege1logbrege0  44972  nn0digval  45014  rrx2vlinest  45155  line2  45166  line2xlem  45167  line2x  45168  itscnhlc0yqe  45173  itsclc0yqsollem2  45177  itsclc0yqsol  45178  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180  itsclc0xyqsolr  45183  itsclquadb  45190  reseccl  45279  recsccl  45280  recotcl  45281