Theorem 0plef 24357

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

Assertion

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

Proof of Theorem 0plef

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rge0ssre 12873	. . 3 ⊢ (0[,)+∞) ⊆ ℝ
2		fss 6505	. . 3 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
3	1, 2	mpan2 691	. 2 ⊢ (𝐹:ℝ⟶(0[,)+∞) → 𝐹:ℝ⟶ℝ)
4		ffvelrn 6833	. . . . 5 ⊢ ((𝐹:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
5		elrege0 12871	. . . . . 6 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
6	5	baib 540	. . . . 5 ⊢ ((𝐹‘𝑥) ∈ ℝ → ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (𝐹‘𝑥)))
7	4, 6	syl 17	. . . 4 ⊢ ((𝐹:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (𝐹‘𝑥)))
8	7	ralbidva 3123	. . 3 ⊢ (𝐹:ℝ⟶ℝ → (∀𝑥 ∈ ℝ (𝐹‘𝑥) ∈ (0[,)+∞) ↔ ∀𝑥 ∈ ℝ 0 ≤ (𝐹‘𝑥)))
9		ffn 6491	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → 𝐹 Fn ℝ)
10		ffnfv 6866	. . . . 5 ⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹 Fn ℝ ∧ ∀𝑥 ∈ ℝ (𝐹‘𝑥) ∈ (0[,)+∞)))
11	10	baib 540	. . . 4 ⊢ (𝐹 Fn ℝ → (𝐹:ℝ⟶(0[,)+∞) ↔ ∀𝑥 ∈ ℝ (𝐹‘𝑥) ∈ (0[,)+∞)))
12	9, 11	syl 17	. . 3 ⊢ (𝐹:ℝ⟶ℝ → (𝐹:ℝ⟶(0[,)+∞) ↔ ∀𝑥 ∈ ℝ (𝐹‘𝑥) ∈ (0[,)+∞)))
13		0cn 10656	. . . . . . 7 ⊢ 0 ∈ ℂ
14		fnconstg 6545	. . . . . . 7 ⊢ (0 ∈ ℂ → (ℂ × {0}) Fn ℂ)
15	13, 14	ax-mp 5	. . . . . 6 ⊢ (ℂ × {0}) Fn ℂ
16		df-0p 24355	. . . . . . 7 ⊢ 0𝑝 = (ℂ × {0})
17	16	fneq1i 6424	. . . . . 6 ⊢ (0𝑝 Fn ℂ ↔ (ℂ × {0}) Fn ℂ)
18	15, 17	mpbir 234	. . . . 5 ⊢ 0𝑝 Fn ℂ
19	18	a1i 11	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → 0𝑝 Fn ℂ)
20		cnex 10641	. . . . 5 ⊢ ℂ ∈ V
21	20	a1i 11	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → ℂ ∈ V)
22		reex 10651	. . . . 5 ⊢ ℝ ∈ V
23	22	a1i 11	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → ℝ ∈ V)
24		ax-resscn 10617	. . . . 5 ⊢ ℝ ⊆ ℂ
25		sseqin2 4116	. . . . 5 ⊢ (ℝ ⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ)
26	24, 25	mpbi 233	. . . 4 ⊢ (ℂ ∩ ℝ) = ℝ
27		0pval 24356	. . . . 5 ⊢ (𝑥 ∈ ℂ → (0𝑝‘𝑥) = 0)
28	27	adantl 486	. . . 4 ⊢ ((𝐹:ℝ⟶ℝ ∧ 𝑥 ∈ ℂ) → (0𝑝‘𝑥) = 0)
29		eqidd 2760	. . . 4 ⊢ ((𝐹:ℝ⟶ℝ ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) = (𝐹‘𝑥))
30	19, 9, 21, 23, 26, 28, 29	ofrfval 7407	. . 3 ⊢ (𝐹:ℝ⟶ℝ → (0𝑝 ∘r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ 0 ≤ (𝐹‘𝑥)))
31	8, 12, 30	3bitr4d 315	. 2 ⊢ (𝐹:ℝ⟶ℝ → (𝐹:ℝ⟶(0[,)+∞) ↔ 0𝑝 ∘r ≤ 𝐹))
32	3, 31	biadanii 822	1 ⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3068  Vcvv 3407   ∩ cin 3853   ⊆ wss 3854  {csn 4515   class class class wbr 5025   × cxp 5515   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7143   ∘_r cofr 7397  ℂcc 10558  ℝcr 10559  0cc0 10560  +∞cpnf 10695   ≤ cle 10699  [,)cico 12766  0_𝑝c0p 24354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-i2m1 10628  ax-rnegex 10631  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-id 5423  df-po 5436  df-so 5437  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7146  df-oprab 7147  df-mpo 7148  df-ofr 7399  df-er 8292  df-en 8521  df-dom 8522  df-sdom 8523  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-ico 12770  df-0p 24355

This theorem is referenced by:  itg2i1fseq  24440  itg2addlem  24443  ftc1anclem8  35402