Theorem recn 7777

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℂcc 7642  ℝcr 7643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7736

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  mulid1  7787  recnd  7818  pnfnre  7831  mnfnre  7832  cnegexlem1  7961  cnegexlem2  7962  cnegexlem3  7963  cnegex  7964  renegcl  8047  resubcl  8050  negf1o  8168  mul02lem2  8174  ltaddneg  8210  ltaddnegr  8211  ltaddsub2  8223  leaddsub2  8225  leltadd  8233  ltaddpos  8238  ltaddpos2  8239  posdif  8241  lenegcon1  8252  lenegcon2  8253  addge01  8258  addge02  8259  leaddle0  8263  mullt0  8266  recexre  8364  msqge0  8402  mulge0  8405  aprcl  8432  recexap  8438  ltm1  8628  prodgt02  8635  prodge02  8637  ltmul2  8638  lemul2  8639  lemul2a  8641  ltmulgt12  8647  lemulge12  8649  gt0div  8652  ge0div  8653  ltmuldiv2  8657  ltdivmul  8658  ltdivmul2  8660  ledivmul2  8662  lemuldiv2  8664  negiso  8737  cju  8743  nnge1  8767  halfpos  8975  lt2halves  8979  addltmul  8980  avgle1  8984  avgle2  8985  div4p1lem1div2  8997  nnrecl  8999  elznn0  9093  elznn  9094  nzadd  9130  zmulcl  9131  elz2  9146  gtndiv  9170  zeo  9180  supminfex  9419  eqreznegel  9433  negm  9434  irradd  9465  irrmul  9466  divlt1lt  9541  divle1le  9542  xnegneg  9646  rexsub  9666  xnegid  9672  xaddcom  9674  xaddid1  9675  xnegdi  9681  xaddass  9682  xleaddadd  9700  divelunit  9815  fzonmapblen  9995  expgt1  10362  mulexpzap  10364  leexp1a  10379  expubnd  10381  sqgt0ap  10392  lt2sq  10397  le2sq  10398  sqge0  10400  sumsqeq0  10402  bernneq  10443  bernneq2  10444  crre  10661  crim  10662  reim0  10665  mulreap  10668  rere  10669  remul2  10677  redivap  10678  immul2  10684  imdivap  10685  cjre  10686  cjreim  10707  rennim  10806  sqrt0rlem  10807  resqrexlemover  10814  absreimsq  10871  absreim  10872  absnid  10877  leabs  10878  absre  10881  absresq  10882  sqabs  10886  ltabs  10891  absdiflt  10896  absdifle  10897  lenegsq  10899  abssuble0  10907  dfabsmax  11021  max0addsup  11023  negfi  11031  minclpr  11040  reefcl  11411  efgt0  11427  reeftlcl  11432  resinval  11458  recosval  11459  resin4p  11461  recos4p  11462  resincl  11463  recoscl  11464  retanclap  11465  efieq  11478  sinbnd  11495  cosbnd  11496  absefi  11511  odd2np1  11606  infssuzex  11678  remetdval  12747  bl2ioo  12750  ioo2bl  12751  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  relogoprlem  12997  logcxp  13026  rpcxpcl  13032  cxpcom  13065  rprelogbdiv  13082  triap  13399  trirec0  13412