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

Theorem elicc2 11510
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 9550 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
2 rexr 9550 . . 3  |-  ( B  e.  RR  ->  B  e.  RR* )
3 elicc1 11494 . . 3  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( C  e.  ( A [,] B )  <->  ( C  e.  RR*  /\  A  <_  C  /\  C  <_  B
) ) )
41, 2, 3syl2an 475 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( C  e.  ( A [,] B )  <-> 
( C  e.  RR*  /\  A  <_  C  /\  C  <_  B ) ) )
5 mnfxr 11244 . . . . . . . 8  |- -oo  e.  RR*
65a1i 11 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> -oo  e.  RR* )
71ad2antrr 723 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  e.  RR* )
8 simpr1 1000 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR* )
9 mnflt 11254 . . . . . . . 8  |-  ( A  e.  RR  -> -oo  <  A )
109ad2antrr 723 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> -oo  <  A )
11 simpr2 1001 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  A  <_  C )
126, 7, 8, 10, 11xrltletrd 11285 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  -> -oo  <  C )
132ad2antlr 724 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  B  e.  RR* )
14 pnfxr 11242 . . . . . . . 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 1002 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  <_  B )
17 ltpnf 11252 . . . . . . . 8  |-  ( B  e.  RR  ->  B  < +oo )
1817ad2antlr 724 . . . . . . 7  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  B  < +oo )
198, 13, 15, 16, 18xrlelttrd 11284 . . . . . 6  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  < +oo )
20 xrrebnd 11290 . . . . . . 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 920 . . . . 5  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  C  e.  RR )
2322, 11, 163jca 1174 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
) )  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B ) )
2423ex 432 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( C  e. 
RR*  /\  A  <_  C  /\  C  <_  B
)  ->  ( C  e.  RR  /\  A  <_  C  /\  C  <_  B
) ) )
25 rexr 9550 . . . 4  |-  ( C  e.  RR  ->  C  e.  RR* )
26253anim1i 1180 . . 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 367    /\ w3a 971    e. wcel 1826   class class class wbr 4367  (class class class)co 6196   RRcr 9402   +oocpnf 9536   -oocmnf 9537   RR*cxr 9538    < clt 9539    <_ cle 9540   [,]cicc 11453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-pre-lttri 9477  ax-pre-lttrn 9478
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-po 4714  df-so 4715  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-icc 11457
This theorem is referenced by:  elicc2i  11511  iccssre  11527  iccsupr  11538  iccneg  11562  iccsplit  11574  iccshftr  11575  iccshftl  11577  iccdil  11579  icccntr  11581  iccf1o  11585  supicc  11589  icco1  13365  iccntr  21411  icccmplem1  21412  icccmplem2  21413  icccmplem3  21414  reconnlem1  21416  reconnlem2  21417  cnmpt2pc  21513  icoopnst  21524  iocopnst  21525  cnheiborlem  21539  ivthlem2  21949  ivthlem3  21950  ivthicc  21955  evthicc2  21957  ovolficc  21965  ovolicc1  22012  ovolicc2lem2  22014  ovolicc2lem5  22017  ovolicopnf  22020  dyadmaxlem  22091  opnmbllem  22095  volsup2  22099  volcn  22100  mbfi1fseqlem6  22212  itgspliticc  22328  itgsplitioo  22329  ditgcl  22347  ditgswap  22348  ditgsplitlem  22349  ditgsplit  22350  dvlip  22479  dvlip2  22481  dveq0  22486  dvgt0lem1  22488  dvivthlem1  22494  dvne0  22497  dvcnvrelem1  22503  dvcnvrelem2  22504  dvcnvre  22505  dvfsumlem2  22513  ftc1lem1  22521  ftc1lem2  22522  ftc1a  22523  ftc1lem4  22525  ftc2  22530  ftc2ditglem  22531  itgsubstlem  22534  pserulm  22902  loglesqrt  23219  log2tlbnd  23392  ppisval  23494  chtleppi  23602  fsumvma2  23606  chpchtsum  23611  chpub  23612  rplogsumlem2  23787  chpdifbndlem1  23855  pntibndlem2a  23892  pntibndlem2  23893  pntlemj  23905  pntlem3  23911  pntleml  23913  rescon  28880  cvmliftlem10  28928  opnmbllem0  30215  ftc2nc  30265  areacirclem2  30274  areacirclem4  30276  areacirc  30278  isbnd3  30446  isbnd3b  30447  prdsbnd  30455  iccbnd  30502  eliccd  31704  eliccre  31706  iccshift  31724  iccsuble  31725  limcicciooub  31809  icccncfext  31856  itgsubsticc  31941  iblcncfioo  31943  itgiccshift  31945  itgperiod  31946  itgsbtaddcnst  31947  fourierdlem42  32097  fourierdlem54  32109  fourierdlem63  32118  fourierdlem65  32120  fourierdlem74  32129  fourierdlem75  32130  fourierdlem82  32137  fourierdlem93  32148  fourierdlem101  32156  fourierdlem104  32159  fourierdlem111  32166
  Copyright terms: Public domain W3C validator