ovolicopnf

Description: The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014)

		Ref	Expression
	Assertion	ovolicopnf	$⊢ A \in ℝ \to {vol}^{*} ([A, +∞)) = +∞$

Proof

Step	Hyp	Ref	Expression
1		pnfxr	$⊢ +∞ \in ℝ^{*}$
2		icossre	$⊢ (A \in ℝ \land +∞ \in ℝ^{*}) \to [A, +∞) \subseteq ℝ$
3	1 2	mpan2	$⊢ A \in ℝ \to [A, +∞) \subseteq ℝ$
4	3	adantr	$⊢ (A \in ℝ \land {vol}^{*} ([A, +∞)) < +∞) \to [A, +∞) \subseteq ℝ$
5		ovolge0	$⊢ [A, +∞) \subseteq ℝ \to 0 \leq {vol}^{*} ([A, +∞))$
6	4 5	syl	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to 0 \leq {vol}^{} ([A, +∞))$
7		mnflt0	$⊢ −∞ < 0$
8		mnfxr	$⊢ −∞ \in ℝ^{*}$
9		0xr	$⊢ 0 \in ℝ^{*}$
10		ovolcl	$⊢ [A, +∞) \subseteq ℝ \to {vol}^{} ([A, +∞)) \in ℝ^{}$
11	3 10	syl	$⊢ A \in ℝ \to {vol}^{} ([A, +∞)) \in ℝ^{}$
12	11	adantr	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) \in ℝ^{*}$
13		xrltletr	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land {vol}^{} ([A, +∞)) \in ℝ^{}) \to ((−∞ < 0 \land 0 \leq {vol}^{} ([A, +∞))) \to −∞ < {vol}^{} ([A, +∞)))$
14	8 9 12 13	mp3an12i	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to ((−∞ < 0 \land 0 \leq {vol}^{} ([A, +∞))) \to −∞ < {vol}^{*} ([A, +∞)))$
15	7 14	mpani	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to (0 \leq {vol}^{} ([A, +∞)) \to −∞ < {vol}^{*} ([A, +∞)))$
16	6 15	mpd	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to −∞ < {vol}^{} ([A, +∞))$
17		simpr	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) < +∞$
18		xrrebnd	$⊢ {vol}^{} ([A, +∞)) \in ℝ^{} \to ({vol}^{} ([A, +∞)) \in ℝ \leftrightarrow (−∞ < {vol}^{} ([A, +∞)) \land {vol}^{*} ([A, +∞)) < +∞))$
19	12 18	syl	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to ({vol}^{} ([A, +∞)) \in ℝ \leftrightarrow (−∞ < {vol}^{} ([A, +∞)) \land {vol}^{} ([A, +∞)) < +∞))$
20	16 17 19	mpbir2and	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) \in ℝ$
21	20	ltp1d	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) < {vol}^{*} ([A, +∞)) + 1$
22		peano2re	$⊢ {vol}^{} ([A, +∞)) \in ℝ \to {vol}^{} ([A, +∞)) + 1 \in ℝ$
23	20 22	syl	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) + 1 \in ℝ$
24		simpl	$⊢ (A \in ℝ \land {vol}^{*} ([A, +∞)) < +∞) \to A \in ℝ$
25	23 24	readdcld	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) + 1 + A \in ℝ$
26		0red	$⊢ (A \in ℝ \land {vol}^{*} ([A, +∞)) < +∞) \to 0 \in ℝ$
27	20	lep1d	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) \leq {vol}^{*} ([A, +∞)) + 1$
28	26 20 23 6 27	letrd	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to 0 \leq {vol}^{} ([A, +∞)) + 1$
29	24 23	addge02d	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to (0 \leq {vol}^{} ([A, +∞)) + 1 \leftrightarrow A \leq {vol}^{*} ([A, +∞)) + 1 + A)$
30	28 29	mpbid	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to A \leq {vol}^{} ([A, +∞)) + 1 + A$
31		ovolicc	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) + 1 + A \in ℝ \land A \leq {vol}^{} ([A, +∞)) + 1 + A) \to {vol}^{} ([A, {vol}^{} ([A, +∞)) + 1 + A]) = ({vol}^{*} ([A, +∞)) + 1) + A - A$
32	24 25 30 31	syl3anc	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, {vol}^{} ([A, +∞)) + 1 + A]) = ({vol}^{} ([A, +∞)) + 1) + A - A$
33	23	recnd	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) + 1 \in ℂ$
34	24	recnd	$⊢ (A \in ℝ \land {vol}^{*} ([A, +∞)) < +∞) \to A \in ℂ$
35	33 34	pncand	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to ({vol}^{} ([A, +∞)) + 1) + A - A = {vol}^{*} ([A, +∞)) + 1$
36	32 35	eqtrd	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, {vol}^{} ([A, +∞)) + 1 + A]) = {vol}^{} ([A, +∞)) + 1$
37		elicc2	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) + 1 + A \in ℝ) \to (x \in [A, {vol}^{} ([A, +∞)) + 1 + A] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq {vol}^{*} ([A, +∞)) + 1 + A))$
38	24 25 37	syl2anc	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to (x \in [A, {vol}^{} ([A, +∞)) + 1 + A] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq {vol}^{*} ([A, +∞)) + 1 + A))$
39	38	biimpa	$⊢ ((A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \land x \in [A, {vol}^{} ([A, +∞)) + 1 + A]) \to (x \in ℝ \land A \leq x \land x \leq {vol}^{*} ([A, +∞)) + 1 + A)$
40	39	simp1d	$⊢ ((A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \land x \in [A, {vol}^{} ([A, +∞)) + 1 + A]) \to x \in ℝ$
41	39	simp2d	$⊢ ((A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \land x \in [A, {vol}^{} ([A, +∞)) + 1 + A]) \to A \leq x$
42		elicopnf	$⊢ A \in ℝ \to (x \in [A, +∞) \leftrightarrow (x \in ℝ \land A \leq x))$
43	42	ad2antrr	$⊢ ((A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \land x \in [A, {vol}^{} ([A, +∞)) + 1 + A]) \to (x \in [A, +∞) \leftrightarrow (x \in ℝ \land A \leq x))$
44	40 41 43	mpbir2and	$⊢ ((A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \land x \in [A, {vol}^{} ([A, +∞)) + 1 + A]) \to x \in [A, +∞)$
45	44	ex	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to (x \in [A, {vol}^{} ([A, +∞)) + 1 + A] \to x \in [A, +∞))$
46	45	ssrdv	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to [A, {vol}^{} ([A, +∞)) + 1 + A] \subseteq [A, +∞)$
47		ovolss	$⊢ ([A, {vol}^{} ([A, +∞)) + 1 + A] \subseteq [A, +∞) \land [A, +∞) \subseteq ℝ) \to {vol}^{} ([A, {vol}^{} ([A, +∞)) + 1 + A]) \leq {vol}^{} ([A, +∞))$
48	46 4 47	syl2anc	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, {vol}^{} ([A, +∞)) + 1 + A]) \leq {vol}^{} ([A, +∞))$
49	36 48	eqbrtrrd	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to {vol}^{} ([A, +∞)) + 1 \leq {vol}^{*} ([A, +∞))$
50	23 20 49	lensymd	$⊢ (A \in ℝ \land {vol}^{} ([A, +∞)) < +∞) \to \neg {vol}^{} ([A, +∞)) < {vol}^{*} ([A, +∞)) + 1$
51	21 50	pm2.65da	$⊢ A \in ℝ \to \neg {vol}^{*} ([A, +∞)) < +∞$
52		nltpnft	$⊢ {vol}^{} ([A, +∞)) \in ℝ^{} \to ({vol}^{} ([A, +∞)) = +∞ \leftrightarrow \neg {vol}^{} ([A, +∞)) < +∞)$
53	11 52	syl	$⊢ A \in ℝ \to ({vol}^{} ([A, +∞)) = +∞ \leftrightarrow \neg {vol}^{} ([A, +∞)) < +∞)$
54	51 53	mpbird	$⊢ A \in ℝ \to {vol}^{*} ([A, +∞)) = +∞$

Metamath Proof Explorer

Theorem ovolicopnf

Proof