Theorem ltpnfd 13020

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005  +∞cpnf 11143   < clt 11146

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-xp 5620  df-pnf 11148  df-xr 11150  df-ltxr 11151

This theorem is referenced by:  qbtwnxr  13099  xltnegi  13115  hashnnn0genn0  14250  limsupgre  15388  fprodge1  15902  xblss2ps  24316  blcvx  24713  reconnlem1  24742  iccpnfhmeo  24870  uniioombllem1  25509  ismbf3d  25582  mbflimsup  25594  itg2seq  25670  lhop2  25947  dvfsumlem2  25960  dvfsumlem2OLD  25961  logccv  26599  xrlimcnp  26905  pntleme  27546  absfico  45325  supxrge  45447  infxr  45475  infleinflem2  45479  xrralrecnnge  45498  iocopn  45630  ge0lere  45642  ressiooinf  45667  uzinico  45669  uzubioo  45675  fsumge0cl  45683  limcicciooub  45745  limcresiooub  45750  limcleqr  45752  limsupresico  45808  limsuppnfdlem  45809  limsupmnflem  45828  liminfresico  45879  limsup10exlem  45880  xlimpnfvlem1  45944  icccncfext  45995  fourierdlem31  46246  fourierdlem33  46248  fourierdlem46  46260  fourierdlem48  46262  fourierdlem49  46263  fourierdlem75  46289  fourierdlem85  46299  fourierdlem88  46302  fourierdlem95  46309  fourierdlem103  46317  fourierdlem104  46318  fourierdlem107  46321  fourierdlem109  46323  fourierdlem112  46326  fouriersw  46339  ioorrnopnxrlem  46414  sge0tsms  46488  sge0isum  46535  sge0ad2en  46539  sge0xaddlem2  46542  voliunsge0lem  46580  meassre  46585  omessre  46618  omeiunltfirp  46627  hoiprodcl  46655  ovnsubaddlem1  46678  hoiprodcl3  46688  hoidmvcl  46690  sge0hsphoire  46697  hoidmv1lelem1  46699  hoidmv1lelem2  46700  hoidmv1lelem3  46701  hoidmv1le  46702  hoidmvlelem1  46703  hoidmvlelem3  46705  hoidmvlelem4  46706  volicorege0  46745  ovolval5lem1  46760