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 13303

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 12991	. . 3 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ 𝐵)
4	3	3ad2ant2 1134	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ≤ 𝐵)
5		elicc1 13229	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ^ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)))
6	5	3adant3 1132	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → (𝐵 ∈ (𝐴[,]𝐵) ↔ (𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵)))
7	1, 2, 4, 6	mpbir3and 1342	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1087 ∈ wcel 2106 class class class wbr 5097 (class class class)co 7342 ℝ^*cxr 11114 ≤ cle 11116 [,]cicc 13188

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 ax-cnex 11033 ax-resscn 11034 ax-pre-lttri 11051 ax-pre-lttrn 11052

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4858 df-br 5098 df-opab 5160 df-mpt 5181 df-id 5523 df-po 5537 df-so 5538 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-ov 7345 df-oprab 7346 df-mpo 7347 df-er 8574 df-en 8810 df-dom 8811 df-sdom 8812 df-pnf 11117 df-mnf 11118 df-xr 11119 df-ltxr 11120 df-le 11121 df-icc 13192

This theorem is referenced by: xnn0xrge0 13344 iccpnfcnv 24213 oprpiece1res2 24221 ivthlem2 24722 ivth2 24725 ivthle 24726 ivthle2 24727 dyadmaxlem 24867 cmvth 25261 mvth 25262 dvlip 25263 c1liplem1 25266 dvgt0lem1 25272 lhop1lem 25283 dvcnvrelem1 25287 dvcvx 25290 dvfsumle 25291 dvfsumge 25292 dvfsumabs 25293 dvfsumlem2 25297 ftc2 25314 ftc2ditglem 25315 itgparts 25317 itgsubstlem 25318 itgpowd 25320 efcvx 25714 pige3ALT 25782 cos0pilt1 25794 logccv 25924 loglesqrt 26017 pntlem3 26863 eliccioo 31490 xrge0iifcnv 32179 lmxrge0 32198 esumpinfval 32337 hashf2 32348 esumcvg 32350 ftc2re 32876 cvmliftlem7 33550 cvmliftlem10 33553 ivthALT 34661 ftc2nc 36013 areacirc 36024 iccintsng 43447 pnfel0pnf 43452 limcicciooub 43564 icccncfext 43814 dvbdfbdioolem1 43855 itgsin0pilem1 43877 itgcoscmulx 43896 itgsincmulx 43901 itgsubsticc 43903 fourierdlem20 44054 fourierdlem54 44087 fourierdlem64 44097 fourierdlem81 44114 fourierdlem102 44135 fourierdlem103 44136 fourierdlem104 44137 fourierdlem114 44147 etransclem46 44207

W3C validator