Theorem ltpnfd 13274

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5106  ℝcr 11223  +∞cpnf 11364   < clt 11367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-xp 5661  df-pnf 11369  df-xr 11371  df-ltxr 11372

This theorem is used by:  qbtwnxr  13354  xltnegi  13370  hashnnn0genn0  14511  limsupgre  15674  fprodge1  16188  xblss2ps  24747  blcvx  25144  reconnlem1  25173  iccpnfhmeo  25293  uniioombllem1  25929  ismbf3d  26002  mbflimsup  26014  itg2seq  26090  lhop2  26362  dvfsumlem2  26374  logccv  27018  xrlimcnp  27323  pntleme  27962  absfico  46434  supxrge  46553  infxr  46581  infleinflem2  46585  xrralrecnnge  46604  iocopn  46735  ge0lere  46747  ressiooinf  46772  uzinico  46774  uzubioo  46780  fsumge0cl  46788  limcicciooub  46850  limcresiooub  46855  limcleqr  46857  limsupresico  46913  limsuppnfdlem  46914  limsupmnflem  46933  liminfresico  46984  limsup10exlem  46985  xlimpnfvlem1  47049  icccncfext  47100  fourierdlem31  47351  fourierdlem33  47353  fourierdlem46  47365  fourierdlem48  47367  fourierdlem49  47368  fourierdlem75  47394  fourierdlem85  47404  fourierdlem88  47407  fourierdlem95  47414  fourierdlem103  47422  fourierdlem104  47423  fourierdlem107  47426  fourierdlem109  47428  fourierdlem112  47431  fouriersw  47444  ioorrnopnxrlem  47519  sge0tsms  47593  sge0isum  47640  sge0ad2en  47644  sge0xaddlem2  47647  voliunsge0lem  47685  meassre  47690  omessre  47723  omeiunltfirp  47732  hoiprodcl  47760  ovnsubaddlem1  47783  hoiprodcl3  47793  hoidmvcl  47795  sge0hsphoire  47802  hoidmv1lelem1  47804  hoidmv1lelem2  47805  hoidmv1lelem3  47806  hoidmv1le  47807  hoidmvlelem1  47808  hoidmvlelem3  47810  hoidmvlelem4  47811  volicorege0  47850  ovolval5lem1  47865  itscnhlinecirc02p  50100