Theorem recn 8100

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℂcc 7965  ℝcr 7966

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-resscn 8059

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  mulrid  8111  recnd  8143  pnfnre  8156  mnfnre  8157  cnegexlem1  8289  cnegexlem2  8290  cnegexlem3  8291  cnegex  8292  renegcl  8375  resubcl  8378  negf1o  8496  mul02lem2  8502  ltaddneg  8539  ltaddnegr  8540  ltaddsub2  8552  leaddsub2  8554  leltadd  8562  ltaddpos  8567  ltaddpos2  8568  posdif  8570  lenegcon1  8581  lenegcon2  8582  addge01  8587  addge02  8588  leaddle0  8592  mullt0  8595  recexre  8693  msqge0  8731  mulge0  8734  aprcl  8761  recexap  8768  rerecapb  8958  ltm1  8961  prodgt02  8968  prodge02  8970  ltmul2  8971  lemul2  8972  lemul2a  8974  ltmulgt12  8980  lemulge12  8982  gt0div  8985  ge0div  8986  ltmuldiv2  8990  ltdivmul  8991  ltdivmul2  8993  ledivmul2  8995  lemuldiv2  8997  negiso  9070  cju  9076  nnge1  9101  halfpos  9310  lt2halves  9315  addltmul  9316  avgle1  9320  avgle2  9321  div4p1lem1div2  9333  nnrecl  9335  elznn0  9429  elznn  9430  nzadd  9467  zmulcl  9468  difgtsumgt  9484  elz2  9486  gtndiv  9510  zeo  9520  supminfex  9760  eqreznegel  9777  negm  9778  irradd  9809  irrmul  9810  divlt1lt  9888  divle1le  9889  xnegneg  9997  rexsub  10017  xnegid  10023  xaddcom  10025  xaddid1  10026  xnegdi  10032  xaddass  10033  xleaddadd  10051  divelunit  10166  fzonmapblen  10355  infssuzex  10420  expgt1  10766  mulexpzap  10768  leexp1a  10783  expubnd  10785  sqgt0ap  10797  lt2sq  10802  le2sq  10803  sqge0  10805  sumsqeq0  10807  bernneq  10849  bernneq2  10850  nn0ltexp2  10898  swrdccatin2  11227  swrdccat3blem  11237  crre  11334  crim  11335  reim0  11338  mulreap  11341  rere  11342  remul2  11350  redivap  11351  immul2  11357  imdivap  11358  cjre  11359  cjreim  11380  rennim  11479  sqrt0rlem  11480  resqrexlemover  11487  absreimsq  11544  absreim  11545  absnid  11550  leabs  11551  absre  11554  absresq  11555  sqabs  11559  ltabs  11564  absdiflt  11569  absdifle  11570  lenegsq  11572  abssuble0  11580  dfabsmax  11694  max0addsup  11696  negfi  11705  minclpr  11714  reefcl  12145  efgt0  12161  reeftlcl  12166  resinval  12192  recosval  12193  resin4p  12195  recos4p  12196  resincl  12197  recoscl  12198  retanclap  12199  efieq  12212  sinbnd  12229  cosbnd  12230  absefi  12246  odd2np1  12350  remetdval  15186  bl2ioo  15189  ioo2bl  15190  hoverb  15287  plyreres  15403  sincosq1sgn  15465  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468  sinq12gt0  15469  relogoprlem  15507  logcxp  15536  rpcxpcl  15542  cxpcom  15577  rprelogbdiv  15596  gausslemma2dlem1a  15702  triap  16308  trirec0  16323