Theorem recn 10311

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

Syntax hints:   → wi 4   ∈ wcel 2156  ℂcc 10219  ℝcr 10220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784  ax-resscn 10278

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783

This theorem is referenced by:  mulid1  10323  recnd  10353  pnfnre  10366  mnfnre  10367  mul02  10499  ltaddneg  10536  ltaddnegr  10537  renegcli  10627  resubcl  10630  negn0  10744  negf1o  10745  ltaddsub2  10788  leaddsub2  10790  leltadd  10797  ltaddpos  10803  ltaddpos2  10804  posdif  10806  lenegcon1  10817  lenegcon2  10818  addge01  10823  addge02  10824  leaddle0  10828  mullt0  10832  recex  10944  ltm1  11148  prodgt02  11154  prodge02OLD  11156  ltmul2  11159  lemul1  11160  lemul2  11161  lemul1a  11162  lemul2a  11163  ltmulgt12  11169  lemulge12  11171  gt0div  11174  ge0div  11175  mulge0b  11178  mulle0b  11179  ltmuldiv2  11182  ltdivmul  11183  ledivmul  11184  ltdivmul2  11185  lt2mul2div  11186  ledivmul2  11187  lemuldiv2  11189  ltdiv2  11194  ltrec1  11195  lerec2  11196  ledivdiv  11197  lediv2  11198  ltdiv23  11199  lediv23  11200  lediv12a  11201  recp1lt1  11206  ledivp1  11210  negfi  11256  fiminre  11257  infm3lem  11266  supmul  11280  riotaneg  11287  negiso  11288  cju  11301  nnge1  11332  halfpos  11529  lt2halves  11534  addltmul  11535  avgle1  11539  avgle2  11540  avgle  11541  div4p1lem1div2  11554  nnrecl  11557  difgtsumgt  11612  elznn0  11658  elznn  11659  elz2  11660  nzadd  11691  zmulcl  11692  gtndiv  11720  zeo  11729  eqreznegel  11993  supminf  11994  rebtwnz  12006  irradd  12031  irrmul  12032  divlt1lt  12113  divle1le  12114  max0sub  12245  xnegneg  12263  rexsub  12282  xnegid  12287  xaddcom  12289  xaddid1  12290  xnegdi  12296  xaddass  12297  rexmul  12319  xmulasslem3  12334  xadddilem  12342  divelunit  12537  fzonmapblen  12738  ico01fl0  12844  flzadd  12851  ltdifltdiv  12859  dfceil2  12864  intfrac2  12881  fldiv2  12884  flpmodeq  12897  mod0  12899  negmod0  12901  modlt  12903  modfrac  12907  flmod  12908  intfrac  12909  modmulnn  12912  modvalp1  12913  modid  12919  modcyc  12929  modcyc2  12930  modadd1  12931  modaddabs  12932  muladdmodid  12934  negmod  12939  modadd2mod  12944  modmul1  12947  modmulmodr  12960  modaddmulmod  12961  moddi  12962  modsubdir  12963  modirr  12965  addmodlteq  12969  expgt1  13121  mulexpz  13123  leexp1a  13142  expubnd  13144  sqgt0  13155  lt2sq  13160  le2sq  13161  sqge0  13163  sumsqeq0  13165  sqlecan  13194  bernneq  13213  bernneq2  13214  expnbnd  13216  digit2  13220  digit1  13221  swrdccatin2  13711  swrdccat3blem  13719  cshweqrep  13791  crre  14077  crim  14078  reim0  14081  mulre  14084  rere  14085  remul2  14093  rediv  14094  immul2  14100  imdiv  14101  cjre  14102  cjreim  14123  rennim  14202  resqrex  14214  resqreu  14216  resqrtcl  14217  resqrtthlem  14218  sqrtneglem  14230  sqrtneg  14231  absreimsq  14255  absreim  14256  absnid  14261  leabs  14262  absre  14264  absresq  14265  sqabs  14270  max0add  14273  absz  14274  absdiflt  14280  absdifle  14281  lenegsq  14283  abssuble0  14291  absmax  14292  rddif  14303  absrdbnd  14304  o1rlimmul  14572  caurcvg2  14631  reefcl  15037  efgt0  15053  reeftlcl  15058  resinval  15085  recosval  15086  resin4p  15088  recos4p  15089  resincl  15090  recoscl  15091  retancl  15092  resinhcl  15106  rpcoshcl  15107  retanhcl  15109  tanhlt1  15110  tanhbnd  15111  efieq  15113  sinbnd  15130  cosbnd  15131  absefi  15146  dvdsaddre2b  15252  odd2np1  15285  bezoutlem1  15475  xrsdsreclb  20001  remulg  20162  resubdrg  20163  remetdval  22805  bl2ioo  22808  ioo2bl  22809  cnperf  22836  icccvx  22962  tchcph  23248  shft2rab  23489  volsup2  23586  volcn  23587  c1lip1  23974  plyreres  24252  aalioulem3  24303  taylthlem2  24342  reeff1o  24415  reefgim  24418  sincosq1sgn  24465  sincosq2sgn  24466  sincosq3sgn  24467  sincosq4sgn  24468  sinq12gt0  24474  pige3  24484  efif1olem4  24506  efifo  24508  relogrn  24522  logrnaddcl  24535  relogoprlem  24551  advlog  24614  advlogexp  24615  logtayl  24620  recxpcl  24635  rpcxpcl  24636  cxpge0  24643  dvcxp1  24695  logreclem  24714  relogbreexp  24727  relogbcxp  24737  angpieqvd  24772  atanre  24826  basellem9  25029  gausslemma2dlem1a  25304  log2sumbnd  25447  brbtwn2  25999  colinearalglem4  26003  colinearalg  26004  crctcshwlkn0lem1  26931  nvsge0  27847  nmoub3i  27956  nmlnoubi  27979  isblo3i  27984  ipasslem3  28016  ipasslem9  28021  ipasslem11  28023  hmopm  29208  riesz1  29252  leopmuli  29320  leopmul  29321  leopmul2i  29322  leopnmid  29325  nmopleid  29326  cdj1i  29620  cdj3lem1  29621  cdj3i  29628  addltmulALT  29633  dpfrac1  29925  rexdiv  29959  xdivid  29961  xdiv0  29962  rmulccn  30299  sgnneg  30927  lediv2aALT  31893  nndivlub  32774  cos2h  33713  tan2h  33714  poimir  33755  mblfinlem2  33760  mblfinlem4  33762  itg2addnclem  33773  itg2addnclem2  33774  dvasin  33808  areacirclem1  33812  areacirclem2  33813  areacirclem4  33815  areacirclem5  33816  areacirc  33817  expmordi  38013  areaquad  38302  radcnvrat  39013  lhe4.4ex1a  39028  expgrowthi  39032  mulltgt0  39675  refsum2cnlem1  39690  infnsuprnmpt  39948  dstregt0  39975  suplesup  40035  infleinflem1  40066  infleinflem2  40067  ltdiv23neg  40096  rexabslelem  40124  supminfrnmpt  40151  supminfxr  40173  fmul01lt1lem1  40296  lptre2pt  40352  cnrefiisplem  40535  dvcosre  40606  itgsin0pilem1  40645  itgsinexplem1  40649  volioc  40667  volico  40679  stoweidlem7  40703  stoweidlem10  40706  stoweidlem19  40715  stoweidlem34  40730  stoweid  40759  dirker2re  40788  dirkerdenne0  40789  dirkerper  40792  dirkertrigeq  40797  dirkeritg  40798  fourierdlem39  40842  fourierdlem42  40845  fourierdlem47  40849  fourierdlem56  40858  fourierdlem57  40859  fourierdlem58  40860  fourierdlem60  40862  fourierdlem61  40863  fourierdlem73  40875  fourierdlem76  40878  fourierdlem77  40879  fourierdlem92  40894  fourierdlem97  40899  etransclem46  40976  volico2  41337  smflimlem4  41464  smfinflem  41505  2leaddle2  41888  ltsubsubaddltsub  41891  m1mod0mod1  41914  bgoldbtbndlem2  42269  flsubz  42880  rege1logbrege0  42920  nn0digval  42962  reseccl  43065  recsccl  43066  recotcl  43067