Theorem lenltt 5510

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

Assertion

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

Proof of Theorem lenltt

Step	Hyp	Ref	Expression
1		xrlenltt 5501	. 2 |- ((A e. RR* /\ B e. RR*) -> (A <_ B <-> -. B < A))
2		rexrt 5499	. 2 |- (A e. RR -> A e. RR*)
3		rexrt 5499	. 2 |- (B e. RR -> B e. RR*)
4	1, 2, 3	syl2an 454	1 |- ((A e. RR /\ B e. RR) -> (A <_ B <-> -. B < A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   e. wcel 958   class class class wbr 2619  RRcr 5233   <_ cle 5295  RR*cxr 5485   < clt 5486

This theorem is referenced by:  ltnlet 5511  letri3t 5517  leloet 5518  eqleltt 5519  pm2.61ltle 5534  lenlt 5578  ne0gt0t 5619  lelttrit 5622  ltaddsubt 5631  lediv1t 5851  lediv1tOLD 5852  lemuldivt 5874  lemuldivtOLD 5875  nnge1t 5943  nnleltp1t 5954  lbinfm 6048  suprub 6056  suprleub 6059  dfinfmr 6067  supxrre 6083  nn0ge0t 6117  elnnz1 6155  zltp1let 6181  recnzt 6191  btwnnzt 6192  primet 6195  zbtwnre 6221  flltt 6234  flval3t 6239  om2uzlt2 6299  ioojoint 6416  indstr 6461  fznt 6493  sqr0 6672  climrecl 7110  climge0 7112  climubi 7153  caucvglem6 7162  ivthlem6 7286  ivthlem7 7287  infpnlem1 7506  metxpfval 7831  metxp 7834  bl2in 7843  lmle 7960  bcthlem18 8016  nmounbi 8439  nmlno0lem 8453  projlem13 9198  nmlnop0ALT 9920

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-xr 5489  df-le 5491

Copyright terms: Public domain