Theorem elxrge0 13452

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 1087	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11277	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11284	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13386	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 691	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13128	. . . 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 205   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2099   class class class wbr 5142  (class class class)co 7414  0cc0 11124  +∞cpnf 11261  ℝ^*cxr 11263   ≤ cle 11265  [,]cicc 13345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-addrcl 11185  ax-rnegex 11195  ax-cnre 11197

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-icc 13349

This theorem is referenced by:  0e0iccpnf  13454  ge0xaddcl  13457  ge0xmulcl  13458  xnn0xrge0  13501  xrge0subm  21320  psmetxrge0  24193  isxmet2d  24207  prdsdsf  24247  prdsxmetlem  24248  comet  24396  stdbdxmet  24398  xrge0gsumle  24723  xrge0tsms  24724  metdsf  24738  metds0  24740  metdstri  24741  metdsre  24743  metdseq0  24744  metdscnlem  24745  metnrmlem1a  24748  xrhmeo  24845  lebnumlem1  24861  xrge0f  25635  itg2const2  25645  itg2uba  25647  itg2mono  25657  itg2gt0  25664  itg2cnlem2  25666  itg2cn  25667  iblss  25708  itgle  25713  itgeqa  25717  ibladdlem  25723  iblabs  25732  iblabsr  25733  iblmulc2  25734  itgsplit  25739  bddmulibl  25742  bddiblnc  25745  xrge0addge  32498  xrge0infss  32501  xrge0addcld  32503  xrge0subcld  32504  xrge00  32711  xrge0tsmsd  32736  esummono  33596  gsumesum  33601  esumsnf  33606  esumrnmpt2  33610  esumpmono  33621  hashf2  33626  measge0  33749  measle0  33750  measssd  33757  measunl  33758  omssubaddlem  33842  omssubadd  33843  carsgsigalem  33858  pmeasmono  33867  sibfinima  33882  prob01  33956  dstrvprob  34014  itg2addnclem  37066  ibladdnclem  37071  iblabsnc  37079  iblmulc2nc  37080  ftc1anclem4  37091  ftc1anclem5  37092  ftc1anclem6  37093  ftc1anclem7  37094  ftc1anclem8  37095  ftc1anc  37096  xrge0ge0  44642  rrxsphere  47734