Theorem ltpnfd 13067

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

Syntax hints:   → wi 4   ∈ wcel 2121   class class class wbr 5075  ℝcr 11032  +∞cpnf 11171   < clt 11174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-xp 5627  df-pnf 11176  df-xr 11178  df-ltxr 11179

This theorem is referenced by:  qbtwnxr  13147  xltnegi  13163  hashnnn0genn0  14300  limsupgre  15438  fprodge1  15955  xblss2ps  24388  blcvx  24785  reconnlem1  24814  iccpnfhmeo  24934  uniioombllem1  25570  ismbf3d  25643  mbflimsup  25655  itg2seq  25731  lhop2  26004  dvfsumlem2  26016  logccv  26649  xrlimcnp  26954  pntleme  27593  absfico  45677  supxrge  45797  infxr  45825  infleinflem2  45829  xrralrecnnge  45848  iocopn  45979  ge0lere  45991  ressiooinf  46016  uzinico  46018  uzubioo  46024  fsumge0cl  46032  limcicciooub  46094  limcresiooub  46099  limcleqr  46101  limsupresico  46157  limsuppnfdlem  46158  limsupmnflem  46177  liminfresico  46228  limsup10exlem  46229  xlimpnfvlem1  46293  icccncfext  46344  fourierdlem31  46595  fourierdlem33  46597  fourierdlem46  46609  fourierdlem48  46611  fourierdlem49  46612  fourierdlem75  46638  fourierdlem85  46648  fourierdlem88  46651  fourierdlem95  46658  fourierdlem103  46666  fourierdlem104  46667  fourierdlem107  46670  fourierdlem109  46672  fourierdlem112  46675  fouriersw  46688  ioorrnopnxrlem  46763  sge0tsms  46837  sge0isum  46884  sge0ad2en  46888  sge0xaddlem2  46891  voliunsge0lem  46929  meassre  46934  omessre  46967  omeiunltfirp  46976  hoiprodcl  47004  ovnsubaddlem1  47027  hoiprodcl3  47037  hoidmvcl  47039  sge0hsphoire  47046  hoidmv1lelem1  47048  hoidmv1lelem2  47049  hoidmv1lelem3  47050  hoidmv1le  47051  hoidmvlelem1  47052  hoidmvlelem3  47054  hoidmvlelem4  47055  volicorege0  47094  ovolval5lem1  47109