Theorem ltpnfd 13057

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043  +∞cpnf 11181   < clt 11184

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-pnf 11186  df-xr 11188  df-ltxr 11189

This theorem is referenced by:  qbtwnxr  13136  xltnegi  13152  hashnnn0genn0  14284  limsupgre  15423  fprodge1  15937  xblss2ps  24322  blcvx  24719  reconnlem1  24748  iccpnfhmeo  24876  uniioombllem1  25515  ismbf3d  25588  mbflimsup  25600  itg2seq  25676  lhop2  25953  dvfsumlem2  25966  dvfsumlem2OLD  25967  logccv  26605  xrlimcnp  26911  pntleme  27552  absfico  45205  supxrge  45327  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