Theorem recn 8140

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8005  ℝcr 8006

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 8099

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 3203  df-ss 3210

This theorem is referenced by:  mulrid  8151  recnd  8183  pnfnre  8196  mnfnre  8197  cnegexlem1  8329  cnegexlem2  8330  cnegexlem3  8331  cnegex  8332  renegcl  8415  resubcl  8418  negf1o  8536  mul02lem2  8542  ltaddneg  8579  ltaddnegr  8580  ltaddsub2  8592  leaddsub2  8594  leltadd  8602  ltaddpos  8607  ltaddpos2  8608  posdif  8610  lenegcon1  8621  lenegcon2  8622  addge01  8627  addge02  8628  leaddle0  8632  mullt0  8635  recexre  8733  msqge0  8771  mulge0  8774  aprcl  8801  recexap  8808  rerecapb  8998  ltm1  9001  prodgt02  9008  prodge02  9010  ltmul2  9011  lemul2  9012  lemul2a  9014  ltmulgt12  9020  lemulge12  9022  gt0div  9025  ge0div  9026  ltmuldiv2  9030  ltdivmul  9031  ltdivmul2  9033  ledivmul2  9035  lemuldiv2  9037  negiso  9110  cju  9116  nnge1  9141  halfpos  9350  lt2halves  9355  addltmul  9356  avgle1  9360  avgle2  9361  div4p1lem1div2  9373  nnrecl  9375  elznn0  9469  elznn  9470  nzadd  9507  zmulcl  9508  difgtsumgt  9524  elz2  9526  gtndiv  9550  zeo  9560  supminfex  9800  eqreznegel  9817  negm  9818  irradd  9849  irrmul  9850  divlt1lt  9928  divle1le  9929  xnegneg  10037  rexsub  10057  xnegid  10063  xaddcom  10065  xaddid1  10066  xnegdi  10072  xaddass  10073  xleaddadd  10091  divelunit  10206  fzonmapblen  10395  infssuzex  10461  expgt1  10807  mulexpzap  10809  leexp1a  10824  expubnd  10826  sqgt0ap  10838  lt2sq  10843  le2sq  10844  sqge0  10846  sumsqeq0  10848  bernneq  10890  bernneq2  10891  nn0ltexp2  10939  swrdccatin2  11269  swrdccat3blem  11279  crre  11376  crim  11377  reim0  11380  mulreap  11383  rere  11384  remul2  11392  redivap  11393  immul2  11399  imdivap  11400  cjre  11401  cjreim  11422  rennim  11521  sqrt0rlem  11522  resqrexlemover  11529  absreimsq  11586  absreim  11587  absnid  11592  leabs  11593  absre  11596  absresq  11597  sqabs  11601  ltabs  11606  absdiflt  11611  absdifle  11612  lenegsq  11614  abssuble0  11622  dfabsmax  11736  max0addsup  11738  negfi  11747  minclpr  11756  reefcl  12187  efgt0  12203  reeftlcl  12208  resinval  12234  recosval  12235  resin4p  12237  recos4p  12238  resincl  12239  recoscl  12240  retanclap  12241  efieq  12254  sinbnd  12271  cosbnd  12272  absefi  12288  odd2np1  12392  remetdval  15229  bl2ioo  15232  ioo2bl  15233  hoverb  15330  plyreres  15446  sincosq1sgn  15508  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  relogoprlem  15550  logcxp  15579  rpcxpcl  15585  cxpcom  15620  rprelogbdiv  15639  gausslemma2dlem1a  15745  triap  16427  trirec0  16442