Theorem ltpnfd 13061

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5074  ℝcr 11026  +∞cpnf 11165   < clt 11168

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 2707  ax-sep 5220  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-cnex 11083

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 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-xp 5626  df-pnf 11170  df-xr 11172  df-ltxr 11173

This theorem is referenced by:  qbtwnxr  13141  xltnegi  13157  hashnnn0genn0  14294  limsupgre  15432  fprodge1  15949  xblss2ps  24354  blcvx  24751  reconnlem1  24780  iccpnfhmeo  24900  uniioombllem1  25536  ismbf3d  25609  mbflimsup  25621  itg2seq  25697  lhop2  25970  dvfsumlem2  25982  logccv  26615  xrlimcnp  26920  pntleme  27559  absfico  45635  supxrge  45756  infxr  45784  infleinflem2  45788  xrralrecnnge  45807  iocopn  45938  ge0lere  45950  ressiooinf  45975  uzinico  45977  uzubioo  45983  fsumge0cl  45991  limcicciooub  46053  limcresiooub  46058  limcleqr  46060  limsupresico  46116  limsuppnfdlem  46117  limsupmnflem  46136  liminfresico  46187  limsup10exlem  46188  xlimpnfvlem1  46252  icccncfext  46303  fourierdlem31  46554  fourierdlem33  46556  fourierdlem46  46568  fourierdlem48  46570  fourierdlem49  46571  fourierdlem75  46597  fourierdlem85  46607  fourierdlem88  46610  fourierdlem95  46617  fourierdlem103  46625  fourierdlem104  46626  fourierdlem107  46629  fourierdlem109  46631  fourierdlem112  46634  fouriersw  46647  ioorrnopnxrlem  46722  sge0tsms  46796  sge0isum  46843  sge0ad2en  46847  sge0xaddlem2  46850  voliunsge0lem  46888  meassre  46893  omessre  46926  omeiunltfirp  46935  hoiprodcl  46963  ovnsubaddlem1  46986  hoiprodcl3  46996  hoidmvcl  46998  sge0hsphoire  47005  hoidmv1lelem1  47007  hoidmv1lelem2  47008  hoidmv1lelem3  47009  hoidmv1le  47010  hoidmvlelem1  47011  hoidmvlelem3  47013  hoidmvlelem4  47014  volicorege0  47053  ovolval5lem1  47068