ovolicc2

Description: The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014)

	Ref	Expression
Hypotheses	ovolicc.1	$⊢ φ \to A \in ℝ$
	ovolicc.2	$⊢ φ \to B \in ℝ$
	ovolicc.3	$⊢ φ \to A \leq B$
	ovolicc2.m	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
Assertion	ovolicc2	$⊢ φ \to B - A \leq {vol}^{*} ([A, B])$

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		ovolicc2.m	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
5	4	elovolm	$⊢ z \in M \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
6		simprr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to [A, B] \subseteq ⋃ ran ((.) \circ f)$
7		unieq	$⊢ u = ran ((.) \circ f) \to ⋃ u = ⋃ ran ((.) \circ f)$
8	7	sseq2d	$⊢ u = ran ((.) \circ f) \to ([A, B] \subseteq ⋃ u \leftrightarrow [A, B] \subseteq ⋃ ran ((.) \circ f))$
9		pweq	$⊢ u = ran ((.) \circ f) \to 𝒫 u = 𝒫 ran ((.) \circ f)$
10	9	ineq1d	$⊢ u = ran ((.) \circ f) \to 𝒫 u \cap Fin = 𝒫 ran ((.) \circ f) \cap Fin$
11	10	rexeqdv	$⊢ u = ran ((.) \circ f) \to (\exists v \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ v \leftrightarrow \exists v \in (𝒫 ran ((.) \circ f) \cap Fin) [A, B] \subseteq ⋃ v)$
12	8 11	imbi12d	$⊢ u = ran ((.) \circ f) \to (([A, B] \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ v) \leftrightarrow ([A, B] \subseteq ⋃ ran ((.) \circ f) \to \exists v \in (𝒫 ran ((.) \circ f) \cap Fin) [A, B] \subseteq ⋃ v))$
13		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
14		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
15	13 14	icccmp	$⊢ (A \in ℝ \land B \in ℝ) \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Comp$
16	1 2 15	syl2anc	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [A, B] \in Comp$
17		retop	$⊢ topGen (ran (.)) \in Top$
18		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
19	1 2 18	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
20		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
21	20	cmpsub	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in Comp \leftrightarrow \forall u \in 𝒫 topGen (ran (.)) ([A, B] \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ v))$
22	17 19 21	sylancr	$⊢ φ \to (topGen (ran (.)) ↾_{𝑡} [A, B] \in Comp \leftrightarrow \forall u \in 𝒫 topGen (ran (.)) ([A, B] \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ v))$
23	16 22	mpbid	$⊢ φ \to \forall u \in 𝒫 topGen (ran (.)) ([A, B] \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ v)$
24	23	adantr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to \forall u \in 𝒫 topGen (ran (.)) ([A, B] \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ v)$
25		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
26		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
27	25 26	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
28		dffn3	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \leftrightarrow (.) : ℝ^{} \times ℝ^{} ⟶ ran (.)$
29	27 28	mpbi	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ ran (.)$
30		elovolmlem	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow f : ℕ ⟶ \leq \cap ℝ^{2}$
31	30	bilani	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
32		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
33		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
34	32 33	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
35		fss	$⊢ (f : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
36	31 34 35	sylancl	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
37		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ ran (.) \land f : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ f) : ℕ ⟶ ran (.)$
38	29 36 37	sylancr	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((.) \circ f) : ℕ ⟶ ran (.)$
39	38	adantrr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ((.) \circ f) : ℕ ⟶ ran (.)$
40	39	frnd	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ran ((.) \circ f) \subseteq ran (.)$
41		retopbas	$⊢ ran (.) \in TopBases$
42		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
43	41 42	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
44	40 43	sstrdi	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ran ((.) \circ f) \subseteq topGen (ran (.))$
45		fvex	$⊢ topGen (ran (.)) \in V$
46	45	elpw2	$⊢ ran ((.) \circ f) \in 𝒫 topGen (ran (.)) \leftrightarrow ran ((.) \circ f) \subseteq topGen (ran (.))$
47	44 46	sylibr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ran ((.) \circ f) \in 𝒫 topGen (ran (.))$
48	12 24 47	rspcdva	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ([A, B] \subseteq ⋃ ran ((.) \circ f) \to \exists v \in (𝒫 ran ((.) \circ f) \cap Fin) [A, B] \subseteq ⋃ v)$
49	6 48	mpd	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to \exists v \in (𝒫 ran ((.) \circ f) \cap Fin) [A, B] \subseteq ⋃ v$
50		simprl	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to v \in (𝒫 ran ((.) \circ f) \cap Fin)$
51		elin	$⊢ v \in (𝒫 ran ((.) \circ f) \cap Fin) \leftrightarrow (v \in 𝒫 ran ((.) \circ f) \land v \in Fin)$
52	50 51	sylib	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to (v \in 𝒫 ran ((.) \circ f) \land v \in Fin)$
53	52	simprd	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to v \in Fin$
54	52	simpld	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to v \in 𝒫 ran ((.) \circ f)$
55	54	elpwid	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to v \subseteq ran ((.) \circ f)$
56	55	sseld	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to (t \in v \to t \in ran ((.) \circ f))$
57	38	ffnd	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((.) \circ f) Fn ℕ$
58	57	adantr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to ((.) \circ f) Fn ℕ$
59		fvelrnb	$⊢ ((.) \circ f) Fn ℕ \to (t \in ran ((.) \circ f) \leftrightarrow \exists k \in ℕ ((.) \circ f) (k) = t)$
60	58 59	syl	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to (t \in ran ((.) \circ f) \leftrightarrow \exists k \in ℕ ((.) \circ f) (k) = t)$
61	56 60	sylibd	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to (t \in v \to \exists k \in ℕ ((.) \circ f) (k) = t)$
62	61	ralrimiv	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to \forall t \in v \exists k \in ℕ ((.) \circ f) (k) = t$
63		fveqeq2	$⊢ k = g (t) \to (((.) \circ f) (k) = t \leftrightarrow ((.) \circ f) (g (t)) = t)$
64	63	ac6sfi	$⊢ (v \in Fin \land \forall t \in v \exists k \in ℕ ((.) \circ f) (k) = t) \to \exists g (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t)$
65	53 62 64	syl2anc	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to \exists g (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t)$
66	1	ad2antrr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to A \in ℝ$
67	2	ad2antrr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to B \in ℝ$
68	3	ad2antrr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to A \leq B$
69		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
70	31	adantr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
71		simprll	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to v \in (𝒫 ran ((.) \circ f) \cap Fin)$
72		simprlr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to [A, B] \subseteq ⋃ v$
73		simprrl	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to g : v ⟶ ℕ$
74		simprrr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to \forall t \in v ((.) \circ f) (g (t)) = t$
75		2fveq3	$⊢ t = x \to ((.) \circ f) (g (t)) = ((.) \circ f) (g (x))$
76		id	$⊢ t = x \to t = x$
77	75 76	eqeq12d	$⊢ t = x \to (((.) \circ f) (g (t)) = t \leftrightarrow ((.) \circ f) (g (x)) = x)$
78	77	rspccva	$⊢ (\forall t \in v ((.) \circ f) (g (t)) = t \land x \in v) \to ((.) \circ f) (g (x)) = x$
79	74 78	sylan	$⊢ (((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \land x \in v) \to ((.) \circ f) (g (x)) = x$
80		eqid	$⊢ \{u \in v \| u \cap [A, B] \neq \emptyset\} = \{u \in v \| u \cap [A, B] \neq \emptyset\}$
81	66 67 68 69 70 71 72 73 79 80	ovolicc2lem5	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land ((v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v) \land (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t))) \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
82	81	expr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to ((g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t) \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
83	82	exlimdv	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to (\exists g (g : v ⟶ ℕ \land \forall t \in v ((.) \circ f) (g (t)) = t) \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
84	65 83	mpd	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
85	84	rexlimdvaa	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (\exists v \in (𝒫 ran ((.) \circ f) \cap Fin) [A, B] \subseteq ⋃ v \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
86	85	adantrr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to (\exists v \in (𝒫 ran ((.) \circ f) \cap Fin) [A, B] \subseteq ⋃ v \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
87	49 86	mpd	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
88		breq2	$⊢ z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \to (B - A \leq z \leftrightarrow B - A \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
89	87 88	syl5ibrcom	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to (z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <) \to B - A \leq z)$
90	89	expr	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ([A, B] \subseteq ⋃ ran ((.) \circ f) \to (z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <) \to B - A \leq z))$
91	90	impd	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (([A, B] \subseteq ⋃ ran ((.) \circ f) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)) \to B - A \leq z)$
92	91	rexlimdva	$⊢ φ \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)) \to B - A \leq z)$
93	5 92	biimtrid	$⊢ φ \to (z \in M \to B - A \leq z)$
94	93	ralrimiv	$⊢ φ \to \forall z \in M B - A \leq z$
95	4	ssrab3	$⊢ M \subseteq ℝ^{*}$
96	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
97	96	rexrd	$⊢ φ \to B - A \in ℝ^{*}$
98		infxrgelb	$⊢ (M \subseteq ℝ^{} \land B - A \in ℝ^{}) \to (B - A \leq inf (M ℝ^{*} <) \leftrightarrow \forall z \in M B - A \leq z)$
99	95 97 98	sylancr	$⊢ φ \to (B - A \leq inf (M ℝ^{*} <) \leftrightarrow \forall z \in M B - A \leq z)$
100	94 99	mpbird	$⊢ φ \to B - A \leq inf (M ℝ^{*} <)$
101	4	ovolval	$⊢ [A, B] \subseteq ℝ \to {vol}^{} ([A, B]) = inf (M ℝ^{} <)$
102	19 101	syl	$⊢ φ \to {vol}^{} ([A, B]) = inf (M ℝ^{} <)$
103	100 102	breqtrrd	$⊢ φ \to B - A \leq {vol}^{*} ([A, B])$

Metamath Proof Explorer

Theorem ovolicc2

Proof