Theorem elxrge0 13510

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 1105	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11280	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11287	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13442	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 705	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13181	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 486	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 569	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 306	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7413  0cc0 11124  +∞cpnf 11264  ℝ^*cxr 11266   ≤ cle 11268  [,]cicc 13401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-addrcl 11185  ax-rnegex 11195  ax-cnre 11197

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-icc 13405

This theorem is used by:  0e0iccpnf  13512  ge0xaddcl  13515  ge0xmulcl  13516  xnn0xrge0  13559  xrge0subm  21656  psmetxrge0  24539  isxmet2d  24553  prdsdsf  24593  prdsxmetlem  24594  comet  24739  stdbdxmet  24741  xrge0gsumle  25060  xrge0tsms  25061  metdsf  25075  metds0  25077  metdstri  25078  metdsre  25080  metdseq0  25081  metdscnlem  25082  metnrmlem1a  25085  xrhmeo  25174  lebnumlem1  25189  xrge0f  25959  itg2const2  25969  itg2uba  25971  itg2mono  25981  itg2gt0  25988  itg2cnlem2  25990  itg2cn  25991  iblss  26032  itgle  26037  itgeqa  26041  ibladdlem  26047  iblabs  26056  iblabsr  26057  iblmulc2  26058  itgsplit  26063  bddmulibl  26066  bddiblnc  26069  xrge0addge  33229  xrge0infss  33231  xrge0addcld  33233  xrge0subcld  33234  xrge00  33454  xrge0tsmsd  33513  fldextrspundglemul  34189  esummono  34564  gsumesum  34569  esumsnf  34574  esumrnmpt2  34578  esumpmono  34589  hashf2  34594  measge0  34718  measle0  34719  measssd  34726  measunl  34727  omssubaddlem  34810  omssubadd  34811  carsgsigalem  34826  pmeasmono  34835  sibfinima  34850  prob01  34924  dstrvprob  34983  itg2addnclem  38420  ibladdnclem  38425  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem4  38445  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  xrge0ge0  46177  rrxsphere  49678