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		simpr	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to f \in ({(\leq \cap ℝ^{2})}^{ℕ})$
31		elovolmlem	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow f : ℕ ⟶ \leq \cap ℝ^{2}$
32	30 31	sylib	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
33		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
34		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
35	33 34	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
36		fss	$⊢ (f : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
37	32 35 36	sylancl	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
38		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ ran (.) \land f : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ f) : ℕ ⟶ ran (.)$
39	29 37 38	sylancr	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((.) \circ f) : ℕ ⟶ ran (.)$
40	39	adantrr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ((.) \circ f) : ℕ ⟶ ran (.)$
41	40	frnd	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ran ((.) \circ f) \subseteq ran (.)$
42		retopbas	$⊢ ran (.) \in TopBases$
43		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
44	42 43	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
45	41 44	sstrdi	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ran ((.) \circ f) \subseteq topGen (ran (.))$
46		fvex	$⊢ topGen (ran (.)) \in V$
47	46	elpw2	$⊢ ran ((.) \circ f) \in 𝒫 topGen (ran (.)) \leftrightarrow ran ((.) \circ f) \subseteq topGen (ran (.))$
48	45 47	sylibr	$⊢ (φ \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land [A, B] \subseteq ⋃ ran ((.) \circ f))) \to ran ((.) \circ f) \in 𝒫 topGen (ran (.))$
49	12 24 48	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)$
50	6 49	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$
51		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)$
52		elin	$⊢ v \in (𝒫 ran ((.) \circ f) \cap Fin) \leftrightarrow (v \in 𝒫 ran ((.) \circ f) \land v \in Fin)$
53	51 52	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)$
54	53	simprd	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to v \in Fin$
55	53	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)$
56	55	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)$
57	56	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))$
58	39	ffnd	$⊢ (φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((.) \circ f) Fn ℕ$
59	58	adantr	$⊢ ((φ \land f \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land (v \in (𝒫 ran ((.) \circ f) \cap Fin) \land [A, B] \subseteq ⋃ v)) \to ((.) \circ f) Fn ℕ$
60		fvelrnb	$⊢ ((.) \circ f) Fn ℕ \to (t \in ran ((.) \circ f) \leftrightarrow \exists k \in ℕ ((.) \circ f) (k) = t)$
61	59 60	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)$
62	57 61	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)$
63	62	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$
64		fveqeq2	$⊢ k = g (t) \to (((.) \circ f) (k) = t \leftrightarrow ((.) \circ f) (g (t)) = t)$
65	64	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)$
66	54 63 65	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)$
67	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 ℝ$
68	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 ℝ$
69	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$
70		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
71	32	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}$
72		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)$
73		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$
74		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 ⟶ ℕ$
75		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$
76		2fveq3	$⊢ t = x \to ((.) \circ f) (g (t)) = ((.) \circ f) (g (x))$
77		id	$⊢ t = x \to t = x$
78	76 77	eqeq12d	$⊢ t = x \to (((.) \circ f) (g (t)) = t \leftrightarrow ((.) \circ f) (g (x)) = x)$
79	78	rspccva	$⊢ (\forall t \in v ((.) \circ f) (g (t)) = t \land x \in v) \to ((.) \circ f) (g (x)) = x$
80	75 79	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$
81		eqid	$⊢ \{u \in v \| u \cap [A, B] \neq \emptyset\} = \{u \in v \| u \cap [A, B] \neq \emptyset\}$
82	67 68 69 70 71 72 73 74 80 81	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)) ℝ^{*} <)$
83	82	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)) ℝ^{*} <))$
84	83	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)) ℝ^{*} <))$
85	66 84	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)) ℝ^{*} <)$
86	85	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)) ℝ^{*} <))$
87	86	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)) ℝ^{*} <))$
88	50 87	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)) ℝ^{*} <)$
89		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)) ℝ^{} <))$
90	88 89	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)$
91	90	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))$
92	91	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)$
93	92	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)$
94	5 93	syl5bi	$⊢ φ \to (z \in M \to B - A \leq z)$
95	94	ralrimiv	$⊢ φ \to \forall z \in M B - A \leq z$
96	4	ssrab3	$⊢ M \subseteq ℝ^{*}$
97	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
98	97	rexrd	$⊢ φ \to B - A \in ℝ^{*}$
99		infxrgelb	$⊢ (M \subseteq ℝ^{} \land B - A \in ℝ^{}) \to (B - A \leq sup (M ℝ^{*} <) \leftrightarrow \forall z \in M B - A \leq z)$
100	96 98 99	sylancr	$⊢ φ \to (B - A \leq sup (M ℝ^{*} <) \leftrightarrow \forall z \in M B - A \leq z)$
101	95 100	mpbird	$⊢ φ \to B - A \leq sup (M ℝ^{*} <)$
102	4	ovolval	$⊢ [A, B] \subseteq ℝ \to {vol}^{} ([A, B]) = sup (M ℝ^{} <)$
103	19 102	syl	$⊢ φ \to {vol}^{} ([A, B]) = sup (M ℝ^{} <)$
104	101 103	breqtrrd	$⊢ φ \to B - A \leq {vol}^{*} ([A, B])$

Metamath Proof Explorer

Theorem ovolicc2

Proof