Theorem ltpnfd 13137

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  ℝcr 11128  +∞cpnf 11266   < clt 11269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-pnf 11271  df-xr 11273  df-ltxr 11274

This theorem is referenced by:  qbtwnxr  13216  xltnegi  13232  hashnnn0genn0  14361  limsupgre  15497  fprodge1  16011  xblss2ps  24340  blcvx  24737  reconnlem1  24766  iccpnfhmeo  24894  uniioombllem1  25534  ismbf3d  25607  mbflimsup  25619  itg2seq  25695  lhop2  25972  dvfsumlem2  25985  dvfsumlem2OLD  25986  logccv  26624  xrlimcnp  26930  pntleme  27571  absfico  45242  supxrge  45365  infxr  45394  infleinflem2  45398  xrralrecnnge  45417  iocopn  45549  ge0lere  45561  ressiooinf  45586  uzinico  45588  uzubioo  45594  fsumge0cl  45602  limcicciooub  45666  limcresiooub  45671  limcleqr  45673  limsupresico  45729  limsuppnfdlem  45730  limsupmnflem  45749  liminfresico  45800  limsup10exlem  45801  xlimpnfvlem1  45865  icccncfext  45916  fourierdlem31  46167  fourierdlem33  46169  fourierdlem46  46181  fourierdlem48  46183  fourierdlem49  46184  fourierdlem75  46210  fourierdlem85  46220  fourierdlem88  46223  fourierdlem95  46230  fourierdlem103  46238  fourierdlem104  46239  fourierdlem107  46242  fourierdlem109  46244  fourierdlem112  46247  fouriersw  46260  ioorrnopnxrlem  46335  sge0tsms  46409  sge0isum  46456  sge0ad2en  46460  sge0xaddlem2  46463  voliunsge0lem  46501  meassre  46506  omessre  46539  omeiunltfirp  46548  hoiprodcl  46576  ovnsubaddlem1  46599  hoiprodcl3  46609  hoidmvcl  46611  sge0hsphoire  46618  hoidmv1lelem1  46620  hoidmv1lelem2  46621  hoidmv1lelem3  46622  hoidmv1le  46623  hoidmvlelem1  46624  hoidmvlelem3  46626  hoidmvlelem4  46627  volicorege0  46666  ovolval5lem1  46681