Theorem recn 8165

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℝcr 8031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  mulrid  8176  recnd  8208  pnfnre  8221  mnfnre  8222  cnegexlem1  8354  cnegexlem2  8355  cnegexlem3  8356  cnegex  8357  renegcl  8440  resubcl  8443  negf1o  8561  mul02lem2  8567  ltaddneg  8604  ltaddnegr  8605  ltaddsub2  8617  leaddsub2  8619  leltadd  8627  ltaddpos  8632  ltaddpos2  8633  posdif  8635  lenegcon1  8646  lenegcon2  8647  addge01  8652  addge02  8653  leaddle0  8657  mullt0  8660  recexre  8758  msqge0  8796  mulge0  8799  aprcl  8826  recexap  8833  rerecapb  9023  ltm1  9026  prodgt02  9033  prodge02  9035  ltmul2  9036  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  gt0div  9050  ge0div  9051  ltmuldiv2  9055  ltdivmul  9056  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  negiso  9135  cju  9141  nnge1  9166  halfpos  9375  lt2halves  9380  addltmul  9381  avgle1  9385  avgle2  9386  div4p1lem1div2  9398  nnrecl  9400  elznn0  9494  elznn  9495  nzadd  9532  zmulcl  9533  difgtsumgt  9549  elz2  9551  gtndiv  9575  zeo  9585  supminfex  9831  eqreznegel  9848  negm  9849  irradd  9880  irrmul  9881  divlt1lt  9959  divle1le  9960  xnegneg  10068  rexsub  10088  xnegid  10094  xaddcom  10096  xaddid1  10097  xnegdi  10103  xaddass  10104  xleaddadd  10122  divelunit  10237  fzonmapblen  10427  infssuzex  10494  expgt1  10840  mulexpzap  10842  leexp1a  10857  expubnd  10859  sqgt0ap  10871  lt2sq  10876  le2sq  10877  sqge0  10879  sumsqeq0  10881  bernneq  10923  bernneq2  10924  nn0ltexp2  10972  swrdccatin2  11311  swrdccat3blem  11321  crre  11419  crim  11420  reim0  11423  mulreap  11426  rere  11427  remul2  11435  redivap  11436  immul2  11442  imdivap  11443  cjre  11444  cjreim  11465  rennim  11564  sqrt0rlem  11565  resqrexlemover  11572  absreimsq  11629  absreim  11630  absnid  11635  leabs  11636  absre  11639  absresq  11640  sqabs  11644  ltabs  11649  absdiflt  11654  absdifle  11655  lenegsq  11657  abssuble0  11665  dfabsmax  11779  max0addsup  11781  negfi  11790  minclpr  11799  reefcl  12231  efgt0  12247  reeftlcl  12252  resinval  12278  recosval  12279  resin4p  12281  recos4p  12282  resincl  12283  recoscl  12284  retanclap  12285  efieq  12298  sinbnd  12315  cosbnd  12316  absefi  12332  odd2np1  12436  remetdval  15274  bl2ioo  15277  ioo2bl  15278  hoverb  15375  plyreres  15491  sincosq1sgn  15553  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  sinq12gt0  15557  relogoprlem  15595  logcxp  15624  rpcxpcl  15630  cxpcom  15665  rprelogbdiv  15684  gausslemma2dlem1a  15790  triap  16654  trirec0  16669