Theorem ltpnf 12785

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
ltpnf	⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Proof of Theorem ltpnf

Step	Hyp	Ref	Expression
1		eqid 2738	. . . 4 ⊢ +∞ = +∞
2		orc 863	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 687	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 870	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10952	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10960	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 12780	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 585	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 256	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   <_ℝ cltrr 10806  +∞cpnf 10937  -∞cmnf 10938  ℝ^*cxr 10939   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-pnf 10942  df-xr 10944  df-ltxr 10945

This theorem is referenced by:  ltpnfd  12786  0ltpnf  12787  xrlttri  12802  xrlttr  12803  xrrebnd  12831  xrre  12832  qbtwnxr  12863  xnn0lem1lt  12907  xrinfmsslem  12971  xrub  12975  supxrunb1  12982  supxrunb2  12983  dfrp2  13057  elioc2  13071  elicc2  13073  ioomax  13083  ioopos  13085  elioopnf  13104  elicopnf  13106  difreicc  13145  hashbnd  13978  hashv01gt1  13987  fprodge0  15631  fprodge1  15633  pcadd  16518  ramubcl  16647  rge0srg  20581  mnfnei  22280  icopnfcld  23837  iocmnfcld  23838  xrtgioo  23875  xrge0tsms  23903  ioombl1lem4  24630  icombl1  24632  mbfmax  24718  upgrfi  27364  topnfbey  28734  isblo3i  29064  htthlem  29180  xlt2addrd  30983  fsumrp0cl  31206  xrge0tsmsd  31219  pnfinf  31339  xrge0slmod  31450  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  lmxrge0  31804  esumcst  31931  esumcvgre  31959  voliune  32097  volfiniune  32098  sxbrsigalem0  32138  orvcgteel  32334  dstfrvclim1  32344  itg2addnclem2  35756  asindmre  35787  dvasin  35788  dvacos  35789  rfcnpre3  42465  supxrgere  42762  supxrgelem  42766  xrlexaddrp  42781  infxr  42796  xrpnf  42916  limsupre  43072  limsuppnflem  43141  liminflelimsupuz  43216  limsupub2  43243  icccncfext  43318  fourierdlem111  43648  fourierdlem113  43650  fouriersw  43662  sge0iunmptlemre  43843  sge0rpcpnf  43849  sge0xaddlem1  43861  meaiuninclem  43908  hoidmvlelem5  44027  ovolval5lem1  44080  pimltpnf  44130  iccpartiltu  44762  itscnhlinecirc02p  46019