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

Theorem ltpnfd 12508
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 12507 . 2 (𝐴 ∈ ℝ → 𝐴 < +∞)
31, 2syl 17 1 (𝜑𝐴 < +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5057  cr 10528  +∞cpnf 10664   < clt 10667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-pnf 10669  df-xr 10671  df-ltxr 10672
This theorem is referenced by:  qbtwnxr  12585  xltnegi  12601  hashnnn0genn0  13695  limsupgre  14830  fprodge1  15341  xblss2ps  23003  blcvx  23398  reconnlem1  23426  iccpnfhmeo  23541  uniioombllem1  24174  ismbf3d  24247  mbflimsup  24259  itg2seq  24335  lhop2  24604  dvfsumlem2  24616  logccv  25238  xrlimcnp  25538  pntleme  26176  absfico  41465  supxrge  41590  infxr  41619  infleinflem2  41623  xrralrecnnge  41646  iocopn  41780  ge0lere  41792  ressiooinf  41817  uzinico  41820  uzubioo  41827  fsumge0cl  41838  limcicciooub  41902  limcresiooub  41907  limcleqr  41909  limsupresico  41965  limsupmnflem  41985  liminfresico  42036  limsup10exlem  42037  xlimpnfvlem1  42101  icccncfext  42154  fourierdlem31  42408  fourierdlem33  42410  fourierdlem46  42422  fourierdlem48  42424  fourierdlem49  42425  fourierdlem75  42451  fourierdlem85  42461  fourierdlem88  42464  fourierdlem95  42471  fourierdlem103  42479  fourierdlem104  42480  fourierdlem107  42483  fourierdlem109  42485  fourierdlem112  42488  fouriersw  42501  ioorrnopnxrlem  42576  sge0tsms  42647  sge0isum  42694  sge0ad2en  42698  sge0xaddlem2  42701  voliunsge0lem  42739  meassre  42744  omessre  42777  omeiunltfirp  42786  hoiprodcl  42814  ovnsubaddlem1  42837  hoiprodcl3  42847  hoidmvcl  42849  sge0hsphoire  42856  hoidmv1lelem1  42858  hoidmv1lelem2  42859  hoidmv1lelem3  42860  hoidmv1le  42861  hoidmvlelem1  42862  hoidmvlelem3  42864  hoidmvlelem4  42865  volicorege0  42904  ovolval5lem1  42919  pimgtpnf2  42970
  Copyright terms: Public domain W3C validator