Theorem ltpnf 13071

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 2736	. . . 4 ⊢ +∞ = +∞
2		orc 868	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 692	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 875	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11191	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11199	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13066	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 587	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   <_ℝ cltrr 11042  +∞cpnf 11176  -∞cmnf 11177  ℝ^*cxr 11178   < clt 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-pnf 11181  df-xr 11183  df-ltxr 11184

This theorem is referenced by:  ltpnfd  13072  0ltpnf  13073  xrlttri  13090  xrlttr  13091  xrrebnd  13120  xrre  13121  qbtwnxr  13152  xnn0lem1lt  13196  xrinfmsslem  13260  xrub  13264  supxrunb1  13271  supxrunb2  13272  dfrp2  13347  elioc2  13362  elicc2  13364  ioomax  13375  ioopos  13377  elioopnf  13396  elicopnf  13398  difreicc  13437  hashbnd  14298  hashv01gt1  14307  fprodge0  15958  fprodge1  15960  pcadd  16860  ramubcl  16989  rge0srg  21418  mnfnei  23186  icopnfcld  24732  iocmnfcld  24733  xrtgioo  24772  xrge0tsms  24800  ioombl1lem4  25528  icombl1  25530  mbfmax  25616  upgrfi  29160  topnfbey  30539  isblo3i  30872  htthlem  30988  xlt2addrd  32832  fsumrp0cl  33081  xrge0tsmsd  33134  pnfinf  33244  xrge0slmod  33408  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  lmxrge0  34096  esumcst  34207  esumcvgre  34235  voliune  34373  volfiniune  34374  sxbrsigalem0  34415  orvcgteel  34612  dstfrvclim1  34622  itg2addnclem2  37993  asindmre  38024  dvasin  38025  dvacos  38026  rfcnpre3  45464  supxrgere  45763  supxrgelem  45767  xrlexaddrp  45782  infxr  45796  xrpnf  45913  limsupre  46069  limsuppnflem  46138  liminflelimsupuz  46213  limsupub2  46240  icccncfext  46315  fourierdlem111  46645  fourierdlem113  46647  fouriersw  46659  sge0iunmptlemre  46843  sge0rpcpnf  46849  sge0xaddlem1  46861  meaiuninclem  46908  hoidmvlelem5  47027  ovolval5lem1  47080  pimltpnff  47131  iccpartiltu  47882  itscnhlinecirc02p  49261