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

Theorem ltpnfd 12996
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 12995 . 2 (𝐴 ∈ ℝ → 𝐴 < +∞)
31, 2syl 17 1 (𝜑𝐴 < +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106   class class class wbr 5103  cr 11008  +∞cpnf 11144   < clt 11147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-cnex 11065
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-xp 5637  df-pnf 11149  df-xr 11151  df-ltxr 11152
This theorem is referenced by:  qbtwnxr  13073  xltnegi  13089  hashnnn0genn0  14197  limsupgre  15323  fprodge1  15838  xblss2ps  23706  blcvx  24113  reconnlem1  24141  iccpnfhmeo  24260  uniioombllem1  24897  ismbf3d  24970  mbflimsup  24982  itg2seq  25059  lhop2  25331  dvfsumlem2  25343  logccv  25970  xrlimcnp  26270  pntleme  26908  absfico  43344  supxrge  43477  infxr  43506  infleinflem2  43510  xrralrecnnge  43530  iocopn  43659  ge0lere  43671  ressiooinf  43696  uzinico  43699  uzubioo  43706  fsumge0cl  43715  limcicciooub  43779  limcresiooub  43784  limcleqr  43786  limsupresico  43842  limsuppnfdlem  43843  limsupmnflem  43862  liminfresico  43913  limsup10exlem  43914  xlimpnfvlem1  43978  icccncfext  44029  fourierdlem31  44280  fourierdlem33  44282  fourierdlem46  44294  fourierdlem48  44296  fourierdlem49  44297  fourierdlem75  44323  fourierdlem85  44333  fourierdlem88  44336  fourierdlem95  44343  fourierdlem103  44351  fourierdlem104  44352  fourierdlem107  44355  fourierdlem109  44357  fourierdlem112  44360  fouriersw  44373  ioorrnopnxrlem  44448  sge0tsms  44522  sge0isum  44569  sge0ad2en  44573  sge0xaddlem2  44576  voliunsge0lem  44614  meassre  44619  omessre  44652  omeiunltfirp  44661  hoiprodcl  44689  ovnsubaddlem1  44712  hoiprodcl3  44722  hoidmvcl  44724  sge0hsphoire  44731  hoidmv1lelem1  44733  hoidmv1lelem2  44734  hoidmv1lelem3  44735  hoidmv1le  44736  hoidmvlelem1  44737  hoidmvlelem3  44739  hoidmvlelem4  44740  volicorege0  44779  ovolval5lem1  44794
  Copyright terms: Public domain W3C validator