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

Theorem elicc2 10711
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 8873 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 8873 . . 3  |-  ( B  e.  RR  ->  B  e.  RR* )
3 elicc1 10696 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( C  e.  ( A [,] B )  <->  ( C  e.  RR*  /\  A  <_  C  /\  C  <_  B
) ) )
41, 2, 3syl2an 463 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,] B )  <-> 
( C  e.  RR*  /\  A  <_  C  /\  C  <_  B ) ) )
5 mnfxr 10452 . . . . . . . 8  |-  -oo  e.  RR*
65a1i 10 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  -oo  e.  RR* )
71ad2antrr 706 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  e.  RR* )
8 simpr1 961 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR* )
9 mnflt 10460 . . . . . . . 8  |-  ( A  e.  RR  ->  -oo  <  A )
109ad2antrr 706 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  -oo  <  A )
11 simpr2 962 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  <_  C )
126, 7, 8, 10, 11xrltletrd 10488 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  -oo  <  C )
132ad2antlr 707 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  B  e.  RR* )
14 pnfxr 10451 . . . . . . . 8  |-  +oo  e.  RR*
1514a1i 10 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  +oo  e.  RR* )
16 simpr3 963 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  <_  B )
17 ltpnf 10459 . . . . . . . 8  |-  ( B  e.  RR  ->  B  <  +oo )
1817ad2antlr 707 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  B  <  +oo )
198, 13, 15, 16, 18xrlelttrd 10487 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  <  +oo )
20 xrrebnd 10493 . . . . . . 7  |-  ( C  e.  RR*  ->  ( C  e.  RR  <->  (  -oo  <  C  /\  C  <  +oo ) ) )
218, 20syl 15 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  ( C  e.  RR  <->  (  -oo  <  C  /\  C  <  +oo ) ) )
2212, 19, 21mpbir2and 888 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR )
2322, 11, 163jca 1132 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B ) )
2423ex 423 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
)  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B
) ) )
25 rexr 8873 . . . 4  |-  ( C  e.  RR  ->  C  e.  RR* )
26253anim1i 1138 . . 3  |-  ( ( C  e.  RR  /\  A  <_  C  /\  C  <_  B )  ->  ( C  e.  RR*  /\  A  <_  C  /\  C  <_  B ) )
2724, 26impbid1 194 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
)  <->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B
) ) )
284, 27bitrd 244 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,] B )  <-> 
( C  e.  RR  /\  A  <_  C  /\  C  <_  B ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    e. wcel 1685   class class class wbr 4024  (class class class)co 5820   RRcr 8732    +oocpnf 8860    -oocmnf 8861   RR*cxr 8862    < clt 8863    <_ cle 8864   [,]cicc 10655
This theorem is referenced by:  elicc2i  10712  iccssre  10727  iccsupr  10732  iccneg  10753  iccsplit  10764  iccshftr  10765  iccshftl  10767  iccdil  10769  icccntr  10771  iccf1o  10774  icco1  12010  iccntr  18322  icccmplem1  18323  icccmplem2  18324  icccmplem3  18325  reconnlem1  18327  reconnlem2  18328  cnmpt2pc  18422  icoopnst  18433  iocopnst  18434  cnheiborlem  18448  ivthlem2  18808  ivthlem3  18809  ivthicc  18814  evthicc2  18816  ovolficc  18824  ovolicc1  18871  ovolicc2lem2  18873  ovolicc2lem5  18876  ovolicopnf  18879  dyadmaxlem  18948  opnmbllem  18952  volsup2  18956  volcn  18957  mbfi1fseqlem6  19071  itgspliticc  19187  itgsplitioo  19188  ditgcl  19204  ditgswap  19205  ditgsplitlem  19206  ditgsplit  19207  dvlip  19336  dvlip2  19338  dveq0  19343  dvgt0lem1  19345  dvivthlem1  19351  dvne0  19354  dvcnvrelem1  19360  dvcnvrelem2  19361  dvcnvre  19362  dvfsumlem2  19370  ftc1lem1  19378  ftc1lem2  19379  ftc1a  19380  ftc1lem4  19382  ftc2  19387  ftc2ditglem  19388  itgsubstlem  19391  pserulm  19794  loglesqr  20094  log2tlbnd  20237  ppisval  20337  chtleppi  20445  fsumvma2  20449  chpchtsum  20454  chpub  20455  rplogsumlem2  20630  chpdifbndlem1  20698  pntibndlem2a  20735  pntibndlem2  20736  pntlemj  20748  pntlem3  20754  pntleml  20756  rescon  23184  cvmliftlem10  23232  areacirclem4  24337  areacirclem5  24339  areacirc  24341  icccon2  25111  icccon3  25112  icccon4  25113  isbnd3  25919  isbnd3b  25920  prdsbnd  25928  iccbnd  25975
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-cnex 8789  ax-resscn 8790  ax-pre-lttri 8807  ax-pre-lttrn 8808
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-po 4313  df-so 4314  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-icc 10659
  Copyright terms: Public domain W3C validator