Theorem lenltd 8299

Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

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

Proof of Theorem lenltd

Step	Hyp	Ref	Expression
1		ltd.1	. 2 |- ( ph -> A e. RR )
2		ltd.2	. 2 |- ( ph -> B e. RR )
3		lenlt 8257	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A <_ B <-> -. B < A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   e. wcel 2201   class class class wbr 4087   RRcr 8033   < clt 8216   <_ cle 8217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4206  ax-pow 4263  ax-pr 4298

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3653  df-sn 3674  df-pr 3675  df-op 3677  df-br 4088  df-opab 4150  df-xp 4730  df-cnv 4732  df-xr 8220  df-le 8222

This theorem is referenced by:  ltnsymd  8301  nltled  8302  lensymd  8303  leadd1  8612  lemul1  8775  leltap  8807  ap0gt0  8822  prodgt0  9034  prodge0  9036  lediv1  9051  lemuldiv  9063  lerec  9066  lt2msq  9068  le2msq  9083  squeeze0  9086  suprleubex  9136  0mnnnnn0  9436  elnn0z  9494  uzm1  9789  infregelbex  9834  fztri3or  10276  fzdisj  10289  uzdisj  10330  nn0disj  10375  fzouzdisj  10419  elfzonelfzo  10478  qdcle  10509  flqeqceilz  10583  modifeq2int  10651  modsumfzodifsn  10661  nn0leexp2  10975  expcanlem  10980  fimaxq  11094  swrdccatin2  11316  resqrexlemoverl  11601  leabs  11654  absle  11669  maxleast  11793  minmax  11810  climge0  11905  pcfac  12943  gsumfzz  13598  cxple  15667  gausslemma2dlem1a  15813