Theorem recn 11245

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℝcr 11154

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 2007  ax-8 2110  ax-resscn 11212

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

This theorem is referenced by:  mulrid  11259  recnd  11289  pnfnre  11302  mnfnre  11304  mul02  11439  ltaddneg  11477  ltaddnegr  11478  renegcli  11570  resubcl  11573  negn0  11692  negf1o  11693  ltaddsub2  11738  leaddsub2  11740  leltadd  11747  ltaddpos  11753  ltaddpos2  11754  posdif  11756  lenegcon1  11767  lenegcon2  11768  addge01  11773  addge02  11774  leaddle0  11778  mullt0  11782  recex  11895  ltm1  12109  prodgt02  12115  ltmul2  12118  lemul1  12119  lemul2  12120  lemul1a  12121  lemul2a  12122  ltmulgt12  12128  lemulge12  12131  gt0div  12134  ge0div  12135  mulge0b  12138  mulle0b  12139  ltmuldiv2  12142  ltdivmul  12143  ledivmul  12144  ltdivmul2  12145  lt2mul2div  12146  ledivmul2  12147  lemuldiv2  12149  ltdiv2  12154  ltrec1  12155  lerec2  12156  ledivdiv  12157  lediv2  12158  ltdiv23  12159  lediv23  12160  lediv12a  12161  recp1lt1  12166  ledivp1  12170  negfi  12217  infm3lem  12226  supmul  12240  riotaneg  12247  negiso  12248  cju  12262  nnge1  12294  halfpos  12496  lt2halves  12501  addltmul  12502  avgle1  12506  avgle2  12507  avgle  12508  div4p1lem1div2  12521  nnrecl  12524  difgtsumgt  12579  elznn0  12628  elznn  12629  elz2  12631  nzadd  12665  zmulcl  12666  gtndiv  12695  zeo  12704  eqreznegel  12976  supminf  12977  rebtwnz  12989  irradd  13015  irrmul  13016  divlt1lt  13104  divle1le  13105  max0sub  13238  xnegneg  13256  rexsub  13275  xnegid  13280  xaddcom  13282  xaddrid  13283  xnegdi  13290  xaddass  13291  rexmul  13313  xmulasslem3  13328  xadddilem  13336  divelunit  13534  fzonmapblen  13748  ico01fl0  13859  flzadd  13866  ltdifltdiv  13874  dfceil2  13879  intfrac2  13898  fldiv2  13901  flpmodeq  13914  mod0  13916  negmod0  13918  modlt  13920  modfrac  13924  flmod  13925  intfrac  13926  modmulnn  13929  modvalp1  13930  modid  13936  modcyc  13946  modcyc2  13947  modadd1  13948  modaddabs  13949  muladdmodid  13951  muladdmod  13953  negmod  13957  modadd2mod  13962  modmul1  13965  modmulmodr  13978  modaddmulmod  13979  moddi  13980  modsubdir  13981  modirr  13983  addmodlteq  13987  expgt1  14141  mulexpz  14143  sqgt0  14166  lt2sq  14173  le2sq  14174  sqge0  14176  expmordi  14207  leexp1a  14215  expubnd  14217  sumsqeq0  14218  sqlecan  14248  bernneq  14268  bernneq2  14269  expnbnd  14271  digit2  14275  digit1  14276  expnngt1  14280  swrdccatin2  14767  swrdccat3blem  14777  cshweqrep  14859  crre  15153  crim  15154  reim0  15157  mulre  15160  rere  15161  remul2  15169  rediv  15170  immul2  15176  imdiv  15177  cjre  15178  cjreim  15199  rennim  15278  resqrex  15289  resqreu  15291  resqrtcl  15292  resqrtthlem  15293  sqrtneglem  15305  sqrtneg  15306  absreimsq  15331  absreim  15332  absnid  15337  leabs  15338  absre  15340  absresq  15341  sqabs  15346  max0add  15349  absz  15350  absdiflt  15356  absdifle  15357  lenegsq  15359  abssuble0  15367  absmax  15368  rddif  15379  absrdbnd  15380  o1rlimmul  15655  caurcvg2  15714  reefcl  16123  efgt0  16139  reeftlcl  16144  resinval  16171  recosval  16172  resin4p  16174  recos4p  16175  resincl  16176  recoscl  16177  retancl  16178  resinhcl  16192  rpcoshcl  16193  retanhcl  16195  tanhlt1  16196  tanhbnd  16197  efieq  16199  sinbnd  16216  cosbnd  16217  absefi  16232  dvdsaddre2b  16344  odd2np1  16378  bezoutlem1  16576  xrsdsreclb  21431  remulg  21625  resubdrg  21626  remetdval  24810  bl2ioo  24813  ioo2bl  24814  cnperf  24842  icccvx  24981  tcphcph  25271  shft2rab  25543  volsup2  25640  volcn  25641  c1lip1  26036  plyreres  26324  aalioulem3  26376  taylthlem2  26416  taylthlem2OLD  26417  reeff1o  26491  reefgim  26494  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sinq12gt0  26549  pige3ALT  26562  efif1olem4  26587  efifo  26589  relogrn  26603  logrnaddcl  26616  relogoprlem  26633  advlog  26696  advlogexp  26697  logtayl  26702  recxpcl  26717  rpcxpcl  26718  cxpge0  26725  cxpcom  26781  dvcxp1  26782  logreclem  26805  relogbreexp  26818  relogbcxp  26828  angpieqvd  26874  atanre  26928  basellem9  27132  gausslemma2dlem1a  27409  2sqnn0  27482  log2sumbnd  27588  brbtwn2  28920  colinearalglem4  28924  colinearalg  28925  crctcshwlkn0lem1  29830  nvsge0  30683  nmoub3i  30792  nmlnoubi  30815  isblo3i  30820  ipasslem3  30852  ipasslem9  30857  ipasslem11  30859  hmopm  32040  riesz1  32084  leopmuli  32152  leopmul  32153  leopmul2i  32154  leopnmid  32157  nmopleid  32158  cdj1i  32452  cdj3lem1  32453  cdj3i  32460  addltmulALT  32465  dpfrac1  32874  rexdiv  32908  xdivid  32910  xdiv0  32911  sgnneg  34543  lediv2aALT  35682  nndivlub  36459  irrdiff  37327  cos2h  37618  tan2h  37619  poimir  37660  mblfinlem2  37665  mblfinlem4  37667  itg2addnclem  37678  itg2addnclem2  37679  dvasin  37711  areacirclem1  37715  areacirclem2  37716  areacirclem4  37718  areacirclem5  37719  areacirc  37720  lcmineqlem12  42041  dvrelog2b  42067  aks4d1p1p6  42074  2xp3dxp2ge1d  42242  retire  42354  readvrec2  42391  readvrec  42392  resubeulem2  42406  renegneg  42441  renegid2  42443  sn-it0e0  42445  sn-negex12  42446  resubeqsub  42459  sn-mullid  42465  sn-mul02  42470  areaquad  43228  reabssgn  43649  radcnvrat  44333  lhe4.4ex1a  44348  expgrowthi  44352  mulltgt0  45027  refsum2cnlem1  45042  infnsuprnmpt  45257  dstregt0  45293  suplesup  45350  infleinflem1  45381  infleinflem2  45382  ltdiv23neg  45405  rexabslelem  45429  supminfrnmpt  45456  supminfxr  45475  fmul01lt1lem1  45599  lptre2pt  45655  cnrefiisplem  45844  dvcosre  45927  itgsin0pilem1  45965  itgsinexplem1  45969  volioc  45987  volico  45998  stoweidlem7  46022  stoweidlem10  46025  stoweidlem19  46034  stoweidlem34  46049  stoweid  46078  dirker2re  46107  dirkerdenne0  46108  dirkerper  46111  dirkertrigeq  46116  dirkeritg  46117  fourierdlem39  46161  fourierdlem42  46164  fourierdlem47  46168  fourierdlem56  46177  fourierdlem57  46178  fourierdlem58  46179  fourierdlem60  46181  fourierdlem61  46182  fourierdlem73  46194  fourierdlem76  46197  fourierdlem77  46198  fourierdlem92  46213  fourierdlem97  46218  etransclem46  46295  volico2  46656  smflimlem4  46789  smfinflem  46832  et-sqrtnegnre  46888  2leaddle2  47310  ltsubsubaddltsub  47313  sqrtnegnre  47319  ceildivmod  47341  m1mod0mod1  47356  requad01  47608  requad1  47609  bgoldbtbndlem2  47793  flsubz  48439  rege1logbrege0  48479  nn0digval  48521  rrx2vlinest  48662  line2  48673  line2xlem  48674  line2x  48675  itscnhlc0yqe  48680  itsclc0yqsollem2  48684  itsclc0yqsol  48685  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itsclc0xyqsolr  48690  itsclquadb  48697  reseccl  49272  recsccl  49273  recotcl  49274