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 13381

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 1137	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ^*)
2		simp3 1138	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵)
3		xrleid 13065	. . 3 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ 𝐵)
4	3	3ad2ant2 1134	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ 𝐵)
5		elicc1 13305	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ^ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)))
6	5	3adant3 1132	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)))
7	1, 2, 4, 6	mpbir3and 1343	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1086 ∈ wcel 2113 class class class wbr 5098 (class class class)co 7358 ℝ^*cxr 11165 ≤ cle 11167 [,]cicc 13264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-pre-lttri 11100 ax-pre-lttrn 11101

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-po 5532 df-so 5533 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7361 df-oprab 7362 df-mpo 7363 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-icc 13268

This theorem is referenced by: xnn0xrge0 13422 iccpnfcnv 24898 oprpiece1res2 24906 ivthlem2 25409 ivth2 25412 ivthle 25413 ivthle2 25414 dyadmaxlem 25554 cmvth 25951 cmvthOLD 25952 mvth 25953 dvlip 25954 c1liplem1 25957 dvgt0lem1 25963 lhop1lem 25974 dvcnvrelem1 25978 dvcvx 25981 dvfsumle 25982 dvfsumleOLD 25983 dvfsumge 25984 dvfsumabs 25985 dvfsumlem2 25989 dvfsumlem2OLD 25990 ftc2 26007 ftc2ditglem 26008 itgparts 26010 itgsubstlem 26011 itgpowd 26013 efcvx 26415 pige3ALT 26485 cos0pilt1 26497 logccv 26628 loglesqrt 26727 pntlem3 27576 eliccioo 33012 xrge0iifcnv 34090 lmxrge0 34109 esumpinfval 34230 hashf2 34241 esumcvg 34243 ftc2re 34755 cvmliftlem7 35485 cvmliftlem10 35488 ivthALT 36529 ftc2nc 37903 areacirc 37914 iccintsng 45769 pnfel0pnf 45774 limcicciooub 45881 icccncfext 46131 dvbdfbdioolem1 46172 itgsin0pilem1 46194 itgcoscmulx 46213 itgsincmulx 46218 itgsubsticc 46220 fourierdlem20 46371 fourierdlem54 46404 fourierdlem64 46414 fourierdlem81 46431 fourierdlem102 46452 fourierdlem103 46453 fourierdlem104 46454 fourierdlem114 46464 etransclem46 46524

W3C validator