Theorem xrge0f

Description: A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	xrge0f	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
2	1	adantr	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 Fn ℝ )
3		ax-resscn	⊢ ℝ ⊆ ℂ
4	3	a1i	⊢ ( 𝐹 : ℝ ⟶ ℝ → ℝ ⊆ ℂ )
5	4 1	0pledm	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 0𝑝 ∘r ≤ 𝐹 ↔ ( ℝ × { 0 } ) ∘r ≤ 𝐹 ) )
6		0re	⊢ 0 ∈ ℝ
7		fnconstg	⊢ ( 0 ∈ ℝ → ( ℝ × { 0 } ) Fn ℝ )
8	6 7	mp1i	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ℝ × { 0 } ) Fn ℝ )
9		reex	⊢ ℝ ∈ V
10	9	a1i	⊢ ( 𝐹 : ℝ ⟶ ℝ → ℝ ∈ V )
11		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
12		c0ex	⊢ 0 ∈ V
13	12	fvconst2	⊢ ( 𝑥 ∈ ℝ → ( ( ℝ × { 0 } ) ‘ 𝑥 ) = 0 )
14	13	adantl	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ℝ × { 0 } ) ‘ 𝑥 ) = 0 )
15		eqidd	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
16	8 1 10 10 11 14 15	ofrfval	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ( ℝ × { 0 } ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
17		ffvelrn	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
18	17	rexrd	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
19	18	biantrurd	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
20		elxrge0	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
21	19 20	bitr4di	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
22	21	ralbidva	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ∀ 𝑥 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
23	5 16 22	3bitrd	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 0𝑝 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
24	23	biimpa	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
25		ffnfv	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 Fn ℝ ∧ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ) )
26	2 24 25	sylanbrc	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )