Theorem lenlt 6679

Description: 'Less than or equal to' expressed in terms of 'less than'.

Assertion

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

Proof of Theorem lenlt

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

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   e. wcel 1300   class class class wbr 3338  RRcr 6385   <_ cle 6448  RR*cxr 6652   < clt 6653

This theorem is referenced by:  ltnle 6680  letri3 6687  leloe 6688  eqlelt 6689  pm2.61ltlei 6705  lenlti 6753  ne0gt0 6801  lelttric 6805  ltaddsub 6814  lediv1 7033  lediv1OLD 7034  lemuldiv 7058  nnge1 7126  nnleltp1 7138  rpneg 7252  lbinfm 7257  suprub 7265  suprleub 7268  dfinfmr 7276  supxrre 7292  nn0ge0 7326  elnnz1 7364  zltp1le 7390  recnz 7403  btwnnz 7404  prime 7407  zbtwnre 7434  fllt 7473  flval3 7479  ioojoin 7585  indstr 7630  fzn 7663  om2uzlt2i 7710  sqr0 7922  climrecl 8370  climge0 8372  climubii 8413  caucvglem6 8422  ivthlem6 8548  ivthlem7 8549  infpnlem1 8775  metxpfval 9108  metxp 9111  bl2in 9120  lmle 9238  bcthlem18 9294  nmounbi 9778  nmlno0lem 9793  projlem13 10831  nmlnop0iALT 11557  dvdsle 13693  divalglem6 13701  infmrlb 15765  infmrgelb 15766  fzdisj 15793  nninfnub 15819  recms 16010  strdif 16719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-xr 6656  df-le 6658

Copyright terms: Public domain