Theorem lenlt 8032

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 8002	. 2 |- ( A e. RR -> A e. RR* )
2		rexr 8002	. 2 |- ( B e. RR -> B e. RR* )
3		xrlenlt 8021	. 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 2148   class class class wbr 4003   RRcr 7809   RR*cxr 7990   < clt 7991   <_ cle 7992

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-xr 7995  df-le 7997

This theorem is referenced by:  letri3  8037  ltleletr  8038  letr  8039  leid  8040  eqlelt  8043  ltle  8044  lelttr  8045  ltletr  8046  lenlti  8057  lenltd  8074  lemul1  8549  msqge0  8572  mulge0  8575  ltleap  8588  recgt0  8806  lediv1  8825  dfinfre  8912  nnge1  8941  nnnlt1  8944  avgle1  9158  avgle2  9159  nn0nlt0  9201  zltnle  9298  zleloe  9299  zdcle  9328  recnz  9345  btwnnz  9346  prime  9351  fznlem  10040  fzonlt0  10166  qltnle  10245  bcval4  10731  resqrexlemgt0  11028  climge0  11332  infpnlem1  12356  efle  14167  logleb  14266  cxple  14307  cxple3  14311  lgsval2lem  14381  lgsneg  14395  lgsdilem  14398  supfz  14788  inffz  14789