Theorem recn 8158

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8023  ℝcr 8024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8117

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  mulrid  8169  recnd  8201  pnfnre  8214  mnfnre  8215  cnegexlem1  8347  cnegexlem2  8348  cnegexlem3  8349  cnegex  8350  renegcl  8433  resubcl  8436  negf1o  8554  mul02lem2  8560  ltaddneg  8597  ltaddnegr  8598  ltaddsub2  8610  leaddsub2  8612  leltadd  8620  ltaddpos  8625  ltaddpos2  8626  posdif  8628  lenegcon1  8639  lenegcon2  8640  addge01  8645  addge02  8646  leaddle0  8650  mullt0  8653  recexre  8751  msqge0  8789  mulge0  8792  aprcl  8819  recexap  8826  rerecapb  9016  ltm1  9019  prodgt02  9026  prodge02  9028  ltmul2  9029  lemul2  9030  lemul2a  9032  ltmulgt12  9038  lemulge12  9040  gt0div  9043  ge0div  9044  ltmuldiv2  9048  ltdivmul  9049  ltdivmul2  9051  ledivmul2  9053  lemuldiv2  9055  negiso  9128  cju  9134  nnge1  9159  halfpos  9368  lt2halves  9373  addltmul  9374  avgle1  9378  avgle2  9379  div4p1lem1div2  9391  nnrecl  9393  elznn0  9487  elznn  9488  nzadd  9525  zmulcl  9526  difgtsumgt  9542  elz2  9544  gtndiv  9568  zeo  9578  supminfex  9824  eqreznegel  9841  negm  9842  irradd  9873  irrmul  9874  divlt1lt  9952  divle1le  9953  xnegneg  10061  rexsub  10081  xnegid  10087  xaddcom  10089  xaddid1  10090  xnegdi  10096  xaddass  10097  xleaddadd  10115  divelunit  10230  fzonmapblen  10419  infssuzex  10486  expgt1  10832  mulexpzap  10834  leexp1a  10849  expubnd  10851  sqgt0ap  10863  lt2sq  10868  le2sq  10869  sqge0  10871  sumsqeq0  10873  bernneq  10915  bernneq2  10916  nn0ltexp2  10964  swrdccatin2  11303  swrdccat3blem  11313  crre  11411  crim  11412  reim0  11415  mulreap  11418  rere  11419  remul2  11427  redivap  11428  immul2  11434  imdivap  11435  cjre  11436  cjreim  11457  rennim  11556  sqrt0rlem  11557  resqrexlemover  11564  absreimsq  11621  absreim  11622  absnid  11627  leabs  11628  absre  11631  absresq  11632  sqabs  11636  ltabs  11641  absdiflt  11646  absdifle  11647  lenegsq  11649  abssuble0  11657  dfabsmax  11771  max0addsup  11773  negfi  11782  minclpr  11791  reefcl  12222  efgt0  12238  reeftlcl  12243  resinval  12269  recosval  12270  resin4p  12272  recos4p  12273  resincl  12274  recoscl  12275  retanclap  12276  efieq  12289  sinbnd  12306  cosbnd  12307  absefi  12323  odd2np1  12427  remetdval  15264  bl2ioo  15267  ioo2bl  15268  hoverb  15365  plyreres  15481  sincosq1sgn  15543  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  relogoprlem  15585  logcxp  15614  rpcxpcl  15620  cxpcom  15655  rprelogbdiv  15674  gausslemma2dlem1a  15780  triap  16583  trirec0  16598