MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrlenlt Structured version   Visualization version   GIF version

Theorem xrlenlt 11323
Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
xrlenlt ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem xrlenlt
StepHypRef Expression
1 df-br 5148 . . 3 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2 opelxpi 5725 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*))
3 df-le 11298 . . . . . . 7 ≤ = ((ℝ* × ℝ*) ∖ < )
43eleq2i 2830 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ))
5 eldif 3972 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
64, 5bitri 275 . . . . 5 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
76baib 535 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
82, 7syl 17 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
91, 8bitrid 283 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
10 df-br 5148 . . . 4 (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11 opelcnvg 5893 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
1210, 11bitr4id 290 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ < ))
1312notbid 318 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
149, 13bitr4d 282 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wcel 2105  cdif 3959  cop 4636   class class class wbr 5147   × cxp 5686  ccnv 5687  *cxr 11291   < clt 11292  cle 11293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-le 11298
This theorem is referenced by:  xrlenltd  11324  xrltnle  11325  lenlt  11336  pnfge  13169  mnfle  13173  xrleloe  13182  xrltlen  13184  xrletri3  13192  xgepnf  13203  xlemnf  13205  xralrple  13243  xleneg  13256  supxr2  13352  supxrbnd1  13359  supxrbnd2  13360  supxrleub  13364  supxrbnd  13366  infxrgelb  13373  ioon0  13409  iccid  13428  icc0  13431  icoun  13511  ioounsn  13513  snunico  13515  ioodisj  13518  ioojoin  13519  hashgt0elex  14436  hashgt12el  14457  hashgt12el2  14458  0ringnnzr  20541  lecldbas  23242  xmetgt0  24383  icopnfcld  24803  ioombl  25613  vitalilem4  25659  itg2gt0  25809  nmlnogt0  30825  xrlelttric  32762  xrsupssd  32769  xrge0infss  32770  joiniooico  32782  xeqlelt  32784  iocinif  32789  esumsnf  34044  esum2d  34073  oms0  34278  omssubadd  34281  cusgracyclt3v  35140  relowlpssretop  37346  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  asindmre  37689  dvrelog2b  42047  iocmbl  43201  supxrgere  45282  iccdifprioo  45468  iccpartnel  47362  iccdisj2  48693
  Copyright terms: Public domain W3C validator