ubicc2 - Metamath Proof Explorer

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

Theorem ubicc2 12703

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

**Assertion**
Ref	Expression
ubicc2	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))

**Proof of Theorem ubicc2**
Step	Hyp	Ref	Expression
1		simp2 1130	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ^*)
2		simp3 1131	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵)
3		xrleid 12394	. . 3 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ 𝐵)
4	3	3ad2ant2 1127	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ 𝐵)
5		elicc1 12632	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ^ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)))
6	5	3adant3 1125	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)))
7	1, 2, 4, 6	mpbir3and 1335	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1080 ∈ wcel 2080 class class class wbr 4964 (class class class)co 7019 ℝ^*cxr 10523 ≤ cle 10525 [,]cicc 12591

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-cnex 10442 ax-resscn 10443 ax-pre-lttri 10460 ax-pre-lttrn 10461

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-po 5365 df-so 5366 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-ov 7022 df-oprab 7023 df-mpo 7024 df-er 8142 df-en 8361 df-dom 8362 df-sdom 8363 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-icc 12595

This theorem is referenced by: xnn0xrge0 12741 iccpnfcnv 23231 oprpiece1res2 23239 ivthlem2 23736 ivth2 23739 ivthle 23740 ivthle2 23741 dyadmaxlem 23881 cmvth 24271 mvth 24272 dvlip 24273 c1liplem1 24276 dvgt0lem1 24282 lhop1lem 24293 dvcnvrelem1 24297 dvcvx 24300 dvfsumle 24301 dvfsumge 24302 dvfsumabs 24303 dvfsumlem2 24307 ftc2 24324 ftc2ditglem 24325 itgparts 24327 itgsubstlem 24328 efcvx 24720 pige3ALT 24788 logccv 24927 loglesqrt 25020 pntlem3 25867 eliccioo 30283 xrge0iifcnv 30785 lmxrge0 30804 esumpinfval 30941 hashf2 30952 esumcvg 30954 ftc2re 31478 cvmliftlem7 32140 cvmliftlem10 32143 ivthALT 33286 ftc2nc 34520 areacirc 34531 itgpowd 39319 iccintsng 41354 pnfel0pnf 41359 limcicciooub 41473 icccncfext 41725 dvbdfbdioolem1 41768 itgsin0pilem1 41790 itgcoscmulx 41809 itgsincmulx 41814 itgsubsticc 41816 fourierdlem20 41968 fourierdlem54 42001 fourierdlem64 42011 fourierdlem81 42028 fourierdlem102 42049 fourierdlem103 42050 fourierdlem104 42051 fourierdlem114 42061 etransclem46 42121

W3C validator