MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltpnfd Structured version   Visualization version   GIF version

Theorem ltpnfd 13043
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
StepHypRef Expression
1 ltpnfd.a . 2 (𝜑𝐴 ∈ ℝ)
2 ltpnf 13042 . 2 (𝐴 ∈ ℝ → 𝐴 < +∞)
31, 2syl 17 1 (𝜑𝐴 < +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106  cr 11051  +∞cpnf 11187   < clt 11190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-xp 5640  df-pnf 11192  df-xr 11194  df-ltxr 11195
This theorem is referenced by:  qbtwnxr  13120  xltnegi  13136  hashnnn0genn0  14244  limsupgre  15364  fprodge1  15879  xblss2ps  23757  blcvx  24164  reconnlem1  24192  iccpnfhmeo  24311  uniioombllem1  24948  ismbf3d  25021  mbflimsup  25033  itg2seq  25110  lhop2  25382  dvfsumlem2  25394  logccv  26021  xrlimcnp  26321  pntleme  26959  absfico  43446  supxrge  43579  infxr  43608  infleinflem2  43612  xrralrecnnge  43632  iocopn  43765  ge0lere  43777  ressiooinf  43802  uzinico  43805  uzubioo  43812  fsumge0cl  43821  limcicciooub  43885  limcresiooub  43890  limcleqr  43892  limsupresico  43948  limsuppnfdlem  43949  limsupmnflem  43968  liminfresico  44019  limsup10exlem  44020  xlimpnfvlem1  44084  icccncfext  44135  fourierdlem31  44386  fourierdlem33  44388  fourierdlem46  44400  fourierdlem48  44402  fourierdlem49  44403  fourierdlem75  44429  fourierdlem85  44439  fourierdlem88  44442  fourierdlem95  44449  fourierdlem103  44457  fourierdlem104  44458  fourierdlem107  44461  fourierdlem109  44463  fourierdlem112  44466  fouriersw  44479  ioorrnopnxrlem  44554  sge0tsms  44628  sge0isum  44675  sge0ad2en  44679  sge0xaddlem2  44682  voliunsge0lem  44720  meassre  44725  omessre  44758  omeiunltfirp  44767  hoiprodcl  44795  ovnsubaddlem1  44818  hoiprodcl3  44828  hoidmvcl  44830  sge0hsphoire  44837  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmv1lelem3  44841  hoidmv1le  44842  hoidmvlelem1  44843  hoidmvlelem3  44845  hoidmvlelem4  44846  volicorege0  44885  ovolval5lem1  44900
  Copyright terms: Public domain W3C validator