MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recn Structured version   Visualization version   GIF version

Theorem recn 10615
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 10582 . 2 ℝ ⊆ ℂ
21sseli 3960 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cc 10523  cr 10524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-resscn 10582
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  mulid1  10627  recnd  10657  pnfnre  10670  mnfnre  10672  mul02  10806  ltaddneg  10843  ltaddnegr  10844  renegcli  10935  resubcl  10938  negn0  11057  negf1o  11058  ltaddsub2  11103  leaddsub2  11105  leltadd  11112  ltaddpos  11118  ltaddpos2  11119  posdif  11121  lenegcon1  11132  lenegcon2  11133  addge01  11138  addge02  11139  leaddle0  11143  mullt0  11147  recex  11260  ltm1  11470  prodgt02  11476  ltmul2  11479  lemul1  11480  lemul2  11481  lemul1a  11482  lemul2a  11483  ltmulgt12  11489  lemulge12  11491  gt0div  11494  ge0div  11495  mulge0b  11498  mulle0b  11499  ltmuldiv2  11502  ltdivmul  11503  ledivmul  11504  ltdivmul2  11505  lt2mul2div  11506  ledivmul2  11507  lemuldiv2  11509  ltdiv2  11514  ltrec1  11515  lerec2  11516  ledivdiv  11517  lediv2  11518  ltdiv23  11519  lediv23  11520  lediv12a  11521  recp1lt1  11526  ledivp1  11530  negfi  11577  fiminreOLD  11578  infm3lem  11587  supmul  11601  riotaneg  11608  negiso  11609  cju  11622  nnge1  11653  halfpos  11855  lt2halves  11860  addltmul  11861  avgle1  11865  avgle2  11866  avgle  11867  div4p1lem1div2  11880  nnrecl  11883  difgtsumgt  11938  elznn0  11984  elznn  11985  elz2  11987  nzadd  12018  zmulcl  12019  gtndiv  12047  zeo  12056  eqreznegel  12322  supminf  12323  rebtwnz  12335  irradd  12360  irrmul  12361  divlt1lt  12446  divle1le  12447  max0sub  12577  xnegneg  12595  rexsub  12614  xnegid  12619  xaddcom  12621  xaddid1  12622  xnegdi  12629  xaddass  12630  rexmul  12652  xmulasslem3  12667  xadddilem  12675  divelunit  12868  fzonmapblen  13071  ico01fl0  13177  flzadd  13184  ltdifltdiv  13192  dfceil2  13197  intfrac2  13214  fldiv2  13217  flpmodeq  13230  mod0  13232  negmod0  13234  modlt  13236  modfrac  13240  flmod  13241  intfrac  13242  modmulnn  13245  modvalp1  13246  modid  13252  modcyc  13262  modcyc2  13263  modadd1  13264  modaddabs  13265  muladdmodid  13267  negmod  13272  modadd2mod  13277  modmul1  13280  modmulmodr  13293  modaddmulmod  13294  moddi  13295  modsubdir  13296  modirr  13298  addmodlteq  13302  expgt1  13455  mulexpz  13457  sqgt0  13479  lt2sq  13486  le2sq  13487  sqge0  13489  expmordi  13519  leexp1a  13527  expubnd  13529  sumsqeq0  13530  sqlecan  13559  bernneq  13578  bernneq2  13579  expnbnd  13581  digit2  13585  digit1  13586  expnngt1  13590  swrdccatin2  14079  swrdccat3blem  14089  cshweqrep  14171  crre  14461  crim  14462  reim0  14465  mulre  14468  rere  14469  remul2  14477  rediv  14478  immul2  14484  imdiv  14485  cjre  14486  cjreim  14507  rennim  14586  resqrex  14598  resqreu  14600  resqrtcl  14601  resqrtthlem  14602  sqrtneglem  14614  sqrtneg  14615  absreimsq  14640  absreim  14641  absnid  14646  leabs  14647  absre  14649  absresq  14650  sqabs  14655  max0add  14658  absz  14659  absdiflt  14665  absdifle  14666  lenegsq  14668  abssuble0  14676  absmax  14677  rddif  14688  absrdbnd  14689  o1rlimmul  14963  caurcvg2  15022  reefcl  15428  efgt0  15444  reeftlcl  15449  resinval  15476  recosval  15477  resin4p  15479  recos4p  15480  resincl  15481  recoscl  15482  retancl  15483  resinhcl  15497  rpcoshcl  15498  retanhcl  15500  tanhlt1  15501  tanhbnd  15502  efieq  15504  sinbnd  15521  cosbnd  15522  absefi  15537  dvdsaddre2b  15645  odd2np1  15678  bezoutlem1  15875  xrsdsreclb  20520  remulg  20679  resubdrg  20680  remetdval  23324  bl2ioo  23327  ioo2bl  23328  cnperf  23355  icccvx  23481  tcphcph  23767  shft2rab  24036  volsup2  24133  volcn  24134  c1lip1  24521  plyreres  24799  aalioulem3  24850  taylthlem2  24889  reeff1o  24962  reefgim  24965  sincosq1sgn  25011  sincosq2sgn  25012  sincosq3sgn  25013  sincosq4sgn  25014  sinq12gt0  25020  pige3ALT  25032  efif1olem4  25056  efifo  25058  relogrn  25072  logrnaddcl  25085  relogoprlem  25101  advlog  25164  advlogexp  25165  logtayl  25170  recxpcl  25185  rpcxpcl  25186  cxpge0  25193  cxpcom  25247  dvcxp1  25248  logreclem  25267  relogbreexp  25280  relogbcxp  25290  angpieqvd  25336  atanre  25390  basellem9  25593  gausslemma2dlem1a  25868  2sqnn0  25941  log2sumbnd  26047  brbtwn2  26618  colinearalglem4  26622  colinearalg  26623  crctcshwlkn0lem1  27515  nvsge0  28368  nmoub3i  28477  nmlnoubi  28500  isblo3i  28505  ipasslem3  28537  ipasslem9  28542  ipasslem11  28544  hmopm  29725  riesz1  29769  leopmuli  29837  leopmul  29838  leopmul2i  29839  leopnmid  29842  nmopleid  29843  cdj1i  30137  cdj3lem1  30138  cdj3i  30145  addltmulALT  30150  dpfrac1  30495  rexdiv  30529  xdivid  30531  xdiv0  30532  rmulccn  31070  sgnneg  31697  lediv2aALT  32817  nndivlub  33703  cos2h  34764  tan2h  34765  poimir  34806  mblfinlem2  34811  mblfinlem4  34813  itg2addnclem  34824  itg2addnclem2  34825  dvasin  34859  areacirclem1  34863  areacirclem2  34864  areacirclem4  34866  areacirclem5  34867  areacirc  34868  resubeulem2  39084  renegneg  39119  areaquad  39701  radcnvrat  40523  lhe4.4ex1a  40538  expgrowthi  40542  mulltgt0  41156  refsum2cnlem1  41171  infnsuprnmpt  41398  dstregt0  41423  suplesup  41483  infleinflem1  41514  infleinflem2  41515  ltdiv23neg  41542  rexabslelem  41568  supminfrnmpt  41595  supminfxr  41616  fmul01lt1lem1  41741  lptre2pt  41797  cnrefiisplem  41986  dvcosre  42072  itgsin0pilem1  42111  itgsinexplem1  42115  volioc  42133  volico  42145  stoweidlem7  42169  stoweidlem10  42172  stoweidlem19  42181  stoweidlem34  42196  stoweid  42225  dirker2re  42254  dirkerdenne0  42255  dirkerper  42258  dirkertrigeq  42263  dirkeritg  42264  fourierdlem39  42308  fourierdlem42  42311  fourierdlem47  42315  fourierdlem56  42324  fourierdlem57  42325  fourierdlem58  42326  fourierdlem60  42328  fourierdlem61  42329  fourierdlem73  42341  fourierdlem76  42344  fourierdlem77  42345  fourierdlem92  42360  fourierdlem97  42365  etransclem46  42442  volico2  42800  smflimlem4  42927  smfinflem  42968  2leaddle2  43375  ltsubsubaddltsub  43378  sqrtnegnre  43384  m1mod0mod1  43406  requad01  43663  requad1  43664  bgoldbtbndlem2  43848  flsubz  44505  rege1logbrege0  44546  nn0digval  44588  rrx2vlinest  44656  line2  44667  line2xlem  44668  line2x  44669  itscnhlc0yqe  44674  itsclc0yqsollem2  44678  itsclc0yqsol  44679  itscnhlc0xyqsol  44680  itschlc0xyqsol1  44681  itsclc0xyqsolr  44684  itsclquadb  44691  reseccl  44780  recsccl  44781  recotcl  44782
  Copyright terms: Public domain W3C validator