Theorem elxrge0 13408

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 1094	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 11190	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11197	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13340	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 698	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13079	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 481	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 564	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 304	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   ∈ wcel 2119   class class class wbr 5079  (class class class)co 7363  0cc0 11036  +∞cpnf 11174  ℝ^*cxr 11176   ≤ cle 11178  [,]cicc 13299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-addrcl 11097  ax-rnegex 11107  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-icc 13303

This theorem is referenced by:  0e0iccpnf  13410  ge0xaddcl  13413  ge0xmulcl  13414  xnn0xrge0  13457  xrge0subm  21425  psmetxrge0  24303  isxmet2d  24317  prdsdsf  24357  prdsxmetlem  24358  comet  24503  stdbdxmet  24505  xrge0gsumle  24824  xrge0tsms  24825  metdsf  24839  metds0  24841  metdstri  24842  metdsre  24844  metdseq0  24845  metdscnlem  24846  metnrmlem1a  24849  xrhmeo  24938  lebnumlem1  24953  xrge0f  25723  itg2const2  25733  itg2uba  25735  itg2mono  25745  itg2gt0  25752  itg2cnlem2  25754  itg2cn  25755  iblss  25797  itgle  25802  itgeqa  25806  ibladdlem  25812  iblabs  25821  iblabsr  25822  iblmulc2  25823  itgsplit  25828  bddmulibl  25831  bddiblnc  25834  xrge0addge  32857  xrge0infss  32859  xrge0addcld  32861  xrge0subcld  32862  xrge00  33100  xrge0tsmsd  33161  fldextrspundglemul  33870  esummono  34245  gsumesum  34250  esumsnf  34255  esumrnmpt2  34259  esumpmono  34270  hashf2  34275  measge0  34398  measle0  34399  measssd  34406  measunl  34407  omssubaddlem  34490  omssubadd  34491  carsgsigalem  34506  pmeasmono  34515  sibfinima  34530  prob01  34604  dstrvprob  34663  itg2addnclem  38045  ibladdnclem  38050  iblabsnc  38058  iblmulc2nc  38059  ftc1anclem4  38070  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  xrge0ge0  45799  rrxsphere  49246