Theorem elxrge0 13495

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 11267	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11274	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13427	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 705	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13166	. . . 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 2146   class class class wbr 5111  (class class class)co 7416  0cc0 11111  +∞cpnf 11251  ℝ^*cxr 11253   ≤ cle 11255  [,]cicc 13386

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-addrcl 11172  ax-rnegex 11182  ax-cnre 11184

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-icc 13390

This theorem is used by:  0e0iccpnf  13497  ge0xaddcl  13500  ge0xmulcl  13501  xnn0xrge0  13544  xrge0subm  21622  psmetxrge0  24499  isxmet2d  24513  prdsdsf  24553  prdsxmetlem  24554  comet  24699  stdbdxmet  24701  xrge0gsumle  25020  xrge0tsms  25021  metdsf  25035  metds0  25037  metdstri  25038  metdsre  25040  metdseq0  25041  metdscnlem  25042  metnrmlem1a  25045  xrhmeo  25134  lebnumlem1  25149  xrge0f  25919  itg2const2  25929  itg2uba  25931  itg2mono  25941  itg2gt0  25948  itg2cnlem2  25950  itg2cn  25951  iblss  25993  itgle  25998  itgeqa  26002  ibladdlem  26008  iblabs  26017  iblabsr  26018  iblmulc2  26019  itgsplit  26024  bddmulibl  26027  bddiblnc  26030  xrge0addge  33132  xrge0infss  33134  xrge0addcld  33136  xrge0subcld  33137  xrge00  33357  xrge0tsmsd  33416  fldextrspundglemul  34092  esummono  34467  gsumesum  34472  esumsnf  34477  esumrnmpt2  34481  esumpmono  34492  hashf2  34497  measge0  34621  measle0  34622  measssd  34629  measunl  34630  omssubaddlem  34713  omssubadd  34714  carsgsigalem  34729  pmeasmono  34738  sibfinima  34753  prob01  34827  dstrvprob  34886  itg2addnclem  38355  ibladdnclem  38360  iblabsnc  38368  iblmulc2nc  38369  ftc1anclem4  38380  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  xrge0ge0  46096  rrxsphere  49561