Theorem lenlt 5559

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

Hypotheses

Ref	Expression
lt.1	|- A e. RR
lt.2	|- B e. RR

Assertion

Ref	Expression
lenlt	|- (A <_ B <-> -. B < A)

Proof of Theorem lenlt

Step	Hyp	Ref	Expression
1		lt.1	. 2 |- A e. RR
2		lt.2	. 2 |- B e. RR
3		lenltt 5490	. 2 |- ((A e. RR /\ B e. RR) -> (A <_ B <-> -. B < A))
4	1, 2, 3	mp2an 696	1 |- (A <_ B <-> -. B < A)

Syntax hints:  -. wn 2   <-> wb 146   e. wcel 956   class class class wbr 2614  RRcr 5213   <_ cle 5275   < clt 5466

This theorem is referenced by:  ltnle 5560  ltadd2 5572  leadd1 5574  prodge0 5784  ltmul1i 5785  lt2msq 5837  le2msq 5838  nnsub 5911  elnnz1 6110  discrlem3 6596  sqrlem8 6618  climubi 7097  efltb 7356  ruclem35 7495  cosh111lem2 8649  projlem13 9137

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-xr 5469  df-le 5471

Copyright terms: Public domain