Theorem ovolfsval

Description: The value of 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	ovolfsval	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to G\left(N\right)=2^{nd}\left(F\left(N\right)\right)-1^{st}\left(F\left(N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovolfs.1	$$⊢G=\left(\mathrm{abs}\circ -\right)\circ F$$
2	1	fveq1i	$$⊢G\left(N\right)=\left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(N\right)$$
3		fvco3	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to \left(\left(\mathrm{abs}\circ -\right)\circ F\right)\left(N\right)=\left(\mathrm{abs}\circ -\right)\left(F\left(N\right)\right)$$
4	2 3	eqtrid	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to G\left(N\right)=\left(\mathrm{abs}\circ -\right)\left(F\left(N\right)\right)$$
5		ffvelrn	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to F\left(N\right)\in \left(\le \cap {ℝ}^2\right)$$
6	5	elin2d	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to F\left(N\right)\in {ℝ}^2$$
7		1st2nd2	$$⊢F\left(N\right)\in {ℝ}^2\to F\left(N\right)=⟨1^{st}\left(F\left(N\right)\right),2^{nd}\left(F\left(N\right)\right)⟩$$
8	6 7	syl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to F\left(N\right)=⟨1^{st}\left(F\left(N\right)\right),2^{nd}\left(F\left(N\right)\right)⟩$$
9	8	fveq2d	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to \left(\mathrm{abs}\circ -\right)\left(F\left(N\right)\right)=\left(\mathrm{abs}\circ -\right)\left(⟨1^{st}\left(F\left(N\right)\right),2^{nd}\left(F\left(N\right)\right)⟩\right)$$
10		df-ov	$$⊢1^{st}\left(F\left(N\right)\right)\left(\mathrm{abs}\circ -\right)2^{nd}\left(F\left(N\right)\right)=\left(\mathrm{abs}\circ -\right)\left(⟨1^{st}\left(F\left(N\right)\right),2^{nd}\left(F\left(N\right)\right)⟩\right)$$
11	9 10	eqtr4di	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to \left(\mathrm{abs}\circ -\right)\left(F\left(N\right)\right)=1^{st}\left(F\left(N\right)\right)\left(\mathrm{abs}\circ -\right)2^{nd}\left(F\left(N\right)\right)$$
12		ovolfcl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to \left(1^{st}\left(F\left(N\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(N\right)\right)\in ℝ\wedge 1^{st}\left(F\left(N\right)\right)\le 2^{nd}\left(F\left(N\right)\right)\right)$$
13	12	simp1d	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to 1^{st}\left(F\left(N\right)\right)\in ℝ$$
14	13	recnd	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to 1^{st}\left(F\left(N\right)\right)\in ℂ$$
15	12	simp2d	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to 2^{nd}\left(F\left(N\right)\right)\in ℝ$$
16	15	recnd	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to 2^{nd}\left(F\left(N\right)\right)\in ℂ$$
17		eqid	$$⊢\mathrm{abs}\circ -=\mathrm{abs}\circ -$$
18	17	cnmetdval	$$⊢\left(1^{st}\left(F\left(N\right)\right)\in ℂ\wedge 2^{nd}\left(F\left(N\right)\right)\in ℂ\right)\to 1^{st}\left(F\left(N\right)\right)\left(\mathrm{abs}\circ -\right)2^{nd}\left(F\left(N\right)\right)=\left|1^{st}\left(F\left(N\right)\right)-2^{nd}\left(F\left(N\right)\right)\right|$$
19	14 16 18	syl2anc	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to 1^{st}\left(F\left(N\right)\right)\left(\mathrm{abs}\circ -\right)2^{nd}\left(F\left(N\right)\right)=\left|1^{st}\left(F\left(N\right)\right)-2^{nd}\left(F\left(N\right)\right)\right|$$
20		abssuble0	$$⊢\left(1^{st}\left(F\left(N\right)\right)\in ℝ\wedge 2^{nd}\left(F\left(N\right)\right)\in ℝ\wedge 1^{st}\left(F\left(N\right)\right)\le 2^{nd}\left(F\left(N\right)\right)\right)\to \left|1^{st}\left(F\left(N\right)\right)-2^{nd}\left(F\left(N\right)\right)\right|=2^{nd}\left(F\left(N\right)\right)-1^{st}\left(F\left(N\right)\right)$$
21	12 20	syl	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to \left|1^{st}\left(F\left(N\right)\right)-2^{nd}\left(F\left(N\right)\right)\right|=2^{nd}\left(F\left(N\right)\right)-1^{st}\left(F\left(N\right)\right)$$
22	19 21	eqtrd	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to 1^{st}\left(F\left(N\right)\right)\left(\mathrm{abs}\circ -\right)2^{nd}\left(F\left(N\right)\right)=2^{nd}\left(F\left(N\right)\right)-1^{st}\left(F\left(N\right)\right)$$
23	11 22	eqtrd	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to \left(\mathrm{abs}\circ -\right)\left(F\left(N\right)\right)=2^{nd}\left(F\left(N\right)\right)-1^{st}\left(F\left(N\right)\right)$$
24	4 23	eqtrd	$$⊢\left(F:\mathbb{N}⟶\le \cap {ℝ}^2\wedge N\in \mathbb{N}\right)\to G\left(N\right)=2^{nd}\left(F\left(N\right)\right)-1^{st}\left(F\left(N\right)\right)$$