ovolfsf

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

		Ref	Expression
	Hypothesis	ovolfs.1	⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
	Assertion	ovolfsf	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		ovolfs.1	⊢ 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2		absf	⊢ abs : ℂ ⟶ ℝ
3		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
4		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
5	2 3 4	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
6		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
7		ax-resscn	⊢ ℝ ⊆ ℂ
8		xpss12	⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
9	7 7 8	mp2an	⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
10	6 9	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℂ × ℂ )
11		fss	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℂ × ℂ ) ) → 𝐹 : ℕ ⟶ ( ℂ × ℂ ) )
12	10 11	mpan2	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℂ × ℂ ) )
13		fco	⊢ ( ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ ∧ 𝐹 : ℕ ⟶ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ℝ )
14	5 12 13	sylancr	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ℝ )
15	1	feq1i	⊢ ( 𝐺 : ℕ ⟶ ℝ ↔ ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ℝ )
16	14 15	sylibr	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ℝ )
17	16	ffnd	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 Fn ℕ )
18	16	ffvelrnda	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
19		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
20		subge0	⊢ ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
21	20	ancoms	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
22	21	biimp3ar	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 0 ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
23	19 22	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
24	1	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
25	23 24	breqtrrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ ( 𝐺 ‘ 𝑥 ) )
26		elrege0	⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐺 ‘ 𝑥 ) ) )
27	18 25 26	sylanbrc	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
28	27	ralrimiva	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∀ 𝑥 ∈ ℕ ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
29		ffnfv	⊢ ( 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐺 Fn ℕ ∧ ∀ 𝑥 ∈ ℕ ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
30	17 28 29	sylanbrc	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )

Metamath Proof Explorer

Theorem ovolfsf

Proof