Theorem elxrge0 12281

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)

Assertion

Ref	Expression
elxrge0	|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )

Proof of Theorem elxrge0

Step	Hyp	Ref	Expression
1		df-3an 1039	. 2 |- ( ( A e. RR* /\ 0 <_ A /\ A <_ +oo ) <-> ( ( A e. RR* /\ 0 <_ A ) /\ A <_ +oo ) )
2		0xr 10086	. . 3 |- 0 e. RR*
3		pnfxr 10092	. . 3 |- +oo e. RR*
4		elicc1 12219	. . 3 |- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A /\ A <_ +oo ) ) )
5	2, 3, 4	mp2an 708	. 2 |- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A /\ A <_ +oo ) )
6		pnfge 11964	. . . 4 |- ( A e. RR* -> A <_ +oo )
7	6	adantr 481	. . 3 |- ( ( A e. RR* /\ 0 <_ A ) -> A <_ +oo )
8	7	pm4.71i 664	. 2 |- ( ( A e. RR* /\ 0 <_ A ) <-> ( ( A e. RR* /\ 0 <_ A ) /\ A <_ +oo ) )
9	1, 5, 8	3bitr4i 292	1 |- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   e. wcel 1990   class class class wbr 4653  (class class class)co 6650   0cc0 9936   +oocpnf 10071   RR*cxr 10073   <_ cle 10075   [,]cicc 12178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-icc 12182

This theorem is referenced by:  0e0iccpnf  12283  ge0xaddcl  12286  ge0xmulcl  12287  xnn0xrge0  12325  xrge0subm  19787  psmetxrge0  22118  isxmet2d  22132  prdsdsf  22172  prdsxmetlem  22173  comet  22318  stdbdxmet  22320  xrge0gsumle  22636  xrge0tsms  22637  metdsf  22651  metds0  22653  metdstri  22654  metdsre  22656  metdseq0  22657  metdscnlem  22658  metnrmlem1a  22661  metnrmlem1  22662  xrhmeo  22745  lebnumlem1  22760  xrge0f  23498  itg2const2  23508  itg2uba  23510  itg2mono  23520  itg2gt0  23527  itg2cnlem2  23529  itg2cn  23530  iblss  23571  itgle  23576  itgeqa  23580  ibladdlem  23586  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgsplit  23602  bddmulibl  23605  xrge0addge  29522  xrge0infss  29525  xrge0addcld  29527  xrge0subcld  29528  xrge00  29686  xrge0tsmsd  29785  esummono  30116  gsumesum  30121  esumsnf  30126  esumrnmpt2  30130  esumpmono  30141  hashf2  30146  measge0  30270  measle0  30271  measssd  30278  measunl  30279  omssubaddlem  30361  omssubadd  30362  carsgsigalem  30377  pmeasmono  30386  sibfinima  30401  prob01  30475  dstrvprob  30533  itg2addnclem  33461  ibladdnclem  33466  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  xrge0ge0  39563