Theorem ltpnfd 12592

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5027  ℝcr 10607  +∞cpnf 10743   < clt 10746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-xp 5525  df-pnf 10748  df-xr 10750  df-ltxr 10751

This theorem is referenced by:  qbtwnxr  12669  xltnegi  12685  hashnnn0genn0  13788  limsupgre  14921  fprodge1  15434  xblss2ps  23147  blcvx  23543  reconnlem1  23571  iccpnfhmeo  23690  uniioombllem1  24326  ismbf3d  24399  mbflimsup  24411  itg2seq  24487  lhop2  24759  dvfsumlem2  24771  logccv  25398  xrlimcnp  25698  pntleme  26336  absfico  42280  supxrge  42399  infxr  42428  infleinflem2  42432  xrralrecnnge  42452  iocopn  42582  ge0lere  42594  ressiooinf  42619  uzinico  42622  uzubioo  42629  fsumge0cl  42640  limcicciooub  42704  limcresiooub  42709  limcleqr  42711  limsupresico  42767  limsuppnfdlem  42768  limsupmnflem  42787  liminfresico  42838  limsup10exlem  42839  xlimpnfvlem1  42903  icccncfext  42954  fourierdlem31  43205  fourierdlem33  43207  fourierdlem46  43219  fourierdlem48  43221  fourierdlem49  43222  fourierdlem75  43248  fourierdlem85  43258  fourierdlem88  43261  fourierdlem95  43268  fourierdlem103  43276  fourierdlem104  43277  fourierdlem107  43280  fourierdlem109  43282  fourierdlem112  43285  fouriersw  43298  ioorrnopnxrlem  43373  sge0tsms  43444  sge0isum  43491  sge0ad2en  43495  sge0xaddlem2  43498  voliunsge0lem  43536  meassre  43541  omessre  43574  omeiunltfirp  43583  hoiprodcl  43611  ovnsubaddlem1  43634  hoiprodcl3  43644  hoidmvcl  43646  sge0hsphoire  43653  hoidmv1lelem1  43655  hoidmv1lelem2  43656  hoidmv1lelem3  43657  hoidmv1le  43658  hoidmvlelem1  43659  hoidmvlelem3  43661  hoidmvlelem4  43662  volicorege0  43701  ovolval5lem1  43716  pimgtpnf2  43767