Theorem elxrge0 13592

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 11360	. . 3 ⊢ 0 ∈ ℝ*
3		pnfxr 11367	. . 3 ⊢ +∞ ∈ ℝ*
4		elicc1 13524	. . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 705	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 13263	. . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)
7	6	adantr 486	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 569	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 306	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7421  0cc0 11204  +∞cpnf 11344  ℝ^*cxr 11346   ≤ cle 11348  [,]cicc 13483

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-1cn 11262  ax-addrcl 11265  ax-rnegex 11275  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6541  df-fv 6547  df-ov 7424  df-oprab 7425  df-mpo 7426  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-icc 13487

This theorem is used by:  0e0iccpnf  13594  ge0xaddcl  13597  ge0xmulcl  13598  xnn0xrge0  13641  xrge0subm  21755  psmetxrge0  24638  isxmet2d  24652  prdsdsf  24692  prdsxmetlem  24693  comet  24838  stdbdxmet  24840  xrge0gsumle  25159  xrge0tsms  25160  metdsf  25174  metds0  25176  metdstri  25177  metdsre  25179  metdseq0  25180  metdscnlem  25181  metnrmlem1a  25184  xrhmeo  25273  lebnumlem1  25288  xrge0f  26058  itg2const2  26068  itg2uba  26070  itg2mono  26080  itg2gt0  26087  itg2cnlem2  26089  itg2cn  26090  iblss  26131  itgle  26136  itgeqa  26140  ibladdlem  26146  iblabs  26155  iblabsr  26156  iblmulc2  26157  itgsplit  26162  bddmulibl  26165  bddiblnc  26168  xrge0addge  33397  xrge0infss  33399  xrge0addcld  33401  xrge0subcld  33402  xrge00  33622  xrge0tsmsd  33681  fldextrspundglemul  34358  esummono  34733  gsumesum  34738  esumsnf  34743  esumrnmpt2  34747  esumpmono  34758  hashf2  34763  measge0  34887  measle0  34888  measssd  34895  measunl  34896  omssubaddlem  34978  omssubadd  34979  carsgsigalem  34994  pmeasmono  35003  sibfinima  35018  prob01  35092  dstrvprob  35151  itg2addnclem  38683  ibladdnclem  38688  iblabsnc  38696  iblmulc2nc  38697  ftc1anclem4  38708  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  xrge0ge0  46453  rrxsphere  49954