Theorem ltpnf 12856

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 2738	. . . 4 ⊢ +∞ = +∞
2		orc 864	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 688	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 871	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11021	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11029	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 12851	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 586	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 256	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870   <_ℝ cltrr 10875  +∞cpnf 11006  -∞cmnf 11007  ℝ^*cxr 11008   < clt 11009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-pnf 11011  df-xr 11013  df-ltxr 11014

This theorem is referenced by:  ltpnfd  12857  0ltpnf  12858  xrlttri  12873  xrlttr  12874  xrrebnd  12902  xrre  12903  qbtwnxr  12934  xnn0lem1lt  12978  xrinfmsslem  13042  xrub  13046  supxrunb1  13053  supxrunb2  13054  dfrp2  13128  elioc2  13142  elicc2  13144  ioomax  13154  ioopos  13156  elioopnf  13175  elicopnf  13177  difreicc  13216  hashbnd  14050  hashv01gt1  14059  fprodge0  15703  fprodge1  15705  pcadd  16590  ramubcl  16719  rge0srg  20669  mnfnei  22372  icopnfcld  23931  iocmnfcld  23932  xrtgioo  23969  xrge0tsms  23997  ioombl1lem4  24725  icombl1  24727  mbfmax  24813  upgrfi  27461  topnfbey  28833  isblo3i  29163  htthlem  29279  xlt2addrd  31081  fsumrp0cl  31304  xrge0tsmsd  31317  pnfinf  31437  xrge0slmod  31548  xrge0iifcnv  31883  xrge0iifiso  31885  xrge0iifhom  31887  lmxrge0  31902  esumcst  32031  esumcvgre  32059  voliune  32197  volfiniune  32198  sxbrsigalem0  32238  orvcgteel  32434  dstfrvclim1  32444  itg2addnclem2  35829  asindmre  35860  dvasin  35861  dvacos  35862  rfcnpre3  42576  supxrgere  42872  supxrgelem  42876  xrlexaddrp  42891  infxr  42906  xrpnf  43026  limsupre  43182  limsuppnflem  43251  liminflelimsupuz  43326  limsupub2  43353  icccncfext  43428  fourierdlem111  43758  fourierdlem113  43760  fouriersw  43772  sge0iunmptlemre  43953  sge0rpcpnf  43959  sge0xaddlem1  43971  meaiuninclem  44018  hoidmvlelem5  44137  ovolval5lem1  44190  pimltpnf  44241  iccpartiltu  44874  itscnhlinecirc02p  46131