Theorem ltpnfd 13145

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136  +∞cpnf 11274   < clt 11277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-xp 5671  df-pnf 11279  df-xr 11281  df-ltxr 11282

This theorem is referenced by:  qbtwnxr  13224  xltnegi  13240  hashnnn0genn0  14364  limsupgre  15499  fprodge1  16013  xblss2ps  24356  blcvx  24755  reconnlem1  24784  iccpnfhmeo  24912  uniioombllem1  25552  ismbf3d  25625  mbflimsup  25637  itg2seq  25713  lhop2  25990  dvfsumlem2  26003  dvfsumlem2OLD  26004  logccv  26641  xrlimcnp  26947  pntleme  27588  absfico  45180  supxrge  45306  infxr  45335  infleinflem2  45339  xrralrecnnge  45358  iocopn  45490  ge0lere  45502  ressiooinf  45527  uzinico  45530  uzubioo  45537  fsumge0cl  45545  limcicciooub  45609  limcresiooub  45614  limcleqr  45616  limsupresico  45672  limsuppnfdlem  45673  limsupmnflem  45692  liminfresico  45743  limsup10exlem  45744  xlimpnfvlem1  45808  icccncfext  45859  fourierdlem31  46110  fourierdlem33  46112  fourierdlem46  46124  fourierdlem48  46126  fourierdlem49  46127  fourierdlem75  46153  fourierdlem85  46163  fourierdlem88  46166  fourierdlem95  46173  fourierdlem103  46181  fourierdlem104  46182  fourierdlem107  46185  fourierdlem109  46187  fourierdlem112  46190  fouriersw  46203  ioorrnopnxrlem  46278  sge0tsms  46352  sge0isum  46399  sge0ad2en  46403  sge0xaddlem2  46406  voliunsge0lem  46444  meassre  46449  omessre  46482  omeiunltfirp  46491  hoiprodcl  46519  ovnsubaddlem1  46542  hoiprodcl3  46552  hoidmvcl  46554  sge0hsphoire  46561  hoidmv1lelem1  46563  hoidmv1lelem2  46564  hoidmv1lelem3  46565  hoidmv1le  46566  hoidmvlelem1  46567  hoidmvlelem3  46569  hoidmvlelem4  46570  volicorege0  46609  ovolval5lem1  46624