Theorem nltled 11370

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2104   class class class wbr 5149  ℝcr 11113   < clt 11254   ≤ cle 11255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-xr 11258  df-le 11260

This theorem is referenced by:  dedekind  11383  suprub  12181  infrelb  12205  suprzub  12929  prodge0rd  13087  seqf1olem1  14013  bitsfzolem  16381  bitsmod  16383  reconnlem2  24565  ioombl1lem4  25312  dgrub  25982  dgrlb  25984  suppssnn0  32282  1smat1  33080  metakunt28  41320  metakunt30  41322  imo72b2  43228  dvbdfbdioolem2  44945  stoweidlem14  45030  fourierdlem10  45133  fourierdlem12  45135  fourierdlem20  45143  fourierdlem24  45147  fourierdlem50  45172  fourierdlem54  45176  fourierdlem63  45185  fourierdlem65  45187  fourierdlem75  45197  fourierdlem79  45201  fouriersw  45247  etransclem3  45253  etransclem7  45257  etransclem10  45260  etransclem15  45265  etransclem20  45270  etransclem21  45271  etransclem22  45272  etransclem24  45274  etransclem25  45275  etransclem27  45277  etransclem32  45282