Theorem lenlt 8150

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 8120	. 2 |- ( A e. RR -> A e. RR* )
2		rexr 8120	. 2 |- ( B e. RR -> B e. RR* )
3		xrlenlt 8139	. 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 2176   class class class wbr 4045   RRcr 7926   RR*cxr 8108   < clt 8109   <_ cle 8110

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046  df-opab 4107  df-xp 4682  df-cnv 4684  df-xr 8113  df-le 8115

This theorem is referenced by:  letri3  8155  ltleletr  8156  letr  8157  leid  8158  eqlelt  8161  ltle  8162  lelttr  8163  ltletr  8164  lenlti  8175  lenltd  8192  lemul1  8668  msqge0  8691  mulge0  8694  ltleap  8707  recgt0  8925  lediv1  8944  dfinfre  9031  nnge1  9061  nnnlt1  9064  avgle1  9280  avgle2  9281  nn0nlt0  9323  zltnle  9420  zleloe  9421  zdcle  9451  recnz  9468  btwnnz  9469  prime  9474  fznlem  10165  nelfzo  10276  fzonlt0  10293  qltnle  10388  bcval4  10899  ccatsymb  11061  swrd0g  11116  resqrexlemgt0  11364  climge0  11669  infpnlem1  12715  efle  15281  logleb  15380  cxple  15422  cxple3  15426  lgsval2lem  15520  lgsneg  15534  lgsdilem  15537  gausslemma2dlem1a  15568  gausslemma2dlem3  15573  supfz  16047  inffz  16048