Theorem ltle 11201

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111   class class class wbr 5091  ℝcr 11005   < clt 11146   ≤ cle 11147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152

This theorem is referenced by:  leltletr  11204  ltleletr  11206  letr  11207  letric  11213  ltlen  11214  ltlei  11235  ltled  11261  lt2add  11602  lep1  11962  lem1  11964  letrp1  11965  ltmul12a  11977  mulge0b  11992  lediv12a  12015  bndndx  12380  ltsubnn0  12432  uzind  12565  fnn0ind  12572  eluz2b2  12819  zmin  12842  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  rpge0  12904  rpneg  12924  iccsplit  13385  zltaddlt1le  13405  difelfznle  13542  fvffz0  13546  elfzouz2  13574  elfzo0le  13603  fzostep1  13686  fllep1  13705  fracle1  13707  expgt1  14007  expnbnd  14139  expnlbnd2  14141  faclbnd  14197  swrdnd0  14565  swrdsbslen  14572  swrdspsleq  14573  pfxccat3  14641  swrdccat  14642  repswswrd  14691  resqrex  15157  sqrtgt0  15165  absmax  15237  eqsqrt2d  15276  rlim2lt  15404  mulcn2  15503  rlimo1  15524  o1rlimmul  15526  climbdd  15579  caucvgrlem  15580  supcvg  15763  efcllem  15984  sin01bnd  16094  cos01bnd  16095  sin01gt0  16099  cos01gt0  16100  absef  16106  efieq1re  16108  ruclem11  16149  nn0o  16294  pythagtriplem12  16738  pythagtriplem13  16739  pythagtriplem14  16740  pythagtriplem16  16742  pclem  16750  prmgaplem4  16966  cshwshashlem2  17008  isabvd  20728  met2ndci  24438  blcvx  24714  iocopnst  24865  nmoleub2a  25045  nmoleub2b  25046  nmhmcn  25048  iscmet3lem2  25220  caubl  25236  ivthlem2  25381  ovolicc2lem4  25449  ioombl1lem4  25490  ioovolcl  25499  volsup2  25534  itg2monolem1  25679  itg2gt0  25689  itg2cnlem1  25690  dvne0  25944  ftc1lem4  25974  dgrlt  26200  aalioulem5  26272  ulmbdd  26335  iblulm  26344  radcnvlem1  26350  abelthlem5  26373  abelthlem7  26376  sincosq1lem  26434  tangtx  26442  tanabsge  26443  sinq12ge0  26445  sineq0  26461  tanord  26475  logcj  26543  argregt0  26547  argrege0  26548  argimgt0  26549  logdmnrp  26578  logcnlem3  26581  logf1o2  26587  cxpsqrtlem  26639  abscxpbnd  26691  logreclem  26700  asinneg  26824  atanlogsublem  26853  atanlogsub  26854  rlimcnp  26903  xrlimcnp  26906  basellem8  27026  chtub  27151  bposlem9  27231  chebbnd1  27411  chtppilimlem1  27412  dchrvmasumiflem1  27440  mulog2sumlem2  27474  pntrmax  27503  pntibndlem2  27530  pntibndlem3  27531  pntlemf  27544  axlowdimlem16  28936  pthdlem1  29745  crctcshwlkn0lem3  29791  crctcshwlkn0lem5  29793  crctcshwlkn0lem7  29795  crctcshwlkn0  29800  nmblolbii  30777  ubthlem1  30848  bcsiALT  31157  nmbdoplbi  32002  nmcexi  32004  nmcoplbi  32006  lnconi  32011  nmbdfnlbi  32027  nmcfnlbi  32030  nmopcoi  32073  branmfn  32083  leopmul  32112  nmopleid  32117  esumcvg  34097  ballotlemfrceq  34540  sinccvglem  35714  opnrebl2  36361  ivthALT  36375  dnibndlem12  36529  poimirlem15  37681  poimirlem31  37697  ftc1cnnclem  37737  ftc1anclem5  37743  incsequz2  37795  nnubfi  37796  bfplem2  37869  60gcd7e1  42044  lcmineqlem10  42077  3cubeslem1  42723  pell14qrgap  42914  pellfundre  42920  pellfundlb  42923  reabsifneg  43671  reabsifnpos  43672  reabsifpos  43673  reabsifnneg  43674  stoweidlem17  46061  stoweidlem34  46078  wallispilem1  46109  sqrtnegnre  47344  2elfz2melfz  47355  elfzelfzlble  47358  subsubelfzo0  47363  m1modmmod  47395  requad01  47658  requad2  47660  bgoldbtbnd  47846  bgoldbachlt  47850  tgblthelfgott  47852  nnolog2flm1  48628  itsclc0yqsol  48802