Theorem ltpnfd 12517

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536  +∞cpnf 10672   < clt 10675

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 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-xp 5561  df-pnf 10677  df-xr 10679  df-ltxr 10680

This theorem is referenced by:  qbtwnxr  12594  xltnegi  12610  hashnnn0genn0  13704  limsupgre  14838  fprodge1  15349  xblss2ps  23011  blcvx  23406  reconnlem1  23434  iccpnfhmeo  23549  uniioombllem1  24182  ismbf3d  24255  mbflimsup  24267  itg2seq  24343  lhop2  24612  dvfsumlem2  24624  logccv  25246  xrlimcnp  25546  pntleme  26184  absfico  41530  supxrge  41655  infxr  41684  infleinflem2  41688  xrralrecnnge  41711  iocopn  41845  ge0lere  41857  ressiooinf  41882  uzinico  41885  uzubioo  41892  fsumge0cl  41903  limcicciooub  41967  limcresiooub  41972  limcleqr  41974  limsupresico  42030  limsuppnfdlem  42031  limsupmnflem  42050  liminfresico  42101  limsup10exlem  42102  xlimpnfvlem1  42166  icccncfext  42219  fourierdlem31  42472  fourierdlem33  42474  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem75  42515  fourierdlem85  42525  fourierdlem88  42528  fourierdlem95  42535  fourierdlem103  42543  fourierdlem104  42544  fourierdlem107  42547  fourierdlem109  42549  fourierdlem112  42552  fouriersw  42565  ioorrnopnxrlem  42640  sge0tsms  42711  sge0isum  42758  sge0ad2en  42762  sge0xaddlem2  42765  voliunsge0lem  42803  meassre  42808  omessre  42841  omeiunltfirp  42850  hoiprodcl  42878  ovnsubaddlem1  42901  hoiprodcl3  42911  hoidmvcl  42913  sge0hsphoire  42920  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem3  42928  hoidmvlelem4  42929  volicorege0  42968  ovolval5lem1  42983  pimgtpnf2  43034