Theorem ltpnfd 13051

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5110  ℝcr 11059  +∞cpnf 11195   < clt 11198

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-pnf 11200  df-xr 11202  df-ltxr 11203

This theorem is referenced by:  qbtwnxr  13129  xltnegi  13145  hashnnn0genn0  14253  limsupgre  15375  fprodge1  15889  xblss2ps  23791  blcvx  24198  reconnlem1  24226  iccpnfhmeo  24345  uniioombllem1  24982  ismbf3d  25055  mbflimsup  25067  itg2seq  25144  lhop2  25416  dvfsumlem2  25428  logccv  26055  xrlimcnp  26355  pntleme  26993  absfico  43560  supxrge  43693  infxr  43722  infleinflem2  43726  xrralrecnnge  43745  iocopn  43878  ge0lere  43890  ressiooinf  43915  uzinico  43918  uzubioo  43925  fsumge0cl  43934  limcicciooub  43998  limcresiooub  44003  limcleqr  44005  limsupresico  44061  limsuppnfdlem  44062  limsupmnflem  44081  liminfresico  44132  limsup10exlem  44133  xlimpnfvlem1  44197  icccncfext  44248  fourierdlem31  44499  fourierdlem33  44501  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem75  44542  fourierdlem85  44552  fourierdlem88  44555  fourierdlem95  44562  fourierdlem103  44570  fourierdlem104  44571  fourierdlem107  44574  fourierdlem109  44576  fourierdlem112  44579  fouriersw  44592  ioorrnopnxrlem  44667  sge0tsms  44741  sge0isum  44788  sge0ad2en  44792  sge0xaddlem2  44795  voliunsge0lem  44833  meassre  44838  omessre  44871  omeiunltfirp  44880  hoiprodcl  44908  ovnsubaddlem1  44931  hoiprodcl3  44941  hoidmvcl  44943  sge0hsphoire  44950  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmv1le  44955  hoidmvlelem1  44956  hoidmvlelem3  44958  hoidmvlelem4  44959  volicorege0  44998  ovolval5lem1  45013