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

Theorem elicc2 11381
Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
Assertion
Ref Expression
elicc2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,] B )  <-> 
( C  e.  RR  /\  A  <_  C  /\  C  <_  B ) ) )

Proof of Theorem elicc2
StepHypRef Expression
1 rexr 9450 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9450 . . 3  |-  ( B  e.  RR  ->  B  e.  RR* )
3 elicc1 11365 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( C  e.  ( A [,] B )  <->  ( C  e.  RR*  /\  A  <_  C  /\  C  <_  B
) ) )
41, 2, 3syl2an 477 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,] B )  <-> 
( C  e.  RR*  /\  A  <_  C  /\  C  <_  B ) ) )
5 mnfxr 11115 . . . . . . . 8  |- -oo  e.  RR*
65a1i 11 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> -oo  e.  RR* )
71ad2antrr 725 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  e.  RR* )
8 simpr1 994 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR* )
9 mnflt 11125 . . . . . . . 8  |-  ( A  e.  RR  -> -oo  <  A )
109ad2antrr 725 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> -oo  <  A )
11 simpr2 995 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  <_  C )
126, 7, 8, 10, 11xrltletrd 11156 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> -oo  <  C )
132ad2antlr 726 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  B  e.  RR* )
14 pnfxr 11113 . . . . . . . 8  |- +oo  e.  RR*
1514a1i 11 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> +oo  e.  RR* )
16 simpr3 996 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  <_  B )
17 ltpnf 11123 . . . . . . . 8  |-  ( B  e.  RR  ->  B  < +oo )
1817ad2antlr 726 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  B  < +oo )
198, 13, 15, 16, 18xrlelttrd 11155 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  < +oo )
20 xrrebnd 11161 . . . . . . 7  |-  ( C  e.  RR*  ->  ( C  e.  RR  <->  ( -oo  <  C  /\  C  < +oo ) ) )
218, 20syl 16 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  ( C  e.  RR  <->  ( -oo  <  C  /\  C  < +oo ) ) )
2212, 19, 21mpbir2and 913 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR )
2322, 11, 163jca 1168 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B ) )
2423ex 434 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
)  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B
) ) )
25 rexr 9450 . . . 4  |-  ( C  e.  RR  ->  C  e.  RR* )
26253anim1i 1174 . . 3  |-  ( ( C  e.  RR  /\  A  <_  C  /\  C  <_  B )  ->  ( C  e.  RR*  /\  A  <_  C  /\  C  <_  B ) )
2724, 26impbid1 203 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
)  <->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B
) ) )
284, 27bitrd 253 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,] B )  <-> 
( C  e.  RR  /\  A  <_  C  /\  C  <_  B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    e. wcel 1756   class class class wbr 4313  (class class class)co 6112   RRcr 9302   +oocpnf 9436   -oocmnf 9437   RR*cxr 9438    < clt 9439    <_ cle 9440   [,]cicc 11324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-cnex 9359  ax-resscn 9360  ax-pre-lttri 9377  ax-pre-lttrn 9378
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-po 4662  df-so 4663  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-er 7122  df-en 7332  df-dom 7333  df-sdom 7334  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-icc 11328
This theorem is referenced by:  elicc2i  11382  iccssre  11398  iccsupr  11403  iccneg  11427  iccsplit  11439  iccshftr  11440  iccshftl  11442  iccdil  11444  icccntr  11446  iccf1o  11450  supicc  11454  icco1  13039  iccntr  20420  icccmplem1  20421  icccmplem2  20422  icccmplem3  20423  reconnlem1  20425  reconnlem2  20426  cnmpt2pc  20522  icoopnst  20533  iocopnst  20534  cnheiborlem  20548  ivthlem2  20958  ivthlem3  20959  ivthicc  20964  evthicc2  20966  ovolficc  20974  ovolicc1  21021  ovolicc2lem2  21023  ovolicc2lem5  21026  ovolicopnf  21029  dyadmaxlem  21099  opnmbllem  21103  volsup2  21107  volcn  21108  mbfi1fseqlem6  21220  itgspliticc  21336  itgsplitioo  21337  ditgcl  21355  ditgswap  21356  ditgsplitlem  21357  ditgsplit  21358  dvlip  21487  dvlip2  21489  dveq0  21494  dvgt0lem1  21496  dvivthlem1  21502  dvne0  21505  dvcnvrelem1  21511  dvcnvrelem2  21512  dvcnvre  21513  dvfsumlem2  21521  ftc1lem1  21529  ftc1lem2  21530  ftc1a  21531  ftc1lem4  21533  ftc2  21538  ftc2ditglem  21539  itgsubstlem  21542  pserulm  21909  loglesqr  22218  log2tlbnd  22362  ppisval  22463  chtleppi  22571  fsumvma2  22575  chpchtsum  22580  chpub  22581  rplogsumlem2  22756  chpdifbndlem1  22824  pntibndlem2a  22861  pntibndlem2  22862  pntlemj  22874  pntlem3  22880  pntleml  22882  rescon  27157  cvmliftlem10  27205  opnmbllem0  28453  ftc2nc  28502  areacirclem2  28511  areacirclem4  28513  areacirc  28515  isbnd3  28709  isbnd3b  28710  prdsbnd  28718  iccbnd  28765
  Copyright terms: Public domain W3C validator