Theorem nltled 11361

Description: 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
nltled.1	⊢ (𝜑 → ¬ 𝐵 < 𝐴)

Assertion

Ref	Expression
nltled	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Proof of Theorem nltled

Step	Hyp	Ref	Expression
1		nltled.1	. 2 ⊢ (𝜑 → ¬ 𝐵 < 𝐴)
2		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	2, 3	lenltd 11357	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
5	1, 4	mpbird 260	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143   class class class wbr 5110  ℝcr 11100   < clt 11244   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-xr 11248  df-le 11250

This theorem is referenced by:  dedekind  11374  suprub  12177  infrelb  12201  suprzub  12964  prodge0rd  13126  seqf1olem1  14079  bitsfzolem  16493  bitsmod  16495  reconnlem2  24966  ioombl1lem4  25701  dgrub  26372  dgrlb  26374  suppssnn0  33131  constrsqrtcl  34150  1smat1  34175  sn-suprubd  43249  imo72b2  44881  dvbdfbdioolem2  46626  stoweidlem14  46711  fourierdlem10  46814  fourierdlem12  46816  fourierdlem20  46824  fourierdlem24  46828  fourierdlem50  46853  fourierdlem54  46857  fourierdlem63  46866  fourierdlem65  46868  fourierdlem75  46878  fourierdlem79  46882  fouriersw  46928  etransclem3  46934  etransclem7  46938  etransclem10  46941  etransclem15  46946  etransclem20  46951  etransclem21  46952  etransclem22  46953  etransclem24  46955  etransclem25  46956  etransclem27  46958  etransclem32  46963