Theorem xrltnle 9674

Description: 'Less than' expressed in terms of 'less than or equal to', for extended reals. (Contributed by NM, 6-Feb-2007.)

Assertion

Ref	Expression
xrltnle

Proof of Theorem xrltnle

Step	Hyp	Ref	Expression
1		xrlenlt 9673	. . 3
2	1	con2bid 329	. 2
3	2	ancoms 453	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818   class class class wbr 4452  cxr 9648  clt 9649  cle 9650

This theorem is referenced by:  xrletri  11386  qextltlem  11430  xralrple  11433  xltadd1  11477  xsubge0  11482  xposdif  11483  xltmul1  11513  ioo0  11583  ico0  11604  ioc0  11605  snunioo  11675  snunioc  11677  difreicc  11681  hashbnd  12411  limsuplt  13302  pcadd  14408  pcadd2  14409  ramubcl  14536  ramlb  14537  leordtvallem1  19711  leordtvallem2  19712  leordtval2  19713  leordtval  19714  lecldbas  19720  blcld  21008  stdbdbl  21020  tmsxpsval2  21042  iocmnfcld  21276  xrsxmet  21314  metdsge  21353  bndth  21458  ovolgelb  21891  ovolunnul  21911  ioombl  21975  volsup2  22014  mbfmax  22056  ismbf3d  22061  itg2seq  22149  itg2monolem2  22158  itg2monolem3  22159  lhop2  22416  mdegleb  22464  deg1ge  22499  deg1add  22504  ig1pdvds  22577  plypf1  22609  radcnvlt1  22813  umgrafi  24322  xrdifh  27591  xrge00  27674  xrge0neqmnf  27679  gsumesum  28067  itg2gt0cn  30070  asindmre  30102  dvasin  30103  radcnvrat  31195  gtnelioc  31523  ltnelicc  31530  gtnelicc  31533  snunioo1  31552  lptioo2  31637  stoweidlem34  31816  fourierdlem20  31909  fouriersw  32014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-cnv 5012  df-le 9655