elxrge0 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > elxrge0		GIF version

Theorem elxrge0 10310

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 1007	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
2		0xr 8319	. . 3 ⊢ 0 ∈ ℝ^*
3		pnfxr 8325	. . 3 ⊢ +∞ ∈ ℝ^*
4		elicc1 10256	. . 3 ⊢ ((0 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ^ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)))
5	2, 3, 4	mp2an 426	. 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))
6		pnfge 10121	. . . 4 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
7	6	adantr 276	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞)
8	7	pm4.71i 391	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞))
9	1, 5, 8	3bitr4i 212	1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴))

Colors of variables: wff set class

Syntax hints: ∧ wa 104 ↔ wb 105 ∧ w3a 1005 ∈ wcel 2203 class class class wbr 4108 (class class class)co 6049 0cc0 8126 +∞cpnf 8304 ℝ^*cxr 8306 ≤ cle 8308 [,]cicc 10223

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-sep 4227 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-cnex 8217 ax-resscn 8218 ax-1re 8220 ax-addrcl 8223 ax-rnegex 8235

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-rab 2529 df-v 2814 df-sbc 3042 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-pw 3670 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-br 4109 df-opab 4171 df-id 4413 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-iota 5311 df-fun 5353 df-fv 5359 df-ov 6052 df-oprab 6053 df-mpo 6054 df-pnf 8309 df-mnf 8310 df-xr 8311 df-ltxr 8312 df-le 8313 df-icc 10227

This theorem is referenced by: 0e0iccpnf 10312 ge0xaddcl 10315 psmetxrge0 15189 isxmet2d 15205 comet 15356 bdxmet 15358

W3C validator