Theorem lenltd 7873

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 7833	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
4	1, 2, 3	syl2anc 408	1 |- ( ph -> ( A <_ B <-> -. B < A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   e. wcel 1480   class class class wbr 3924   RRcr 7612   < clt 7793   <_ cle 7794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-rex 2420  df-v 2683  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925  df-opab 3985  df-xp 4540  df-cnv 4542  df-xr 7797  df-le 7799

This theorem is referenced by:  ltnsymd  7875  nltled  7876  lensymd  7877  leadd1  8185  lemul1  8348  leltap  8380  ap0gt0  8395  prodgt0  8603  prodge0  8605  lediv1  8620  lemuldiv  8632  lerec  8635  lt2msq  8637  le2msq  8652  squeeze0  8655  suprleubex  8705  0mnnnnn0  9002  elnn0z  9060  uzm1  9349  fztri3or  9812  fzdisj  9825  uzdisj  9866  nn0disj  9908  fzouzdisj  9950  elfzonelfzo  10000  flqeqceilz  10084  modifeq2int  10152  modsumfzodifsn  10162  expcanlem  10455  fimaxq  10566  resqrexlemoverl  10786  leabs  10839  absle  10854  maxleast  10978  minmax  10994  climge0  11087  efler  11394