Theorem ltle 11378

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324   ≤ cle 11325

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 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttri 11258

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330

This theorem is referenced by:  leltletr  11381  ltleletr  11383  letr  11384  letric  11390  ltlen  11391  ltlei  11412  ltled  11438  lt2add  11775  lep1  12135  lem1  12137  letrp1  12138  ltmul12a  12150  mulge0b  12165  lediv12a  12188  bndndx  12552  ltsubnn0  12604  uzind  12735  fnn0ind  12742  eluz2b2  12986  zmin  13009  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  rpge0  13070  rpneg  13089  iccsplit  13545  zltaddlt1le  13565  difelfznle  13699  fvffz0  13703  elfzouz2  13731  elfzo0le  13760  fzostep1  13833  fllep1  13852  fracle1  13854  expgt1  14151  expnbnd  14281  expnlbnd2  14283  faclbnd  14339  swrdnd0  14705  swrdsbslen  14712  swrdspsleq  14713  pfxccat3  14782  swrdccat  14783  repswswrd  14832  resqrex  15299  sqrtgt0  15307  absmax  15378  eqsqrt2d  15417  rlim2lt  15543  mulcn2  15642  rlimo1  15663  o1rlimmul  15665  climbdd  15720  caucvgrlem  15721  supcvg  15904  efcllem  16125  sin01bnd  16233  cos01bnd  16234  sin01gt0  16238  cos01gt0  16239  absef  16245  efieq1re  16247  ruclem11  16288  nn0o  16431  pythagtriplem12  16873  pythagtriplem13  16874  pythagtriplem14  16875  pythagtriplem16  16877  pclem  16885  prmgaplem4  17101  cshwshashlem2  17144  isabvd  20835  met2ndci  24556  blcvx  24839  iocopnst  24989  nmoleub2a  25169  nmoleub2b  25170  nmhmcn  25172  iscmet3lem2  25345  caubl  25361  ivthlem2  25506  ovolicc2lem4  25574  ioombl1lem4  25615  ioovolcl  25624  volsup2  25659  itg2monolem1  25805  itg2gt0  25815  itg2cnlem1  25816  dvne0  26070  ftc1lem4  26100  dgrlt  26326  aalioulem5  26396  ulmbdd  26459  iblulm  26468  radcnvlem1  26474  abelthlem5  26497  abelthlem7  26500  sincosq1lem  26557  tangtx  26565  tanabsge  26566  sinq12ge0  26568  sineq0  26584  tanord  26598  logcj  26666  argregt0  26670  argrege0  26671  argimgt0  26672  logdmnrp  26701  logcnlem3  26704  logf1o2  26710  cxpsqrtlem  26762  abscxpbnd  26814  logreclem  26823  asinneg  26947  atanlogsublem  26976  atanlogsub  26977  rlimcnp  27026  xrlimcnp  27029  basellem8  27149  chtub  27274  bposlem9  27354  chebbnd1  27534  chtppilimlem1  27535  dchrvmasumiflem1  27563  mulog2sumlem2  27597  pntrmax  27626  pntibndlem2  27653  pntibndlem3  27654  pntlemf  27667  axlowdimlem16  28990  pthdlem1  29802  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  crctcshwlkn0lem7  29849  crctcshwlkn0  29854  nmblolbii  30831  ubthlem1  30902  bcsiALT  31211  nmbdoplbi  32056  nmcexi  32058  nmcoplbi  32060  lnconi  32065  nmbdfnlbi  32081  nmcfnlbi  32084  nmopcoi  32127  branmfn  32137  leopmul  32166  nmopleid  32171  esumcvg  34050  ballotlemfrceq  34493  sinccvglem  35640  opnrebl2  36287  ivthALT  36301  dnibndlem12  36455  poimirlem15  37595  poimirlem31  37611  ftc1cnnclem  37651  ftc1anclem5  37657  incsequz2  37709  nnubfi  37710  bfplem2  37783  60gcd7e1  41962  lcmineqlem10  41995  factwoffsmonot  42199  3cubeslem1  42640  pell14qrgap  42831  pellfundre  42837  pellfundlb  42840  reabsifneg  43594  reabsifnpos  43595  reabsifpos  43596  reabsifnneg  43597  stoweidlem17  45938  stoweidlem34  45955  wallispilem1  45986  sqrtnegnre  47222  2elfz2melfz  47233  elfzelfzlble  47236  subsubelfzo0  47241  requad01  47495  requad2  47497  bgoldbtbnd  47683  bgoldbachlt  47687  tgblthelfgott  47689  m1modmmod  48255  nnolog2flm1  48324  itsclc0yqsol  48498