Theorem elxrge0 13474

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 11282	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11289	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13406	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 692	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13146	. . . 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 2108   class class class wbr 5119  (class class class)co 7405  0cc0 11129  +∞cpnf 11266  ℝ^*cxr 11268   ≤ cle 11270  [,]cicc 13365

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-addrcl 11190  ax-rnegex 11200  ax-cnre 11202

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-icc 13369

This theorem is referenced by:  0e0iccpnf  13476  ge0xaddcl  13479  ge0xmulcl  13480  xnn0xrge0  13523  xrge0subm  21375  psmetxrge0  24252  isxmet2d  24266  prdsdsf  24306  prdsxmetlem  24307  comet  24452  stdbdxmet  24454  xrge0gsumle  24773  xrge0tsms  24774  metdsf  24788  metds0  24790  metdstri  24791  metdsre  24793  metdseq0  24794  metdscnlem  24795  metnrmlem1a  24798  xrhmeo  24895  lebnumlem1  24911  xrge0f  25684  itg2const2  25694  itg2uba  25696  itg2mono  25706  itg2gt0  25713  itg2cnlem2  25715  itg2cn  25716  iblss  25758  itgle  25763  itgeqa  25767  ibladdlem  25773  iblabs  25782  iblabsr  25783  iblmulc2  25784  itgsplit  25789  bddmulibl  25792  bddiblnc  25795  xrge0addge  32735  xrge0infss  32737  xrge0addcld  32739  xrge0subcld  32740  xrge00  33007  xrge0tsmsd  33056  fldextrspundglemul  33720  esummono  34085  gsumesum  34090  esumsnf  34095  esumrnmpt2  34099  esumpmono  34110  hashf2  34115  measge0  34238  measle0  34239  measssd  34246  measunl  34247  omssubaddlem  34331  omssubadd  34332  carsgsigalem  34347  pmeasmono  34356  sibfinima  34371  prob01  34445  dstrvprob  34504  itg2addnclem  37695  ibladdnclem  37700  iblabsnc  37708  iblmulc2nc  37709  ftc1anclem4  37720  ftc1anclem5  37721  ftc1anclem6  37722  ftc1anclem7  37723  ftc1anclem8  37724  ftc1anc  37725  xrge0ge0  45374  rrxsphere  48728