Theorem ltnle 6680

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

Assertion

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

Proof of Theorem ltnle

Step	Hyp	Ref	Expression
1		lenlt 6679	. . 3 |- ((B e. RR /\ A e. RR) -> (B <_ A <-> -. A < B))
2	1	ancoms 484	. 2 |- ((A e. RR /\ B e. RR) -> (B <_ A <-> -. A < B))
3	2	con2bid 585	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   < clt 6653

This theorem is referenced by:  letric 6802  letricOLD 6803  leaddsub 6816  lt1nnn 7130  avgle 7231  nn0ltp1le 7336  znnnlt1 7365  zltp1le 7390  uzwo4OLD 7422  qsqueeze 7461  icounlem 7581  uzwo 7624  uzwoOLD 7625  fzneuz 7697  cardfz 7719  absmax 8149  facdiv 8194  bcval4 8213  bccl2 8223  znnenlem 8770  znnen 8771  cdrci 10182  alzdvds 13695  divalglem5 13700  divalglem6 13701  algcvgblem 13745  reconnlem4 15449  fsumlt1 15831  oprpiece1res2 15881  piececn 15894  txmet 15925  phtpycolem2 16052  pcoval2 16075  pcohtpylem2 16081  pcopt 16084  pcoass 16085  pcorevlem 16086

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