Theorem ltpnfd 12519

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538  +∞cpnf 10674   < clt 10677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-pnf 10679  df-xr 10681  df-ltxr 10682

This theorem is referenced by:  qbtwnxr  12596  xltnegi  12612  hashnnn0genn0  13706  limsupgre  14840  fprodge1  15351  xblss2ps  23013  blcvx  23408  reconnlem1  23436  iccpnfhmeo  23551  uniioombllem1  24184  ismbf3d  24257  mbflimsup  24269  itg2seq  24345  lhop2  24614  dvfsumlem2  24626  logccv  25248  xrlimcnp  25548  pntleme  26186  absfico  41488  supxrge  41613  infxr  41642  infleinflem2  41646  xrralrecnnge  41669  iocopn  41803  ge0lere  41815  ressiooinf  41840  uzinico  41843  uzubioo  41850  fsumge0cl  41861  limcicciooub  41925  limcresiooub  41930  limcleqr  41932  limsupresico  41988  limsuppnfdlem  41989  limsupmnflem  42008  liminfresico  42059  limsup10exlem  42060  xlimpnfvlem1  42124  icccncfext  42177  fourierdlem31  42430  fourierdlem33  42432  fourierdlem46  42444  fourierdlem48  42446  fourierdlem49  42447  fourierdlem75  42473  fourierdlem85  42483  fourierdlem88  42486  fourierdlem95  42493  fourierdlem103  42501  fourierdlem104  42502  fourierdlem107  42505  fourierdlem109  42507  fourierdlem112  42510  fouriersw  42523  ioorrnopnxrlem  42598  sge0tsms  42669  sge0isum  42716  sge0ad2en  42720  sge0xaddlem2  42723  voliunsge0lem  42761  meassre  42766  omessre  42799  omeiunltfirp  42808  hoiprodcl  42836  ovnsubaddlem1  42859  hoiprodcl3  42869  hoidmvcl  42871  sge0hsphoire  42878  hoidmv1lelem1  42880  hoidmv1lelem2  42881  hoidmv1lelem3  42882  hoidmv1le  42883  hoidmvlelem1  42884  hoidmvlelem3  42886  hoidmvlelem4  42887  volicorege0  42926  ovolval5lem1  42941  pimgtpnf2  42992