lbicc2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lbicc2		Structured version Visualization version GIF version

Theorem lbicc2 13467

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	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))

**Proof of Theorem lbicc2**
Step	Hyp	Ref	Expression
1		simp1 1134	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ^*)
2		xrleid 13156	. . 3 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ 𝐴)
3	2	3ad2ant1 1131	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐴)
4		simp3 1136	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵)
5		elicc1 13394	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ^ ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)))
6	5	3adant3 1130	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ^* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)))
7	1, 3, 4, 6	mpbir3and 1340	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1085 ∈ wcel 2099 class class class wbr 5142 (class class class)co 7414 ℝ^*cxr 11271 ≤ cle 11273 [,]cicc 13353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11188 ax-resscn 11189 ax-pre-lttri 11206 ax-pre-lttrn 11207

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5570 df-po 5584 df-so 5585 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7417 df-oprab 7418 df-mpo 7419 df-er 8718 df-en 8958 df-dom 8959 df-sdom 8960 df-pnf 11274 df-mnf 11275 df-xr 11276 df-ltxr 11277 df-le 11278 df-icc 13357

This theorem is referenced by: icccmplem1 24731 reconnlem2 24736 oprpiece1res1 24869 pcoass 24944 ivthlem1 25373 ivth2 25377 ivthle 25378 ivthle2 25379 evthicc 25381 ovolicc2lem5 25443 dyadmaxlem 25519 rolle 25915 cmvth 25916 cmvthOLD 25917 mvth 25918 dvlip 25919 c1liplem1 25922 dveq0 25926 dvgt0lem1 25928 lhop1lem 25939 dvcnvrelem1 25943 dvcvx 25946 dvfsumle 25947 dvfsumleOLD 25948 dvfsumge 25949 dvfsumabs 25950 dvfsumlem2 25954 dvfsumlem2OLD 25955 ftc2 25972 ftc2ditglem 25973 itgparts 25975 itgsubstlem 25976 itgpowd 25978 taylfval 26286 tayl0 26289 efcvx 26379 pige3ALT 26447 logccv 26590 loglesqrt 26686 eliccioo 32648 ftc2re 34224 cvmliftlem6 34894 cvmliftlem8 34896 cvmliftlem9 34897 cvmliftlem10 34898 cvmliftlem13 34900 ivthALT 35813 ftc2nc 37169 areacirc 37180 iccintsng 44902 icccncfext 45269 cncfiooicclem1 45275 dvbdfbdioolem1 45310 itgsin0pilem1 45332 itgcoscmulx 45351 itgsincmulx 45356 fourierdlem20 45509 fourierdlem51 45539 fourierdlem54 45542 fourierdlem64 45552 fourierdlem73 45561 fourierdlem81 45569 fourierdlem102 45590 fourierdlem103 45591 fourierdlem104 45592 fourierdlem114 45602 etransclem46 45662 hoidmv1lelem1 45973

W3C validator

	
		OSZAR »