Theorem nltled 10880

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 10876	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
5	1, 4	mpbird 260	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   class class class wbr 5040  ℝcr 10626   < clt 10765   ≤ cle 10766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-br 5041  df-opab 5103  df-xp 5541  df-cnv 5543  df-xr 10769  df-le 10771

This theorem is referenced by:  dedekind  10893  suprub  11691  infrelb  11715  suprzub  12433  prodge0rd  12591  seqf1olem1  13513  bitsfzolem  15889  bitsmod  15891  reconnlem2  23591  ioombl1lem4  24325  dgrub  24995  dgrlb  24997  1smat1  31338  metakunt28  39783  metakunt30  39785  imo72b2  41370  dvbdfbdioolem2  43052  stoweidlem14  43137  fourierdlem10  43240  fourierdlem12  43242  fourierdlem20  43250  fourierdlem24  43254  fourierdlem50  43279  fourierdlem54  43283  fourierdlem63  43292  fourierdlem65  43294  fourierdlem75  43304  fourierdlem79  43308  fouriersw  43354  etransclem3  43360  etransclem7  43364  etransclem10  43367  etransclem15  43372  etransclem20  43377  etransclem21  43378  etransclem22  43379  etransclem24  43381  etransclem25  43382  etransclem27  43384  etransclem32  43389