Theorem elxrge0 13480

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 1103	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11252	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11259	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13412	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 704	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13151	. . . 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 1101   ∈ wcel 2149   class class class wbr 5110  (class class class)co 7408  0cc0 11096  +∞cpnf 11236  ℝ^*cxr 11238   ≤ cle 11240  [,]cicc 13371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-addrcl 11157  ax-rnegex 11167  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7411  df-oprab 7412  df-mpo 7413  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-icc 13375

This theorem is referenced by:  0e0iccpnf  13482  ge0xaddcl  13485  ge0xmulcl  13486  xnn0xrge0  13529  xrge0subm  21558  psmetxrge0  24435  isxmet2d  24449  prdsdsf  24489  prdsxmetlem  24490  comet  24635  stdbdxmet  24637  xrge0gsumle  24956  xrge0tsms  24957  metdsf  24971  metds0  24973  metdstri  24974  metdsre  24976  metdseq0  24977  metdscnlem  24978  metnrmlem1a  24981  xrhmeo  25070  lebnumlem1  25085  xrge0f  25855  itg2const2  25865  itg2uba  25867  itg2mono  25877  itg2gt0  25884  itg2cnlem2  25886  itg2cn  25887  iblss  25929  itgle  25934  itgeqa  25938  ibladdlem  25944  iblabs  25953  iblabsr  25954  iblmulc2  25955  itgsplit  25960  bddmulibl  25963  bddiblnc  25966  xrge0addge  33040  xrge0infss  33042  xrge0addcld  33044  xrge0subcld  33045  xrge00  33271  xrge0tsmsd  33330  fldextrspundglemul  34010  esummono  34385  gsumesum  34390  esumsnf  34395  esumrnmpt2  34399  esumpmono  34410  hashf2  34415  measge0  34538  measle0  34539  measssd  34546  measunl  34547  omssubaddlem  34630  omssubadd  34631  carsgsigalem  34646  pmeasmono  34655  sibfinima  34670  prob01  34744  dstrvprob  34803  itg2addnclem  38205  ibladdnclem  38210  iblabsnc  38218  iblmulc2nc  38219  ftc1anclem4  38230  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  xrge0ge0  45948  rrxsphere  49406