Theorem lenlt 8095

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 8065	. 2 |- ( A e. RR -> A e. RR* )
2		rexr 8065	. 2 |- ( B e. RR -> B e. RR* )
3		xrlenlt 8084	. 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 2164   class class class wbr 4029   RRcr 7871   RR*cxr 8053   < clt 8054   <_ cle 8055

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030  df-opab 4091  df-xp 4665  df-cnv 4667  df-xr 8058  df-le 8060

This theorem is referenced by:  letri3  8100  ltleletr  8101  letr  8102  leid  8103  eqlelt  8106  ltle  8107  lelttr  8108  ltletr  8109  lenlti  8120  lenltd  8137  lemul1  8612  msqge0  8635  mulge0  8638  ltleap  8651  recgt0  8869  lediv1  8888  dfinfre  8975  nnge1  9005  nnnlt1  9008  avgle1  9223  avgle2  9224  nn0nlt0  9266  zltnle  9363  zleloe  9364  zdcle  9393  recnz  9410  btwnnz  9411  prime  9416  fznlem  10107  nelfzo  10218  fzonlt0  10234  qltnle  10313  bcval4  10823  resqrexlemgt0  11164  climge0  11468  infpnlem1  12497  efle  14911  logleb  15010  cxple  15051  cxple3  15055  lgsval2lem  15126  lgsneg  15140  lgsdilem  15143  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  supfz  15561  inffz  15562