Theorem ltpnfd 13023

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008  +∞cpnf 11146   < clt 11149

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-pnf 11151  df-xr 11153  df-ltxr 11154

This theorem is referenced by:  qbtwnxr  13102  xltnegi  13118  hashnnn0genn0  14250  limsupgre  15388  fprodge1  15902  xblss2ps  24287  blcvx  24684  reconnlem1  24713  iccpnfhmeo  24841  uniioombllem1  25480  ismbf3d  25553  mbflimsup  25565  itg2seq  25641  lhop2  25918  dvfsumlem2  25931  dvfsumlem2OLD  25932  logccv  26570  xrlimcnp  26876  pntleme  27517  absfico  45206  supxrge  45328  infxr  45356  infleinflem2  45360  xrralrecnnge  45379  iocopn  45511  ge0lere  45523  ressiooinf  45548  uzinico  45550  uzubioo  45556  fsumge0cl  45564  limcicciooub  45628  limcresiooub  45633  limcleqr  45635  limsupresico  45691  limsuppnfdlem  45692  limsupmnflem  45711  liminfresico  45762  limsup10exlem  45763  xlimpnfvlem1  45827  icccncfext  45878  fourierdlem31  46129  fourierdlem33  46131  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem75  46172  fourierdlem85  46182  fourierdlem88  46185  fourierdlem95  46192  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem109  46206  fourierdlem112  46209  fouriersw  46222  ioorrnopnxrlem  46297  sge0tsms  46371  sge0isum  46418  sge0ad2en  46422  sge0xaddlem2  46425  voliunsge0lem  46463  meassre  46468  omessre  46501  omeiunltfirp  46510  hoiprodcl  46538  ovnsubaddlem1  46561  hoiprodcl3  46571  hoidmvcl  46573  sge0hsphoire  46580  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem3  46588  hoidmvlelem4  46589  volicorege0  46628  ovolval5lem1  46643