Theorem xrltled 13101

Description: 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 13100. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
xrltled.a	⊢ (𝜑 → 𝐴 ∈ ℝ*)
xrltled.b	⊢ (𝜑 → 𝐵 ∈ ℝ*)
xrltled.altb	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
xrltled	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Proof of Theorem xrltled

Step	Hyp	Ref	Expression
1		xrltled.altb	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		xrltled.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
3		xrltled.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
4		xrltle 13100	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5	2, 3, 4	syl2anc 585	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
6	1, 5	mpd 15	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185

This theorem is referenced by:  qextltlem  13154  ioounsn  13430  snunioc  13433  pcadd2  16861  xblss2ps  24366  xblss2  24367  blhalf  24370  blssps  24389  blss  24390  blcvx  24763  tgqioo  24765  metdcnlem  24802  ioorcl2  25539  volivth  25574  itg2monolem2  25718  itg2cnlem2  25729  dvferm1lem  25951  dvferm2lem  25953  dvferm  25955  dvivthlem1  25975  lhop2  25982  radcnvle  26385  difioo  32855  heicant  37976  ftc1anclem7  38020  supxrgere  45763  suplesup  45769  infrpge  45781  xralrple2  45784  xrralrecnnle  45812  xrralrecnnge  45819  supxrunb3  45828  unb2ltle  45843  xrpnf  45913  snunioo1  45942  iccdifprioo  45946  iccdificc  45969  lptioo1  46062  limsupub  46132  limsuppnflem  46138  limsupre3lem  46160  xlimmnfvlem1  46260  xlimpnfvlem1  46264  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem74  46608  fourierdlem75  46609  fourierdlem113  46647  ioorrnopnxrlem  46734  salexct2  46767  sge0iunmptlemre  46843  sge0rpcpnf  46849  sge0xaddlem1  46861  meaiuninc3v  46912  ovnsubaddlem1  46998  hoidmv1le  47022  hoidmvlelem5  47027  ovolval4lem1  47077  ovolval5lem1  47080  preimageiingt  47148  preimaleiinlt  47149  fsupdm  47270  finfdm  47274  iccpartleu  47888  iccpartgel  47889