Theorem elxrge0 13485

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 11257	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11264	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13417	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 704	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13156	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 485	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 568	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 306	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   ∈ wcel 2143   class class class wbr 5110  (class class class)co 7412  0cc0 11101  +∞cpnf 11241  ℝ^*cxr 11243   ≤ cle 11245  [,]cicc 13376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-addrcl 11162  ax-rnegex 11172  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-icc 13380

This theorem is referenced by:  0e0iccpnf  13487  ge0xaddcl  13490  ge0xmulcl  13491  xnn0xrge0  13534  xrge0subm  21574  psmetxrge0  24451  isxmet2d  24465  prdsdsf  24505  prdsxmetlem  24506  comet  24651  stdbdxmet  24653  xrge0gsumle  24972  xrge0tsms  24973  metdsf  24987  metds0  24989  metdstri  24990  metdsre  24992  metdseq0  24993  metdscnlem  24994  metnrmlem1a  24997  xrhmeo  25086  lebnumlem1  25101  xrge0f  25871  itg2const2  25881  itg2uba  25883  itg2mono  25893  itg2gt0  25900  itg2cnlem2  25902  itg2cn  25903  iblss  25945  itgle  25950  itgeqa  25954  ibladdlem  25960  iblabs  25969  iblabsr  25970  iblmulc2  25971  itgsplit  25976  bddmulibl  25979  bddiblnc  25982  xrge0addge  33084  xrge0infss  33086  xrge0addcld  33088  xrge0subcld  33089  xrge00  33315  xrge0tsmsd  33374  fldextrspundglemul  34050  esummono  34425  gsumesum  34430  esumsnf  34435  esumrnmpt2  34439  esumpmono  34450  hashf2  34455  measge0  34578  measle0  34579  measssd  34586  measunl  34587  omssubaddlem  34670  omssubadd  34671  carsgsigalem  34686  pmeasmono  34695  sibfinima  34710  prob01  34784  dstrvprob  34843  itg2addnclem  38303  ibladdnclem  38308  iblabsnc  38316  iblmulc2nc  38317  ftc1anclem4  38328  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  xrge0ge0  46046  rrxsphere  49511