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

Theorem xrlenlt 10063
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 4624 . . 3 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2 opelxpi 5118 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*))
3 df-le 10040 . . . . . . 7 ≤ = ((ℝ* × ℝ*) ∖ < )
43eleq2i 2690 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ))
5 eldif 3570 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
64, 5bitri 264 . . . . 5 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
76baib 943 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
82, 7syl 17 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
91, 8syl5bb 272 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
10 opelcnvg 5272 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
11 df-br 4624 . . . 4 (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
1210, 11syl6rbbr 279 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ < ))
1312notbid 308 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
149, 13bitr4d 271 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wcel 1987  cdif 3557  cop 4161   class class class wbr 4623   × cxp 5082  ccnv 5083  *cxr 10033   < clt 10034  cle 10035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-cnv 5092  df-le 10040
This theorem is referenced by:  xrlenltd  10064  xrltnle  10065  xrnltled  10066  lenlt  10076  pnfge  11924  mnfle  11929  xrleloe  11937  xrltlen  11939  xrletri3  11945  xgepnf  11956  xralrple  11995  xleneg  12008  supxr2  12103  supxrbnd1  12110  supxrbnd2  12111  supxrub  12113  supxrleub  12115  supxrbnd  12117  infxrgelb  12124  ixxub  12154  ioon0  12159  iccid  12178  icc0  12181  icoun  12254  icodisj  12255  snunico  12257  ioodisj  12260  ioojoin  12261  supicclub2  12281  hashgt0elex  13145  hashgt12el  13166  hashgt12el2  13167  0ringnnzr  19209  lecldbas  20963  xmetgt0  22103  bldisj  22143  icopnfcld  22511  icombl  23272  ioombl  23273  ioorcl2  23280  vitalilem4  23320  itg2gt0  23467  ply1divmo  23833  ig1peu  23869  radcnvle  24112  psercnlem1  24117  nmlnogt0  27540  xlemnf  29400  xrlelttric  29401  xrsupssd  29409  xrge0infss  29410  joiniooico  29421  xeqlelt  29423  iocinif  29428  esumsnf  29949  esum2d  29978  oms0  30182  omssubadd  30185  relowlpssretop  32883  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  asindmre  33166  ioounsn  37315  iocmbl  37318  supxrgere  39048  snunioo2  39177  iccdifprioo  39188  iccpartnel  40702
  Copyright terms: Public domain W3C validator