Theorem xrltnle 11326

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2106   class class class wbr 5148  ℝ^*cxr 11292   < clt 11293   ≤ cle 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-le 11299

This theorem is referenced by:  xrletri  13192  qextltlem  13241  xralrple  13244  xltadd1  13295  xsubge0  13300  xposdif  13301  xltmul1  13331  ioo0  13409  ico0  13430  ioc0  13431  snunioo  13515  snunioc  13517  difreicc  13521  hashbnd  14372  limsuplt  15512  pcadd  16923  pcadd2  16924  ramubcl  17052  ramlb  17053  leordtvallem1  23234  leordtvallem2  23235  leordtval2  23236  leordtval  23237  lecldbas  23243  blcld  24534  stdbdbl  24546  tmsxpsval2  24568  iocmnfcld  24805  xrsxmet  24845  metdsge  24885  bndth  25004  ovolgelb  25529  ovolunnul  25549  ioombl  25614  volsup2  25654  mbfmax  25698  ismbf3d  25703  itg2seq  25792  itg2monolem2  25801  itg2monolem3  25802  lhop2  26069  mdegleb  26118  deg1ge  26152  deg1add  26157  ig1pdvds  26234  plypf1  26266  radcnvlt1  26476  upgrfi  29123  xrdifh  32789  xrge00  33000  gsumesum  34040  itg2gt0cn  37662  asindmre  37690  dvasin  37691  aks6d1c6lem3  42154  aks6d1c7lem2  42163  iocioodisjd  42334  radcnvrat  44310  supxrgelem  45287  infrpge  45301  xrlexaddrp  45302  xrltnled  45313  xrpnf  45436  gtnelioc  45444  ltnelicc  45450  gtnelicc  45453  snunioo1  45465  eliccnelico  45482  xrgtnelicc  45491  lptioo2  45587  stoweidlem34  45990  fourierdlem20  46083  fouriersw  46187  nltle2tri  47263  iccelpart  47358