elico2 - Metamath Proof Explorer

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

Theorem elico2 13534

Description: Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)

**Assertion**
Ref	Expression
elico2	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))

**Proof of Theorem elico2**
Step	Hyp	Ref	Expression
1		rexr 11348	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
2		elico1 13512	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
3	1, 2	sylan 592	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
4		mnfxr 11359	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
5	4	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ ∈ ℝ^*)
6	1	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐴 ∈ ℝ^*)
7		simpr1 1213	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈ ℝ^*)
8		mnflt 13245	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
9	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ < 𝐴)
10		simpr2 1214	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐴 ≤ 𝐶)
11	5, 6, 7, 9, 10	xrltletrd 13283	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → -∞ < 𝐶)
12		simplr 781	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐵 ∈ ℝ^*)
13		pnfxr 11356	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
14	13	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → +∞ ∈ ℝ^*)
15		simpr3 1215	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 < 𝐵)
16		pnfge 13252	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ^* → 𝐵 ≤ +∞)
17	16	ad2antlr 740	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐵 ≤ +∞)
18	7, 12, 14, 15, 17	xrltletrd 13283	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 < +∞)
19		xrrebnd 13291	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
20	7, 19	syl 18	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞)))
21	11, 18, 20	mpbir2and 726	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → 𝐶 ∈ ℝ)
22	21, 10, 15	3jca 1146	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) ∧ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))
23	22	ex 418	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → ((𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
24		rexr 11348	. . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ^*)
25	24	3anim1i 1170	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → (𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))
26	23, 25	impbid1 228	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^) → ((𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
27	3, 26	bitrd 282	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∈ wcel 2145 class class class wbr 5103 (class class class)co 7418 ℝcr 11192 +∞cpnf 11333 -∞cmnf 11334 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 [,)cico 13471

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-pre-lttri 11267 ax-pre-lttrn 11268

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-po 5559 df-so 5560 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7421 df-oprab 7422 df-mpo 7423 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-ico 13475

This theorem is used by: icossre 13552 elicopnf 13569 icoshft 13597 nnge2recico01 13631 modelico 14014 muladdmodid 14046 icodiamlt 15598 fprodge0 16153 fprodge1 16155 rge0srg 21737 metustexhalf 24868 cnbl0 25085 icoopnst 25253 iocopnst 25254 icopnfcnv 25256 icopnfhmeo 25257 iccpnfcnv 25258 psercnlem2 26744 psercnlem1 26745 psercn 26746 abelth 26761 cosq34lt1 26848 tanord1 26858 tanord 26859 efopnlem1 26977 logtayl 26981 rlimcnp 27286 rlimcnp2 27287 dchrvmasumlem2 27818 dchrvmasumiflem1 27821 pntlemb 27917 pnt 27934 ubico 33360 xrge0slmod 33902 voliune 34855 volfiniune 34856 dya2icoseg 34902 sibfinima 34964 relowlpssretop 38267 tan2h 38515 itg2addnclem2 38570 binomcxplemdvbinom 45322 binomcxplemcvg 45323 binomcxplemnotnn0 45325 limciccioolb 46602 fourierdlem32 47118 fourierdlem43 47129 fourierdlem63 47148 fourierdlem79 47164 fouriersw 47210 flmrecm1 48382 expnegico01 49599 dignnld 49684 eenglngeehlnmlem1 49818 i0oii 49997 sepfsepc 50005

W3C validator