Theorem lbicc2 11739

Description: The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.)

Assertion

Ref	Expression
lbicc2	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )

Proof of Theorem lbicc2

Step	Hyp	Ref	Expression
1		simp1 1009	. 2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. RR* )
2		xrleid 11439	. . 3 |- ( A e. RR* -> A <_ A )
3	2	3ad2ant1 1030	. 2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ A )
4		simp3 1011	. 2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ B )
5		elicc1 11670	. . 3 |- ( ( A e. RR* /\ B e. RR* ) -> ( A e. ( A [,] B ) <-> ( A e. RR* /\ A <_ A /\ A <_ B ) ) )
6	5	3adant3 1029	. 2 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A e. ( A [,] B ) <-> ( A e. RR* /\ A <_ A /\ A <_ B ) ) )
7	1, 3, 4, 6	mpbir3and 1192	1 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ w3a 986   e. wcel 1891   class class class wbr 4374  (class class class)co 6276   RR*cxr 9661   <_ cle 9663   [,]cicc 11628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-cnex 9582  ax-resscn 9583  ax-pre-lttri 9600  ax-pre-lttrn 9601

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-po 4733  df-so 4734  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-icc 11632

This theorem is referenced by:  icccmplem1  21851  reconnlem2  21856  oprpiece1res1  21990  pcoass  22066  ivthlem1  22413  ivth2  22417  ivthle  22418  ivthle2  22419  evthicc  22421  ovolicc2lem5  22486  dyadmaxlem  22567  rolle  22954  cmvth  22955  mvth  22956  dvlip  22957  c1liplem1  22960  dveq0  22964  dvgt0lem1  22966  lhop1lem  22977  dvcnvrelem1  22981  dvcvx  22984  dvfsumle  22985  dvfsumge  22986  dvfsumabs  22987  dvfsumlem2  22991  ftc2  23008  ftc2ditglem  23009  itgparts  23011  itgsubstlem  23012  taylfval  23326  tayl0  23329  efcvx  23416  pige3  23484  logccv  23620  loglesqrt  23710  eliccioo  28408  oms0OLD  29135  cvmliftlem6  30019  cvmliftlem8  30021  cvmliftlem9  30022  cvmliftlem10  30023  cvmliftlem13  30025  ivthALT  30997  ftc2nc  32028  areacirc  32039  itgpowd  36101  iccintsng  37665  icccncfext  37807  cncfiooicclem1  37813  dvbdfbdioolem1  37842  itgsin0pilem1  37868  itgcoscmulx  37888  itgsincmulx  37893  fourierdlem20  38046  fourierdlem51  38078  fourierdlem54  38081  fourierdlem64  38091  fourierdlem73  38100  fourierdlem81  38108  fourierdlem102  38129  fourierdlem103  38130  fourierdlem104  38131  fourierdlem114  38141  etransclem46  38202  hoidmv1lelem1  38476