Theorem ltpnf 13032

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 2734	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11176	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11184	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13027	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 586	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   <_ℝ cltrr 11028  +∞cpnf 11161  -∞cmnf 11162  ℝ^*cxr 11163   < clt 11164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-pnf 11166  df-xr 11168  df-ltxr 11169

This theorem is referenced by:  ltpnfd  13033  0ltpnf  13034  xrlttri  13051  xrlttr  13052  xrrebnd  13081  xrre  13082  qbtwnxr  13113  xnn0lem1lt  13157  xrinfmsslem  13221  xrub  13225  supxrunb1  13232  supxrunb2  13233  dfrp2  13308  elioc2  13323  elicc2  13325  ioomax  13336  ioopos  13338  elioopnf  13357  elicopnf  13359  difreicc  13398  hashbnd  14257  hashv01gt1  14266  fprodge0  15914  fprodge1  15916  pcadd  16815  ramubcl  16944  rge0srg  21391  mnfnei  23163  icopnfcld  24709  iocmnfcld  24710  xrtgioo  24749  xrge0tsms  24777  ioombl1lem4  25516  icombl1  25518  mbfmax  25604  upgrfi  29113  topnfbey  30493  isblo3i  30825  htthlem  30941  xlt2addrd  32788  fsumrp0cl  33052  xrge0tsmsd  33104  pnfinf  33214  xrge0slmod  33378  xrge0iifcnv  34039  xrge0iifiso  34041  xrge0iifhom  34043  lmxrge0  34058  esumcst  34169  esumcvgre  34197  voliune  34335  volfiniune  34336  sxbrsigalem0  34377  orvcgteel  34574  dstfrvclim1  34584  itg2addnclem2  37812  asindmre  37843  dvasin  37844  dvacos  37845  rfcnpre3  45220  supxrgere  45520  supxrgelem  45524  xrlexaddrp  45539  infxr  45553  xrpnf  45671  limsupre  45827  limsuppnflem  45896  liminflelimsupuz  45971  limsupub2  45998  icccncfext  46073  fourierdlem111  46403  fourierdlem113  46405  fouriersw  46417  sge0iunmptlemre  46601  sge0rpcpnf  46607  sge0xaddlem1  46619  meaiuninclem  46666  hoidmvlelem5  46785  ovolval5lem1  46838  pimltpnff  46889  iccpartiltu  47610  itscnhlinecirc02p  48973