Theorem ltpnf 13171

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 2760	. . . 4 ⊢ +∞ = +∞
2		orc 881	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 888	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11279	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11287	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13166	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 598	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ℝcr 11123   <_ℝ cltrr 11128  +∞cpnf 11264  -∞cmnf 11265  ℝ^*cxr 11266   < clt 11267

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-pnf 11269  df-xr 11271  df-ltxr 11272

This theorem is used by:  ltpnfd  13172  0ltpnf  13173  xrlttri  13190  xrlttr  13191  xrrebnd  13220  xrre  13221  qbtwnxr  13252  xnn0lem1lt  13296  xrinfmsslem  13360  xrub  13364  supxrunb1  13371  supxrunb2  13372  dfrp2  13447  elioc2  13462  elicc2  13464  ioomax  13475  ioopos  13477  elioopnf  13496  elicopnf  13498  difreicc  13537  hashbnd  14400  hashv01gt1  14409  fprodge0  16080  fprodge1  16082  pcadd  16981  ramubcl  17110  rge0srg  21651  mnfnei  23446  icopnfcld  24993  iocmnfcld  24994  xrtgioo  25033  xrge0tsms  25061  ioombl1lem4  25789  icombl1  25791  mbfmax  25877  upgrfi  29548  topnfbey  30949  isblo3i  31282  htthlem  31398  xlt2addrd  33230  fsumrp0cl  33461  xrge0tsmsd  33513  pnfinf  33623  xrge0slmod  33788  xrge0iifcnv  34443  xrge0iifiso  34445  xrge0iifhom  34447  lmxrge0  34462  esumcst  34573  esumcvgre  34601  voliune  34740  volfiniune  34741  sxbrsigalem0  34782  orvcgteel  34979  dstfrvclim1  34989  itg2addnclem2  38421  asindmre  38452  dvasin  38453  dvacos  38454  rfcnpre3  45867  supxrgere  46163  supxrgelem  46167  xrlexaddrp  46182  infxr  46196  xrpnf  46313  limsupre  46469  limsuppnflem  46538  liminflelimsupuz  46613  limsupub2  46640  icccncfext  46715  fourierdlem111  47045  fouriersw  47059  sge0iunmptlemre  47243  sge0rpcpnf  47249  sge0xaddlem1  47261  meaiuninclem  47308  hoidmvlelem5  47427  ovolval5lem1  47480  pimltpnff  47531  iccpartiltu  48322  itscnhlinecirc02p  49715