Theorem 0plef

Description: Two ways to say that the function F on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
2		fss	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
3	1 2	mpan2	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) → 𝐹 : ℝ ⟶ ℝ )
4		ffvelcdm	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
5		elrege0	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
6	5	baib	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
7	4 6	syl	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
8	7	ralbidva	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
9		ffn	⊢ ( 𝐹 : ℝ ⟶ ℝ → 𝐹 Fn ℝ )
10		ffnfv	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 Fn ℝ ∧ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
11	10	baib	⊢ ( 𝐹 Fn ℝ → ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
12	9 11	syl	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ↔ ∀ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) )
13		0cn	⊢ 0 ∈ ℂ
14		fnconstg	⊢ ( 0 ∈ ℂ → ( ℂ × { 0 } ) Fn ℂ )
15	13 14	ax-mp	⊢ ( ℂ × { 0 } ) Fn ℂ
16		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
17	16	fneq1i	⊢ ( 0𝑝 Fn ℂ ↔ ( ℂ × { 0 } ) Fn ℂ )
18	15 17	mpbir	⊢ 0𝑝 Fn ℂ
19	18	a1i	⊢ ( 𝐹 : ℝ ⟶ ℝ → 0𝑝 Fn ℂ )
20		cnex	⊢ ℂ ∈ V
21	20	a1i	⊢ ( 𝐹 : ℝ ⟶ ℝ → ℂ ∈ V )
22		reex	⊢ ℝ ∈ V
23	22	a1i	⊢ ( 𝐹 : ℝ ⟶ ℝ → ℝ ∈ V )
24		ax-resscn	⊢ ℝ ⊆ ℂ
25		sseqin2	⊢ ( ℝ ⊆ ℂ ↔ ( ℂ ∩ ℝ ) = ℝ )
26	24 25	mpbi	⊢ ( ℂ ∩ ℝ ) = ℝ
27		0pval	⊢ ( 𝑥 ∈ ℂ → ( 0𝑝 ‘ 𝑥 ) = 0 )
28	27	adantl	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℂ ) → ( 0𝑝 ‘ 𝑥 ) = 0 )
29		eqidd	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
30	19 9 21 23 26 28 29	ofrfval	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 0𝑝 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
31	8 12 30	3bitr4d	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ↔ 0𝑝 ∘r ≤ 𝐹 ) )
32	3 31	biadanii	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) )