Theorem ltle 11252

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   class class class wbr 5110  ℝcr 11059   < clt 11198   ≤ cle 11199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-pre-lttri 11134

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204

This theorem is referenced by:  leltletr  11255  ltleletr  11257  letr  11258  letric  11264  ltlen  11265  ltlei  11286  ltled  11312  lt2add  11649  lep1  12005  lem1  12007  letrp1  12008  ltmul12a  12020  mulge0b  12034  lediv12a  12057  bndndx  12421  ltsubnn0  12473  uzind  12604  fnn0ind  12611  eluz2b2  12855  zmin  12878  rpnnen1lem2  12911  rpnnen1lem1  12912  rpnnen1lem3  12913  rpnnen1lem5  12915  rpge0  12937  rpneg  12956  iccsplit  13412  zltaddlt1le  13432  difelfznle  13565  fvffz0  13569  elfzouz2  13597  elfzo0le  13626  fzostep1  13698  fllep1  13716  fracle1  13718  expgt1  14016  expnbnd  14145  expnlbnd2  14147  faclbnd  14200  swrdnd0  14557  swrdsbslen  14564  swrdspsleq  14565  pfxccat3  14634  swrdccat  14635  repswswrd  14684  resqrex  15147  sqrtgt0  15155  absmax  15226  eqsqrt2d  15265  rlim2lt  15391  mulcn2  15490  rlimo1  15511  o1rlimmul  15513  climbdd  15568  caucvgrlem  15569  supcvg  15752  efcllem  15971  sin01bnd  16078  cos01bnd  16079  sin01gt0  16083  cos01gt0  16084  absef  16090  efieq1re  16092  ruclem11  16133  nn0o  16276  pythagtriplem12  16709  pythagtriplem13  16710  pythagtriplem14  16711  pythagtriplem16  16713  pclem  16721  prmgaplem4  16937  cshwshashlem2  16980  isabvd  20335  met2ndci  23915  blcvx  24198  iocopnst  24340  nmoleub2a  24517  nmoleub2b  24518  nmhmcn  24520  iscmet3lem2  24693  caubl  24709  ivthlem2  24853  ovolicc2lem4  24921  ioombl1lem4  24962  ioovolcl  24971  volsup2  25006  itg2monolem1  25152  itg2gt0  25162  itg2cnlem1  25163  dvne0  25412  ftc1lem4  25440  dgrlt  25664  aalioulem5  25733  ulmbdd  25794  iblulm  25803  radcnvlem1  25809  abelthlem5  25831  abelthlem7  25834  sincosq1lem  25891  tangtx  25899  tanabsge  25900  sinq12ge0  25902  sineq0  25917  tanord  25931  logcj  25998  argregt0  26002  argrege0  26003  argimgt0  26004  logdmnrp  26033  logcnlem3  26036  logf1o2  26042  cxpsqrtlem  26094  abscxpbnd  26143  logreclem  26149  asinneg  26273  atanlogsublem  26302  atanlogsub  26303  rlimcnp  26352  xrlimcnp  26355  basellem8  26474  chtub  26597  bposlem9  26677  chebbnd1  26857  chtppilimlem1  26858  dchrvmasumiflem1  26886  mulog2sumlem2  26920  pntrmax  26949  pntibndlem2  26976  pntibndlem3  26977  pntlemf  26990  axlowdimlem16  27969  pthdlem1  28777  crctcshwlkn0lem3  28820  crctcshwlkn0lem5  28822  crctcshwlkn0lem7  28824  crctcshwlkn0  28829  nmblolbii  29804  ubthlem1  29875  bcsiALT  30184  nmbdoplbi  31029  nmcexi  31031  nmcoplbi  31033  lnconi  31038  nmbdfnlbi  31054  nmcfnlbi  31057  nmopcoi  31100  branmfn  31110  leopmul  31139  nmopleid  31144  esumcvg  32774  ballotlemfrceq  33217  sinccvglem  34347  opnrebl2  34869  ivthALT  34883  dnibndlem12  35028  poimirlem15  36166  poimirlem31  36182  ftc1cnnclem  36222  ftc1anclem5  36228  incsequz2  36281  nnubfi  36282  bfplem2  36355  60gcd7e1  40535  lcmineqlem10  40568  factwoffsmonot  40688  3cubeslem1  41065  pell14qrgap  41256  pellfundre  41262  pellfundlb  41265  reabsifneg  42026  reabsifnpos  42027  reabsifpos  42028  reabsifnneg  42029  stoweidlem17  44378  stoweidlem34  44395  wallispilem1  44426  sqrtnegnre  45659  2elfz2melfz  45670  elfzelfzlble  45673  subsubelfzo0  45678  requad01  45933  requad2  45935  bgoldbtbnd  46121  bgoldbachlt  46125  tgblthelfgott  46127  m1modmmod  46727  nnolog2flm1  46796  itsclc0yqsol  46970