Theorem recn 8256

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8121  ℝcr 8122

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8215

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  mulrid  8267  recnd  8298  pnfnre  8311  mnfnre  8312  cnegexlem1  8444  cnegexlem2  8445  cnegexlem3  8446  cnegex  8447  renegcl  8530  resubcl  8533  negf1o  8651  mul02lem2  8657  ltaddneg  8694  ltaddnegr  8695  ltaddsub2  8707  leaddsub2  8709  leltadd  8717  ltaddpos  8722  ltaddpos2  8723  posdif  8725  lenegcon1  8736  lenegcon2  8737  addge01  8742  addge02  8743  leaddle0  8747  mullt0  8750  recexre  8848  msqge0  8886  mulge0  8889  aprcl  8916  recexap  8923  rerecapb  9113  ltm1  9116  prodgt02  9123  prodge02  9125  ltmul2  9126  lemul2  9127  lemul2a  9129  ltmulgt12  9135  lemulge12  9137  gt0div  9140  ge0div  9141  ltmuldiv2  9145  ltdivmul  9146  ltdivmul2  9148  ledivmul2  9150  lemuldiv2  9152  negiso  9225  cju  9231  nnge1  9256  halfpos  9465  lt2halves  9470  addltmul  9471  avgle1  9475  avgle2  9476  div4p1lem1div2  9488  nnrecl  9490  elznn0  9588  elznn  9589  nzadd  9626  zmulcl  9627  difgtsumgt  9643  elz2  9645  gtndiv  9669  zeo  9679  supminfex  9925  eqreznegel  9942  negm  9943  irradd  9974  irrmul  9975  divlt1lt  10053  divle1le  10054  xnegneg  10162  rexsub  10182  xnegid  10188  xaddcom  10190  xaddid1  10191  xnegdi  10197  xaddass  10198  xleaddadd  10216  divelunit  10331  fzonmapblen  10522  infssuzex  10589  expgt1  10935  mulexpzap  10937  leexp1a  10952  expubnd  10954  sqgt0ap  10966  lt2sq  10971  le2sq  10972  sqge0  10974  sumsqeq0  10976  bernneq  11018  bernneq2  11019  nn0ltexp2  11067  swrdccatin2  11414  swrdccat3blem  11424  crre  11535  crim  11536  reim0  11539  mulreap  11542  rere  11543  remul2  11551  redivap  11552  immul2  11558  imdivap  11559  cjre  11560  cjreim  11581  rennim  11680  sqrt0rlem  11681  resqrexlemover  11688  absreimsq  11745  absreim  11746  absnid  11751  leabs  11752  absre  11755  absresq  11756  sqabs  11760  ltabs  11765  absdiflt  11770  absdifle  11771  lenegsq  11773  abssuble0  11781  dfabsmax  11895  max0addsup  11897  negfi  11906  minclpr  11915  reefcl  12347  efgt0  12363  reeftlcl  12368  resinval  12394  recosval  12395  resin4p  12397  recos4p  12398  resincl  12399  recoscl  12400  retanclap  12401  efieq  12414  sinbnd  12431  cosbnd  12432  absefi  12448  odd2np1  12552  remetdval  15399  bl2ioo  15402  ioo2bl  15403  hoverb  15500  plyreres  15616  sincosq1sgn  15678  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  sinq12gt0  15682  relogoprlem  15720  logcxp  15749  rpcxpcl  15755  cxpcom  15790  rprelogbdiv  15809  gausslemma2dlem1a  15918  triap  16800  trirec0  16815