Theorem ltled 10185

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

Step	Hyp	Ref	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 10126	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
5	2, 3, 4	syl2anc 693	. 2 |- ( ph -> ( A < B -> A <_ B ) )
6	1, 5	mpd 15	1 |- ( ph -> A <_ B )

Syntax hints:   -> wi 4   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttri 10010

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  ltnsymd  10186  mulge0  10546  msqge0  10549  addgt0d  10602  lt2addd  10650  lt2msq1  10907  uzwo3  11783  fznatpl1  12395  flflp1  12608  modaddmodup  12733  expmulnbnd  12996  fzsdom2  13215  repswcshw  13558  isercolllem1  14395  caucvgrlem  14403  climcnds  14583  geomulcvg  14607  mertenslem1  14616  ruclem2  14961  ruclem12  14970  bitsfzo  15157  bitsmod  15158  lcmgcdlem  15319  isprm7  15420  4sqlem7  15648  vdwlem1  15685  met1stc  22326  cfilucfil  22364  nlmvscnlem2  22489  icccmplem2  22626  reconnlem2  22630  xrhmeo  22745  cnheibor  22754  nmoleub2lem3  22915  ipcnlem2  23043  minveclem3b  23199  ivthlem1  23220  ivthlem2  23221  ivth2  23224  ivthle  23225  ivthle2  23226  ovollb2lem  23256  ovolicc2lem4  23288  ovolicc2lem5  23289  ioombl1lem4  23329  uniioombllem4  23354  uniioombllem5  23355  opnmbllem  23369  ismbf3d  23421  mbfi1fseqlem6  23487  itg2gt0  23527  dveflem  23742  dvferm1lem  23747  dvferm2lem  23749  rollelem  23752  rolle  23753  cmvth  23754  mvth  23755  c1liplem1  23759  dvgt0lem1  23765  dvivthlem1  23771  lhop1lem  23776  lhop1  23777  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcvx  23783  dgradd2  24024  aaliou3lem8  24100  aaliou3lem7  24104  ulmdvlem1  24154  itgulm  24162  radcnvlt1  24172  radcnvle  24174  abelthlem7  24192  efcvx  24203  coseq0negpitopi  24255  tangtx  24257  tanabsge  24258  tanord  24284  abslogimle  24320  divlogrlim  24381  logno1  24382  logcnlem3  24390  logcnlem4  24391  logtayl  24406  logccv  24409  cxple  24441  chordthmlem4  24562  asinsin  24619  atanlogaddlem  24640  atantan  24650  cxp2limlem  24702  logdifbnd  24720  emcllem4  24725  harmonicbnd4  24737  lgamucov  24764  ftalem1  24799  ftalem2  24800  ftalem3  24801  basellem5  24811  basellem8  24814  chpchtsum  24944  bposlem1  25009  lgseisenlem1  25100  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  chebbnd1lem2  25159  chebbnd1lem3  25160  chtppilimlem1  25162  chto1ub  25165  chpo1ubb  25170  vmadivsumb  25172  dchrisumlem3  25180  mulog2sumlem1  25223  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  selbergb  25238  selberg2b  25241  chpdifbndlem1  25242  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrsumbnd  25255  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6a  25271  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntlemb  25286  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemp  25299  ostth2lem2  25323  axpaschlem  25820  axlowdimlem16  25837  smcnlem  27552  bcm1n  29554  smatrcl  29862  fiunelros  30237  dya2icoseg  30339  eulerpartlemgc  30424  dstfrvunirn  30536  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemimin  30567  ballotlemsgt1  30572  ballotlemfrcn0  30591  sgnmul  30604  fdvposlt  30677  breprexp  30711  logdivsqrle  30728  hgt750leme  30736  tgoldbachgt  30741  subfacval3  31171  erdszelem8  31180  cvmliftlem6  31272  cvmliftlem7  31273  cvmliftlem8  31274  cvmliftlem9  31275  cvmliftlem10  31276  sinccvglem  31566  dnibndlem9  32476  unbdqndv2lem2  32501  knoppndvlem14  32516  knoppndvlem18  32520  knoppndvlem19  32521  poimirlem7  33416  poimirlem15  33424  opnmbllem0  33445  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  areacirclem1  33500  areacirc  33505  isbnd3  33583  cntotbnd  33595  rrnequiv  33634  irrapxlem3  37388  pellexlem2  37394  pellfundglb  37449  monotuz  37506  monotoddzzfi  37507  acongrep  37547  cvgdvgrat  38512  hashnzfz2  38520  hashnzfzclim  38521  binomcxplemnotnn0  38555  monoords  39511  xralrple2  39570  reclt0d  39607  reclt0  39614  uzublem  39657  iooiinicc  39769  iooiinioc  39783  limciccioolb  39853  limcicciooub  39869  lptre2pt  39872  limsupubuzlem  39944  limsup10exlem  40004  icccncfext  40100  cncfiooicclem1  40106  dvdivbd  40138  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnxpaek  40157  dvnmul  40158  volioc  40188  iblspltprt  40189  itgspltprt  40195  volico  40200  volioore  40207  voliooico  40209  voliccico  40216  stoweidlem1  40218  stoweidlem3  40220  stoweidlem7  40224  stoweidlem24  40241  stoweidlem26  40243  stoweidlem42  40259  wallispilem5  40286  stirlinglem1  40291  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem12  40302  stirlinglem13  40303  stirlingr  40307  dirkertrigeqlem1  40315  fourierdlem10  40334  fourierdlem11  40335  fourierdlem12  40336  fourierdlem14  40338  fourierdlem15  40339  fourierdlem17  40341  fourierdlem19  40343  fourierdlem30  40354  fourierdlem37  40361  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem68  40391  fourierdlem73  40396  fourierdlem74  40397  fourierdlem76  40399  fourierdlem77  40400  fourierdlem78  40401  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem92  40415  fourierdlem93  40416  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem111  40434  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem19  40470  etransclem23  40474  etransclem35  40486  etransclem41  40492  qndenserrnbllem  40514  iundjiun  40677  carageniuncllem2  40736  caratheodorylem1  40740  hoicvr  40762  ovnsubaddlem1  40784  hsphoidmvle2  40799  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoiqssbllem1  40836  hoiqssbllem2  40837  volico2  40855  iinhoiicclem  40887  iunhoiioolem  40889  vonioolem2  40895  vonicclem2  40898  pimdecfgtioo  40927  pimincfltioo  40928  smflimlem4  40982  smfmullem1  40998  smflimsuplem4  41029  expnegico01  42308