MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elicopnf Structured version   Unicode version

Theorem elicopnf 11375
Description: Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
Assertion
Ref Expression
elicopnf  |-  ( A  e.  RR  ->  ( B  e.  ( A [,) +oo )  <->  ( B  e.  RR  /\  A  <_  B ) ) )

Proof of Theorem elicopnf
StepHypRef Expression
1 pnfxr 11082 . . 3  |- +oo  e.  RR*
2 elico2 11349 . . 3  |-  ( ( A  e.  RR  /\ +oo  e.  RR* )  ->  ( B  e.  ( A [,) +oo )  <->  ( B  e.  RR  /\  A  <_  B  /\  B  < +oo ) ) )
31, 2mpan2 666 . 2  |-  ( A  e.  RR  ->  ( B  e.  ( A [,) +oo )  <->  ( B  e.  RR  /\  A  <_  B  /\  B  < +oo ) ) )
4 ltpnf 11092 . . . . 5  |-  ( B  e.  RR  ->  B  < +oo )
54adantr 462 . . . 4  |-  ( ( B  e.  RR  /\  A  <_  B )  ->  B  < +oo )
65pm4.71i 627 . . 3  |-  ( ( B  e.  RR  /\  A  <_  B )  <->  ( ( B  e.  RR  /\  A  <_  B )  /\  B  < +oo ) )
7 df-3an 962 . . 3  |-  ( ( B  e.  RR  /\  A  <_  B  /\  B  < +oo )  <->  ( ( B  e.  RR  /\  A  <_  B )  /\  B  < +oo ) )
86, 7bitr4i 252 . 2  |-  ( ( B  e.  RR  /\  A  <_  B )  <->  ( B  e.  RR  /\  A  <_  B  /\  B  < +oo ) )
93, 8syl6bbr 263 1  |-  ( A  e.  RR  ->  ( B  e.  ( A [,) +oo )  <->  ( B  e.  RR  /\  A  <_  B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 960    e. wcel 1757   class class class wbr 4282  (class class class)co 6082   RRcr 9271   +oocpnf 9405   RR*cxr 9407    < clt 9408    <_ cle 9409   [,)cico 11292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-pre-lttri 9346  ax-pre-lttrn 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-opab 4341  df-mpt 4342  df-id 4625  df-po 4630  df-so 4631  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-ico 11296
This theorem is referenced by:  elrege0  11382  rexico  12827  limsupgle  12941  limsupgre  12945  rlim3  12962  ello12  12980  lo1bdd2  12988  elo12  12991  lo1resb  13028  rlimresb  13029  o1resb  13030  lo1eq  13032  rlimeq  13033  rlimsqzlem  13112  o1fsum  13261  ovolicopnf  20851  dvfsumrlimge0  21346  dvfsumrlim  21347  dvfsumrlim2  21348  cxp2lim  22257  chebbnd1  22608  chtppilimlem1  22609  chtppilimlem2  22610  chtppilim  22611  chebbnd2  22613  chto1lb  22614  chpchtlim  22615  chpo1ub  22616  vmadivsumb  22619  dchrisumlema  22624  dchrisumlem2  22626  dchrisumlem3  22627  dchrmusumlema  22629  dchrmusum2  22630  dchrvmasumlem2  22634  dchrvmasumiflem1  22637  dchrisum0lema  22650  dchrisum0lem1b  22651  dchrisum0lem2a  22653  dchrisum0lem2  22654  2vmadivsumlem  22676  selbergb  22685  selberg2b  22688  chpdifbndlem1  22689  selberg3lem1  22693  selberg3lem2  22694  selberg4lem1  22696  pntrsumo1  22701  selbergsb  22711  pntrlog2bndlem3  22715  pntpbnd1  22722  pntpbnd2  22723  pntibndlem3  22728  pntlemn  22736  pntlem3  22745  pntleml  22747  pnt2  22749  itg2addnclem2  28290
  Copyright terms: Public domain W3C validator