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

Theorem ltpnfd 12160
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 12159 . 2 (𝐴 ∈ ℝ → 𝐴 < +∞)
31, 2syl 17 1 (𝜑𝐴 < +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145   class class class wbr 4786  cr 10137  +∞cpnf 10273   < clt 10276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-pnf 10278  df-xr 10280  df-ltxr 10281
This theorem is referenced by:  limsupgre  14420  fprodge1  14932  mbflimsup  23653  absfico  39928  supxrge  40070  infxr  40099  infleinflem2  40103  xrralrecnnge  40129  iocopn  40265  ge0lere  40277  ressiooinf  40302  uzinico  40305  uzubioo  40312  fsumge0cl  40323  limcicciooub  40387  limcresiooub  40392  limcleqr  40394  limsupresico  40450  limsupmnflem  40470  liminfresico  40521  limsup10exlem  40522  xlimpnfvlem1  40580  icccncfext  40618  fourierdlem31  40872  fourierdlem33  40874  fourierdlem46  40886  fourierdlem48  40888  fourierdlem49  40889  fourierdlem75  40915  fourierdlem85  40925  fourierdlem88  40928  fourierdlem95  40935  fourierdlem103  40943  fourierdlem104  40944  fourierdlem107  40947  fourierdlem109  40949  fourierdlem112  40952  fouriersw  40965  ioorrnopnxrlem  41043  sge0tsms  41114  sge0isum  41161  sge0ad2en  41165  sge0xaddlem2  41168  voliunsge0lem  41206  meassre  41211  omessre  41244  omeiunltfirp  41253  hoiprodcl  41281  ovnsubaddlem1  41304  hoiprodcl3  41314  hoidmvcl  41316  sge0hsphoire  41323  hoidmv1lelem1  41325  hoidmv1lelem2  41326  hoidmv1lelem3  41327  hoidmv1le  41328  hoidmvlelem1  41329  hoidmvlelem3  41331  hoidmvlelem4  41332  volicorege0  41371  ovolval5lem1  41386  pimgtpnf2  41437
  Copyright terms: Public domain W3C validator