Theorem ltpnfd 13069

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11034  +∞cpnf 11173   < clt 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5634  df-pnf 11178  df-xr 11180  df-ltxr 11181

This theorem is referenced by:  qbtwnxr  13149  xltnegi  13165  hashnnn0genn0  14302  limsupgre  15440  fprodge1  15957  xblss2ps  24382  blcvx  24779  reconnlem1  24808  iccpnfhmeo  24928  uniioombllem1  25564  ismbf3d  25637  mbflimsup  25649  itg2seq  25725  lhop2  25998  dvfsumlem2  26010  logccv  26646  xrlimcnp  26951  pntleme  27591  absfico  45673  supxrge  45794  infxr  45822  infleinflem2  45826  xrralrecnnge  45845  iocopn  45976  ge0lere  45988  ressiooinf  46013  uzinico  46015  uzubioo  46021  fsumge0cl  46029  limcicciooub  46091  limcresiooub  46096  limcleqr  46098  limsupresico  46154  limsuppnfdlem  46155  limsupmnflem  46174  liminfresico  46225  limsup10exlem  46226  xlimpnfvlem1  46290  icccncfext  46341  fourierdlem31  46592  fourierdlem33  46594  fourierdlem46  46606  fourierdlem48  46608  fourierdlem49  46609  fourierdlem75  46635  fourierdlem85  46645  fourierdlem88  46648  fourierdlem95  46655  fourierdlem103  46663  fourierdlem104  46664  fourierdlem107  46667  fourierdlem109  46669  fourierdlem112  46672  fouriersw  46685  ioorrnopnxrlem  46760  sge0tsms  46834  sge0isum  46881  sge0ad2en  46885  sge0xaddlem2  46888  voliunsge0lem  46926  meassre  46931  omessre  46964  omeiunltfirp  46973  hoiprodcl  47001  ovnsubaddlem1  47024  hoiprodcl3  47034  hoidmvcl  47036  sge0hsphoire  47043  hoidmv1lelem1  47045  hoidmv1lelem2  47046  hoidmv1lelem3  47047  hoidmv1le  47048  hoidmvlelem1  47049  hoidmvlelem3  47051  hoidmvlelem4  47052  volicorege0  47091  ovolval5lem1  47106