Theorem elxrge0 13199

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)

Assertion

Ref	Expression
elxrge0	⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Proof of Theorem elxrge0

Step	Hyp	Ref	Expression
1		df-3an 1088	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11032	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11039	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13133	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 689	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 12876	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 481	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 560	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 303	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   ∈ wcel 2106   class class class wbr 5073  (class class class)co 7267  0cc0 10881  +∞cpnf 11016  ℝ^*cxr 11018   ≤ cle 11020  [,]cicc 13092

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578  ax-cnex 10937  ax-resscn 10938  ax-1cn 10939  ax-addrcl 10942  ax-rnegex 10952  ax-cnre 10954

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3431  df-sbc 3716  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5074  df-opab 5136  df-id 5484  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-iota 6384  df-fun 6428  df-fv 6434  df-ov 7270  df-oprab 7271  df-mpo 7272  df-pnf 11021  df-mnf 11022  df-xr 11023  df-ltxr 11024  df-le 11025  df-icc 13096

This theorem is referenced by:  0e0iccpnf  13201  ge0xaddcl  13204  ge0xmulcl  13205  xnn0xrge0  13248  xrge0subm  20649  psmetxrge0  23476  isxmet2d  23490  prdsdsf  23530  prdsxmetlem  23531  comet  23679  stdbdxmet  23681  xrge0gsumle  24006  xrge0tsms  24007  metdsf  24021  metds0  24023  metdstri  24024  metdsre  24026  metdseq0  24027  metdscnlem  24028  metnrmlem1a  24031  xrhmeo  24119  lebnumlem1  24134  xrge0f  24906  itg2const2  24916  itg2uba  24918  itg2mono  24928  itg2gt0  24935  itg2cnlem2  24937  itg2cn  24938  iblss  24979  itgle  24984  itgeqa  24988  ibladdlem  24994  iblabs  25003  iblabsr  25004  iblmulc2  25005  itgsplit  25010  bddmulibl  25013  bddiblnc  25016  xrge0addge  31088  xrge0infss  31091  xrge0addcld  31093  xrge0subcld  31094  xrge00  31303  xrge0tsmsd  31325  esummono  32030  gsumesum  32035  esumsnf  32040  esumrnmpt2  32044  esumpmono  32055  hashf2  32060  measge0  32183  measle0  32184  measssd  32191  measunl  32192  omssubaddlem  32274  omssubadd  32275  carsgsigalem  32290  pmeasmono  32299  sibfinima  32314  prob01  32388  dstrvprob  32446  itg2addnclem  35836  ibladdnclem  35841  iblabsnc  35849  iblmulc2nc  35850  ftc1anclem4  35861  ftc1anclem5  35862  ftc1anclem6  35863  ftc1anclem7  35864  ftc1anclem8  35865  ftc1anc  35866  xrge0ge0  42867  rrxsphere  46072