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 13402

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 13087	. . 3 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ 𝐵)
4	3	3ad2ant2 1134	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ 𝐵)
5		elicc1 13326	. . 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 2109 class class class wbr 5102 (class class class)co 7369 ℝ^*cxr 11183 ≤ cle 11185 [,]cicc 13285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-pre-lttri 11118 ax-pre-lttrn 11119

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-icc 13289

This theorem is referenced by: xnn0xrge0 13443 iccpnfcnv 24818 oprpiece1res2 24826 ivthlem2 25329 ivth2 25332 ivthle 25333 ivthle2 25334 dyadmaxlem 25474 cmvth 25871 cmvthOLD 25872 mvth 25873 dvlip 25874 c1liplem1 25877 dvgt0lem1 25883 lhop1lem 25894 dvcnvrelem1 25898 dvcvx 25901 dvfsumle 25902 dvfsumleOLD 25903 dvfsumge 25904 dvfsumabs 25905 dvfsumlem2 25909 dvfsumlem2OLD 25910 ftc2 25927 ftc2ditglem 25928 itgparts 25930 itgsubstlem 25931 itgpowd 25933 efcvx 26335 pige3ALT 26405 cos0pilt1 26417 logccv 26548 loglesqrt 26647 pntlem3 27496 eliccioo 32824 xrge0iifcnv 33896 lmxrge0 33915 esumpinfval 34036 hashf2 34047 esumcvg 34049 ftc2re 34562 cvmliftlem7 35251 cvmliftlem10 35254 ivthALT 36296 ftc2nc 37669 areacirc 37680 iccintsng 45494 pnfel0pnf 45499 limcicciooub 45608 icccncfext 45858 dvbdfbdioolem1 45899 itgsin0pilem1 45921 itgcoscmulx 45940 itgsincmulx 45945 itgsubsticc 45947 fourierdlem20 46098 fourierdlem54 46131 fourierdlem64 46141 fourierdlem81 46158 fourierdlem102 46179 fourierdlem103 46180 fourierdlem104 46181 fourierdlem114 46191 etransclem46 46251

W3C validator