Theorem ltpnfd 13033

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023  +∞cpnf 11161   < clt 11164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-pnf 11166  df-xr 11168  df-ltxr 11169

This theorem is referenced by:  qbtwnxr  13113  xltnegi  13129  hashnnn0genn0  14264  limsupgre  15402  fprodge1  15916  xblss2ps  24343  blcvx  24740  reconnlem1  24769  iccpnfhmeo  24897  uniioombllem1  25536  ismbf3d  25609  mbflimsup  25621  itg2seq  25697  lhop2  25974  dvfsumlem2  25987  dvfsumlem2OLD  25988  logccv  26626  xrlimcnp  26932  pntleme  27573  absfico  45404  supxrge  45525  infxr  45553  infleinflem2  45557  xrralrecnnge  45576  iocopn  45708  ge0lere  45720  ressiooinf  45745  uzinico  45747  uzubioo  45753  fsumge0cl  45761  limcicciooub  45823  limcresiooub  45828  limcleqr  45830  limsupresico  45886  limsuppnfdlem  45887  limsupmnflem  45906  liminfresico  45957  limsup10exlem  45958  xlimpnfvlem1  46022  icccncfext  46073  fourierdlem31  46324  fourierdlem33  46326  fourierdlem46  46338  fourierdlem48  46340  fourierdlem49  46341  fourierdlem75  46367  fourierdlem85  46377  fourierdlem88  46380  fourierdlem95  46387  fourierdlem103  46395  fourierdlem104  46396  fourierdlem107  46399  fourierdlem109  46401  fourierdlem112  46404  fouriersw  46417  ioorrnopnxrlem  46492  sge0tsms  46566  sge0isum  46613  sge0ad2en  46617  sge0xaddlem2  46620  voliunsge0lem  46658  meassre  46663  omessre  46696  omeiunltfirp  46705  hoiprodcl  46733  ovnsubaddlem1  46756  hoiprodcl3  46766  hoidmvcl  46768  sge0hsphoire  46775  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmv1le  46780  hoidmvlelem1  46781  hoidmvlelem3  46783  hoidmvlelem4  46784  volicorege0  46823  ovolval5lem1  46838