Theorem ltle 11223

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ℝcr 11026   < clt 11168   ≤ cle 11169

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-pre-lttri 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  leltletr  11226  ltleletr  11228  letr  11229  letric  11235  ltlen  11236  ltlei  11257  ltled  11283  lt2add  11624  lep1  11985  lem1  11987  letrp1  11988  ltmul12a  12000  mulge0b  12015  lediv12a  12038  bndndx  12425  ltsubnn0  12477  uzind  12610  fnn0ind  12617  eluz2b2  12860  zmin  12883  rpnnen1lem2  12916  rpnnen1lem1  12917  rpnnen1lem3  12918  rpnnen1lem5  12920  rpge0  12945  rpneg  12965  iccsplit  13427  zltaddlt1le  13447  difelfznle  13585  fvffz0  13589  elfzouz2  13618  elfzo0le  13647  fzostep1  13730  fllep1  13749  fracle1  13751  expgt1  14051  expnbnd  14183  expnlbnd2  14185  faclbnd  14241  swrdnd0  14609  swrdsbslen  14616  swrdspsleq  14617  pfxccat3  14685  swrdccat  14686  repswswrd  14735  resqrex  15201  sqrtgt0  15209  absmax  15281  eqsqrt2d  15320  rlim2lt  15448  mulcn2  15547  rlimo1  15568  o1rlimmul  15570  climbdd  15623  caucvgrlem  15624  supcvg  15810  efcllem  16031  sin01bnd  16141  cos01bnd  16142  sin01gt0  16146  cos01gt0  16147  absef  16153  efieq1re  16155  ruclem11  16196  nn0o  16341  pythagtriplem12  16786  pythagtriplem13  16787  pythagtriplem14  16788  pythagtriplem16  16790  pclem  16798  prmgaplem4  17014  cshwshashlem2  17056  isabvd  20778  met2ndci  24495  blcvx  24771  iocopnst  24915  nmoleub2a  25092  nmoleub2b  25093  nmhmcn  25095  iscmet3lem2  25267  caubl  25283  ivthlem2  25427  ovolicc2lem4  25495  ioombl1lem4  25536  ioovolcl  25545  volsup2  25580  itg2monolem1  25725  itg2gt0  25735  itg2cnlem1  25736  dvne0  25986  ftc1lem4  26014  dgrlt  26239  aalioulem5  26311  ulmbdd  26374  iblulm  26383  radcnvlem1  26389  abelthlem5  26411  abelthlem7  26414  sincosq1lem  26472  tangtx  26480  tanabsge  26481  sinq12ge0  26483  sineq0  26499  tanord  26513  logcj  26581  argregt0  26585  argrege0  26586  argimgt0  26587  logdmnrp  26616  logcnlem3  26619  logf1o2  26625  cxpsqrtlem  26677  abscxpbnd  26728  logreclem  26737  asinneg  26861  atanlogsublem  26890  atanlogsub  26891  rlimcnp  26940  xrlimcnp  26943  basellem8  27063  chtub  27187  bposlem9  27267  chebbnd1  27447  chtppilimlem1  27448  dchrvmasumiflem1  27476  mulog2sumlem2  27510  pntrmax  27539  pntibndlem2  27566  pntibndlem3  27567  pntlemf  27580  axlowdimlem16  29038  pthdlem1  29847  crctcshwlkn0lem3  29893  crctcshwlkn0lem5  29895  crctcshwlkn0lem7  29897  crctcshwlkn0  29902  nmblolbii  30883  ubthlem1  30954  bcsiALT  31263  nmbdoplbi  32108  nmcexi  32110  nmcoplbi  32112  lnconi  32117  nmbdfnlbi  32133  nmcfnlbi  32136  nmopcoi  32179  branmfn  32189  leopmul  32218  nmopleid  32223  esumcvg  34244  ballotlemfrceq  34687  sinccvglem  35868  opnrebl2  36517  ivthALT  36531  dnibndlem12  36755  poimirlem15  37960  poimirlem31  37976  ftc1cnnclem  38016  ftc1anclem5  38022  incsequz2  38074  nnubfi  38075  bfplem2  38148  60gcd7e1  42448  lcmineqlem10  42481  3cubeslem1  43120  pell14qrgap  43311  pellfundre  43317  pellfundlb  43320  reabsifneg  44067  reabsifnpos  44068  reabsifpos  44069  reabsifnneg  44070  stoweidlem17  46453  stoweidlem34  46470  wallispilem1  46501  sqrtnegnre  47757  2elfz2melfz  47768  elfzelfzlble  47771  subsubelfzo0  47777  m1modmmod  47814  requad01  48099  requad2  48101  bgoldbtbnd  48287  bgoldbachlt  48291  tgblthelfgott  48293  nnolog2flm1  49068  itsclc0yqsol  49242