Theorem ltpnfd 13205

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11156  +∞cpnf 11297   < clt 11300

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 2732  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5654  df-pnf 11302  df-xr 11304  df-ltxr 11305

This theorem is used by:  qbtwnxr  13285  xltnegi  13301  hashnnn0genn0  14440  limsupgre  15601  fprodge1  16115  xblss2ps  24667  blcvx  25064  reconnlem1  25093  iccpnfhmeo  25213  uniioombllem1  25849  ismbf3d  25922  mbflimsup  25934  itg2seq  26010  lhop2  26282  dvfsumlem2  26294  logccv  26940  xrlimcnp  27245  pntleme  27884  absfico  46146  supxrge  46266  infxr  46294  infleinflem2  46298  xrralrecnnge  46317  iocopn  46448  ge0lere  46460  ressiooinf  46485  uzinico  46487  uzubioo  46493  fsumge0cl  46501  limcicciooub  46563  limcresiooub  46568  limcleqr  46570  limsupresico  46626  limsuppnfdlem  46627  limsupmnflem  46646  liminfresico  46697  limsup10exlem  46698  xlimpnfvlem1  46762  icccncfext  46813  fourierdlem31  47064  fourierdlem33  47066  fourierdlem46  47078  fourierdlem48  47080  fourierdlem49  47081  fourierdlem75  47107  fourierdlem85  47117  fourierdlem88  47120  fourierdlem95  47127  fourierdlem103  47135  fourierdlem104  47136  fourierdlem107  47139  fourierdlem109  47141  fourierdlem112  47144  fouriersw  47157  ioorrnopnxrlem  47232  sge0tsms  47306  sge0isum  47353  sge0ad2en  47357  sge0xaddlem2  47360  voliunsge0lem  47398  meassre  47403  omessre  47436  omeiunltfirp  47445  hoiprodcl  47473  ovnsubaddlem1  47496  hoiprodcl3  47506  hoidmvcl  47508  sge0hsphoire  47515  hoidmv1lelem1  47517  hoidmv1lelem2  47518  hoidmv1lelem3  47519  hoidmv1le  47520  hoidmvlelem1  47521  hoidmvlelem3  47523  hoidmvlelem4  47524  volicorege0  47563  ovolval5lem1  47578