This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≤ 𝐹 ) )