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

Theorem recnd 7817
Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
recnd.1 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
recnd (𝜑𝐴 ∈ ℂ)

Proof of Theorem recnd
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 recn 7776 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
31, 2syl 14 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1481  cc 7641  cr 7642
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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7735
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3081  df-ss 3088
This theorem is referenced by:  readdcan  7925  ltadd2  8204  ltadd1  8214  leadd2  8216  ltsubadd  8217  ltsubadd2  8218  lesubadd  8219  lesubadd2  8220  ltaddsub  8221  leaddsub  8223  lesub1  8241  lesub2  8242  ltsub1  8243  ltsub2  8244  ltnegcon1  8248  ltnegcon2  8249  add20  8259  subge0  8260  suble0  8261  lesub0  8264  eqord2  8269  possumd  8354  sublt0d  8355  rimul  8370  rereim  8371  apreap  8372  ltmul1a  8376  ltmul1  8377  reapmul1  8380  remulext2  8385  cru  8387  apreim  8388  mulreim  8389  apadd1  8393  apneg  8396  mulext1  8397  ltapd  8423  aprcl  8431  rerecclap  8513  redivclap  8514  recgt0  8631  prodgt0gt0  8632  prodgt0  8633  prodge0  8635  lemul1a  8639  ltdiv1  8649  ltmuldiv  8655  ledivmul  8658  lt2mul2div  8660  ltrec  8664  lt2msq  8667  ltdiv2  8668  ltrec1  8669  lerec2  8670  ledivdiv  8671  lediv2  8672  ltdiv23  8673  lediv23  8674  lediv12a  8675  recp1lt1  8680  recreclt  8681  ledivp1  8684  mulle0r  8725  negiso  8736  avglt1  8981  avglt2  8982  div4p1lem1div2  8996  nn0cnd  9055  zcn  9082  peano2z  9113  zaddcllemneg  9116  ztri3or  9120  zeo  9179  zcnd  9197  eluzelcn  9360  infrenegsupex  9415  supinfneg  9416  infsupneg  9417  supminfex  9418  cnref1o  9468  rpcn  9478  rpcnd  9514  ltaddrp2d  9547  mul2lt0rlt0  9575  mul2lt0rgt0  9576  mul2lt0llt0  9577  mul2lt0lgt0  9578  mul2lt0np  9579  mul2lt0pn  9580  xpncan  9683  icoshftf1o  9803  lincmb01cmp  9815  iccf1o  9816  qbtwnrelemcalc  10063  flhalf  10105  intfracq  10123  flqdiv  10124  modqid  10152  modqid0  10153  mulqaddmodid  10167  ser3le  10321  expcl2lemap  10335  expnegzap  10357  expaddzaplem  10366  expaddzap  10367  expmulzap  10369  ltexp2a  10375  leexp2a  10376  leexp2r  10377  exple1  10379  expubnd  10380  sq11  10395  bernneq2  10443  expnbnd  10445  nn0opthlem2d  10498  faclbnd  10518  bcp1nk  10539  remim  10663  reim0b  10665  rereb  10666  mulreap  10667  cjreb  10669  recj  10670  reneg  10671  readd  10672  resub  10673  remullem  10674  remul2  10676  redivap  10677  imcj  10678  imneg  10679  imadd  10680  imsub  10681  immul2  10683  imdivap  10684  cjcj  10686  cjadd  10687  ipcnval  10689  cjmulval  10691  cjneg  10693  imval2  10697  cjreim2  10707  cjap  10709  cnrecnv  10713  caucvgrelemrec  10782  cvg1nlemres  10788  recvguniqlem  10797  recvguniq  10798  resqrexlemover  10813  resqrexlemcalc1  10817  resqrexlemcalc2  10818  resqrexlemcalc3  10819  resqrexlemnmsq  10820  resqrexlemnm  10821  resqrexlemgt0  10823  resqrexlemoverl  10824  resqrexlemglsq  10825  remsqsqrt  10835  sqrtmul  10838  sqrtdiv  10845  sqrtmsq  10848  abs00ap  10865  absext  10866  abs00  10867  absdivap  10873  absid  10874  absexp  10882  absexpzap  10883  absimle  10887  abslt  10891  absle  10892  abssubap0  10893  abssubne0  10894  releabs  10899  recvalap  10900  abstri  10907  abs2difabs  10911  amgm2  10921  icodiamlt  10983  maxabsle  11007  maxabslemab  11009  maxabslemlub  11010  maxabslemval  11011  maxcl  11013  maxltsup  11021  max0addsup  11022  minmax  11032  minabs  11038  minclpr  11039  bdtrilem  11041  bdtri  11042  mul0inf  11043  climabs0  11107  reccn2ap  11113  climrecl  11124  climge0  11125  climle  11134  climsqz  11135  climsqz2  11136  climlec2  11141  climrecvg1n  11148  climcvg1nlem  11149  isumrecl  11229  isumge0  11230  fsumlessfi  11260  fsumge1  11261  fsum00  11262  fsumle  11263  fsumlt  11264  fsumabs  11265  iserabs  11275  isumrpcl  11294  isumle  11295  isumlessdc  11296  trireciplem  11300  trirecip  11301  expcnvre  11303  expcnv  11304  explecnv  11305  absltap  11309  geo2sum  11314  cvgratnnlembern  11323  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  cvgratnnlemabsle  11327  cvgratnnlemsumlt  11328  cvgratnnlemfm  11329  cvgratnnlemrate  11330  cvgratz  11332  mertenslemi1  11335  mertenslem2  11336  efcllemp  11399  ege2le3  11412  efaddlem  11415  efgt0  11425  reeftlcl  11430  eftlub  11431  effsumlt  11433  efltim  11439  eflegeo  11442  resin4p  11459  recos4p  11460  efeul  11475  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  sin01gt0  11502  cos01gt0  11503  sin02gt0  11504  cos12dec  11508  absefi  11509  absef  11510  absefib  11511  efieq1re  11512  eirraplem  11517  dvdslelemd  11575  odd2np1  11604  divalglemnqt  11651  infssuzcldc  11678  nn0seqcvgd  11756  sqnprm  11850  metrtri  12583  bl2in  12609  blhalf  12614  blssps  12633  blss  12634  dedekindeu  12807  dedekindicclemicc  12816  ivthinclemlopn  12820  ivthinclemuopn  12822  ivthinc  12827  ivthdec  12828  dvcjbr  12878  dvfre  12880  dveflem  12893  reeff1olem  12898  reeff1oleme  12899  eflt  12902  sin0pilem1  12908  sin0pilem2  12909  pilem3  12910  sincosq2sgn  12954  sincosq3sgn  12955  sincosq4sgn  12956  sinq12gt0  12957  sinq34lt0t  12958  cosq14gt0  12959  cosq23lt0  12960  coseq0q4123  12961  coseq0negpitopi  12963  tanrpcl  12964  tangtx  12965  coskpi  12975  cosordlem  12976  cosq34lt1  12977  cos11  12980  reexplog  12998  relogexp  12999  logdivlti  13008  rpcxpef  13021  rpcncxpcl  13029  cxpap0  13031  rpcxpadd  13032  rpmulcxp  13036  cxpmul  13039  abscxp  13041  cxplt  13042  cxplt3  13046  logsqrt  13049  apcxp2  13064  rpabscxpbnd  13065  rplogbid1  13070  rplogb1  13071  rpelogb  13072  rplogbchbase  13073  rplogbreexp  13076  rprelogbmul  13078  rprelogbdiv  13080  rplogbcxp  13086  rpcxplogb  13087  logbgcd1irraplemexp  13091  logbgcd1irraplemap  13092  qdencn  13395  refeq  13396  cvgcmp2nlemabs  13400  cvgcmp2n  13401  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407  trirec0  13410  apdifflemf  13412  apdifflemr  13413  apdiff  13414
  Copyright terms: Public domain W3C validator