Theorem ltpnfd 13049

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11039  +∞cpnf 11177   < clt 11180

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 5245  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096

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 5640  df-pnf 11182  df-xr 11184  df-ltxr 11185

This theorem is referenced by:  qbtwnxr  13129  xltnegi  13145  hashnnn0genn0  14280  limsupgre  15418  fprodge1  15932  xblss2ps  24362  blcvx  24759  reconnlem1  24788  iccpnfhmeo  24916  uniioombllem1  25555  ismbf3d  25628  mbflimsup  25640  itg2seq  25716  lhop2  25993  dvfsumlem2  26006  dvfsumlem2OLD  26007  logccv  26645  xrlimcnp  26951  pntleme  27592  absfico  45605  supxrge  45726  infxr  45754  infleinflem2  45758  xrralrecnnge  45777  iocopn  45909  ge0lere  45921  ressiooinf  45946  uzinico  45948  uzubioo  45954  fsumge0cl  45962  limcicciooub  46024  limcresiooub  46029  limcleqr  46031  limsupresico  46087  limsuppnfdlem  46088  limsupmnflem  46107  liminfresico  46158  limsup10exlem  46159  xlimpnfvlem1  46223  icccncfext  46274  fourierdlem31  46525  fourierdlem33  46527  fourierdlem46  46539  fourierdlem48  46541  fourierdlem49  46542  fourierdlem75  46568  fourierdlem85  46578  fourierdlem88  46581  fourierdlem95  46588  fourierdlem103  46596  fourierdlem104  46597  fourierdlem107  46600  fourierdlem109  46602  fourierdlem112  46605  fouriersw  46618  ioorrnopnxrlem  46693  sge0tsms  46767  sge0isum  46814  sge0ad2en  46818  sge0xaddlem2  46821  voliunsge0lem  46859  meassre  46864  omessre  46897  omeiunltfirp  46906  hoiprodcl  46934  ovnsubaddlem1  46957  hoiprodcl3  46967  hoidmvcl  46969  sge0hsphoire  46976  hoidmv1lelem1  46978  hoidmv1lelem2  46979  hoidmv1lelem3  46980  hoidmv1le  46981  hoidmvlelem1  46982  hoidmvlelem3  46984  hoidmvlelem4  46985  volicorege0  47024  ovolval5lem1  47039