Theorem ltpnf 13019

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 2731	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11158	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11166	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13014	. . 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 2111   class class class wbr 5089  ℝcr 11005   <_ℝ cltrr 11010  +∞cpnf 11143  -∞cmnf 11144  ℝ^*cxr 11145   < clt 11146

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-xp 5620  df-pnf 11148  df-xr 11150  df-ltxr 11151

This theorem is referenced by:  ltpnfd  13020  0ltpnf  13021  xrlttri  13038  xrlttr  13039  xrrebnd  13067  xrre  13068  qbtwnxr  13099  xnn0lem1lt  13143  xrinfmsslem  13207  xrub  13211  supxrunb1  13218  supxrunb2  13219  dfrp2  13294  elioc2  13309  elicc2  13311  ioomax  13322  ioopos  13324  elioopnf  13343  elicopnf  13345  difreicc  13384  hashbnd  14243  hashv01gt1  14252  fprodge0  15900  fprodge1  15902  pcadd  16801  ramubcl  16930  rge0srg  21375  mnfnei  23136  icopnfcld  24682  iocmnfcld  24683  xrtgioo  24722  xrge0tsms  24750  ioombl1lem4  25489  icombl1  25491  mbfmax  25577  upgrfi  29069  topnfbey  30449  isblo3i  30781  htthlem  30897  xlt2addrd  32742  fsumrp0cl  33002  xrge0tsmsd  33042  pnfinf  33152  xrge0slmod  33313  xrge0iifcnv  33946  xrge0iifiso  33948  xrge0iifhom  33950  lmxrge0  33965  esumcst  34076  esumcvgre  34104  voliune  34242  volfiniune  34243  sxbrsigalem0  34284  orvcgteel  34481  dstfrvclim1  34491  itg2addnclem2  37720  asindmre  37751  dvasin  37752  dvacos  37753  rfcnpre3  45078  supxrgere  45380  supxrgelem  45384  xrlexaddrp  45399  infxr  45413  xrpnf  45531  limsupre  45687  limsuppnflem  45756  liminflelimsupuz  45831  limsupub2  45858  icccncfext  45933  fourierdlem111  46263  fourierdlem113  46265  fouriersw  46277  sge0iunmptlemre  46461  sge0rpcpnf  46467  sge0xaddlem1  46479  meaiuninclem  46526  hoidmvlelem5  46645  ovolval5lem1  46698  pimltpnff  46749  iccpartiltu  47461  itscnhlinecirc02p  48825