Theorem lenlt 8255

Description: 'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.)

Assertion

Ref	Expression
lenlt	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )

Proof of Theorem lenlt

Step	Hyp	Ref	Expression
1		rexr 8225	. 2 |- ( A e. RR -> A e. RR* )
2		rexr 8225	. 2 |- ( B e. RR -> B e. RR* )
3		xrlenlt 8244	. 2 |- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
4	1, 2, 3	syl2an 289	1 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2202   class class class wbr 4088   RRcr 8031   RR*cxr 8213   < clt 8214   <_ cle 8215

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 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-xp 4731  df-cnv 4733  df-xr 8218  df-le 8220

This theorem is referenced by:  letri3  8260  ltleletr  8261  letr  8262  leid  8263  eqlelt  8266  ltle  8267  lelttr  8268  ltletr  8269  lenlti  8280  lenltd  8297  lemul1  8773  msqge0  8796  mulge0  8799  ltleap  8812  recgt0  9030  lediv1  9049  dfinfre  9136  nnge1  9166  nnnlt1  9169  avgle1  9385  avgle2  9386  nn0nlt0  9428  zltnle  9525  zleloe  9526  zdcle  9556  recnz  9573  btwnnz  9574  prime  9579  fznlem  10276  nelfzo  10387  fzonlt0  10404  qltnle  10504  bcval4  11015  ccatsymb  11183  swrd0g  11245  resqrexlemgt0  11585  climge0  11890  infpnlem1  12937  efle  15506  logleb  15605  cxple  15647  cxple3  15651  lgsval2lem  15745  lgsneg  15759  lgsdilem  15762  gausslemma2dlem1a  15793  gausslemma2dlem3  15798  supfz  16701  inffz  16702