Theorem elxrge0 13425

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 11228	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11235	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13357	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 692	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13097	. . . 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 5110  (class class class)co 7390  0cc0 11075  +∞cpnf 11212  ℝ^*cxr 11214   ≤ cle 11216  [,]cicc 13316

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-icc 13320

This theorem is referenced by:  0e0iccpnf  13427  ge0xaddcl  13430  ge0xmulcl  13431  xnn0xrge0  13474  xrge0subm  21331  psmetxrge0  24208  isxmet2d  24222  prdsdsf  24262  prdsxmetlem  24263  comet  24408  stdbdxmet  24410  xrge0gsumle  24729  xrge0tsms  24730  metdsf  24744  metds0  24746  metdstri  24747  metdsre  24749  metdseq0  24750  metdscnlem  24751  metnrmlem1a  24754  xrhmeo  24851  lebnumlem1  24867  xrge0f  25639  itg2const2  25649  itg2uba  25651  itg2mono  25661  itg2gt0  25668  itg2cnlem2  25670  itg2cn  25671  iblss  25713  itgle  25718  itgeqa  25722  ibladdlem  25728  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgsplit  25744  bddmulibl  25747  bddiblnc  25750  xrge0addge  32688  xrge0infss  32690  xrge0addcld  32692  xrge0subcld  32693  xrge00  32960  xrge0tsmsd  33009  fldextrspundglemul  33681  esummono  34051  gsumesum  34056  esumsnf  34061  esumrnmpt2  34065  esumpmono  34076  hashf2  34081  measge0  34204  measle0  34205  measssd  34212  measunl  34213  omssubaddlem  34297  omssubadd  34298  carsgsigalem  34313  pmeasmono  34322  sibfinima  34337  prob01  34411  dstrvprob  34470  itg2addnclem  37672  ibladdnclem  37677  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  xrge0ge0  45350  rrxsphere  48741