ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recn GIF version

Theorem recn 7767
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 7726 . 2 ℝ ⊆ ℂ
21sseli 3093 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  cc 7632  cr 7633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7726
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  mulid1  7777  recnd  7808  pnfnre  7821  mnfnre  7822  cnegexlem1  7951  cnegexlem2  7952  cnegexlem3  7953  cnegex  7954  renegcl  8037  resubcl  8040  negf1o  8158  mul02lem2  8164  ltaddneg  8200  ltaddnegr  8201  ltaddsub2  8213  leaddsub2  8215  leltadd  8223  ltaddpos  8228  ltaddpos2  8229  posdif  8231  lenegcon1  8242  lenegcon2  8243  addge01  8248  addge02  8249  leaddle0  8253  mullt0  8256  recexre  8354  msqge0  8392  mulge0  8395  aprcl  8422  recexap  8428  ltm1  8618  prodgt02  8625  prodge02  8627  ltmul2  8628  lemul2  8629  lemul2a  8631  ltmulgt12  8637  lemulge12  8639  gt0div  8642  ge0div  8643  ltmuldiv2  8647  ltdivmul  8648  ltdivmul2  8650  ledivmul2  8652  lemuldiv2  8654  negiso  8727  cju  8733  nnge1  8757  halfpos  8965  lt2halves  8969  addltmul  8970  avgle1  8974  avgle2  8975  div4p1lem1div2  8987  nnrecl  8989  elznn0  9083  elznn  9084  nzadd  9120  zmulcl  9121  elz2  9136  gtndiv  9160  zeo  9170  supminfex  9406  eqreznegel  9420  negm  9421  irradd  9452  irrmul  9453  divlt1lt  9525  divle1le  9526  xnegneg  9630  rexsub  9650  xnegid  9656  xaddcom  9658  xaddid1  9659  xnegdi  9665  xaddass  9666  xleaddadd  9684  divelunit  9799  fzonmapblen  9978  expgt1  10345  mulexpzap  10347  leexp1a  10362  expubnd  10364  sqgt0ap  10375  lt2sq  10380  le2sq  10381  sqge0  10383  sumsqeq0  10385  bernneq  10426  bernneq2  10427  crre  10643  crim  10644  reim0  10647  mulreap  10650  rere  10651  remul2  10659  redivap  10660  immul2  10666  imdivap  10667  cjre  10668  cjreim  10689  rennim  10788  sqrt0rlem  10789  resqrexlemover  10796  absreimsq  10853  absreim  10854  absnid  10859  leabs  10860  absre  10863  absresq  10864  sqabs  10868  ltabs  10873  absdiflt  10878  absdifle  10879  lenegsq  10881  abssuble0  10889  dfabsmax  11003  max0addsup  11005  negfi  11013  minclpr  11022  reefcl  11388  efgt0  11404  reeftlcl  11409  resinval  11435  recosval  11436  resin4p  11438  recos4p  11439  resincl  11440  recoscl  11441  retanclap  11442  efieq  11455  sinbnd  11472  cosbnd  11473  absefi  11488  odd2np1  11583  infssuzex  11655  remetdval  12724  bl2ioo  12727  ioo2bl  12728  sincosq1sgn  12931  sincosq2sgn  12932  sincosq3sgn  12933  sincosq4sgn  12934  sinq12gt0  12935  relogoprlem  12973  logcxp  12999  rpcxpcl  13005  cxpcom  13038  triap  13333  trirec0  13346
  Copyright terms: Public domain W3C validator