Theorem ltle 11299

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

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   class class class wbr 5110  ℝcr 11100   < clt 11244   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-pre-lttri 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250

This theorem is referenced by:  leltletr  11302  ltleletr  11304  letr  11305  letric  11311  ltlen  11312  ltlei  11333  ltled  11359  lt2add  11700  lep1  12057  lem1  12059  letrp1  12060  ltmul12a  12072  mulge0b  12086  lediv12a  12109  bndndx  12504  ltsubnn0  12556  uzind  12689  fnn0ind  12696  eluz2b2  12946  zmin  12969  rpnnen1lem2  13002  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  rpge0  13031  rpneg  13051  iccsplit  13513  zltaddlt1le  13533  difelfznle  13672  fvffz0  13676  elfzouz2  13705  elfzo0le  13734  fzostep1  13817  fllep1  13836  fracle1  13838  expgt1  14138  expnbnd  14270  expnlbnd2  14272  faclbnd  14328  swrdnd0  14697  swrdsbslen  14704  swrdspsleq  14705  pfxccat3  14773  swrdccat  14774  repswswrd  14823  resqrex  15303  sqrtgt0  15311  absmax  15383  eqsqrt2d  15422  rlim2lt  15550  mulcn2  15649  rlimo1  15670  o1rlimmul  15672  climbdd  15725  caucvgrlem  15726  supcvg  15912  efcllem  16132  sin01bnd  16242  cos01bnd  16243  sin01gt0  16247  cos01gt0  16248  absef  16254  efieq1re  16256  ruclem11  16297  nn0o  16442  pythagtriplem12  16887  pythagtriplem13  16888  pythagtriplem14  16889  pythagtriplem16  16891  pclem  16899  prmgaplem4  17115  cshwshashlem2  17157  isabvd  20896  met2ndci  24660  blcvx  24936  iocopnst  25080  nmoleub2a  25257  nmoleub2b  25258  nmhmcn  25260  iscmet3lem2  25432  caubl  25448  ivthlem2  25592  ovolicc2lem4  25660  ioombl1lem4  25701  ioovolcl  25710  volsup2  25745  itg2monolem1  25890  itg2gt0  25900  itg2cnlem1  25901  dvne0  26151  ftc1lem4  26179  dgrlt  26404  aalioulem5  26480  ulmbdd  26542  iblulm  26551  radcnvlem1  26557  abelthlem5  26579  abelthlem7  26582  sincosq1lem  26643  tangtx  26651  tanabsge  26652  sinq12ge0  26654  sineq0  26670  tanord  26684  logcj  26752  argregt0  26756  argrege0  26757  argimgt0  26758  logdmnrp  26787  logcnlem3  26790  logf1o2  26796  cxpsqrtlem  26848  abscxpbnd  26899  logreclem  26908  asinneg  27032  atanlogsublem  27061  atanlogsub  27062  rlimcnp  27111  xrlimcnp  27114  basellem8  27233  chtub  27357  bposlem9  27437  chebbnd1  27617  chtppilimlem1  27618  dchrvmasumiflem1  27646  mulog2sumlem2  27680  pntrmax  27709  pntibndlem2  27736  pntibndlem3  27737  pntlemf  27750  axlowdimlem16  29288  pthdlem1  30096  crctcshwlkn0lem3  30142  crctcshwlkn0lem5  30144  crctcshwlkn0lem7  30146  crctcshwlkn0  30151  nmblolbii  31132  ubthlem1  31203  bcsiALT  31512  nmbdoplbi  32357  nmcexi  32359  nmcoplbi  32361  lnconi  32366  nmbdfnlbi  32382  nmcfnlbi  32385  nmopcoi  32428  branmfn  32438  leopmul  32467  nmopleid  32472  esumcvg  34457  ballotlemfrceq  34900  sinccvglem  36145  opnrebl2  36813  ivthALT  36827  dnibndlem12  37059  poimirlem15  38267  poimirlem31  38283  ftc1cnnclem  38323  ftc1anclem5  38329  incsequz2  38381  nnubfi  38382  bfplem2  38455  60gcd7e1  42753  lcmineqlem10  42786  3cubeslem1  43398  pell14qrgap  43585  pellfundre  43591  pellfundlb  43594  reabsifneg  44341  reabsifnpos  44342  reabsifpos  44343  reabsifnneg  44344  stoweidlem17  46714  stoweidlem34  46731  wallispilem1  46762  sqrtnegnre  48027  2elfz2melfz  48038  elfzelfzlble  48041  subsubelfzo0  48047  m1modmmod  48084  requad01  48369  requad2  48371  bgoldbtbnd  48557  bgoldbachlt  48561  tgblthelfgott  48563  nnolog2flm1  49353  itsclc0yqsol  49527