Theorem ltpnfd 13184

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  +∞cpnf 11321   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-pnf 11326  df-xr 11328  df-ltxr 11329

This theorem is referenced by:  qbtwnxr  13262  xltnegi  13278  hashnnn0genn0  14392  limsupgre  15527  fprodge1  16043  xblss2ps  24432  blcvx  24839  reconnlem1  24867  iccpnfhmeo  24995  uniioombllem1  25635  ismbf3d  25708  mbflimsup  25720  itg2seq  25797  lhop2  26074  dvfsumlem2  26087  dvfsumlem2OLD  26088  logccv  26723  xrlimcnp  27029  pntleme  27670  absfico  45125  supxrge  45253  infxr  45282  infleinflem2  45286  xrralrecnnge  45305  iocopn  45438  ge0lere  45450  ressiooinf  45475  uzinico  45478  uzubioo  45485  fsumge0cl  45494  limcicciooub  45558  limcresiooub  45563  limcleqr  45565  limsupresico  45621  limsuppnfdlem  45622  limsupmnflem  45641  liminfresico  45692  limsup10exlem  45693  xlimpnfvlem1  45757  icccncfext  45808  fourierdlem31  46059  fourierdlem33  46061  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem75  46102  fourierdlem85  46112  fourierdlem88  46115  fourierdlem95  46122  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem109  46136  fourierdlem112  46139  fouriersw  46152  ioorrnopnxrlem  46227  sge0tsms  46301  sge0isum  46348  sge0ad2en  46352  sge0xaddlem2  46355  voliunsge0lem  46393  meassre  46398  omessre  46431  omeiunltfirp  46440  hoiprodcl  46468  ovnsubaddlem1  46491  hoiprodcl3  46501  hoidmvcl  46503  sge0hsphoire  46510  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem3  46518  hoidmvlelem4  46519  volicorege0  46558  ovolval5lem1  46573