Theorem ltle 11286

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 880	. 2 ⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
2		leloe 11284	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	imbitrrid 249	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1563   ∈ wcel 2145   class class class wbr 5104  ℝcr 11087   < clt 11231   ≤ cle 11232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-pre-lttri 11162

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237

This theorem is referenced by:  leltletr  11289  ltleletr  11291  letr  11292  letric  11298  ltlen  11299  ltlei  11320  ltled  11346  lt2add  11687  lep1  12044  lem1  12046  letrp1  12047  ltmul12a  12059  mulge0b  12073  lediv12a  12096  bndndx  12491  ltsubnn0  12543  uzind  12676  fnn0ind  12683  eluz2b2  12933  zmin  12956  rpnnen1lem2  12989  rpnnen1lem1  12990  rpnnen1lem3  12991  rpnnen1lem5  12993  rpge0  13018  rpneg  13038  iccsplit  13500  zltaddlt1le  13520  difelfznle  13658  fvffz0  13662  elfzouz2  13691  elfzo0le  13720  fzostep1  13803  fllep1  13822  fracle1  13824  expgt1  14124  expnbnd  14256  expnlbnd2  14258  faclbnd  14314  swrdnd0  14683  swrdsbslen  14690  swrdspsleq  14691  pfxccat3  14759  swrdccat  14760  repswswrd  14809  resqrex  15289  sqrtgt0  15297  absmax  15369  eqsqrt2d  15408  rlim2lt  15536  mulcn2  15635  rlimo1  15656  o1rlimmul  15658  climbdd  15711  caucvgrlem  15712  supcvg  15898  efcllem  16119  sin01bnd  16229  cos01bnd  16230  sin01gt0  16234  cos01gt0  16235  absef  16241  efieq1re  16243  ruclem11  16284  nn0o  16429  pythagtriplem12  16874  pythagtriplem13  16875  pythagtriplem14  16876  pythagtriplem16  16878  pclem  16886  prmgaplem4  17102  cshwshashlem2  17144  isabvd  20881  met2ndci  24636  blcvx  24912  iocopnst  25056  nmoleub2a  25233  nmoleub2b  25234  nmhmcn  25236  iscmet3lem2  25408  caubl  25424  ivthlem2  25568  ovolicc2lem4  25636  ioombl1lem4  25677  ioovolcl  25686  volsup2  25721  itg2monolem1  25866  itg2gt0  25876  itg2cnlem1  25877  dvne0  26127  ftc1lem4  26155  dgrlt  26380  aalioulem5  26454  ulmbdd  26515  iblulm  26524  radcnvlem1  26530  abelthlem5  26552  abelthlem7  26555  sincosq1lem  26616  tangtx  26624  tanabsge  26625  sinq12ge0  26627  sineq0  26643  tanord  26657  logcj  26725  argregt0  26729  argrege0  26730  argimgt0  26731  logdmnrp  26760  logcnlem3  26763  logf1o2  26769  cxpsqrtlem  26821  abscxpbnd  26872  logreclem  26881  asinneg  27005  atanlogsublem  27034  atanlogsub  27035  rlimcnp  27084  xrlimcnp  27087  basellem8  27206  chtub  27330  bposlem9  27410  chebbnd1  27590  chtppilimlem1  27591  dchrvmasumiflem1  27619  mulog2sumlem2  27653  pntrmax  27682  pntibndlem2  27709  pntibndlem3  27710  pntlemf  27723  axlowdimlem16  29212  pthdlem1  30020  crctcshwlkn0lem3  30066  crctcshwlkn0lem5  30068  crctcshwlkn0lem7  30070  crctcshwlkn0  30075  nmblolbii  31056  ubthlem1  31127  bcsiALT  31436  nmbdoplbi  32281  nmcexi  32283  nmcoplbi  32285  lnconi  32290  nmbdfnlbi  32306  nmcfnlbi  32309  nmopcoi  32352  branmfn  32362  leopmul  32391  nmopleid  32396  esumcvg  34388  ballotlemfrceq  34831  sinccvglem  36030  opnrebl2  36689  ivthALT  36703  dnibndlem12  36935  poimirlem15  38141  poimirlem31  38157  ftc1cnnclem  38197  ftc1anclem5  38203  incsequz2  38255  nnubfi  38256  bfplem2  38329  60gcd7e1  42629  lcmineqlem10  42662  3cubeslem1  43272  pell14qrgap  43459  pellfundre  43465  pellfundlb  43468  reabsifneg  44215  reabsifnpos  44216  reabsifpos  44217  reabsifnneg  44218  stoweidlem17  46590  stoweidlem34  46607  wallispilem1  46638  sqrtnegnre  47900  2elfz2melfz  47911  elfzelfzlble  47914  subsubelfzo0  47920  m1modmmod  47957  requad01  48242  requad2  48244  bgoldbtbnd  48430  bgoldbachlt  48434  tgblthelfgott  48436  nnolog2flm1  49222  itsclc0yqsol  49396