Theorem nltled 11287

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   < clt 11170   ≤ cle 11171

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-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-xr 11174  df-le 11176

This theorem is referenced by:  dedekind  11300  suprub  12108  infrelb  12132  suprzub  12880  prodge0rd  13042  seqf1olem1  13994  bitsfzolem  16394  bitsmod  16396  reconnlem2  24803  ioombl1lem4  25538  dgrub  26209  dgrlb  26211  suppssnn0  32893  constrsqrtcl  33939  1smat1  33964  sn-suprubd  42953  imo72b2  44617  dvbdfbdioolem2  46375  stoweidlem14  46460  fourierdlem10  46563  fourierdlem12  46565  fourierdlem20  46573  fourierdlem24  46577  fourierdlem50  46602  fourierdlem54  46606  fourierdlem63  46615  fourierdlem65  46617  fourierdlem75  46627  fourierdlem79  46631  fouriersw  46677  etransclem3  46683  etransclem7  46687  etransclem10  46690  etransclem15  46695  etransclem20  46700  etransclem21  46701  etransclem22  46702  etransclem24  46704  etransclem25  46705  etransclem27  46707  etransclem32  46712