# Metamath Proof Explorer

## 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}:ℕ⟶\le \cap {ℝ}^{2}\to {G}:ℕ⟶\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 ${⊢}-:ℂ×ℂ⟶ℂ$
4 fco ${⊢}\left(\mathrm{abs}:ℂ⟶ℝ\wedge -:ℂ×ℂ⟶ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
5 2 3 4 mp2an ${⊢}\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ$
6 inss2 ${⊢}\le \cap {ℝ}^{2}\subseteq {ℝ}^{2}$
7 ax-resscn ${⊢}ℝ\subseteq ℂ$
8 xpss12 ${⊢}\left(ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to {ℝ}^{2}\subseteq ℂ×ℂ$
9 7 7 8 mp2an ${⊢}{ℝ}^{2}\subseteq ℂ×ℂ$
10 6 9 sstri ${⊢}\le \cap {ℝ}^{2}\subseteq ℂ×ℂ$
11 fss ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge \le \cap {ℝ}^{2}\subseteq ℂ×ℂ\right)\to {F}:ℕ⟶ℂ×ℂ$
12 10 11 mpan2 ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {F}:ℕ⟶ℂ×ℂ$
13 fco ${⊢}\left(\left(\mathrm{abs}\circ -\right):ℂ×ℂ⟶ℝ\wedge {F}:ℕ⟶ℂ×ℂ\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right):ℕ⟶ℝ$
14 5 12 13 sylancr ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \left(\left(\mathrm{abs}\circ -\right)\circ {F}\right):ℕ⟶ℝ$
15 1 feq1i ${⊢}{G}:ℕ⟶ℝ↔\left(\left(\mathrm{abs}\circ -\right)\circ {F}\right):ℕ⟶ℝ$
16 14 15 sylibr ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {G}:ℕ⟶ℝ$
17 16 ffnd ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {G}Fnℕ$
18 16 ffvelrnda ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to {G}\left({x}\right)\in ℝ$
19 ovolfcl ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\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)↔{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)↔{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}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\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}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\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}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to 0\le {G}\left({x}\right)$
26 elrege0 ${⊢}{G}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({G}\left({x}\right)\in ℝ\wedge 0\le {G}\left({x}\right)\right)$
27 18 25 26 sylanbrc ${⊢}\left({F}:ℕ⟶\le \cap {ℝ}^{2}\wedge {x}\in ℕ\right)\to {G}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
28 27 ralrimiva ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to \forall {x}\in ℕ\phantom{\rule{.4em}{0ex}}{G}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
29 ffnfv ${⊢}{G}:ℕ⟶\left[0,\mathrm{+\infty }\right)↔\left({G}Fnℕ\wedge \forall {x}\in ℕ\phantom{\rule{.4em}{0ex}}{G}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)\right)$
30 17 28 29 sylanbrc ${⊢}{F}:ℕ⟶\le \cap {ℝ}^{2}\to {G}:ℕ⟶\left[0,\mathrm{+\infty }\right)$