ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lenlt Unicode version

Theorem lenlt 7968
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
StepHypRef Expression
1 rexr 7938 . 2  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 7938 . 2  |-  ( B  e.  RR  ->  B  e.  RR* )
3 xrlenlt 7957 . 2  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  <->  -.  B  <  A ) )
41, 2, 3syl2an 287 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  -.  B  <  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    e. wcel 2135   class class class wbr 3979   RRcr 7746   RR*cxr 7926    < clt 7927    <_ cle 7928
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 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4097  ax-pow 4150  ax-pr 4184
This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2726  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-br 3980  df-opab 4041  df-xp 4607  df-cnv 4609  df-xr 7931  df-le 7933
This theorem is referenced by:  letri3  7973  ltleletr  7974  letr  7975  leid  7976  eqlelt  7979  ltle  7980  lelttr  7981  ltletr  7982  lenlti  7993  lenltd  8010  lemul1  8485  msqge0  8508  mulge0  8511  ltleap  8524  recgt0  8739  lediv1  8758  dfinfre  8845  nnge1  8874  nnnlt1  8877  avgle1  9091  avgle2  9092  nn0nlt0  9134  zltnle  9231  zleloe  9232  zdcle  9261  recnz  9278  btwnnz  9279  prime  9284  fznlem  9970  fzonlt0  10096  qltnle  10175  bcval4  10659  resqrexlemgt0  10956  climge0  11260  infpnlem1  12283  efle  13295  logleb  13394  cxple  13435  cxple3  13439  supfz  13840  inffz  13841
  Copyright terms: Public domain W3C validator