Theorem ltpnf 13080

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 2729	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11220	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11228	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13075	. . 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 1540   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   <_ℝ cltrr 11072  +∞cpnf 11205  -∞cmnf 11206  ℝ^*cxr 11207   < clt 11208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-pnf 11210  df-xr 11212  df-ltxr 11213

This theorem is referenced by:  ltpnfd  13081  0ltpnf  13082  xrlttri  13099  xrlttr  13100  xrrebnd  13128  xrre  13129  qbtwnxr  13160  xnn0lem1lt  13204  xrinfmsslem  13268  xrub  13272  supxrunb1  13279  supxrunb2  13280  dfrp2  13355  elioc2  13370  elicc2  13372  ioomax  13383  ioopos  13385  elioopnf  13404  elicopnf  13406  difreicc  13445  hashbnd  14301  hashv01gt1  14310  fprodge0  15959  fprodge1  15961  pcadd  16860  ramubcl  16989  rge0srg  21355  mnfnei  23108  icopnfcld  24655  iocmnfcld  24656  xrtgioo  24695  xrge0tsms  24723  ioombl1lem4  25462  icombl1  25464  mbfmax  25550  upgrfi  29018  topnfbey  30398  isblo3i  30730  htthlem  30846  xlt2addrd  32682  fsumrp0cl  32962  xrge0tsmsd  33002  pnfinf  33137  xrge0slmod  33319  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  lmxrge0  33942  esumcst  34053  esumcvgre  34081  voliune  34219  volfiniune  34220  sxbrsigalem0  34262  orvcgteel  34459  dstfrvclim1  34469  itg2addnclem2  37666  asindmre  37697  dvasin  37698  dvacos  37699  rfcnpre3  45027  supxrgere  45329  supxrgelem  45333  xrlexaddrp  45348  infxr  45363  xrpnf  45481  limsupre  45639  limsuppnflem  45708  liminflelimsupuz  45783  limsupub2  45810  icccncfext  45885  fourierdlem111  46215  fourierdlem113  46217  fouriersw  46229  sge0iunmptlemre  46413  sge0rpcpnf  46419  sge0xaddlem1  46431  meaiuninclem  46478  hoidmvlelem5  46597  ovolval5lem1  46650  pimltpnff  46701  iccpartiltu  47423  itscnhlinecirc02p  48774