Theorem ltpnfd 13163

Description: Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
ltpnfd.a	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
ltpnfd	⊢ (𝜑 → 𝐴 < +∞)

Proof of Theorem ltpnfd

Step	Hyp	Ref	Expression
1		ltpnfd.a	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltpnf 13162	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 < +∞)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154  +∞cpnf 11292   < clt 11295

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-pnf 11297  df-xr 11299  df-ltxr 11300

This theorem is referenced by:  qbtwnxr  13242  xltnegi  13258  hashnnn0genn0  14382  limsupgre  15517  fprodge1  16031  xblss2ps  24411  blcvx  24819  reconnlem1  24848  iccpnfhmeo  24976  uniioombllem1  25616  ismbf3d  25689  mbflimsup  25701  itg2seq  25777  lhop2  26054  dvfsumlem2  26067  dvfsumlem2OLD  26068  logccv  26705  xrlimcnp  27011  pntleme  27652  absfico  45223  supxrge  45349  infxr  45378  infleinflem2  45382  xrralrecnnge  45401  iocopn  45533  ge0lere  45545  ressiooinf  45570  uzinico  45573  uzubioo  45580  fsumge0cl  45588  limcicciooub  45652  limcresiooub  45657  limcleqr  45659  limsupresico  45715  limsuppnfdlem  45716  limsupmnflem  45735  liminfresico  45786  limsup10exlem  45787  xlimpnfvlem1  45851  icccncfext  45902  fourierdlem31  46153  fourierdlem33  46155  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem75  46196  fourierdlem85  46206  fourierdlem88  46209  fourierdlem95  46216  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem109  46230  fourierdlem112  46233  fouriersw  46246  ioorrnopnxrlem  46321  sge0tsms  46395  sge0isum  46442  sge0ad2en  46446  sge0xaddlem2  46449  voliunsge0lem  46487  meassre  46492  omessre  46525  omeiunltfirp  46534  hoiprodcl  46562  ovnsubaddlem1  46585  hoiprodcl3  46595  hoidmvcl  46597  sge0hsphoire  46604  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem3  46612  hoidmvlelem4  46613  volicorege0  46652  ovolval5lem1  46667