Theorem xrltnle 11210

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079  ℝ^*cxr 11176   < clt 11177   ≤ cle 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-le 11183

This theorem is referenced by:  xrltnled  11211  xrletri  13102  qextltlem  13152  xralrple  13155  xltadd1  13206  xsubge0  13211  xposdif  13212  xltmul1  13242  ioo0  13321  ico0  13342  ioc0  13343  snunioo  13429  snunioc  13431  difreicc  13435  hashbnd  14296  limsuplt  15439  pcadd  16858  pcadd2  16859  ramubcl  16987  ramlb  16988  leordtvallem1  23200  leordtvallem2  23201  leordtval2  23202  leordtval  23203  lecldbas  23209  blcld  24495  stdbdbl  24507  tmsxpsval2  24529  iocmnfcld  24758  xrsxmet  24800  metdsge  24840  bndth  24950  ovolgelb  25472  ovolunnul  25492  ioombl  25557  volsup2  25597  mbfmax  25641  ismbf3d  25646  itg2seq  25734  itg2monolem2  25743  itg2monolem3  25744  lhop2  26007  mdegleb  26054  deg1ge  26088  deg1add  26093  ig1pdvds  26170  plypf1  26202  radcnvlt1  26408  upgrfi  29185  xrdifh  32879  xrge00  33100  gsumesum  34250  itg2gt0cn  38049  asindmre  38077  dvasin  38078  aks6d1c6lem3  42664  aks6d1c7lem2  42673  iocioodisjd  42804  radcnvrat  44765  supxrgelem  45789  infrpge  45803  xrlexaddrp  45804  xrpnf  45935  gtnelioc  45943  ltnelicc  45949  gtnelicc  45952  snunioo1  45964  eliccnelico  45981  xrgtnelicc  45990  lptioo2  46083  stoweidlem34  46484  fourierdlem20  46577  fouriersw  46681  nltle2tri  47783  iccelpart  47915