Theorem ltpnfd 13174

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  ℝcr 11126  +∞cpnf 11267   < clt 11270

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-xp 5665  df-pnf 11272  df-xr 11274  df-ltxr 11275

This theorem is used by:  qbtwnxr  13254  xltnegi  13270  hashnnn0genn0  14409  limsupgre  15570  fprodge1  16086  xblss2ps  24628  blcvx  25025  reconnlem1  25054  iccpnfhmeo  25174  uniioombllem1  25810  ismbf3d  25883  mbflimsup  25895  itg2seq  25971  lhop2  26244  dvfsumlem2  26256  logccv  26898  xrlimcnp  27203  pntleme  27842  absfico  46035  supxrge  46155  infxr  46183  infleinflem2  46187  xrralrecnnge  46206  iocopn  46337  ge0lere  46349  ressiooinf  46374  uzinico  46376  uzubioo  46382  fsumge0cl  46390  limcicciooub  46452  limcresiooub  46457  limcleqr  46459  limsupresico  46515  limsuppnfdlem  46516  limsupmnflem  46535  liminfresico  46586  limsup10exlem  46587  xlimpnfvlem1  46651  icccncfext  46702  fourierdlem31  46953  fourierdlem33  46955  fourierdlem46  46967  fourierdlem48  46969  fourierdlem49  46970  fourierdlem75  46996  fourierdlem85  47006  fourierdlem88  47009  fourierdlem95  47016  fourierdlem103  47024  fourierdlem104  47025  fourierdlem107  47028  fourierdlem109  47030  fourierdlem112  47033  fouriersw  47046  ioorrnopnxrlem  47121  sge0tsms  47195  sge0isum  47242  sge0ad2en  47246  sge0xaddlem2  47249  voliunsge0lem  47287  meassre  47292  omessre  47325  omeiunltfirp  47334  hoiprodcl  47362  ovnsubaddlem1  47385  hoiprodcl3  47395  hoidmvcl  47397  sge0hsphoire  47404  hoidmv1lelem1  47406  hoidmv1lelem2  47407  hoidmv1lelem3  47408  hoidmv1le  47409  hoidmvlelem1  47410  hoidmvlelem3  47412  hoidmvlelem4  47413  volicorege0  47452  ovolval5lem1  47467