Theorem recn 11158

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℝcr 11067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3931

This theorem is referenced by:  mulrid  11172  recnd  11202  pnfnre  11215  mnfnre  11217  mul02  11352  ltaddneg  11390  ltaddnegr  11391  renegcli  11483  resubcl  11486  negn0  11607  negf1o  11608  ltaddsub2  11653  leaddsub2  11655  leltadd  11662  ltaddpos  11668  ltaddpos2  11669  posdif  11671  lenegcon1  11682  lenegcon2  11683  addge01  11688  addge02  11689  leaddle0  11693  mullt0  11697  recex  11810  ltm1  12024  prodgt02  12030  ltmul2  12033  lemul1  12034  lemul2  12035  lemul1a  12036  lemul2a  12037  ltmulgt12  12043  lemulge12  12046  gt0div  12049  ge0div  12050  mulge0b  12053  mulle0b  12054  ltmuldiv2  12057  ltdivmul  12058  ledivmul  12059  ltdivmul2  12060  lt2mul2div  12061  ledivmul2  12062  lemuldiv2  12064  ltdiv2  12069  ltrec1  12070  lerec2  12071  ledivdiv  12072  lediv2  12073  ltdiv23  12074  lediv23  12075  lediv12a  12076  recp1lt1  12081  ledivp1  12085  negfi  12132  infm3lem  12141  supmul  12155  riotaneg  12162  negiso  12163  cju  12182  nnge1  12214  halfpos  12412  lt2halves  12417  addltmul  12418  avgle1  12422  avgle2  12423  avgle  12424  div4p1lem1div2  12437  nnrecl  12440  difgtsumgt  12495  elznn0  12544  elznn  12545  elz2  12547  nzadd  12581  zmulcl  12582  gtndiv  12611  zeo  12620  eqreznegel  12893  supminf  12894  rebtwnz  12906  irradd  12932  irrmul  12933  divlt1lt  13022  divle1le  13023  max0sub  13156  xnegneg  13174  rexsub  13193  xnegid  13198  xaddcom  13200  xaddrid  13201  xnegdi  13208  xaddass  13209  rexmul  13231  xmulasslem3  13246  xadddilem  13254  divelunit  13455  fzonmapblen  13669  ico01fl0  13781  flzadd  13788  ltdifltdiv  13796  dfceil2  13801  intfrac2  13820  fldiv2  13823  flpmodeq  13836  mod0  13838  negmod0  13840  modlt  13842  modfrac  13846  flmod  13847  intfrac  13848  modmulnn  13851  modvalp1  13852  modid  13858  modcyc  13868  modcyc2  13869  modadd1  13870  modaddabs  13873  muladdmodid  13875  muladdmod  13877  negmod  13881  modadd2mod  13886  modmul1  13889  modmulmodr  13902  modaddmulmod  13903  moddi  13904  modsubdir  13905  modirr  13907  addmodlteq  13911  expgt1  14065  mulexpz  14067  sqgt0  14091  lt2sq  14098  le2sq  14099  sqge0  14101  expmordi  14132  leexp1a  14140  expubnd  14143  sumsqeq0  14144  sqlecan  14174  bernneq  14194  bernneq2  14195  expnbnd  14197  digit2  14201  digit1  14202  expnngt1  14206  swrdccatin2  14694  swrdccat3blem  14704  cshweqrep  14786  crre  15080  crim  15081  reim0  15084  mulre  15087  rere  15088  remul2  15096  rediv  15097  immul2  15103  imdiv  15104  cjre  15105  cjreim  15126  rennim  15205  resqrex  15216  resqreu  15218  resqrtcl  15219  resqrtthlem  15220  sqrtneglem  15232  sqrtneg  15233  absreimsq  15258  absreim  15259  absnid  15264  leabs  15265  absre  15267  absresq  15268  sqabs  15273  max0add  15276  absz  15277  absdiflt  15284  absdifle  15285  lenegsq  15287  abssuble0  15295  absmax  15296  rddif  15307  absrdbnd  15308  o1rlimmul  15585  caurcvg2  15644  reefcl  16053  efgt0  16071  reeftlcl  16076  resinval  16103  recosval  16104  resin4p  16106  recos4p  16107  resincl  16108  recoscl  16109  retancl  16110  resinhcl  16124  rpcoshcl  16125  retanhcl  16127  tanhlt1  16128  tanhbnd  16129  efieq  16131  sinbnd  16148  cosbnd  16149  absefi  16164  dvdsaddre2b  16277  odd2np1  16311  bezoutlem1  16509  xrsdsreclb  21330  remulg  21516  resubdrg  21517  remetdval  24677  bl2ioo  24680  ioo2bl  24681  cnperf  24709  icccvx  24848  tcphcph  25137  shft2rab  25409  volsup2  25506  volcn  25507  c1lip1  25902  plyreres  26190  aalioulem3  26242  taylthlem2  26282  taylthlem2OLD  26283  reeff1o  26357  reefgim  26360  sincosq1sgn  26407  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  sinq12gt0  26416  pige3ALT  26429  efif1olem4  26454  efifo  26456  relogrn  26470  logrnaddcl  26483  relogoprlem  26500  advlog  26563  advlogexp  26564  logtayl  26569  recxpcl  26584  rpcxpcl  26585  cxpge0  26592  cxpcom  26648  dvcxp1  26649  logreclem  26672  relogbreexp  26685  relogbcxp  26695  angpieqvd  26741  atanre  26795  basellem9  26999  gausslemma2dlem1a  27276  2sqnn0  27349  log2sumbnd  27455  brbtwn2  28832  colinearalglem4  28836  colinearalg  28837  crctcshwlkn0lem1  29740  nvsge0  30593  nmoub3i  30702  nmlnoubi  30725  isblo3i  30730  ipasslem3  30762  ipasslem9  30767  ipasslem11  30769  hmopm  31950  riesz1  31994  leopmuli  32062  leopmul  32063  leopmul2i  32064  leopnmid  32067  nmopleid  32068  cdj1i  32362  cdj3lem1  32363  cdj3i  32370  addltmulALT  32375  sgnneg  32758  dpfrac1  32812  rexdiv  32846  xdivid  32848  xdiv0  32849  lediv2aALT  35664  nndivlub  36446  irrdiff  37314  cos2h  37605  tan2h  37606  poimir  37647  mblfinlem2  37652  mblfinlem4  37654  itg2addnclem  37665  itg2addnclem2  37666  dvasin  37698  areacirclem1  37702  areacirclem2  37703  areacirclem4  37705  areacirclem5  37706  areacirc  37707  lcmineqlem12  42028  dvrelog2b  42054  aks4d1p1p6  42061  retire  42307  readvrec2  42349  readvrec  42350  resubeulem2  42364  renegneg  42400  renegid2  42402  sn-it0e0  42404  sn-negex12  42405  resubeqsub  42418  sn-mullid  42424  sn-mul02  42440  areaquad  43205  reabssgn  43625  radcnvrat  44303  lhe4.4ex1a  44318  expgrowthi  44322  mulltgt0  45016  refsum2cnlem1  45031  infnsuprnmpt  45244  dstregt0  45280  suplesup  45335  infleinflem1  45366  infleinflem2  45367  ltdiv23neg  45390  rexabslelem  45414  supminfrnmpt  45441  supminfxr  45460  fmul01lt1lem1  45582  lptre2pt  45638  cnrefiisplem  45827  dvcosre  45910  itgsin0pilem1  45948  itgsinexplem1  45952  volioc  45970  volico  45981  stoweidlem7  46005  stoweidlem10  46008  stoweidlem19  46017  stoweidlem34  46032  stoweid  46061  dirker2re  46090  dirkerdenne0  46091  dirkerper  46094  dirkertrigeq  46099  dirkeritg  46100  fourierdlem39  46144  fourierdlem42  46147  fourierdlem47  46151  fourierdlem56  46160  fourierdlem57  46161  fourierdlem58  46162  fourierdlem60  46164  fourierdlem61  46165  fourierdlem73  46177  fourierdlem76  46180  fourierdlem77  46181  fourierdlem92  46196  fourierdlem97  46201  etransclem46  46278  volico2  46639  smflimlem4  46772  smfinflem  46815  et-sqrtnegnre  46871  squeezedltsq  46887  2leaddle2  47299  ltsubsubaddltsub  47302  sqrtnegnre  47308  ceildivmod  47340  m1mod0mod1  47355  requad01  47622  requad1  47623  bgoldbtbndlem2  47807  flsubz  48511  rege1logbrege0  48547  nn0digval  48589  rrx2vlinest  48730  line2  48741  line2xlem  48742  line2x  48743  itscnhlc0yqe  48748  itsclc0yqsollem2  48752  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  itsclquadb  48765  reseccl  49742  recsccl  49743  recotcl  49744