Theorem ltpnf 13161

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 2765	. . . 4 ⊢ +∞ = +∞
2		orc 881	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 888	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11270	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11278	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13156	. . 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 2146   class class class wbr 5111  ℝcr 11114   <_ℝ cltrr 11119  +∞cpnf 11255  -∞cmnf 11256  ℝ^*cxr 11257   < clt 11258

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-pnf 11260  df-xr 11262  df-ltxr 11263

This theorem is used by:  ltpnfd  13162  0ltpnf  13163  xrlttri  13180  xrlttr  13181  xrrebnd  13210  xrre  13211  qbtwnxr  13242  xnn0lem1lt  13286  xrinfmsslem  13350  xrub  13354  supxrunb1  13361  supxrunb2  13362  dfrp2  13437  elioc2  13452  elicc2  13454  ioomax  13465  ioopos  13467  elioopnf  13486  elicopnf  13488  difreicc  13527  hashbnd  14390  hashv01gt1  14399  fprodge0  16070  fprodge1  16072  pcadd  16971  ramubcl  17100  rge0srg  21638  mnfnei  23428  icopnfcld  24975  iocmnfcld  24976  xrtgioo  25015  xrge0tsms  25043  ioombl1lem4  25771  icombl1  25773  mbfmax  25859  upgrfi  29496  topnfbey  30891  isblo3i  31224  htthlem  31340  xlt2addrd  33174  fsumrp0cl  33405  xrge0tsmsd  33457  pnfinf  33567  xrge0slmod  33732  xrge0iifcnv  34387  xrge0iifiso  34389  xrge0iifhom  34391  lmxrge0  34406  esumcst  34517  esumcvgre  34545  voliune  34684  volfiniune  34685  sxbrsigalem0  34726  orvcgteel  34923  dstfrvclim1  34933  itg2addnclem2  38380  asindmre  38411  dvasin  38412  dvacos  38413  rfcnpre3  45811  supxrgere  46107  supxrgelem  46111  xrlexaddrp  46126  infxr  46140  xrpnf  46257  limsupre  46413  limsuppnflem  46482  liminflelimsupuz  46557  limsupub2  46584  icccncfext  46659  fourierdlem111  46989  fouriersw  47003  sge0iunmptlemre  47187  sge0rpcpnf  47193  sge0xaddlem1  47205  meaiuninclem  47252  hoidmvlelem5  47371  ovolval5lem1  47424  pimltpnff  47475  iccpartiltu  48229  itscnhlinecirc02p  49622