Theorem ltpnfd 13047

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  +∞cpnf 11175   < clt 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-pnf 11180  df-xr 11182  df-ltxr 11183

This theorem is referenced by:  qbtwnxr  13127  xltnegi  13143  hashnnn0genn0  14278  limsupgre  15416  fprodge1  15930  xblss2ps  24360  blcvx  24757  reconnlem1  24786  iccpnfhmeo  24914  uniioombllem1  25553  ismbf3d  25626  mbflimsup  25638  itg2seq  25714  lhop2  25991  dvfsumlem2  26004  dvfsumlem2OLD  26005  logccv  26643  xrlimcnp  26949  pntleme  27590  absfico  45580  supxrge  45701  infxr  45729  infleinflem2  45733  xrralrecnnge  45752  iocopn  45884  ge0lere  45896  ressiooinf  45921  uzinico  45923  uzubioo  45929  fsumge0cl  45937  limcicciooub  45999  limcresiooub  46004  limcleqr  46006  limsupresico  46062  limsuppnfdlem  46063  limsupmnflem  46082  liminfresico  46133  limsup10exlem  46134  xlimpnfvlem1  46198  icccncfext  46249  fourierdlem31  46500  fourierdlem33  46502  fourierdlem46  46514  fourierdlem48  46516  fourierdlem49  46517  fourierdlem75  46543  fourierdlem85  46553  fourierdlem88  46556  fourierdlem95  46563  fourierdlem103  46571  fourierdlem104  46572  fourierdlem107  46575  fourierdlem109  46577  fourierdlem112  46580  fouriersw  46593  ioorrnopnxrlem  46668  sge0tsms  46742  sge0isum  46789  sge0ad2en  46793  sge0xaddlem2  46796  voliunsge0lem  46834  meassre  46839  omessre  46872  omeiunltfirp  46881  hoiprodcl  46909  ovnsubaddlem1  46932  hoiprodcl3  46942  hoidmvcl  46944  sge0hsphoire  46951  hoidmv1lelem1  46953  hoidmv1lelem2  46954  hoidmv1lelem3  46955  hoidmv1le  46956  hoidmvlelem1  46957  hoidmvlelem3  46959  hoidmvlelem4  46960  volicorege0  46999  ovolval5lem1  47014