ovolfsval

Description: The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Hypothesis	ovolfs.1	⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
	Assertion	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ 𝑁 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovolfs.1	⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2	1	fveq1i	⊢ ( 𝐺 ‘ 𝑁 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑁 )
3		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑁 ) = ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) )
4	2 3	syl5eq	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ 𝑁 ) = ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) )
5		ffvelrn	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
6	5	elin2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) )
7		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑁 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
8	6 7	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ 𝑁 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
9	8	fveq2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ ) )
10		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( ( abs ∘ − ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ )
11	9 10	eqtr4di	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
12		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
13	12	simp1d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
14	13	recnd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ )
15	12	simp2d	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
16	15	recnd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ )
17		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
18	17	cnmetdval	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
19	14 16 18	syl2anc	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
20		abssuble0	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) → ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
21	12 20	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( abs ‘ ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
22	19 21	eqtrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ( abs ∘ − ) ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
23	11 22	eqtrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( ( abs ∘ − ) ‘ ( 𝐹 ‘ 𝑁 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
24	4 23	eqtrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ 𝑁 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑁 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑁 ) ) ) )

Metamath Proof Explorer

Theorem ovolfsval

Proof