Theorem xrltnle 11357

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-le 11330

This theorem is used by:  xrltnled  11358  xrletri  13263  qextltlem  13313  xralrple  13316  xltadd1  13367  xsubge0  13372  xposdif  13373  xltmul1  13403  ioo0  13482  ico0  13503  ioc0  13504  snunioo  13590  snunioc  13592  difreicc  13596  hashbnd  14460  limsuplt  15626  pcadd  17047  pcadd2  17048  ramubcl  17176  ramlb  17177  leordtvallem1  23508  leordtvallem2  23509  leordtval2  23510  leordtval  23511  lecldbas  23517  blcld  24804  stdbdbl  24816  tmsxpsval2  24838  iocmnfcld  25067  xrsxmet  25109  metdsge  25149  bndth  25259  ovolgelb  25781  ovolunnul  25801  ioombl  25866  volsup2  25906  mbfmax  25950  ismbf3d  25955  itg2seq  26043  itg2monolem2  26052  itg2monolem3  26053  lhop2  26315  mdegleb  26362  deg1ge  26396  deg1add  26401  ig1pdvds  26478  plypf1  26511  radcnvlt1  26727  upgrfi  29651  xrdifh  33354  xrge00  33557  gsumesum  34673  itg2gt0cn  38561  asindmre  38589  dvasin  38590  aks6d1c6lem3  43190  aks6d1c7lem2  43199  iocioodisjd  43345  radcnvrat  45257  supxrgelem  46293  infrpge  46307  xrlexaddrp  46308  xrpnf  46439  gtnelioc  46447  ltnelicc  46453  gtnelicc  46456  snunioo1  46468  eliccnelico  46485  xrgtnelicc  46494  lptioo2  46587  stoweidlem34  46988  fourierdlem20  47081  fouriersw  47185  nltle2tri  48327  iccelpart  48459