Theorem ltpnfd 13088

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 13087	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 < +∞)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  +∞cpnf 11212   < clt 11215

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-pnf 11217  df-xr 11219  df-ltxr 11220

This theorem is referenced by:  qbtwnxr  13167  xltnegi  13183  hashnnn0genn0  14315  limsupgre  15454  fprodge1  15968  xblss2ps  24296  blcvx  24693  reconnlem1  24722  iccpnfhmeo  24850  uniioombllem1  25489  ismbf3d  25562  mbflimsup  25574  itg2seq  25650  lhop2  25927  dvfsumlem2  25940  dvfsumlem2OLD  25941  logccv  26579  xrlimcnp  26885  pntleme  27526  absfico  45219  supxrge  45341  infxr  45370  infleinflem2  45374  xrralrecnnge  45393  iocopn  45525  ge0lere  45537  ressiooinf  45562  uzinico  45564  uzubioo  45570  fsumge0cl  45578  limcicciooub  45642  limcresiooub  45647  limcleqr  45649  limsupresico  45705  limsuppnfdlem  45706  limsupmnflem  45725  liminfresico  45776  limsup10exlem  45777  xlimpnfvlem1  45841  icccncfext  45892  fourierdlem31  46143  fourierdlem33  46145  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem75  46186  fourierdlem85  46196  fourierdlem88  46199  fourierdlem95  46206  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem109  46220  fourierdlem112  46223  fouriersw  46236  ioorrnopnxrlem  46311  sge0tsms  46385  sge0isum  46432  sge0ad2en  46436  sge0xaddlem2  46439  voliunsge0lem  46477  meassre  46482  omessre  46515  omeiunltfirp  46524  hoiprodcl  46552  ovnsubaddlem1  46575  hoiprodcl3  46585  hoidmvcl  46587  sge0hsphoire  46594  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem3  46602  hoidmvlelem4  46603  volicorege0  46642  ovolval5lem1  46657