Theorem nltled 11348

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2145   class class class wbr 5104  ℝcr 11087   < clt 11231   ≤ cle 11232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5657  df-cnv 5659  df-xr 11235  df-le 11237

This theorem is referenced by:  dedekind  11361  suprub  12164  infrelb  12188  suprzub  12951  prodge0rd  13113  seqf1olem1  14065  bitsfzolem  16480  bitsmod  16482  reconnlem2  24942  ioombl1lem4  25677  dgrub  26348  dgrlb  26350  suppssnn0  33058  constrsqrtcl  34081  1smat1  34106  sn-suprubd  43123  imo72b2  44755  dvbdfbdioolem2  46502  stoweidlem14  46587  fourierdlem10  46690  fourierdlem12  46692  fourierdlem20  46700  fourierdlem24  46704  fourierdlem50  46729  fourierdlem54  46733  fourierdlem63  46742  fourierdlem65  46744  fourierdlem75  46754  fourierdlem79  46758  fouriersw  46804  etransclem3  46810  etransclem7  46814  etransclem10  46817  etransclem15  46822  etransclem20  46827  etransclem21  46828  etransclem22  46829  etransclem24  46831  etransclem25  46832  etransclem27  46834  etransclem32  46839