Theorem ltpnf 13096

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 2732	. . . 4 ⊢ +∞ = +∞
2		orc 865	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 689	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 872	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11256	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11264	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13091	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 586	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 256	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   class class class wbr 5147  ℝcr 11105   <_ℝ cltrr 11110  +∞cpnf 11241  -∞cmnf 11242  ℝ^*cxr 11243   < clt 11244

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-pnf 11246  df-xr 11248  df-ltxr 11249

This theorem is referenced by:  ltpnfd  13097  0ltpnf  13098  xrlttri  13114  xrlttr  13115  xrrebnd  13143  xrre  13144  qbtwnxr  13175  xnn0lem1lt  13219  xrinfmsslem  13283  xrub  13287  supxrunb1  13294  supxrunb2  13295  dfrp2  13369  elioc2  13383  elicc2  13385  ioomax  13395  ioopos  13397  elioopnf  13416  elicopnf  13418  difreicc  13457  hashbnd  14292  hashv01gt1  14301  fprodge0  15933  fprodge1  15935  pcadd  16818  ramubcl  16947  rge0srg  21008  mnfnei  22716  icopnfcld  24275  iocmnfcld  24276  xrtgioo  24313  xrge0tsms  24341  ioombl1lem4  25069  icombl1  25071  mbfmax  25157  upgrfi  28340  topnfbey  29711  isblo3i  30041  htthlem  30157  xlt2addrd  31958  fsumrp0cl  32183  xrge0tsmsd  32196  pnfinf  32316  xrge0slmod  32451  xrge0iifcnv  32901  xrge0iifiso  32903  xrge0iifhom  32905  lmxrge0  32920  esumcst  33049  esumcvgre  33077  voliune  33215  volfiniune  33216  sxbrsigalem0  33258  orvcgteel  33454  dstfrvclim1  33464  itg2addnclem2  36528  asindmre  36559  dvasin  36560  dvacos  36561  rfcnpre3  43702  supxrgere  44029  supxrgelem  44033  xrlexaddrp  44048  infxr  44063  xrpnf  44182  limsupre  44343  limsuppnflem  44412  liminflelimsupuz  44487  limsupub2  44514  icccncfext  44589  fourierdlem111  44919  fourierdlem113  44921  fouriersw  44933  sge0iunmptlemre  45117  sge0rpcpnf  45123  sge0xaddlem1  45135  meaiuninclem  45182  hoidmvlelem5  45301  ovolval5lem1  45354  pimltpnff  45405  iccpartiltu  46076  itscnhlinecirc02p  47424