ovolicc1

Description: The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

	Ref	Expression
Hypotheses	ovolicc.1	$⊢ φ \to A \in ℝ$
	ovolicc.2	$⊢ φ \to B \in ℝ$
	ovolicc.3	$⊢ φ \to A \leq B$
	ovolicc1.4	$⊢ G = (n \in ℕ ⟼ if (n = 1, ⟨A, B⟩, ⟨0, 0⟩))$
Assertion	ovolicc1	$⊢ φ \to {vol}^{*} ([A, B]) \leq B - A$

Proof

Step	Hyp	Ref	Expression
1		ovolicc.1	$⊢ φ \to A \in ℝ$
2		ovolicc.2	$⊢ φ \to B \in ℝ$
3		ovolicc.3	$⊢ φ \to A \leq B$
4		ovolicc1.4	$⊢ G = (n \in ℕ ⟼ if (n = 1, ⟨A, B⟩, ⟨0, 0⟩))$
5		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
6	1 2 5	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
7		ovolcl	$⊢ [A, B] \subseteq ℝ \to {vol}^{} ([A, B]) \in ℝ^{}$
8	6 7	syl	$⊢ φ \to {vol}^{} ([A, B]) \in ℝ^{}$
9		df-br	$⊢ A \leq B \leftrightarrow ⟨A, B⟩ \in \leq$
10	3 9	sylib	$⊢ φ \to ⟨A, B⟩ \in \leq$
11	1 2	opelxpd	$⊢ φ \to ⟨A, B⟩ \in ℝ^{2}$
12	10 11	elind	$⊢ φ \to ⟨A, B⟩ \in (\leq \cap ℝ^{2})$
13	12	adantr	$⊢ (φ \land n \in ℕ) \to ⟨A, B⟩ \in (\leq \cap ℝ^{2})$
14		0le0	$⊢ 0 \leq 0$
15		df-br	$⊢ 0 \leq 0 \leftrightarrow ⟨0, 0⟩ \in \leq$
16	14 15	mpbi	$⊢ ⟨0, 0⟩ \in \leq$
17		0re	$⊢ 0 \in ℝ$
18		opelxpi	$⊢ (0 \in ℝ \land 0 \in ℝ) \to ⟨0, 0⟩ \in ℝ^{2}$
19	17 17 18	mp2an	$⊢ ⟨0, 0⟩ \in ℝ^{2}$
20	16 19	elini	$⊢ ⟨0, 0⟩ \in (\leq \cap ℝ^{2})$
21		ifcl	$⊢ (⟨A, B⟩ \in (\leq \cap ℝ^{2}) \land ⟨0, 0⟩ \in (\leq \cap ℝ^{2})) \to if (n = 1, ⟨A, B⟩, ⟨0, 0⟩) \in (\leq \cap ℝ^{2})$
22	13 20 21	sylancl	$⊢ (φ \land n \in ℕ) \to if (n = 1, ⟨A, B⟩, ⟨0, 0⟩) \in (\leq \cap ℝ^{2})$
23	22 4	fmptd	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
24		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
25		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ G)) = seq 1 (+ ((abs \circ -) \circ G))$
26	24 25	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ G)) : ℕ ⟶ [0, +∞)$
27	23 26	syl	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) : ℕ ⟶ [0, +∞)$
28	27	frnd	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq [0, +∞)$
29		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
30	28 29	sstrdi	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq ℝ^{*}$
31		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \in ℝ^{*}$
32	30 31	syl	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \in ℝ^{}$
33	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
34	33	rexrd	$⊢ φ \to B - A \in ℝ^{*}$
35		1nn	$⊢ 1 \in ℕ$
36	35	a1i	$⊢ (φ \land x \in [A, B]) \to 1 \in ℕ$
37		op1stg	$⊢ (A \in ℝ \land B \in ℝ) \to 1^{st} (⟨A, B⟩) = A$
38	1 2 37	syl2anc	$⊢ φ \to 1^{st} (⟨A, B⟩) = A$
39	38	adantr	$⊢ (φ \land x \in [A, B]) \to 1^{st} (⟨A, B⟩) = A$
40		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
41	1 2 40	syl2anc	$⊢ φ \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
42	41	biimpa	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
43	42	simp2d	$⊢ (φ \land x \in [A, B]) \to A \leq x$
44	39 43	eqbrtrd	$⊢ (φ \land x \in [A, B]) \to 1^{st} (⟨A, B⟩) \leq x$
45	42	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
46		op2ndg	$⊢ (A \in ℝ \land B \in ℝ) \to 2^{nd} (⟨A, B⟩) = B$
47	1 2 46	syl2anc	$⊢ φ \to 2^{nd} (⟨A, B⟩) = B$
48	47	adantr	$⊢ (φ \land x \in [A, B]) \to 2^{nd} (⟨A, B⟩) = B$
49	45 48	breqtrrd	$⊢ (φ \land x \in [A, B]) \to x \leq 2^{nd} (⟨A, B⟩)$
50		fveq2	$⊢ n = 1 \to G (n) = G (1)$
51		iftrue	$⊢ n = 1 \to if (n = 1, ⟨A, B⟩, ⟨0, 0⟩) = ⟨A, B⟩$
52		opex	$⊢ ⟨A, B⟩ \in V$
53	51 4 52	fvmpt	$⊢ 1 \in ℕ \to G (1) = ⟨A, B⟩$
54	35 53	ax-mp	$⊢ G (1) = ⟨A, B⟩$
55	50 54	eqtrdi	$⊢ n = 1 \to G (n) = ⟨A, B⟩$
56	55	fveq2d	$⊢ n = 1 \to 1^{st} (G (n)) = 1^{st} (⟨A, B⟩)$
57	56	breq1d	$⊢ n = 1 \to (1^{st} (G (n)) \leq x \leftrightarrow 1^{st} (⟨A, B⟩) \leq x)$
58	55	fveq2d	$⊢ n = 1 \to 2^{nd} (G (n)) = 2^{nd} (⟨A, B⟩)$
59	58	breq2d	$⊢ n = 1 \to (x \leq 2^{nd} (G (n)) \leftrightarrow x \leq 2^{nd} (⟨A, B⟩))$
60	57 59	anbi12d	$⊢ n = 1 \to ((1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))) \leftrightarrow (1^{st} (⟨A, B⟩) \leq x \land x \leq 2^{nd} (⟨A, B⟩)))$
61	60	rspcev	$⊢ (1 \in ℕ \land (1^{st} (⟨A, B⟩) \leq x \land x \leq 2^{nd} (⟨A, B⟩))) \to \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n)))$
62	36 44 49 61	syl12anc	$⊢ (φ \land x \in [A, B]) \to \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n)))$
63	62	ralrimiva	$⊢ φ \to \forall x \in [A, B] \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n)))$
64		ovolficc	$⊢ ([A, B] \subseteq ℝ \land G : ℕ ⟶ \leq \cap ℝ^{2}) \to ([A, B] \subseteq ⋃ ran ([.] \circ G) \leftrightarrow \forall x \in [A, B] \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
65	6 23 64	syl2anc	$⊢ φ \to ([A, B] \subseteq ⋃ ran ([.] \circ G) \leftrightarrow \forall x \in [A, B] \exists n \in ℕ (1^{st} (G (n)) \leq x \land x \leq 2^{nd} (G (n))))$
66	63 65	mpbird	$⊢ φ \to [A, B] \subseteq ⋃ ran ([.] \circ G)$
67	25	ovollb2	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land [A, B] \subseteq ⋃ ran ([.] \circ G)) \to {vol}^{} ([A, B]) \leq sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <)$
68	23 66 67	syl2anc	$⊢ φ \to {vol}^{} ([A, B]) \leq sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <)$
69		addrid	$⊢ k \in ℂ \to k + 0 = k$
70	69	adantl	$⊢ ((φ \land x \in ℕ) \land k \in ℂ) \to k + 0 = k$
71		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
72	35 71	eleqtri	$⊢ 1 \in ℤ_{\geq 1}$
73	72	a1i	$⊢ (φ \land x \in ℕ) \to 1 \in ℤ_{\geq 1}$
74		simpr	$⊢ (φ \land x \in ℕ) \to x \in ℕ$
75	74 71	eleqtrdi	$⊢ (φ \land x \in ℕ) \to x \in ℤ_{\geq 1}$
76		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
77	27	adantr	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) : ℕ ⟶ [0, +∞)$
78		ffvelcdm	$⊢ (seq 1 (+ ((abs \circ -) \circ G)) : ℕ ⟶ [0, +∞) \land 1 \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (1) \in [0, +∞)$
79	77 35 78	sylancl	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (1) \in [0, +∞)$
80	76 79	sselid	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (1) \in ℝ$
81	80	recnd	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (1) \in ℂ$
82	23	ad2antrr	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
83		elfzuz	$⊢ k \in (1 + 1 \dots x) \to k \in ℤ_{\geq (1 + 1)}$
84	83	adantl	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to k \in ℤ_{\geq (1 + 1)}$
85		df-2	$⊢ 2 = 1 + 1$
86	85	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
87	84 86	eleqtrrdi	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to k \in ℤ_{\geq 2}$
88		eluz2nn	$⊢ k \in ℤ_{\geq 2} \to k \in ℕ$
89	87 88	syl	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to k \in ℕ$
90	24	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land k \in ℕ) \to ((abs \circ -) \circ G) (k) = 2^{nd} (G (k)) - 1^{st} (G (k))$
91	82 89 90	syl2anc	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to ((abs \circ -) \circ G) (k) = 2^{nd} (G (k)) - 1^{st} (G (k))$
92		eqeq1	$⊢ n = k \to (n = 1 \leftrightarrow k = 1)$
93	92	ifbid	$⊢ n = k \to if (n = 1, ⟨A, B⟩, ⟨0, 0⟩) = if (k = 1, ⟨A, B⟩, ⟨0, 0⟩)$
94		opex	$⊢ ⟨0, 0⟩ \in V$
95	52 94	ifex	$⊢ if (k = 1, ⟨A, B⟩, ⟨0, 0⟩) \in V$
96	93 4 95	fvmpt	$⊢ k \in ℕ \to G (k) = if (k = 1, ⟨A, B⟩, ⟨0, 0⟩)$
97	89 96	syl	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to G (k) = if (k = 1, ⟨A, B⟩, ⟨0, 0⟩)$
98		eluz2b3	$⊢ k \in ℤ_{\geq 2} \leftrightarrow (k \in ℕ \land k \neq 1)$
99	98	simprbi	$⊢ k \in ℤ_{\geq 2} \to k \neq 1$
100	87 99	syl	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to k \neq 1$
101	100	neneqd	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to \neg k = 1$
102	101	iffalsed	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to if (k = 1, ⟨A, B⟩, ⟨0, 0⟩) = ⟨0, 0⟩$
103	97 102	eqtrd	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to G (k) = ⟨0, 0⟩$
104	103	fveq2d	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to 2^{nd} (G (k)) = 2^{nd} (⟨0, 0⟩)$
105		c0ex	$⊢ 0 \in V$
106	105 105	op2nd	$⊢ 2^{nd} (⟨0, 0⟩) = 0$
107	104 106	eqtrdi	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to 2^{nd} (G (k)) = 0$
108	103	fveq2d	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to 1^{st} (G (k)) = 1^{st} (⟨0, 0⟩)$
109	105 105	op1st	$⊢ 1^{st} (⟨0, 0⟩) = 0$
110	108 109	eqtrdi	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to 1^{st} (G (k)) = 0$
111	107 110	oveq12d	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to 2^{nd} (G (k)) - 1^{st} (G (k)) = 0 - 0$
112		0m0e0	$⊢ 0 - 0 = 0$
113	111 112	eqtrdi	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to 2^{nd} (G (k)) - 1^{st} (G (k)) = 0$
114	91 113	eqtrd	$⊢ ((φ \land x \in ℕ) \land k \in (1 + 1 \dots x)) \to ((abs \circ -) \circ G) (k) = 0$
115	70 73 75 81 114	seqid2	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (1) = seq 1 (+ ((abs \circ -) \circ G)) (x)$
116		1z	$⊢ 1 \in ℤ$
117	23	adantr	$⊢ (φ \land x \in ℕ) \to G : ℕ ⟶ \leq \cap ℝ^{2}$
118	24	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land 1 \in ℕ) \to ((abs \circ -) \circ G) (1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
119	117 35 118	sylancl	$⊢ (φ \land x \in ℕ) \to ((abs \circ -) \circ G) (1) = 2^{nd} (G (1)) - 1^{st} (G (1))$
120	54	fveq2i	$⊢ 2^{nd} (G (1)) = 2^{nd} (⟨A, B⟩)$
121	47	adantr	$⊢ (φ \land x \in ℕ) \to 2^{nd} (⟨A, B⟩) = B$
122	120 121	eqtrid	$⊢ (φ \land x \in ℕ) \to 2^{nd} (G (1)) = B$
123	54	fveq2i	$⊢ 1^{st} (G (1)) = 1^{st} (⟨A, B⟩)$
124	38	adantr	$⊢ (φ \land x \in ℕ) \to 1^{st} (⟨A, B⟩) = A$
125	123 124	eqtrid	$⊢ (φ \land x \in ℕ) \to 1^{st} (G (1)) = A$
126	122 125	oveq12d	$⊢ (φ \land x \in ℕ) \to 2^{nd} (G (1)) - 1^{st} (G (1)) = B - A$
127	119 126	eqtrd	$⊢ (φ \land x \in ℕ) \to ((abs \circ -) \circ G) (1) = B - A$
128	116 127	seq1i	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (1) = B - A$
129	115 128	eqtr3d	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (x) = B - A$
130	33	leidd	$⊢ φ \to B - A \leq B - A$
131	130	adantr	$⊢ (φ \land x \in ℕ) \to B - A \leq B - A$
132	129 131	eqbrtrd	$⊢ (φ \land x \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (x) \leq B - A$
133	132	ralrimiva	$⊢ φ \to \forall x \in ℕ seq 1 (+ ((abs \circ -) \circ G)) (x) \leq B - A$
134	27	ffnd	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) Fn ℕ$
135		breq1	$⊢ z = seq 1 (+ ((abs \circ -) \circ G)) (x) \to (z \leq B - A \leftrightarrow seq 1 (+ ((abs \circ -) \circ G)) (x) \leq B - A)$
136	135	ralrn	$⊢ seq 1 (+ ((abs \circ -) \circ G)) Fn ℕ \to (\forall z \in ran seq 1 (+ ((abs \circ -) \circ G)) z \leq B - A \leftrightarrow \forall x \in ℕ seq 1 (+ ((abs \circ -) \circ G)) (x) \leq B - A)$
137	134 136	syl	$⊢ φ \to (\forall z \in ran seq 1 (+ ((abs \circ -) \circ G)) z \leq B - A \leftrightarrow \forall x \in ℕ seq 1 (+ ((abs \circ -) \circ G)) (x) \leq B - A)$
138	133 137	mpbird	$⊢ φ \to \forall z \in ran seq 1 (+ ((abs \circ -) \circ G)) z \leq B - A$
139		supxrleub	$⊢ (ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq ℝ^{} \land B - A \in ℝ^{}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{*} <) \leq B - A \leftrightarrow \forall z \in ran seq 1 (+ ((abs \circ -) \circ G)) z \leq B - A)$
140	30 34 139	syl2anc	$⊢ φ \to (sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{*} <) \leq B - A \leftrightarrow \forall z \in ran seq 1 (+ ((abs \circ -) \circ G)) z \leq B - A)$
141	138 140	mpbird	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{*} <) \leq B - A$
142	8 32 34 68 141	xrletrd	$⊢ φ \to {vol}^{*} ([A, B]) \leq B - A$

Metamath Proof Explorer

Theorem ovolicc1

Proof