Theorem recn 10362

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 10329	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 3817	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10270  ℝcr 10271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-resscn 10329

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  mulid1  10374  recnd  10405  pnfnre  10418  mnfnre  10419  mul02  10554  ltaddneg  10591  ltaddnegr  10592  renegcli  10684  resubcl  10687  negn0  10804  negf1o  10805  ltaddsub2  10850  leaddsub2  10852  leltadd  10859  ltaddpos  10865  ltaddpos2  10866  posdif  10868  lenegcon1  10879  lenegcon2  10880  addge01  10885  addge02  10886  leaddle0  10890  mullt0  10894  recex  11007  ltm1  11217  prodgt02  11223  prodge02OLD  11225  ltmul2  11228  lemul1  11229  lemul2  11230  lemul1a  11231  lemul2a  11232  ltmulgt12  11238  lemulge12  11240  gt0div  11243  ge0div  11244  mulge0b  11247  mulle0b  11248  ltmuldiv2  11251  ltdivmul  11252  ledivmul  11253  ltdivmul2  11254  lt2mul2div  11255  ledivmul2  11256  lemuldiv2  11258  ltdiv2  11263  ltrec1  11264  lerec2  11265  ledivdiv  11266  lediv2  11267  ltdiv23  11268  lediv23  11269  lediv12a  11270  recp1lt1  11275  ledivp1  11279  negfi  11325  fiminre  11326  infm3lem  11335  supmul  11349  riotaneg  11356  negiso  11357  cju  11370  nnge1  11404  halfpos  11612  lt2halves  11617  addltmul  11618  avgle1  11622  avgle2  11623  avgle  11624  div4p1lem1div2  11637  nnrecl  11640  difgtsumgt  11697  elznn0  11743  elznn  11744  elz2  11745  nzadd  11777  zmulcl  11778  gtndiv  11806  zeo  11815  eqreznegel  12081  supminf  12082  rebtwnz  12094  irradd  12120  irrmul  12121  divlt1lt  12208  divle1le  12209  max0sub  12339  xnegneg  12357  rexsub  12376  xnegid  12381  xaddcom  12383  xaddid1  12384  xnegdi  12390  xaddass  12391  rexmul  12413  xmulasslem3  12428  xadddilem  12436  divelunit  12631  fzonmapblen  12833  ico01fl0  12939  flzadd  12946  ltdifltdiv  12954  dfceil2  12959  intfrac2  12976  fldiv2  12979  flpmodeq  12992  mod0  12994  negmod0  12996  modlt  12998  modfrac  13002  flmod  13003  intfrac  13004  modmulnn  13007  modvalp1  13008  modid  13014  modcyc  13024  modcyc2  13025  modadd1  13026  modaddabs  13027  muladdmodid  13029  negmod  13034  modadd2mod  13039  modmul1  13042  modmulmodr  13055  modaddmulmod  13056  moddi  13057  modsubdir  13058  modirr  13060  addmodlteq  13064  expgt1  13216  mulexpz  13218  leexp1a  13237  expubnd  13239  sqgt0  13250  lt2sq  13256  le2sq  13257  sqge0  13259  sumsqeq0  13261  sqlecan  13290  bernneq  13309  bernneq2  13310  expnbnd  13312  digit2  13316  digit1  13317  expnngt1  13347  swrdccatin2  13856  swrdccat3blem  13871  cshweqrep  13972  crre  14261  crim  14262  reim0  14265  mulre  14268  rere  14269  remul2  14277  rediv  14278  immul2  14284  imdiv  14285  cjre  14286  cjreim  14307  rennim  14386  resqrex  14398  resqreu  14400  resqrtcl  14401  resqrtthlem  14402  sqrtneglem  14414  sqrtneg  14415  absreimsq  14439  absreim  14440  absnid  14445  leabs  14446  absre  14448  absresq  14449  sqabs  14454  max0add  14457  absz  14458  absdiflt  14464  absdifle  14465  lenegsq  14467  abssuble0  14475  absmax  14476  rddif  14487  absrdbnd  14488  o1rlimmul  14757  caurcvg2  14816  reefcl  15219  efgt0  15235  reeftlcl  15240  resinval  15267  recosval  15268  resin4p  15270  recos4p  15271  resincl  15272  recoscl  15273  retancl  15274  resinhcl  15288  rpcoshcl  15289  retanhcl  15291  tanhlt1  15292  tanhbnd  15293  efieq  15295  sinbnd  15312  cosbnd  15313  absefi  15328  dvdsaddre2b  15436  odd2np1  15469  bezoutlem1  15662  xrsdsreclb  20189  remulg  20350  resubdrg  20351  remetdval  23000  bl2ioo  23003  ioo2bl  23004  cnperf  23031  icccvx  23157  tcphcph  23443  shft2rab  23712  volsup2  23809  volcn  23810  c1lip1  24197  plyreres  24475  aalioulem3  24526  taylthlem2  24565  reeff1o  24638  reefgim  24641  sincosq1sgn  24688  sincosq2sgn  24689  sincosq3sgn  24690  sincosq4sgn  24691  sinq12gt0  24697  pige3  24707  efif1olem4  24729  efifo  24731  relogrn  24745  logrnaddcl  24758  relogoprlem  24774  advlog  24837  advlogexp  24838  logtayl  24843  recxpcl  24858  rpcxpcl  24859  cxpge0  24866  cxpcom  24920  dvcxp1  24921  logreclem  24940  relogbreexp  24953  relogbcxp  24963  angpieqvd  25009  atanre  25063  basellem9  25267  gausslemma2dlem1a  25542  log2sumbnd  25685  brbtwn2  26254  colinearalglem4  26258  colinearalg  26259  crctcshwlkn0lem1  27159  nvsge0  28091  nmoub3i  28200  nmlnoubi  28223  isblo3i  28228  ipasslem3  28260  ipasslem9  28265  ipasslem11  28267  hmopm  29452  riesz1  29496  leopmuli  29564  leopmul  29565  leopmul2i  29566  leopnmid  29569  nmopleid  29570  cdj1i  29864  cdj3lem1  29865  cdj3i  29872  addltmulALT  29877  dpfrac1  30162  rexdiv  30196  xdivid  30198  xdiv0  30199  rmulccn  30572  sgnneg  31201  lediv2aALT  32168  nndivlub  33040  cos2h  34025  tan2h  34026  poimir  34068  mblfinlem2  34073  mblfinlem4  34075  itg2addnclem  34086  itg2addnclem2  34087  dvasin  34121  areacirclem1  34125  areacirclem2  34126  areacirclem4  34128  areacirclem5  34129  areacirc  34130  resubeulem2  38185  expmordi  38471  areaquad  38760  radcnvrat  39469  lhe4.4ex1a  39484  expgrowthi  39488  mulltgt0  40114  refsum2cnlem1  40129  infnsuprnmpt  40376  dstregt0  40403  suplesup  40463  infleinflem1  40494  infleinflem2  40495  ltdiv23neg  40523  rexabslelem  40551  supminfrnmpt  40578  supminfxr  40599  fmul01lt1lem1  40724  lptre2pt  40780  cnrefiisplem  40969  dvcosre  41054  itgsin0pilem1  41093  itgsinexplem1  41097  volioc  41115  volico  41127  stoweidlem7  41151  stoweidlem10  41154  stoweidlem19  41163  stoweidlem34  41178  stoweid  41207  dirker2re  41236  dirkerdenne0  41237  dirkerper  41240  dirkertrigeq  41245  dirkeritg  41246  fourierdlem39  41290  fourierdlem42  41293  fourierdlem47  41297  fourierdlem56  41306  fourierdlem57  41307  fourierdlem58  41308  fourierdlem60  41310  fourierdlem61  41311  fourierdlem73  41323  fourierdlem76  41326  fourierdlem77  41327  fourierdlem92  41342  fourierdlem97  41347  etransclem46  41424  volico2  41782  smflimlem4  41909  smfinflem  41950  2leaddle2  42340  ltsubsubaddltsub  42343  sqrtnegnre  42349  m1mod0mod1  42371  requad01  42559  requad1  42560  bgoldbtbndlem2  42719  flsubz  43327  rege1logbrege0  43367  nn0digval  43409  rrx2vlinest  43477  line2  43488  line2xlem  43489  line2x  43490  itscnhlc0yqe  43495  itsclc0yqsollem2  43499  itsclc0yqsol  43500  itscnhlc0xyqsol  43501  itschlc0xyqsol1  43502  itsclc0xyqsolr  43505  itsclquadb  43512  reseccl  43602  recsccl  43603  recotcl  43604