Theorem ltpnfd 13250

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11199  +∞cpnf 11340   < clt 11343

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-pnf 11345  df-xr 11347  df-ltxr 11348

This theorem is used by:  qbtwnxr  13330  xltnegi  13346  hashnnn0genn0  14487  limsupgre  15648  fprodge1  16162  xblss2ps  24720  blcvx  25117  reconnlem1  25146  iccpnfhmeo  25266  uniioombllem1  25902  ismbf3d  25975  mbflimsup  25987  itg2seq  26063  lhop2  26335  dvfsumlem2  26347  logccv  26991  xrlimcnp  27296  pntleme  27935  absfico  46231  supxrge  46350  infxr  46378  infleinflem2  46382  xrralrecnnge  46401  iocopn  46532  ge0lere  46544  ressiooinf  46569  uzinico  46571  uzubioo  46577  fsumge0cl  46585  limcicciooub  46647  limcresiooub  46652  limcleqr  46654  limsupresico  46710  limsuppnfdlem  46711  limsupmnflem  46730  liminfresico  46781  limsup10exlem  46782  xlimpnfvlem1  46846  icccncfext  46897  fourierdlem31  47148  fourierdlem33  47150  fourierdlem46  47162  fourierdlem48  47164  fourierdlem49  47165  fourierdlem75  47191  fourierdlem85  47201  fourierdlem88  47204  fourierdlem95  47211  fourierdlem103  47219  fourierdlem104  47220  fourierdlem107  47223  fourierdlem109  47225  fourierdlem112  47228  fouriersw  47241  ioorrnopnxrlem  47316  sge0tsms  47390  sge0isum  47437  sge0ad2en  47441  sge0xaddlem2  47444  voliunsge0lem  47482  meassre  47487  omessre  47520  omeiunltfirp  47529  hoiprodcl  47557  ovnsubaddlem1  47580  hoiprodcl3  47590  hoidmvcl  47592  sge0hsphoire  47599  hoidmv1lelem1  47601  hoidmv1lelem2  47602  hoidmv1lelem3  47603  hoidmv1le  47604  hoidmvlelem1  47605  hoidmvlelem3  47607  hoidmvlelem4  47608  volicorege0  47647  ovolval5lem1  47662