Theorem xrltnle 11147

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 11145	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	con2bid 355	. 2 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
3	2	ancoms 460	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2106   class class class wbr 5096  ℝ^*cxr 11113   < clt 11114   ≤ cle 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pr 5376

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-br 5097  df-opab 5159  df-xp 5630  df-cnv 5632  df-le 11120

This theorem is referenced by:  xrletri  12992  qextltlem  13041  xralrple  13044  xltadd1  13095  xsubge0  13100  xposdif  13101  xltmul1  13131  ioo0  13209  ico0  13230  ioc0  13231  snunioo  13315  snunioc  13317  difreicc  13321  hashbnd  14155  limsuplt  15287  pcadd  16687  pcadd2  16688  ramubcl  16816  ramlb  16817  leordtvallem1  22466  leordtvallem2  22467  leordtval2  22468  leordtval  22469  lecldbas  22475  blcld  23766  stdbdbl  23778  tmsxpsval2  23800  iocmnfcld  24037  xrsxmet  24077  metdsge  24117  bndth  24226  ovolgelb  24749  ovolunnul  24769  ioombl  24834  volsup2  24874  mbfmax  24918  ismbf3d  24923  itg2seq  25012  itg2monolem2  25021  itg2monolem3  25022  lhop2  25284  mdegleb  25334  deg1ge  25368  deg1add  25373  ig1pdvds  25446  plypf1  25478  radcnvlt1  25682  upgrfi  27749  xrdifh  31386  xrge00  31580  gsumesum  32323  itg2gt0cn  35988  asindmre  36016  dvasin  36017  radcnvrat  42305  supxrgelem  43263  infrpge  43277  xrlexaddrp  43278  xrltnled  43289  xrpnf  43413  gtnelioc  43417  ltnelicc  43423  gtnelicc  43426  snunioo1  43438  eliccnelico  43455  xrgtnelicc  43464  lptioo2  43560  stoweidlem34  43963  fourierdlem20  44056  fouriersw  44160  nltle2tri  45223  iccelpart  45303