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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-le 11330

This theorem is referenced by:  xrletri  13215  qextltlem  13264  xralrple  13267  xltadd1  13318  xsubge0  13323  xposdif  13324  xltmul1  13354  ioo0  13432  ico0  13453  ioc0  13454  snunioo  13538  snunioc  13540  difreicc  13544  hashbnd  14385  limsuplt  15525  pcadd  16936  pcadd2  16937  ramubcl  17065  ramlb  17066  leordtvallem1  23239  leordtvallem2  23240  leordtval2  23241  leordtval  23242  lecldbas  23248  blcld  24539  stdbdbl  24551  tmsxpsval2  24573  iocmnfcld  24810  xrsxmet  24850  metdsge  24890  bndth  25009  ovolgelb  25534  ovolunnul  25554  ioombl  25619  volsup2  25659  mbfmax  25703  ismbf3d  25708  itg2seq  25797  itg2monolem2  25806  itg2monolem3  25807  lhop2  26074  mdegleb  26123  deg1ge  26157  deg1add  26162  ig1pdvds  26239  plypf1  26271  radcnvlt1  26479  upgrfi  29126  xrdifh  32785  xrge00  32998  gsumesum  34023  itg2gt0cn  37635  asindmre  37663  dvasin  37664  aks6d1c6lem3  42129  aks6d1c7lem2  42138  radcnvrat  44283  supxrgelem  45252  infrpge  45266  xrlexaddrp  45267  xrltnled  45278  xrpnf  45401  gtnelioc  45409  ltnelicc  45415  gtnelicc  45418  snunioo1  45430  eliccnelico  45447  xrgtnelicc  45456  lptioo2  45552  stoweidlem34  45955  fourierdlem20  46048  fouriersw  46152  nltle2tri  47228  iccelpart  47307