Theorem ovolfsf

Description: Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Hypothesis	ovolfs.1	$$⊢G=\left(\mathrm{abs}\circ -\right)\circ F$$
Assertion	ovolfsf	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to G:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovolfs.1	$$⊢G=\left(\mathrm{abs}\circ -\right)\circ F$$
2		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
3		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
4		fco	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge -:ℂ\times ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
5	2 3 4	mp2an	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
6		inss2	$$⊢\le \cap {ℝ}^2\subseteq {ℝ}^2$$
7		ax-resscn	$$⊢ℝ\subseteq ℂ$$
8		xpss12	$$⊢\left(ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to {ℝ}^2\subseteq ℂ\times ℂ$$
9	7 7 8	mp2an	$$⊢{ℝ}^2\subseteq ℂ\times ℂ$$
10	6 9	sstri	$$⊢\le \cap {ℝ}^2\subseteq ℂ\times ℂ$$
11		fss	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge \le \cap {ℝ}^2\subseteq ℂ\times ℂ\right)\to F:\mathbb{N}⟶ℂ\times ℂ$$
12	10 11	mpan2	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to F:\mathbb{N}⟶ℂ\times ℂ$$
13		fco	$$⊢\left(\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ\wedge F:\mathbb{N}⟶ℂ\times ℂ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ F\right):\mathbb{N}⟶ℝ$$
14	5 12 13	sylancr	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to \left(\left(\mathrm{abs}\circ -\right)\circ F\right):\mathbb{N}⟶ℝ$$
15	1	feq1i	$$⊢G:\mathbb{N}⟶ℝ\leftrightarrow \left(\left(\mathrm{abs}\circ -\right)\circ F\right):\mathbb{N}⟶ℝ$$
16	14 15	sylibr	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to G:\mathbb{N}⟶ℝ$$
17	16	ffnd	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to GFn\mathbb{N}$$
18	16	ffvelcdmda	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to G\left(x\right)\in ℝ$$
19		ovolfcl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to \left(1^{st}\left(F\left(x\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(x\right)\right)\in ℝ\wedge 1^{st}\left(F\left(x\right)\right)\le 2^{nd}\left(F\left(x\right)\right)\right)$$
20		subge0	$$⊢\left(2^{nd}\left(F\left(x\right)\right)\in ℝ\wedge 1^{st}\left(F\left(x\right)\right)\in ℝ\right)\to \left(0\le 2^{nd}\left(F\left(x\right)\right)-1^{st}\left(F\left(x\right)\right)\leftrightarrow 1^{st}\left(F\left(x\right)\right)\le 2^{nd}\left(F\left(x\right)\right)\right)$$
21	20	ancoms	$$⊢\left(1^{st}\left(F\left(x\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(x\right)\right)\in ℝ\right)\to \left(0\le 2^{nd}\left(F\left(x\right)\right)-1^{st}\left(F\left(x\right)\right)\leftrightarrow 1^{st}\left(F\left(x\right)\right)\le 2^{nd}\left(F\left(x\right)\right)\right)$$
22	21	biimp3ar	$$⊢\left(1^{st}\left(F\left(x\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(x\right)\right)\in ℝ\wedge 1^{st}\left(F\left(x\right)\right)\le 2^{nd}\left(F\left(x\right)\right)\right)\to 0\le 2^{nd}\left(F\left(x\right)\right)-1^{st}\left(F\left(x\right)\right)$$
23	19 22	syl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to 0\le 2^{nd}\left(F\left(x\right)\right)-1^{st}\left(F\left(x\right)\right)$$
24	1	ovolfsval	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to G\left(x\right)=2^{nd}\left(F\left(x\right)\right)-1^{st}\left(F\left(x\right)\right)$$
25	23 24	breqtrrd	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to 0\le G\left(x\right)$$
26		elrege0	$$⊢G\left(x\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(G\left(x\right)\in ℝ\wedge 0\le G\left(x\right)\right)$$
27	18 25 26	sylanbrc	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge x\in \mathbb{N}\right)\to G\left(x\right)\in \left[0,\mathrm{+\infty }\right)$$
28	27	ralrimiva	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to \forall x\in \mathbb{N}G\left(x\right)\in \left[0,\mathrm{+\infty }\right)$$
29		ffnfv	$$⊢G:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)\leftrightarrow \left(GFn\mathbb{N}\wedge \forall x\in \mathbb{N}G\left(x\right)\in \left[0,\mathrm{+\infty }\right)\right)$$
30	17 28 29	sylanbrc	$$⊢F:\mathbb{N}⟶\le \cap {ℝ}^2\to G:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$