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

Theorem elicc2 11580
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 9630 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9630 . . 3  |-  ( B  e.  RR  ->  B  e.  RR* )
3 elicc1 11564 . . 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 11314 . . . . . . . 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 997 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR* )
9 mnflt 11324 . . . . . . . 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 998 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  <_  C )
126, 7, 8, 10, 11xrltletrd 11355 . . . . . 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 11312 . . . . . . . 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 999 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  <_  B )
17 ltpnf 11322 . . . . . . . 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 11354 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  < +oo )
20 xrrebnd 11360 . . . . . . 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 915 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR )
2322, 11, 163jca 1171 . . . 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 9630 . . . 4  |-  ( C  e.  RR  ->  C  e.  RR* )
26253anim1i 1177 . . 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 968    e. wcel 1762   class class class wbr 4442  (class class class)co 6277   RRcr 9482   +oocpnf 9616   -oocmnf 9617   RR*cxr 9618    < clt 9619    <_ cle 9620   [,]cicc 11523
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 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-cnex 9539  ax-resscn 9540  ax-pre-lttri 9557  ax-pre-lttrn 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-mpt 4502  df-id 4790  df-po 4795  df-so 4796  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7303  df-en 7509  df-dom 7510  df-sdom 7511  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-icc 11527
This theorem is referenced by:  elicc2i  11581  iccssre  11597  iccsupr  11608  iccneg  11632  iccsplit  11644  iccshftr  11645  iccshftl  11647  iccdil  11649  icccntr  11651  iccf1o  11655  supicc  11659  icco1  13314  iccntr  21056  icccmplem1  21057  icccmplem2  21058  icccmplem3  21059  reconnlem1  21061  reconnlem2  21062  cnmpt2pc  21158  icoopnst  21169  iocopnst  21170  cnheiborlem  21184  ivthlem2  21594  ivthlem3  21595  ivthicc  21600  evthicc2  21602  ovolficc  21610  ovolicc1  21657  ovolicc2lem2  21659  ovolicc2lem5  21662  ovolicopnf  21665  dyadmaxlem  21736  opnmbllem  21740  volsup2  21744  volcn  21745  mbfi1fseqlem6  21857  itgspliticc  21973  itgsplitioo  21974  ditgcl  21992  ditgswap  21993  ditgsplitlem  21994  ditgsplit  21995  dvlip  22124  dvlip2  22126  dveq0  22131  dvgt0lem1  22133  dvivthlem1  22139  dvne0  22142  dvcnvrelem1  22148  dvcnvrelem2  22149  dvcnvre  22150  dvfsumlem2  22158  ftc1lem1  22166  ftc1lem2  22167  ftc1a  22168  ftc1lem4  22170  ftc2  22175  ftc2ditglem  22176  itgsubstlem  22179  pserulm  22546  loglesqr  22855  log2tlbnd  22999  ppisval  23100  chtleppi  23208  fsumvma2  23212  chpchtsum  23217  chpub  23218  rplogsumlem2  23393  chpdifbndlem1  23461  pntibndlem2a  23498  pntibndlem2  23499  pntlemj  23511  pntlem3  23517  pntleml  23519  rescon  28319  cvmliftlem10  28367  opnmbllem0  29616  ftc2nc  29665  areacirclem2  29674  areacirclem4  29676  areacirc  29678  isbnd3  29872  isbnd3b  29873  prdsbnd  29881  iccbnd  29928  eliccd  31059  eliccre  31061  iccshift  31079  iccsuble  31080  limciccioolb  31120  limcicciooub  31136  icccncfext  31183  cncfiooicclem1  31189  itgsubsticc  31251  iblcncfioo  31253  itgspltprt  31254  itgiccshift  31255  itgperiod  31256  itgsbtaddcnst  31257  fourierdlem15  31379  fourierdlem40  31404  fourierdlem42  31406  fourierdlem54  31418  fourierdlem62  31426  fourierdlem63  31427  fourierdlem65  31429  fourierdlem74  31438  fourierdlem75  31439  fourierdlem78  31442  fourierdlem81  31445  fourierdlem82  31446  fourierdlem92  31456  fourierdlem93  31457  fourierdlem101  31465  fourierdlem104  31468  fourierdlem107  31471  fourierdlem111  31475  sqwvfoura  31486  sqwvfourb  31487
  Copyright terms: Public domain W3C validator