Theorem xrltled 13205

Description: 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 13204. (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 13204	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5	2, 3, 4	syl2anc 596	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
6	1, 5	mpd 16	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  ℝ^*cxr 11270   < clt 11271   ≤ cle 11272

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277

This theorem is used by:  qextltlem  13258  ioounsn  13534  snunioc  13537  pcadd2  16988  xblss2ps  24633  xblss2  24634  blhalf  24637  blssps  24656  blss  24657  blcvx  25030  tgqioo  25032  metdcnlem  25069  ioorcl2  25806  volivth  25841  itg2monolem2  25985  itg2cnlem2  25996  dvferm1lem  26218  dvferm2lem  26220  dvferm  26222  dvivthlem1  26242  lhop2  26249  radcnvle  26663  difioo  33261  heicant  38412  ftc1anclem7  38456  supxrgere  46171  suplesup  46177  infrpge  46189  xralrple2  46192  xrralrecnnle  46220  xrralrecnnge  46227  supxrunb3  46236  unb2ltle  46251  xrpnf  46321  snunioo1  46350  iccdifprioo  46354  iccdificc  46377  lptioo1  46470  limsupub  46540  limsuppnflem  46546  limsupre3lem  46568  xlimmnfvlem1  46668  xlimpnfvlem1  46672  fourierdlem46  46988  fourierdlem74  47016  fourierdlem75  47017  ioorrnopnxrlem  47142  salexct2  47175  sge0iunmptlemre  47251  sge0rpcpnf  47257  sge0xaddlem1  47269  meaiuninc3v  47320  ovnsubaddlem1  47406  hoidmv1le  47430  hoidmvlelem5  47435  ovolval4lem1  47485  ovolval5lem1  47488  preimageiingt  47556  preimaleiinlt  47557  fsupdm  47678  finfdm  47682  iccpartleu  48336  iccpartgel  48337