Theorem ltle 11091

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1537   ∈ wcel 2101   class class class wbr 5077  ℝcr 10898   < clt 11037   ≤ cle 11038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7608  ax-resscn 10956  ax-pre-lttri 10973

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-br 5078  df-opab 5140  df-mpt 5161  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-er 8518  df-en 8754  df-dom 8755  df-sdom 8756  df-pnf 11039  df-mnf 11040  df-xr 11041  df-ltxr 11042  df-le 11043

This theorem is referenced by:  leltletr  11094  ltleletr  11096  letr  11097  letric  11103  ltlen  11104  ltlei  11125  ltled  11151  lt2add  11488  lep1  11844  lem1  11846  letrp1  11847  ltmul12a  11859  mulge0b  11873  lediv12a  11896  bndndx  12260  ltsubnn0  12312  uzind  12440  fnn0ind  12447  eluz2b2  12689  zmin  12712  rpnnen1lem2  12745  rpnnen1lem1  12746  rpnnen1lem3  12747  rpnnen1lem5  12749  rpge0  12771  rpneg  12790  iccsplit  13245  zltaddlt1le  13265  difelfznle  13398  fvffz0  13402  elfzouz2  13430  elfzo0le  13459  fzostep1  13531  fllep1  13549  fracle1  13551  expgt1  13849  expnbnd  13975  expnlbnd2  13977  faclbnd  14032  swrdnd0  14398  swrdsbslen  14405  swrdspsleq  14406  pfxccat3  14475  swrdccat  14476  repswswrd  14525  resqrex  14990  sqrtgt0  14998  absmax  15069  eqsqrt2d  15108  rlim2lt  15234  mulcn2  15333  rlimo1  15354  o1rlimmul  15356  climbdd  15411  caucvgrlem  15412  supcvg  15596  efcllem  15815  sin01bnd  15922  cos01bnd  15923  sin01gt0  15927  cos01gt0  15928  absef  15934  efieq1re  15936  ruclem11  15977  nn0o  16120  pythagtriplem12  16555  pythagtriplem13  16556  pythagtriplem14  16557  pythagtriplem16  16559  pclem  16567  prmgaplem4  16783  cshwshashlem2  16826  isabvd  20108  met2ndci  23706  blcvx  23989  iocopnst  24131  nmoleub2a  24308  nmoleub2b  24309  nmhmcn  24311  iscmet3lem2  24484  caubl  24500  ivthlem2  24644  ovolicc2lem4  24712  ioombl1lem4  24753  ioovolcl  24762  volsup2  24797  itg2monolem1  24943  itg2gt0  24953  itg2cnlem1  24954  dvne0  25203  ftc1lem4  25231  dgrlt  25455  aalioulem5  25524  ulmbdd  25585  iblulm  25594  radcnvlem1  25600  abelthlem5  25622  abelthlem7  25625  sincosq1lem  25682  tangtx  25690  tanabsge  25691  sinq12ge0  25693  sineq0  25708  tanord  25722  logcj  25789  argregt0  25793  argrege0  25794  argimgt0  25795  logdmnrp  25824  logcnlem3  25827  logf1o2  25833  cxpsqrtlem  25885  abscxpbnd  25934  logreclem  25940  asinneg  26064  atanlogsublem  26093  atanlogsub  26094  rlimcnp  26143  xrlimcnp  26146  basellem8  26265  chtub  26388  bposlem9  26468  chebbnd1  26648  chtppilimlem1  26649  dchrvmasumiflem1  26677  mulog2sumlem2  26711  pntrmax  26740  pntibndlem2  26767  pntibndlem3  26768  pntlemf  26781  axlowdimlem16  27353  pthdlem1  28162  crctcshwlkn0lem3  28205  crctcshwlkn0lem5  28207  crctcshwlkn0lem7  28209  crctcshwlkn0  28214  nmblolbii  29189  ubthlem1  29260  bcsiALT  29569  nmbdoplbi  30414  nmcexi  30416  nmcoplbi  30418  lnconi  30423  nmbdfnlbi  30439  nmcfnlbi  30442  nmopcoi  30485  branmfn  30495  leopmul  30524  nmopleid  30529  esumcvg  32082  ballotlemfrceq  32523  sinccvglem  33658  opnrebl2  34538  ivthALT  34552  dnibndlem12  34697  poimirlem15  35820  poimirlem31  35836  ftc1cnnclem  35876  ftc1anclem5  35882  incsequz2  35935  nnubfi  35936  bfplem2  36009  60gcd7e1  40039  lcmineqlem10  40072  factwoffsmonot  40189  3cubeslem1  40529  pell14qrgap  40720  pellfundre  40726  pellfundlb  40729  reabsifneg  41264  reabsifnpos  41265  reabsifpos  41266  reabsifnneg  41267  stoweidlem17  43593  stoweidlem34  43610  wallispilem1  43641  sqrtnegnre  44839  2elfz2melfz  44850  elfzelfzlble  44853  subsubelfzo0  44858  requad01  45113  requad2  45115  bgoldbtbnd  45301  bgoldbachlt  45305  tgblthelfgott  45307  m1modmmod  45907  nnolog2flm1  45976  itsclc0yqsol  46150