Theorem ltpnfd 13251

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11200  +∞cpnf 11341   < clt 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-pnf 11346  df-xr 11348  df-ltxr 11349

This theorem is used by:  qbtwnxr  13331  xltnegi  13347  hashnnn0genn0  14488  limsupgre  15649  fprodge1  16163  xblss2ps  24721  blcvx  25118  reconnlem1  25147  iccpnfhmeo  25267  uniioombllem1  25903  ismbf3d  25976  mbflimsup  25988  itg2seq  26064  lhop2  26336  dvfsumlem2  26348  logccv  26992  xrlimcnp  27297  pntleme  27936  absfico  46275  supxrge  46394  infxr  46422  infleinflem2  46426  xrralrecnnge  46445  iocopn  46576  ge0lere  46588  ressiooinf  46613  uzinico  46615  uzubioo  46621  fsumge0cl  46629  limcicciooub  46691  limcresiooub  46696  limcleqr  46698  limsupresico  46754  limsuppnfdlem  46755  limsupmnflem  46774  liminfresico  46825  limsup10exlem  46826  xlimpnfvlem1  46890  icccncfext  46941  fourierdlem31  47192  fourierdlem33  47194  fourierdlem46  47206  fourierdlem48  47208  fourierdlem49  47209  fourierdlem75  47235  fourierdlem85  47245  fourierdlem88  47248  fourierdlem95  47255  fourierdlem103  47263  fourierdlem104  47264  fourierdlem107  47267  fourierdlem109  47269  fourierdlem112  47272  fouriersw  47285  ioorrnopnxrlem  47360  sge0tsms  47434  sge0isum  47481  sge0ad2en  47485  sge0xaddlem2  47488  voliunsge0lem  47526  meassre  47531  omessre  47564  omeiunltfirp  47573  hoiprodcl  47601  ovnsubaddlem1  47624  hoiprodcl3  47634  hoidmvcl  47636  sge0hsphoire  47643  hoidmv1lelem1  47645  hoidmv1lelem2  47646  hoidmv1lelem3  47647  hoidmv1le  47648  hoidmvlelem1  47649  hoidmvlelem3  47651  hoidmvlelem4  47652  volicorege0  47691  ovolval5lem1  47706