Theorem ltpnf 12601

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 2739	. . . 4 ⊢ +∞ = +∞
2		orc 866	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 873	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10768	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10776	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 12596	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 589	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 846   = wceq 1542   ∈ wcel 2114   class class class wbr 5031  ℝcr 10617   <_ℝ cltrr 10622  +∞cpnf 10753  -∞cmnf 10754  ℝ^*cxr 10755   < clt 10756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482  ax-cnex 10674

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-v 3401  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-opab 5094  df-xp 5532  df-pnf 10758  df-xr 10760  df-ltxr 10761

This theorem is referenced by:  ltpnfd  12602  0ltpnf  12603  xrlttri  12618  xrlttr  12619  xrrebnd  12647  xrre  12648  qbtwnxr  12679  xnn0lem1lt  12723  xrinfmsslem  12787  xrub  12791  supxrunb1  12798  supxrunb2  12799  dfrp2  12873  elioc2  12887  elicc2  12889  ioomax  12899  ioopos  12901  elioopnf  12920  elicopnf  12922  difreicc  12961  hashbnd  13791  hashv01gt1  13800  fprodge0  15442  fprodge1  15444  pcadd  16328  ramubcl  16457  rge0srg  20291  mnfnei  21975  icopnfcld  23523  iocmnfcld  23524  xrtgioo  23561  xrge0tsms  23589  ioombl1lem4  24316  icombl1  24318  mbfmax  24404  upgrfi  27039  topnfbey  28409  isblo3i  28739  htthlem  28855  xlt2addrd  30659  fsumrp0cl  30884  xrge0tsmsd  30897  pnfinf  31017  xrge0slmod  31123  xrge0iifcnv  31458  xrge0iifiso  31460  xrge0iifhom  31462  lmxrge0  31477  esumcst  31604  esumcvgre  31632  voliune  31770  volfiniune  31771  sxbrsigalem0  31811  orvcgteel  32007  dstfrvclim1  32017  itg2addnclem2  35475  asindmre  35506  dvasin  35507  dvacos  35508  rfcnpre3  42137  supxrgere  42433  supxrgelem  42437  xrlexaddrp  42452  infxr  42467  xrpnf  42589  limsupre  42747  limsuppnflem  42816  liminflelimsupuz  42891  limsupub2  42918  icccncfext  42993  fourierdlem111  43323  fourierdlem113  43325  fouriersw  43337  sge0iunmptlemre  43518  sge0rpcpnf  43524  sge0xaddlem1  43536  meaiuninclem  43583  hoidmvlelem5  43702  ovolval5lem1  43755  pimltpnf  43805  iccpartiltu  44438  itscnhlinecirc02p  45695