Theorem recn 8065

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℂcc 7930  ℝcr 7931

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8024

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180

This theorem is referenced by:  mulrid  8076  recnd  8108  pnfnre  8121  mnfnre  8122  cnegexlem1  8254  cnegexlem2  8255  cnegexlem3  8256  cnegex  8257  renegcl  8340  resubcl  8343  negf1o  8461  mul02lem2  8467  ltaddneg  8504  ltaddnegr  8505  ltaddsub2  8517  leaddsub2  8519  leltadd  8527  ltaddpos  8532  ltaddpos2  8533  posdif  8535  lenegcon1  8546  lenegcon2  8547  addge01  8552  addge02  8553  leaddle0  8557  mullt0  8560  recexre  8658  msqge0  8696  mulge0  8699  aprcl  8726  recexap  8733  rerecapb  8923  ltm1  8926  prodgt02  8933  prodge02  8935  ltmul2  8936  lemul2  8937  lemul2a  8939  ltmulgt12  8945  lemulge12  8947  gt0div  8950  ge0div  8951  ltmuldiv2  8955  ltdivmul  8956  ltdivmul2  8958  ledivmul2  8960  lemuldiv2  8962  negiso  9035  cju  9041  nnge1  9066  halfpos  9275  lt2halves  9280  addltmul  9281  avgle1  9285  avgle2  9286  div4p1lem1div2  9298  nnrecl  9300  elznn0  9394  elznn  9395  nzadd  9432  zmulcl  9433  difgtsumgt  9449  elz2  9451  gtndiv  9475  zeo  9485  supminfex  9725  eqreznegel  9742  negm  9743  irradd  9774  irrmul  9775  divlt1lt  9853  divle1le  9854  xnegneg  9962  rexsub  9982  xnegid  9988  xaddcom  9990  xaddid1  9991  xnegdi  9997  xaddass  9998  xleaddadd  10016  divelunit  10131  fzonmapblen  10318  infssuzex  10383  expgt1  10729  mulexpzap  10731  leexp1a  10746  expubnd  10748  sqgt0ap  10760  lt2sq  10765  le2sq  10766  sqge0  10768  sumsqeq0  10770  bernneq  10812  bernneq2  10813  nn0ltexp2  10861  crre  11212  crim  11213  reim0  11216  mulreap  11219  rere  11220  remul2  11228  redivap  11229  immul2  11235  imdivap  11236  cjre  11237  cjreim  11258  rennim  11357  sqrt0rlem  11358  resqrexlemover  11365  absreimsq  11422  absreim  11423  absnid  11428  leabs  11429  absre  11432  absresq  11433  sqabs  11437  ltabs  11442  absdiflt  11447  absdifle  11448  lenegsq  11450  abssuble0  11458  dfabsmax  11572  max0addsup  11574  negfi  11583  minclpr  11592  reefcl  12023  efgt0  12039  reeftlcl  12044  resinval  12070  recosval  12071  resin4p  12073  recos4p  12074  resincl  12075  recoscl  12076  retanclap  12077  efieq  12090  sinbnd  12107  cosbnd  12108  absefi  12124  odd2np1  12228  remetdval  15063  bl2ioo  15066  ioo2bl  15067  hoverb  15164  plyreres  15280  sincosq1sgn  15342  sincosq2sgn  15343  sincosq3sgn  15344  sincosq4sgn  15345  sinq12gt0  15346  relogoprlem  15384  logcxp  15413  rpcxpcl  15419  cxpcom  15454  rprelogbdiv  15473  gausslemma2dlem1a  15579  triap  16042  trirec0  16057