Theorem ltle 11391

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttri 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  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 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342

This theorem is used by:  leltletr  11394  ltleletr  11396  letr  11397  letric  11403  ltlen  11404  ltlei  11425  ltled  11451  lt2add  11794  lep1  12151  lem1  12153  letrp1  12154  ltmul12a  12166  mulge0b  12180  lediv12a  12203  bndndx  12598  ltsubnn0  12650  uzind  12784  fnn0ind  12791  eluz2b2  13041  zmin  13064  rpnnen1lem2  13098  rpnnen1lem1  13099  rpnnen1lem3  13100  rpnnen1lem5  13102  rpge0  13127  rpneg  13147  iccsplit  13609  zltaddlt1le  13629  difelfznle  13769  fvffz0  13773  elfzouz2  13802  elfzo0le  13831  fzostep1  13914  fllep1  13934  fracle1  13936  expgt1  14236  expnbnd  14369  expnlbnd2  14371  faclbnd  14427  swrdnd0  14800  swrdsbslen  14807  swrdspsleq  14808  pfxccat3  14876  swrdccat  14877  repswswrd  14928  resqrex  15410  sqrtgt0  15418  absmax  15490  eqsqrt2d  15529  rlim2lt  15657  mulcn2  15756  rlimo1  15777  o1rlimmul  15779  climbdd  15832  caucvgrlem  15833  supcvg  16018  efcllem  16236  sin01bnd  16346  cos01bnd  16347  sin01gt0  16351  cos01gt0  16352  absef  16358  efieq1re  16360  ruclem11  16401  nn0o  16546  pythagtriplem12  16997  pythagtriplem13  16998  pythagtriplem14  16999  pythagtriplem16  17001  pclem  17009  prmgaplem4  17225  cshwshashlem2  17267  isabvd  21062  met2ndci  24834  blcvx  25110  iocopnst  25254  nmoleub2a  25431  nmoleub2b  25432  nmhmcn  25434  iscmet3lem2  25606  caubl  25622  ivthlem2  25766  ovolicc2lem4  25834  ioombl1lem4  25875  ioovolcl  25884  volsup2  25919  itg2monolem1  26064  itg2gt0  26074  itg2cnlem1  26075  dvne0  26324  ftc1lem4  26352  dgrlt  26578  aalioulem5  26656  ulmbdd  26718  iblulm  26727  radcnvlem1  26733  abelthlem5  26755  abelthlem7  26758  sincosq1lem  26819  tangtx  26827  tanabsge  26828  sinq12ge0  26830  sineq0  26845  tanord  26859  logcj  26927  argregt0  26931  argrege0  26932  argimgt0  26933  logdmnrp  26962  logcnlem3  26965  logf1o2  26971  cxpsqrtlem  27023  abscxpbnd  27074  logreclem  27083  asinneg  27207  atanlogsublem  27236  atanlogsub  27237  rlimcnp  27286  xrlimcnp  27289  basellem8  27408  chtub  27532  bposlem9  27612  chebbnd1  27792  chtppilimlem1  27793  dchrvmasumiflem1  27821  mulog2sumlem2  27855  pntrmax  27884  pntibndlem2  27911  pntibndlem3  27912  pntlemf  27925  axlowdimlem16  29528  pthdlem1  30345  crctcshwlkn0lem3  30394  crctcshwlkn0lem5  30396  crctcshwlkn0lem7  30398  crctcshwlkn0  30403  nmblolbii  31394  ubthlem1  31465  bcsiALT  31774  nmbdoplbi  32619  nmcexi  32621  nmcoplbi  32623  lnconi  32628  nmbdfnlbi  32644  nmcfnlbi  32647  nmopcoi  32690  branmfn  32700  leopmul  32729  nmopleid  32734  esumcvg  34711  ballotlemfrceq  35154  sinccvglem  36416  opnrebl2  37089  ivthALT  37103  dnibndlem12  37335  poimirlem15  38533  poimirlem31  38549  ftc1cnnclem  38589  ftc1anclem5  38595  incsequz2  38663  nnubfi  38664  bfplem2  38737  60gcd7e1  43035  lcmineqlem10  43068  3cubeslem1  43674  pell14qrgap  43861  pellfundre  43867  pellfundlb  43870  reabsifneg  44617  reabsifnpos  44618  reabsifpos  44619  reabsifnneg  44620  stoweidlem17  46996  stoweidlem34  47013  wallispilem1  47044  sqrtnegnre  48346  2elfz2melfz  48357  elfzelfzlble  48360  subsubelfzo0  48366  m1modmmod  48403  requad01  48688  requad2  48690  bgoldbtbnd  48876  bgoldbachlt  48880  tgblthelfgott  48882  nnolog2flm1  49671  itsclc0yqsol  49845