Theorem nltled 9810

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

Hypotheses

Ref	Expression
ltd.1	|- ( ph -> A e. RR )
ltd.2	|- ( ph -> B e. RR )
nltled.1	|- ( ph -> -. B < A )

Assertion

Ref	Expression
nltled	|- ( ph -> A <_ B )

Proof of Theorem nltled

Step	Hyp	Ref	Expression
1		nltled.1	. 2 |- ( ph -> -. B < A )
2		ltd.1	. . 3 |- ( ph -> A e. RR )
3		ltd.2	. . 3 |- ( ph -> B e. RR )
4	2, 3	lenltd 9806	. 2 |- ( ph -> ( A <_ B <-> -. B < A ) )
5	1, 4	mpbird 240	1 |- ( ph -> A <_ B )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1897   class class class wbr 4415   RRcr 9563   < clt 9700   <_ cle 9701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-xp 4858  df-cnv 4860  df-xr 9704  df-le 9706

This theorem is referenced by:  infrelb  10623  1smat1  28678  imo72b2  36662  dvbdfbdioolem2  37838  stoweidlem14  37911  fourierdlem10  38016  fourierdlem12  38018  fourierdlem20  38026  fourierdlem24  38030  fourierdlem50  38057  fourierdlem54  38061  fourierdlem63  38070  fourierdlem65  38072  fourierdlem75  38082  fourierdlem79  38086  fouriersw  38132  etransclem3  38139  etransclem7  38143  etransclem10  38146  etransclem15  38151  etransclem20  38156  etransclem21  38157  etransclem22  38158  etransclem24  38160  etransclem25  38161  etransclem27  38163  etransclem32  38168