Theorem ltle 10005

Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)

Assertion

Ref	Expression
ltle	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Proof of Theorem ltle

Step	Hyp	Ref	Expression
1		orc 399	. 2 ⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
2		leloe 10003	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	syl5ibr 235	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  ltleletr  10009  letr  10010  letric  10016  ltlen  10017  ltlei  10038  ltled  10064  lt2add  10392  lep1  10741  lem1  10743  letrp1  10744  ltmul12a  10758  mulge0b  10772  lediv12a  10795  bndndx  11168  ltsubnn0  11221  uzind  11345  fnn0ind  11352  eluz2b2  11637  zmin  11660  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  rpge0  11721  rpneg  11739  iccsplit  12176  zltaddlt1le  12195  difelfznle  12322  fvffz0  12326  elfzouz2  12353  elfzo0le  12379  fzosplitprm1  12443  fzostep1  12446  fllep1  12464  fracle1  12466  expgt1  12760  expnbnd  12855  expnlbnd2  12857  faclbnd  12939  swrdsbslen  13300  swrdspsleq  13301  swrdccat3  13343  repswswrd  13382  resqrex  13839  sqrtgt0  13847  absmax  13917  eqsqrt2d  13956  rlim2lt  14076  mulcn2  14174  rlimo1  14195  o1rlimmul  14197  climbdd  14250  caucvgrlem  14251  supcvg  14427  efcllem  14647  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  cos01gt0  14760  absef  14766  efieq1re  14768  ruclem11  14808  nn0o  14937  pythagtriplem12  15369  pythagtriplem13  15370  pythagtriplem14  15371  pythagtriplem16  15373  pclem  15381  prmgaplem4  15596  cshwshashlem2  15641  isabvd  18643  met2ndci  22137  blcvx  22409  iocopnst  22547  nmoleub2a  22725  nmoleub2b  22726  nmhmcn  22728  iscmet3lem2  22898  caubl  22914  ivthlem2  23028  ovolicc2lem4  23095  ioombl1lem4  23136  ioovolcl  23144  volsup2  23179  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  dvne0  23578  ftc1lem4  23606  dgrlt  23826  aalioulem5  23895  ulmbdd  23956  iblulm  23965  radcnvlem1  23971  abelthlem5  23993  abelthlem7  23996  sincosq1lem  24053  tangtx  24061  tanabsge  24062  sinq12ge0  24064  sineq0  24077  tanord  24088  logcj  24156  argregt0  24160  argrege0  24161  argimgt0  24162  logdmnrp  24187  logcnlem3  24190  logf1o2  24196  cxpsqrtlem  24248  abscxpbnd  24294  logreclem  24300  asinneg  24413  atanlogsublem  24442  atanlogsub  24443  rlimcnp  24492  xrlimcnp  24495  basellem8  24614  chtub  24737  bposlem9  24817  chebbnd1  24961  chtppilimlem1  24962  dchrvmasumiflem1  24990  mulog2sumlem2  25024  pntrmax  25053  pntibndlem2  25080  pntibndlem3  25081  pntlemf  25094  axlowdimlem16  25637  nmblolbii  27038  ubthlem1  27110  bcsiALT  27420  nmbdoplbi  28267  nmcexi  28269  nmcoplbi  28271  lnconi  28276  nmbdfnlbi  28292  nmcfnlbi  28295  nmopcoi  28338  branmfn  28348  leopmul  28377  nmopleid  28382  esumcvg  29475  ballotlemfrceq  29917  sinccvglem  30820  opnrebl2  31486  ivthALT  31500  dnibndlem12  31649  poimirlem15  32594  poimirlem31  32610  ftc1cnnclem  32653  ftc1anclem5  32659  incsequz2  32715  nnubfi  32716  bfplem2  32792  pell14qrgap  36457  pellfundre  36463  pellfundlb  36466  stoweidlem17  38910  stoweidlem34  38927  wallispilem1  38958  leltletr  39940  bgoldbtbnd  40225  bgoldbachlt  40227  tgblthelfgott  40229  bgoldbachltOLD  40234  tgblthelfgottOLD  40236  pfxccat3  40289  2elfz2melfz  40355  elfzelfzlble  40358  subsubelfzo0  40359  pthdlem1  40972  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem7  41019  crctcsh1wlkn0  41024  m1modmmod  42110  nnolog2flm1  42182