Theorem ltpnfd 13125

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

Syntax hints:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11074  +∞cpnf 11215   < clt 11218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5655  df-pnf 11220  df-xr 11222  df-ltxr 11223

This theorem is referenced by:  qbtwnxr  13205  xltnegi  13221  hashnnn0genn0  14358  limsupgre  15510  fprodge1  16027  xblss2ps  24463  blcvx  24860  reconnlem1  24889  iccpnfhmeo  25009  uniioombllem1  25645  ismbf3d  25718  mbflimsup  25730  itg2seq  25806  lhop2  26079  dvfsumlem2  26091  logccv  26730  xrlimcnp  27035  pntleme  27674  absfico  45799  supxrge  45919  infxr  45947  infleinflem2  45951  xrralrecnnge  45970  iocopn  46101  ge0lere  46113  ressiooinf  46138  uzinico  46140  uzubioo  46146  fsumge0cl  46154  limcicciooub  46216  limcresiooub  46221  limcleqr  46223  limsupresico  46279  limsuppnfdlem  46280  limsupmnflem  46299  liminfresico  46350  limsup10exlem  46351  xlimpnfvlem1  46415  icccncfext  46466  fourierdlem31  46717  fourierdlem33  46719  fourierdlem46  46731  fourierdlem48  46733  fourierdlem49  46734  fourierdlem75  46760  fourierdlem85  46770  fourierdlem88  46773  fourierdlem95  46780  fourierdlem103  46788  fourierdlem104  46789  fourierdlem107  46792  fourierdlem109  46794  fourierdlem112  46797  fouriersw  46810  ioorrnopnxrlem  46885  sge0tsms  46959  sge0isum  47006  sge0ad2en  47010  sge0xaddlem2  47013  voliunsge0lem  47051  meassre  47056  omessre  47089  omeiunltfirp  47098  hoiprodcl  47126  ovnsubaddlem1  47149  hoiprodcl3  47159  hoidmvcl  47161  sge0hsphoire  47168  hoidmv1lelem1  47170  hoidmv1lelem2  47171  hoidmv1lelem3  47172  hoidmv1le  47173  hoidmvlelem1  47174  hoidmvlelem3  47176  hoidmvlelem4  47177  volicorege0  47216  ovolval5lem1  47231