Theorem 0e0iccpnf 13202

Description: 0 is a member of (0[,]+∞). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0e0iccpnf	⊢ 0 ∈ (0[,]+∞)

Proof of Theorem 0e0iccpnf

Step	Hyp	Ref	Expression
1		0xr 11033	. 2 ⊢ 0 ∈ ℝ*
2		0le0 12085	. 2 ⊢ 0 ≤ 0
3		elxrge0 13200	. 2 ⊢ (0 ∈ (0[,]+∞) ↔ (0 ∈ ℝ* ∧ 0 ≤ 0))
4	1, 2, 3	mpbir2an 708	1 ⊢ 0 ∈ (0[,]+∞)

Syntax hints:   ∈ wcel 2110   class class class wbr 5079  (class class class)co 7272  0cc0 10882  +∞cpnf 11017  ℝ^*cxr 11019   ≤ cle 11021  [,]cicc 13093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7583  ax-cnex 10938  ax-resscn 10939  ax-1cn 10940  ax-addrcl 10943  ax-rnegex 10953  ax-cnre 10955  ax-pre-lttri 10956

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7275  df-oprab 7276  df-mpo 7277  df-er 8490  df-en 8726  df-dom 8727  df-sdom 8728  df-pnf 11022  df-mnf 11023  df-xr 11024  df-ltxr 11025  df-le 11026  df-icc 13097

This theorem is referenced by:  xrge0subm  20650  itg2const2  24917  itg2splitlem  24924  itg2split  24925  itg2gt0  24936  itg2cnlem2  24938  itg2cn  24939  iblss  24980  itgle  24985  itgeqa  24989  ibladdlem  24995  iblabs  25004  iblabsr  25005  iblmulc2  25006  bddmulibl  25014  bddiblnc  25017  xrge0infss  31092  xrge00  31304  unitssxrge0  31859  xrge0mulc1cn  31900  esum0  32026  esumpad  32032  esumpad2  32033  esumrnmpt2  32045  esumpinfval  32050  esummulc1  32058  ddemeas  32213  oms0  32273  itg2gt0cn  35841  ibladdnclem  35842  iblabsnc  35850  iblmulc2nc  35851  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  iblsplit  43489  gsumge0cl  43891  sge0cl  43901  sge0ss  43932  0ome  44049  ovnf  44083