Theorem xrltle 11858

Description: 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)

Assertion

Ref	Expression
xrltle	⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Proof of Theorem xrltle

Step	Hyp	Ref	Expression
1		orc 399	. 2 ⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
2		xrleloe 11853	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	syl5ibr 235	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  xrletri  11860  xrletr  11865  qextltlem  11907  xmulge0  11986  supxrunb1  12021  ico0  12092  ioc0  12093  ioossicc  12130  icossicc  12131  iocssicc  12132  ioossico  12133  snunioo  12169  snunico  12170  snunioc  12171  ioopnfsup  12525  icopnfsup  12526  hashnnn0genn0  12993  pcadd2  15432  leordtval2  20826  lecldbas  20833  xblss2ps  22016  xblss2  22017  blhalf  22020  blssps  22039  blss  22040  blcls  22121  stdbdxmet  22130  stdbdmopn  22133  metcnpi3  22161  blcvx  22409  tgqioo  22411  xrsmopn  22423  metdcnlem  22447  metnrmlem1a  22469  bndth  22565  ovolgelb  23055  icombl  23139  ioorcl2  23146  ioorf  23147  ioorinv2  23149  volivth  23181  itg2seq  23315  itg2monolem2  23324  itg2cnlem2  23335  dvferm1lem  23551  dvferm2lem  23553  dvferm  23555  dvivthlem1  23575  lhop2  23582  radcnvle  23978  tanord1  24087  dvloglem  24194  iocinif  28933  difioo  28934  esumpinfsum  29466  omssubadd  29689  elicc3  31481  tan2h  32571  heicant  32614  itg2addnclem  32631  ftc1anclem7  32661  ioounsn  36814  radcnvrat  37535  xrltled  38427  ioossioc  38560  ioossioobi  38590  fouriersw  39124  iccpartleu  39966  iccpartgel  39967  iccpartnel  39976