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

Theorem elicc2 11618
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

Proof of Theorem elicc2
StepHypRef Expression
1 rexr 9660 . . 3
2 rexr 9660 . . 3
3 elicc1 11602 . . 3
41, 2, 3syl2an 477 . 2
5 mnfxr 11352 . . . . . . . 8
65a1i 11 . . . . . . 7
71ad2antrr 725 . . . . . . 7
8 simpr1 1002 . . . . . . 7
9 mnflt 11362 . . . . . . . 8
109ad2antrr 725 . . . . . . 7
11 simpr2 1003 . . . . . . 7
126, 7, 8, 10, 11xrltletrd 11393 . . . . . 6
132ad2antlr 726 . . . . . . 7
14 pnfxr 11350 . . . . . . . 8
1514a1i 11 . . . . . . 7
16 simpr3 1004 . . . . . . 7
17 ltpnf 11360 . . . . . . . 8
1817ad2antlr 726 . . . . . . 7
198, 13, 15, 16, 18xrlelttrd 11392 . . . . . 6
20 xrrebnd 11398 . . . . . . 7
218, 20syl 16 . . . . . 6
2212, 19, 21mpbir2and 922 . . . . 5
2322, 11, 163jca 1176 . . . 4
2423ex 434 . . 3
25 rexr 9660 . . . 4
26253anim1i 1182 . . 3
2724, 26impbid1 203 . 2
284, 27bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  e.wcel 1818   class class class wbr 4452  (class class class)co 6296   cr 9512   cpnf 9646   cmnf 9647   cxr 9648   clt 9649   cle 9650   cicc 11561
This theorem is referenced by:  elicc2i  11619  iccssre  11635  iccsupr  11646  iccneg  11670  iccsplit  11682  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  iccf1o  11693  supicc  11697  icco1  13363  iccntr  21326  icccmplem1  21327  icccmplem2  21328  icccmplem3  21329  reconnlem1  21331  reconnlem2  21332  cnmpt2pc  21428  icoopnst  21439  iocopnst  21440  cnheiborlem  21454  ivthlem2  21864  ivthlem3  21865  ivthicc  21870  evthicc2  21872  ovolficc  21880  ovolicc1  21927  ovolicc2lem2  21929  ovolicc2lem5  21932  ovolicopnf  21935  dyadmaxlem  22006  opnmbllem  22010  volsup2  22014  volcn  22015  mbfi1fseqlem6  22127  itgspliticc  22243  itgsplitioo  22244  ditgcl  22262  ditgswap  22263  ditgsplitlem  22264  ditgsplit  22265  dvlip  22394  dvlip2  22396  dveq0  22401  dvgt0lem1  22403  dvivthlem1  22409  dvne0  22412  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvfsumlem2  22428  ftc1lem1  22436  ftc1lem2  22437  ftc1a  22438  ftc1lem4  22440  ftc2  22445  ftc2ditglem  22446  itgsubstlem  22449  pserulm  22817  loglesqrt  23132  log2tlbnd  23276  ppisval  23377  chtleppi  23485  fsumvma2  23489  chpchtsum  23494  chpub  23495  rplogsumlem2  23670  chpdifbndlem1  23738  pntibndlem2a  23775  pntibndlem2  23776  pntlemj  23788  pntlem3  23794  pntleml  23796  rescon  28691  cvmliftlem10  28739  opnmbllem0  30050  ftc2nc  30099  areacirclem2  30108  areacirclem4  30110  areacirc  30112  isbnd3  30280  isbnd3b  30281  prdsbnd  30289  iccbnd  30336  eliccd  31538  eliccre  31540  iccshift  31558  iccsuble  31559  limcicciooub  31643  icccncfext  31690  itgsubsticc  31775  iblcncfioo  31777  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  fourierdlem42  31931  fourierdlem54  31943  fourierdlem63  31952  fourierdlem65  31954  fourierdlem74  31963  fourierdlem75  31964  fourierdlem82  31971  fourierdlem93  31982  fourierdlem101  31990  fourierdlem104  31993  fourierdlem111  32000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-pre-lttri 9587  ax-pre-lttrn 9588
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-icc 11565
  Copyright terms: Public domain W3C validator