MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recnd Unicode version

Theorem recnd 9643
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 9603 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   cr 9512
This theorem is referenced by:  00id  9776  mul02lem1  9777  addid1  9781  cnegex  9782  ltadd1  10044  leadd2  10046  ltsubadd  10047  ltsubadd2  10048  lesubadd  10049  lesubadd2  10050  lesub1  10071  lesub2  10072  ltnegcon1  10078  ltnegcon2  10079  add20  10089  subge0  10090  suble0  10091  lesub0  10094  mulge0  10095  eqord2  10109  rereccl  10287  redivcl  10288  recgt0  10411  prodgt0  10412  prodge0  10414  ltmul1a  10416  ltdiv1  10431  ltmuldiv  10440  ltrec  10451  recp1lt1  10468  recreclt  10469  ledivp1  10472  infmsup  10546  infmrcl  10547  rimul  10552  cru  10553  avglt1  10801  avglt2  10802  nn0cnd  10879  zcn  10894  zeo  10973  zcnd  10995  eluzelcn  11121  cnref1o  11244  rpcn  11257  rpcnd  11287  ltaddrp2d  11315  qbtwnre  11427  xralrple  11433  xpncan  11472  xmulcom  11487  xmulneg1  11490  xlemul1  11511  icoshftf1o  11672  lincmb01cmp  11692  iccf1o  11693  fladdz  11958  flzadd  11959  flhalf  11962  ceim1l  11974  intfracq  11986  fldiv  11987  modvalr  11999  flpmodeq  12001  mod0  12003  modlt  12006  moddiffl  12007  modfrac  12009  flmod  12010  intfrac  12011  modmulnn  12013  modvalp1  12014  modid  12020  modcyc  12031  modadd1  12033  modaddabs  12034  modadd2mod  12037  modnegd  12042  modadd12d  12043  modsub12d  12044  modaddmulmod  12053  moddi  12054  modsubdir  12055  modeqmodmin  12056  modirr  12057  seqf1olem1  12146  serle  12162  expcl2lem  12178  expnegz  12200  expaddzlem  12209  expaddz  12210  expmulz  12212  ltexp2a  12217  leexp2a  12221  leexp2r  12223  exple1  12225  expubnd  12226  sq11  12240  bernneq2  12293  expmulnbnd  12298  discr1  12302  discr  12303  faclbnd  12368  bcp1nk  12395  cshweqrep  12789  remim  12950  reim0b  12952  rereb  12953  mulre  12954  cjreb  12956  recj  12957  reneg  12958  readd  12959  resub  12960  remullem  12961  remul2  12963  rediv  12964  imcj  12965  imneg  12966  imadd  12967  imsub  12968  immul2  12970  imdiv  12971  cjcj  12973  cjadd  12974  ipcnval  12976  cjmulval  12978  cjneg  12980  imval2  12984  cjreim2  12994  sqr0lem  13074  sqrlem5  13080  sqrlem7  13082  resqrtthlem  13088  remsqsqrt  13090  sqrtmul  13093  sqrtdiv  13099  sqrtneg  13101  sqrtmsq  13104  absdiv  13128  absid  13129  absexp  13137  absexpz  13138  absimle  13142  abslt  13147  absle  13148  abssubne0  13149  releabs  13154  recval  13155  abstri  13163  abs2difabs  13167  abs1m  13168  abslem2  13172  absrdbnd  13174  sqreulem  13192  sqreu  13193  amgm2  13202  lo1bddrp  13348  o1lo1  13360  rlimrecl  13403  rlimge0  13404  climrecl  13406  climge0  13407  climabs0  13408  reccn2  13419  o1rlimmul  13441  lo1mul2  13451  lo1sub  13453  climle  13462  climsqz  13463  climsqz2  13464  rlimsqz  13472  rlimsqz2  13473  climlec2  13481  isercolllem1  13487  climsup  13492  caucvgrlem  13495  caurcvgr  13496  caucvgrlem2  13497  iseraltlem1  13504  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  isumrecl  13580  isumge0  13581  fsumless  13610  fsumge1  13611  fsum00  13612  fsumle  13613  fsumlt  13614  fsumabs  13615  o1fsum  13627  seqabs  13628  cvgcmp  13630  cvgcmpce  13632  abscvgcvg  13633  isumrpcl  13655  isumle  13656  isumless  13657  isumsup  13659  climcndslem1  13661  climcndslem2  13662  climcnds  13663  flo1  13666  supcvg  13667  trireciplem  13673  trirecip  13674  explecnv  13676  geo2sum  13682  geo2lim  13684  geomulcvg  13685  cvgrat  13692  mertenslem1  13693  mertenslem2  13694  fprodabs  13778  iprodrecl  13795  efcllem  13813  ege2le3  13825  efaddlem  13828  efgt0  13838  eftlub  13844  effsumlt  13846  eflt  13852  eflegeo  13856  resin4p  13873  recos4p  13874  retanhcl  13894  tanhlt1  13895  efeul  13897  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  absefi  13931  absef  13932  absefib  13933  efieq1re  13934  eirrlem  13937  rpnnen2lem5  13952  rpnnen2lem8  13955  rpnnen2lem9  13956  rpnnen2lem11  13958  rpnnen2  13959  moddvds  13993  odd2np1  14046  divalglem5  14055  bitsp1o  14083  bitsfzo  14085  bitscmp  14088  sadcaddlem  14107  nn0seqcvgd  14199  sqnprm  14239  isprm5  14253  nonsq  14292  eulerthlem2  14312  prmdiveq  14316  odzdvds  14322  pythagtriplem14  14352  pcid  14396  fldivp1  14416  pcfac  14418  pockthlem  14423  prmreclem3  14436  prmreclem4  14437  prmreclem5  14438  prmrec  14440  4sqlem5  14460  4sqlem10  14465  mul4sqlem  14471  4sqlem15  14477  4sqlem16  14478  mulgneg  16160  ghmmulg  16279  odmodnn0  16564  mndodconglem  16565  pgpfaclem2  17133  isabvd  17469  abv1z  17481  abvneg  17483  abvrec  17485  abvdiv  17486  abvdom  17487  rege0subm  18474  cnsubrg  18478  gzrngunitlem  18482  prmirredlem  18523  prmirredlemOLD  18526  remulg  18643  regsumsupp  18658  bl2in  20903  blhalf  20908  blssps  20927  blss  20928  methaus  21023  nrmmetd  21095  nm2dif  21144  nminvr  21178  nmdvr  21179  nlmmul0or  21192  nrginvrcnlem  21199  nmolb2d  21225  nmoi2  21237  nmoleub  21238  nmo0  21242  nmoeq0  21243  nmoco  21244  nmotri  21246  nmoid  21249  blcvx  21303  xrsxmet  21314  recld2  21319  reconnlem2  21332  opnreen  21336  metdstri  21355  metnrmlem3  21365  icchmeo  21441  icopnfcnv  21442  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  icccvx  21450  cnheiborlem  21454  evth  21459  lebnumii  21466  pcoass  21524  pcorevlem  21526  pcorev2  21528  pi1xfrcnv  21557  nmoleub2lem  21597  nmoleub2lem3  21598  nmoleub3  21602  cphsqrtcl2  21633  ipcau2  21677  tchcphlem1  21678  tchcphlem2  21679  tchcph  21680  iscau3  21717  rrxnm  21823  rrxcph  21824  csbren  21826  trirn  21827  rrxmval  21832  rrxmetlem  21834  rrxmet  21835  rrxdstprj1  21836  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  minveclem7  21850  pjthlem1  21852  ivthlem2  21864  ivthlem3  21865  ivth2  21867  ovolfsval  21882  ovollb2lem  21899  ovolctb  21901  ovolunlem1a  21907  ovolunnul  21911  ovolfiniun  21912  ovoliunlem1  21913  ovoliun2  21917  shft2rab  21919  ovolshftlem1  21920  sca2rab  21923  ovolscalem1  21924  ovolsca  21926  ovolicc1  21927  ovolicc2lem4  21931  ovolicopnf  21935  cmmbl  21945  nulmbl  21946  nulmbl2  21947  unmbl  21948  volinun  21956  volfiniun  21957  voliunlem1  21960  voliunlem3  21962  ioombl1lem3  21970  ioombl1lem4  21971  ovolioo  21978  ioorcl2  21981  uniioovol  21988  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombllem6  21997  dyadovol  22002  dyaddisjlem  22004  opnmbllem  22010  vitalilem1  22017  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  ismbf  22037  mbfmulc2lem  22054  mbfmulc2re  22055  mbfmulc2  22070  mbfinf  22072  itg1val2  22091  itg11  22098  i1fmullem  22101  i1fadd  22102  itg1addlem4  22106  itg1addlem5  22107  i1fmulclem  22109  i1fmulc  22110  itg1mulc  22111  itg1sub  22116  itg10a  22117  itg1ge0a  22118  itg1climres  22121  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  mbfi1flimlem  22129  mbfmullem2  22131  itg2const  22147  itg2const2  22148  itg2mulclem  22153  itg2mulc  22154  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2monolem3  22159  itg2addlem  22165  itgcl  22190  itgcnlem  22196  itgrevallem1  22201  itgposval  22202  iblneg  22209  itgneg  22210  i1fibl  22214  itgitg1  22215  itgconst  22225  ibladd  22227  itgaddlem2  22230  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgmulc2lem2  22239  itgmulc2  22240  itgabs  22241  itgsplit  22242  bddmulibl  22245  dvcjbr  22352  dvfre  22354  dvexp3  22379  dveflem  22380  dvferm1lem  22385  dvferm2lem  22387  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvlipcn  22395  c1liplem1  22397  c1lip1  22398  dveq0  22401  dv11cn  22402  dvlt0  22406  dvle  22408  dvivthlem1  22409  dvivth  22411  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvcvx  22421  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem2  22428  dvfsumlem4  22430  dvfsumrlimge0  22431  dvfsumrlim2  22433  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  ftc1lem5  22441  plyeq0lem  22607  coemulhi  22651  plyrecj  22676  plydivlem3  22691  aalioulem2  22729  aalioulem3  22730  aalioulem4  22731  aalioulem5  22732  aalioulem6  22733  aaliou  22734  aaliou2  22736  aaliou2b  22737  aaliou3lem3  22740  aaliou3lem7  22745  aaliou3lem9  22746  taylthlem2  22769  ulmcn  22794  ulmdvlem1  22795  mtest  22799  mtestbdd  22800  itgulm  22803  radcnvlem1  22808  radcnvlem2  22809  radcnvlt1  22813  radcnvle  22815  dvradcnv  22816  pserulm  22817  abelthlem2  22827  abelthlem5  22830  abelthlem7  22833  abelth2  22837  reeff1olem  22841  efcvx  22844  pilem2  22847  pilem3  22848  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  coseq0negpitopi  22896  tanrpcl  22897  tangtx  22898  tanabsge  22899  sinq12gt0  22900  sinq34lt0t  22902  cosq14gt0  22903  cosq14ge0  22904  pige3  22910  coskpi  22913  sineq0  22914  cosordlem  22918  sinord  22921  tanord1  22924  tanord  22925  tanregt0  22926  efif1olem2  22930  efif1olem4  22932  eff1olem  22935  rzgrp  22941  logrnaddcl  22962  logneg  22972  lognegb  22974  reexplog  22979  relogexp  22980  logfac  22985  efiarg  22992  cosargd  22993  cosarg0d  22994  argregt0  22995  argrege0  22996  argimgt0  22997  logneg2  23000  logmul2  23001  logdiv2  23002  abslogle  23003  tanarg  23004  logdivlti  23005  divlogrlim  23016  logcnlem2  23024  logcnlem3  23025  logcnlem4  23026  logcn  23028  logf1o2  23031  advlog  23035  advlogexp  23036  efopnlem1  23037  logtayllem  23040  logtayl  23041  logccv  23044  logcxp  23050  mulcxp  23066  divcxp  23068  cxpmul  23069  cxproot  23071  cxpmul2z  23072  abscxp  23073  abscxp2  23074  cxplt  23075  cxplea  23077  cxple2  23078  cxple2a  23080  cxplt3  23081  cxpsqrtlem  23083  cxpsqrt  23084  logsqrt  23085  dvcxp2  23117  cxpcn3lem  23121  resqrtcn  23123  cxpaddlelem  23125  cxpaddle  23126  abscxpbnd  23127  root1id  23128  root1eq1  23129  root1cj  23130  cxpeq  23131  loglesqrt  23132  cosangneg2d  23139  angrtmuld  23140  ang180lem2  23142  lawcoslem1  23147  lawcos  23148  pythag  23149  isosctrlem1  23152  isosctrlem2  23153  isosctrlem3  23154  ssscongptld  23156  chordthmlem  23163  chordthmlem2  23164  chordthmlem3  23165  chordthmlem4  23166  chordthmlem5  23167  heron  23169  asinsinlem  23222  reasinsin  23227  acosrecl  23234  atancj  23241  atanrecl  23242  atanlogaddlem  23244  atanlogsublem  23246  atanbndlem  23256  atans2  23262  ressatans  23265  atantayl  23268  leibpilem2  23272  leibpi  23273  leibpisum  23274  log2tlbnd  23276  log2ublem2  23278  birthdaylem2  23282  birthdaylem3  23283  cxp2limlem  23305  cxp2lim  23306  cxploglim  23307  cxploglim2  23308  divsqrtsumo1  23313  cvxcl  23314  scvxcvx  23315  jensenlem2  23317  jensen  23318  amgmlem  23319  logdiflbnd  23324  emcllem2  23326  emcllem3  23327  emcllem5  23329  emcllem6  23330  emcllem7  23331  harmonicbnd4  23340  fsumharmonic  23341  ftalem1  23346  ftalem2  23347  ftalem4  23349  ftalem5  23350  basellem3  23356  basellem4  23357  basellem5  23358  basellem6  23359  basellem7  23360  basellem8  23361  basellem9  23362  efnnfsumcl  23376  chtprm  23427  chpp1  23429  chtdif  23432  efchtdvds  23433  prmorcht  23452  mumullem2  23454  fsumfldivdiaglem  23465  ppiub  23479  chtleppi  23485  chtublem  23486  chtub  23487  pclogsum  23490  vmasum  23491  logfac2  23492  chpval2  23493  chpchtsum  23494  chpub  23495  logfaclbnd  23497  logfacbnd3  23498  logfacrlim  23499  logexprlim  23500  logfacrlim2  23501  mersenne  23502  dchrabs  23535  dchrptlem1  23539  dchrptlem2  23540  bcmax  23553  bcp1ctr  23554  bposlem1  23559  bposlem9  23567  lgsvalmod  23590  lgsdilem  23597  lgsne0  23608  lgsqrlem2  23617  lgseisenlem1  23624  lgseisenlem2  23625  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  mul2sq  23640  2sqlem3  23641  2sqlem8  23647  chebbnd1lem1  23654  chebbnd1lem2  23655  chebbnd1lem3  23656  chtppilimlem1  23658  chtppilimlem2  23659  chtppilim  23660  chto1ub  23661  chto1lb  23663  chpchtlim  23664  chpo1ub  23665  vmadivsum  23667  vmadivsumb  23668  rplogsumlem1  23669  rplogsumlem2  23670  rpvmasumlem  23672  dchrisumlema  23673  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasum2if  23682  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrvmasumiflem2  23687  dchrisum0flblem1  23693  dchrisum0fno1  23696  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  dchrmusumlem  23707  dchrvmasumlem  23708  rpvmasum  23711  rplogsum  23712  dirith2  23713  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  logdivsum  23718  mulog2sumlem1  23719  mulog2sumlem2  23720  mulog2sumlem3  23721  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  logsqvma  23727  logsqvma2  23728  log2sumbnd  23729  selberglem1  23730  selberglem2  23731  selberglem3  23732  selberg  23733  selbergb  23734  selberg2lem  23735  selberg2  23736  selberg2b  23737  chpdifbndlem1  23738  logdivbnd  23741  selberg3lem1  23742  selberg3lem2  23743  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrmax  23749  pntrsumo1  23750  pntrsumbnd  23751  pntrsumbnd2  23752  selbergr  23753  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntsval2  23761  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6a  23767  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2  23776  pntibndlem3  23777  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemn  23785  pntlemr  23787  pntlemj  23788  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntlem3  23794  pntleml  23796  pnt2  23798  pnt  23799  abvcxp  23800  ostth2lem1  23803  qabvexp  23811  padicabv  23815  padicabvcxp  23817  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth2  23822  ostth3  23823  ttgcontlem1  24188  fveecn  24205  eqeelen  24207  brbtwn2  24208  colinearalglem4  24212  colinearalg  24213  axsegconlem9  24228  axsegconlem10  24229  ax5seglem1  24231  ax5seglem2  24232  ax5seglem3  24234  ax5seglem5  24236  ax5seglem6  24237  ax5seglem9  24240  ax5seg  24241  axbtwnid  24242  axpaschlem  24243  axpasch  24244  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  eupap1  24976  nvm1  25567  nvpi  25569  nvz0  25571  nvmtri  25574  nvabs  25576  nvge0  25577  nv1  25579  smcnlem  25607  ipval2lem4  25616  ipval2  25617  4ipval2  25618  4ipval3  25622  ipidsq  25623  dipcj  25627  dip0r  25630  ipz  25632  nmoub3i  25688  nmlno0lem  25708  nmblolbii  25714  blocnilem  25719  cncph  25734  ipasslem4  25749  ipasslem5  25750  ipblnfi  25771  minvecolem2  25791  minvecolem4  25796  minvecolem6  25798  minvecolem7  25799  htthlem  25834  normpyc  26063  hhph  26095  bcs2  26099  norm1  26167  norm1exi  26168  pjhthlem1  26309  eigvalcl  26880  eighmorth  26883  nmlnop0iALT  26914  nmbdoplbi  26943  nmcexi  26945  nmcoplbi  26947  nmbdfnlbi  26968  nmcfnlbi  26971  riesz4i  26982  cnlnadjlem2  26987  cnlnadjlem7  26992  nmopcoi  27014  nmopcoadji  27020  branmfn  27024  leopnmid  27057  opsqrlem1  27059  hst1h  27146  hstle  27149  hstoh  27151  sto2i  27156  stadd3i  27167  strlem1  27169  golem1  27190  stcltrlem1  27195  cdj1i  27352  cdj3lem1  27353  cdj3lem3b  27359  cdj3i  27360  lt2addrd  27563  mul2lt0rlt0  27565  mul2lt0rgt0  27566  mul2lt0llt0  27567  mul2lt0lgt0  27568  mul2lt0bi  27569  le2halvesd  27576  fzsplit3  27599  bcm1n  27600  bhmafibid1  27632  bhmafibid2  27633  2sqmod  27636  regsumfsum  27772  elunitcn  27880  sqsscirc1  27890  sqsscirc2  27891  cnre2csqima  27893  rmulccn  27910  xrge0iifcnv  27915  xrge0iifhom  27919  zrhnm  27950  rezh  27952  nexple  28005  nnlogbexp  28020  logbrec  28021  indsum  28036  esumpcvgval  28084  dya2ub  28241  dya2icoseg  28248  eulerpartlemgc  28301  ballotlemsi  28453  sgnmul  28481  sgnsub  28483  eluzmn  28491  plymulx0  28504  signsply0  28508  signsvtp  28540  signsvtn  28541  signsvfpn  28542  signsvfnn  28543  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgambdd  28579  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  regamcl  28603  relgamcl  28604  lgam1  28606  subfacval2  28631  subfaclim  28632  subfacval3  28633  rescon  28691  sinccvglem  29038  circum  29040  possumd  29116  climlec3  29120  faclimlem1  29168  faclimlem2  29169  faclimlem3  29170  faclim  29171  iprodfac  29172  faclim2  29173  bpolydiflem  29816  bpoly4  29821  supadd  30042  ltflcei  30043  sin2h  30045  cos2h  30046  tan2h  30047  opnmbllem0  30050  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  mbfposadd  30062  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ibladdnc  30072  itgaddnclem2  30074  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  itgmulc2nclem2  30082  itgmulc2nc  30083  itgabsnc  30084  bddiblnc  30085  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anclem1  30090  ftc1anclem2  30091  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem1  30107  areacirclem5  30111  areacirc  30112  mettrifi  30250  lmclim2  30251  geomcau  30252  isbnd3  30280  ssbnd  30284  cntotbnd  30292  bfplem1  30318  bfplem2  30319  bfp  30320  rrnmet  30325  rrndstprj1  30326  rrndstprj2  30327  rrncmslem  30328  rrnequiv  30331  rrntotbnd  30332  ismrer1  30334  eldioph2lem1  30693  lzenom  30703  rencldnfilem  30754  icodiamlt  30756  irrapxlem1  30758  irrapxlem2  30759  irrapxlem3  30760  irrapxlem4  30761  irrapxlem5  30762  pellexlem2  30766  pellexlem6  30770  pell1234qrreccl  30790  pell14qrgt0  30795  pell14qrdivcl  30801  pell14qrexpclnn0  30802  pell14qrexpcl  30803  pell14qrdich  30805  pell1qrgaplem  30809  pellfundex  30822  reglogmul  30829  reglogexp  30830  reglogbas  30831  reglog1  30832  pellfund14  30834  rmspecsqrtnq  30842  rmspecfund  30845  monotoddzzfi  30878  expmordi  30883  jm2.24nn  30897  jm2.17a  30898  jm2.17b  30899  jm2.17c  30900  jm2.24  30901  acongrep  30918  fzmaxdif  30919  acongeq  30921  modabsdifz  30927  jm2.19lem4  30934  jm2.19  30935  jm2.26lem3  30943  jm3.1lem1  30959  jm3.1lem2  30960  itgpowd  31182  areaquad  31184  cvgdvgrat  31194  radcnvrat  31195  hashnzfzclim  31227  dvconstbi  31239  binomcxplemnn0  31254  binomcxplemnotnn0  31261  oddfl  31459  dstregt0  31463  zltlesub  31468  lt2addmuld  31473  sublt0d  31495  lt3addmuld  31501  fperiodmullem  31503  fperiodmul  31504  lt4addmuld  31506  fzdifsuc2  31512  iooabslt  31532  iccshift  31558  iooshift  31562  fmul01  31574  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fprodabs2  31602  fprodle  31604  climinf  31612  limcrecl  31635  lptre2pt  31646  limcleqr  31650  0ellimcdiv  31655  limclner  31657  sinaover2ne0  31668  cncfperiod  31681  ioccncflimc  31688  cncficcgt0  31691  icocncflimc  31692  cncfshiftioo  31695  cncfiooicc  31697  fperdvper  31715  dvbdfbdioolem1  31725  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc1  31730  ioodvbdlimc2lem  31731  ioodvbdlimc2  31732  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  itgcoscmulx  31768  volioc  31771  itgsincmulx  31773  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem7  31789  stoweidlem11  31793  stoweidlem13  31795  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem21  31803  stoweidlem22  31804  stoweidlem23  31805  stoweidlem24  31806  stoweidlem26  31808  stoweidlem32  31814  stoweidlem36  31818  stoweidlem44  31826  stoweidlem47  31829  wallispilem3  31849  wallispi2lem1  31853  stirlinglem1  31856  stirlinglem5  31860  stirlinglem11  31866  stirlinglem12  31867  stirlinglem14  31869  dirkerval2  31876  dirkerre  31877  dirkertrigeqlem2  31881  dirkertrigeq  31883  dirkeritg  31884  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem6  31895  fourierdlem7  31896  fourierdlem13  31902  fourierdlem14  31903  fourierdlem16  31905  fourierdlem18  31907  fourierdlem19  31908  fourierdlem21  31910  fourierdlem22  31911  fourierdlem24  31913  fourierdlem26  31915  fourierdlem28  31917  fourierdlem30  31919  fourierdlem35  31924  fourierdlem39  31928  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem43  31932  fourierdlem44  31933  fourierdlem47  31936  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem53  31942  fourierdlem56  31945  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem66  31955  fourierdlem68  31957  fourierdlem70  31959  fourierdlem71  31960  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem77  31966  fourierdlem78  31967  fourierdlem79  31968  fourierdlem80  31969  fourierdlem81  31970  fourierdlem83  31972  fourierdlem84  31973  fourierdlem85  31974  fourierdlem87  31976  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem95  31984  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem109  31998  fourierdlem111  32000  fourierdlem112  32001  fouriercnp  32009  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  etransclem14  32031  etransclem18  32035  etransclem23  32040  etransclem24  32041  etransclem27  32044  etransclem46  32063  etransclem48  32065  sigaras  32072  sigarms  32073  sigarls  32074  sigarexp  32076  sigarperm  32077  sigarimcd  32079  sigarcol  32081  sharhght  32082  cevathlem2  32085  isosctrlem1ALT  33734  sineq0ALT  33737  absmulrposd  37971  extoimad  37981  imo72b2lem0  37982  imo72b2lem1  37988  imo72b2  37993  int-addcomd  37994  int-addassocd  37995  int-addsimpd  37996  int-mulcomd  37997  int-mulassocd  37998  int-mulsimpd  37999  int-leftdistd  38000  int-rightdistd  38001  int-sqdefd  38002  int-mul11d  38003  int-mul12d  38004  int-add01d  38005  int-add02d  38006  int-sqgeq0d  38007  int-eqmvtd  38010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator