Theorem ltpnfd 13146

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5111  ℝcr 11099  +∞cpnf 11240   < clt 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5668  df-pnf 11245  df-xr 11247  df-ltxr 11248

This theorem is referenced by:  qbtwnxr  13226  xltnegi  13242  hashnnn0genn0  14379  limsupgre  15532  fprodge1  16049  xblss2ps  24527  blcvx  24924  reconnlem1  24953  iccpnfhmeo  25073  uniioombllem1  25709  ismbf3d  25782  mbflimsup  25794  itg2seq  25870  lhop2  26143  dvfsumlem2  26155  logccv  26794  xrlimcnp  27099  pntleme  27738  absfico  45861  supxrge  45981  infxr  46009  infleinflem2  46013  xrralrecnnge  46032  iocopn  46163  ge0lere  46175  ressiooinf  46200  uzinico  46202  uzubioo  46208  fsumge0cl  46216  limcicciooub  46278  limcresiooub  46283  limcleqr  46285  limsupresico  46341  limsuppnfdlem  46342  limsupmnflem  46361  liminfresico  46412  limsup10exlem  46413  xlimpnfvlem1  46477  icccncfext  46528  fourierdlem31  46779  fourierdlem33  46781  fourierdlem46  46793  fourierdlem48  46795  fourierdlem49  46796  fourierdlem75  46822  fourierdlem85  46832  fourierdlem88  46835  fourierdlem95  46842  fourierdlem103  46850  fourierdlem104  46851  fourierdlem107  46854  fourierdlem109  46856  fourierdlem112  46859  fouriersw  46872  ioorrnopnxrlem  46947  sge0tsms  47021  sge0isum  47068  sge0ad2en  47072  sge0xaddlem2  47075  voliunsge0lem  47113  meassre  47118  omessre  47151  omeiunltfirp  47160  hoiprodcl  47188  ovnsubaddlem1  47211  hoiprodcl3  47221  hoidmvcl  47223  sge0hsphoire  47230  hoidmv1lelem1  47232  hoidmv1lelem2  47233  hoidmv1lelem3  47234  hoidmv1le  47235  hoidmvlelem1  47236  hoidmvlelem3  47238  hoidmvlelem4  47239  volicorege0  47278  ovolval5lem1  47293