Theorem elxrge0 13418

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 11221	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11228	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13350	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 692	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13090	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 480	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 559	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 303	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5107  (class class class)co 7387  0cc0 11068  +∞cpnf 11205  ℝ^*cxr 11207   ≤ cle 11209  [,]cicc 13309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-icc 13313

This theorem is referenced by:  0e0iccpnf  13420  ge0xaddcl  13423  ge0xmulcl  13424  xnn0xrge0  13467  xrge0subm  21324  psmetxrge0  24201  isxmet2d  24215  prdsdsf  24255  prdsxmetlem  24256  comet  24401  stdbdxmet  24403  xrge0gsumle  24722  xrge0tsms  24723  metdsf  24737  metds0  24739  metdstri  24740  metdsre  24742  metdseq0  24743  metdscnlem  24744  metnrmlem1a  24747  xrhmeo  24844  lebnumlem1  24860  xrge0f  25632  itg2const2  25642  itg2uba  25644  itg2mono  25654  itg2gt0  25661  itg2cnlem2  25663  itg2cn  25664  iblss  25706  itgle  25711  itgeqa  25715  ibladdlem  25721  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgsplit  25737  bddmulibl  25740  bddiblnc  25743  xrge0addge  32681  xrge0infss  32683  xrge0addcld  32685  xrge0subcld  32686  xrge00  32953  xrge0tsmsd  33002  fldextrspundglemul  33674  esummono  34044  gsumesum  34049  esumsnf  34054  esumrnmpt2  34058  esumpmono  34069  hashf2  34074  measge0  34197  measle0  34198  measssd  34205  measunl  34206  omssubaddlem  34290  omssubadd  34291  carsgsigalem  34306  pmeasmono  34315  sibfinima  34330  prob01  34404  dstrvprob  34463  itg2addnclem  37665  ibladdnclem  37670  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  xrge0ge0  45343  rrxsphere  48737