Theorem recn 7946

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7811  ℝcr 7812

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  mulrid  7956  recnd  7988  pnfnre  8001  mnfnre  8002  cnegexlem1  8134  cnegexlem2  8135  cnegexlem3  8136  cnegex  8137  renegcl  8220  resubcl  8223  negf1o  8341  mul02lem2  8347  ltaddneg  8383  ltaddnegr  8384  ltaddsub2  8396  leaddsub2  8398  leltadd  8406  ltaddpos  8411  ltaddpos2  8412  posdif  8414  lenegcon1  8425  lenegcon2  8426  addge01  8431  addge02  8432  leaddle0  8436  mullt0  8439  recexre  8537  msqge0  8575  mulge0  8578  aprcl  8605  recexap  8612  rerecapb  8802  ltm1  8805  prodgt02  8812  prodge02  8814  ltmul2  8815  lemul2  8816  lemul2a  8818  ltmulgt12  8824  lemulge12  8826  gt0div  8829  ge0div  8830  ltmuldiv2  8834  ltdivmul  8835  ltdivmul2  8837  ledivmul2  8839  lemuldiv2  8841  negiso  8914  cju  8920  nnge1  8944  halfpos  9152  lt2halves  9156  addltmul  9157  avgle1  9161  avgle2  9162  div4p1lem1div2  9174  nnrecl  9176  elznn0  9270  elznn  9271  nzadd  9307  zmulcl  9308  difgtsumgt  9324  elz2  9326  gtndiv  9350  zeo  9360  supminfex  9599  eqreznegel  9616  negm  9617  irradd  9648  irrmul  9649  divlt1lt  9726  divle1le  9727  xnegneg  9835  rexsub  9855  xnegid  9861  xaddcom  9863  xaddid1  9864  xnegdi  9870  xaddass  9871  xleaddadd  9889  divelunit  10004  fzonmapblen  10189  expgt1  10560  mulexpzap  10562  leexp1a  10577  expubnd  10579  sqgt0ap  10591  lt2sq  10596  le2sq  10597  sqge0  10599  sumsqeq0  10601  bernneq  10643  bernneq2  10644  nn0ltexp2  10691  crre  10868  crim  10869  reim0  10872  mulreap  10875  rere  10876  remul2  10884  redivap  10885  immul2  10891  imdivap  10892  cjre  10893  cjreim  10914  rennim  11013  sqrt0rlem  11014  resqrexlemover  11021  absreimsq  11078  absreim  11079  absnid  11084  leabs  11085  absre  11088  absresq  11089  sqabs  11093  ltabs  11098  absdiflt  11103  absdifle  11104  lenegsq  11106  abssuble0  11114  dfabsmax  11228  max0addsup  11230  negfi  11238  minclpr  11247  reefcl  11678  efgt0  11694  reeftlcl  11699  resinval  11725  recosval  11726  resin4p  11728  recos4p  11729  resincl  11730  recoscl  11731  retanclap  11732  efieq  11745  sinbnd  11762  cosbnd  11763  absefi  11778  odd2np1  11880  infssuzex  11952  remetdval  14078  bl2ioo  14081  ioo2bl  14082  sincosq1sgn  14286  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  sinq12gt0  14290  relogoprlem  14328  logcxp  14357  rpcxpcl  14363  cxpcom  14396  rprelogbdiv  14414  triap  14816  trirec0  14831