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

Theorem ltled 9514
Description: 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
ltled.1  |-  ( ph  ->  A  <  B )
Assertion
Ref Expression
ltled  |-  ( ph  ->  A  <_  B )

Proof of Theorem ltled
StepHypRef Expression
1 ltled.1 . 2  |-  ( ph  ->  A  <  B )
2 ltd.1 . . 3  |-  ( ph  ->  A  e.  RR )
3 ltd.2 . . 3  |-  ( ph  ->  B  e.  RR )
4 ltle 9455 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 661 . 2  |-  ( ph  ->  ( A  <  B  ->  A  <_  B )
)
61, 5mpd 15 1  |-  ( ph  ->  A  <_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   class class class wbr 4287   RRcr 9273    < clt 9410    <_ cle 9411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-pre-lttri 9348
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416
This theorem is referenced by:  ltnsymd  9515  mulge0  9849  msqge0  9853  addgt0d  9906  lt2addd  9953  lt2msq1  10207  uzwo3  10940  fznatpl1  11502  modaddmodup  11754  expmulnbnd  11988  fzsdom2  12181  repswcshw  12438  isercolllem1  13134  caucvgrlem  13142  climcnds  13306  geomulcvg  13328  mertenslem1  13336  ruclem2  13506  ruclem12  13515  bitsfzo  13623  bitsmod  13624  4sqlem7  13997  vdwlem1  14034  met1stc  20076  cfilucfilOLD  20124  cfilucfil  20125  nlmvscnlem2  20246  icccmplem2  20380  reconnlem2  20384  xrhmeo  20498  cnheibor  20507  nmoleub2lem3  20650  ipcnlem2  20736  minveclem3b  20895  ivthlem1  20915  ivthlem2  20916  ivth2  20919  ivthle  20920  ivthle2  20921  ovollb2lem  20951  ovolicc2lem4  20983  ovolicc2lem5  20984  ioombl1lem4  21022  uniioombllem4  21046  uniioombllem5  21047  opnmbllem  21061  ismbf3d  21112  mbfi1fseqlem6  21178  itg2gt0  21218  dveflem  21431  dvferm1lem  21436  dvferm2lem  21438  rollelem  21441  rolle  21442  cmvth  21443  mvth  21444  c1liplem1  21448  dvgt0lem1  21454  dvivthlem1  21460  lhop1lem  21465  lhop1  21466  dvcnvrelem1  21469  dvcnvrelem2  21470  dvcvx  21472  dgradd2  21715  aaliou3lem8  21791  aaliou3lem7  21795  ulmdvlem1  21845  itgulm  21853  radcnvlt1  21863  radcnvle  21865  abelthlem7  21883  efcvx  21894  coseq0negpitopi  21945  tangtx  21947  tanabsge  21948  tanord  21974  abslogimle  22005  divlogrlim  22060  logno1  22061  logcnlem3  22069  logcnlem4  22070  logtayl  22085  logccv  22088  cxple  22120  chordthmlem4  22210  asinsin  22267  atanlogaddlem  22288  atantan  22298  cxp2limlem  22349  logdifbnd  22367  emcllem4  22372  harmonicbnd4  22384  ftalem1  22390  ftalem2  22391  ftalem3  22392  basellem5  22402  basellem8  22405  chpchtsum  22538  bposlem1  22603  lgseisenlem1  22668  lgsquadlem1  22673  lgsquadlem2  22674  lgsquadlem3  22675  chebbnd1lem2  22699  chebbnd1lem3  22700  chtppilimlem1  22702  chto1ub  22705  chpo1ubb  22710  vmadivsumb  22712  dchrisumlem3  22720  mulog2sumlem1  22763  vmalogdivsum2  22767  vmalogdivsum  22768  2vmadivsumlem  22769  selbergb  22778  selberg2b  22781  chpdifbndlem1  22782  selberg3lem2  22787  selberg3  22788  selberg4lem1  22789  selberg4  22790  pntrsumbnd  22795  selberg3r  22798  selberg4r  22799  selberg34r  22800  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntrlog2bndlem6a  22811  pntrlog2bndlem6  22812  pntrlog2bnd  22813  pntpbnd1a  22814  pntpbnd1  22815  pntpbnd2  22816  pntibndlem2  22820  pntlemb  22826  pntlemq  22830  pntlemr  22831  pntlemj  22832  pntlemf  22834  pntlemp  22839  ostth2lem2  22863  axpaschlem  23154  axlowdimlem16  23171  smcnlem  24060  bcm1n  26047  dya2icoseg  26661  eulerpartlemgc  26714  dstfrvunirn  26826  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemimin  26857  ballotlemsgt1  26862  ballotlemfrcn0  26881  sgnmul  26894  lgamucov  26993  subfacval3  27046  erdszelem8  27055  cvmliftlem6  27148  cvmliftlem7  27149  cvmliftlem8  27150  cvmliftlem9  27151  cvmliftlem10  27152  sinccvglem  27286  lxflflp1  28392  opnmbllem0  28398  itg2addnclem  28414  itg2addnclem3  28416  itg2addnc  28417  itg2gt0cn  28418  areacirclem1  28455  areacirc  28460  isbnd3  28654  cntotbnd  28666  rrnequiv  28705  irrapxlem3  29136  pellexlem2  29142  pellfundglb  29197  monotuz  29253  monotoddzzfi  29254  acongrep  29294  stoweidlem1  29767  stoweidlem3  29769  stoweidlem7  29773  stoweidlem24  29790  stoweidlem26  29792  stoweidlem42  29808  wallispilem5  29835  stirlinglem1  29840  stirlinglem6  29845  stirlinglem7  29846  stirlinglem10  29849  stirlinglem12  29851  stirlinglem13  29852  stirlingr  29856
  Copyright terms: Public domain W3C validator