ltpnf - Intuitionistic Logic Explorer

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

Theorem ltpnf 9972

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
ltpnf	⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

**Proof of Theorem ltpnf**
Step	Hyp	Ref	Expression
1		eqid 2229	. . . 4 ⊢ +∞ = +∞
2		orc 717	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 425	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 739	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <_ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 8188	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
6		pnfxr 8195	. . 3 ⊢ +∞ ∈ ℝ^*
7		ltxr 9967	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <_ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 413	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <_ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 167	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 713 = wceq 1395 ∈ wcel 2200 class class class wbr 4082 ℝcr 7994 <_ℝ cltrr 7999 +∞cpnf 8174 -∞cmnf 8175 ℝ^*cxr 8176 < clt 8177

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-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4201 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-cnex 8086

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-br 4083 df-opab 4145 df-xp 4724 df-pnf 8179 df-xr 8181 df-ltxr 8182

This theorem is referenced by: ltpnfd 9973 0ltpnf 9974 xrlttr 9987 xrltso 9988 xrlttri3 9989 nltpnft 10006 npnflt 10007 xrrebnd 10011 xrre 10012 xltnegi 10027 xltadd1 10068 xposdif 10074 elioc2 10128 elicc2 10130 ioomax 10140 ioopos 10142 elioopnf 10159 elicopnf 10161 qbtwnxr 10472 dfrp2 10478 filtinf 11008 xrmaxltsup 11764 fprodge0 12143 fprodge1 12145 xblss2ps 15072

W3C validator