Theorem xrltnle 11203

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-le 11176

This theorem is referenced by:  xrltnled  11204  xrletri  13095  qextltlem  13145  xralrple  13148  xltadd1  13199  xsubge0  13204  xposdif  13205  xltmul1  13235  ioo0  13314  ico0  13335  ioc0  13336  snunioo  13422  snunioc  13424  difreicc  13428  hashbnd  14289  limsuplt  15432  pcadd  16851  pcadd2  16852  ramubcl  16980  ramlb  16981  leordtvallem1  23185  leordtvallem2  23186  leordtval2  23187  leordtval  23188  lecldbas  23194  blcld  24480  stdbdbl  24492  tmsxpsval2  24514  iocmnfcld  24743  xrsxmet  24785  metdsge  24825  bndth  24935  ovolgelb  25457  ovolunnul  25477  ioombl  25542  volsup2  25582  mbfmax  25626  ismbf3d  25631  itg2seq  25719  itg2monolem2  25728  itg2monolem3  25729  lhop2  25992  mdegleb  26039  deg1ge  26073  deg1add  26078  ig1pdvds  26155  plypf1  26187  radcnvlt1  26396  upgrfi  29174  xrdifh  32868  xrge00  33089  gsumesum  34219  itg2gt0cn  38010  asindmre  38038  dvasin  38039  aks6d1c6lem3  42625  aks6d1c7lem2  42634  iocioodisjd  42766  radcnvrat  44759  supxrgelem  45785  infrpge  45799  xrlexaddrp  45800  xrpnf  45931  gtnelioc  45939  ltnelicc  45945  gtnelicc  45948  snunioo1  45960  eliccnelico  45977  xrgtnelicc  45986  lptioo2  46079  stoweidlem34  46480  fourierdlem20  46573  fouriersw  46677  nltle2tri  47773  iccelpart  47905