Theorem ltpnf 13256

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 2760	. . . 4 ⊢ +∞ = +∞
2		orc 881	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 888	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11362	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11370	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13251	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 598	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144   class class class wbr 5102  ℝcr 11206   <_ℝ cltrr 11211  +∞cpnf 11347  -∞cmnf 11348  ℝ^*cxr 11349   < clt 11350

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 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263

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 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5657  df-pnf 11352  df-xr 11354  df-ltxr 11355

This theorem is used by:  ltpnfd  13257  0ltpnf  13258  xrlttri  13275  xrlttr  13276  xrrebnd  13305  xrre  13306  qbtwnxr  13337  xnn0lem1lt  13381  xrinfmsslem  13445  xrub  13449  supxrunb1  13456  supxrunb2  13457  dfrp2  13532  elioc2  13547  elicc2  13549  ioomax  13560  ioopos  13562  elioopnf  13581  elicopnf  13583  difreicc  13622  hashbnd  14487  hashv01gt1  14496  fprodge0  16169  fprodge1  16171  pcadd  17076  ramubcl  17205  rge0srg  21753  mnfnei  23548  icopnfcld  25095  iocmnfcld  25096  xrtgioo  25135  xrge0tsms  25163  ioombl1lem4  25891  icombl1  25893  mbfmax  25979  upgrfi  29678  topnfbey  31079  isblo3i  31412  htthlem  31528  xlt2addrd  33401  fsumrp0cl  33632  xrge0tsmsd  33684  pnfinf  33794  xrge0slmod  33959  xrge0iifcnv  34615  xrge0iifiso  34617  xrge0iifhom  34619  lmxrge0  34634  esumcst  34745  esumcvgre  34773  voliune  34912  volfiniune  34913  sxbrsigalem0  34953  orvcgteel  35150  dstfrvclim1  35160  itg2addnclem2  38699  asindmre  38730  dvasin  38731  dvacos  38732  rfcnpre3  46158  supxrgere  46453  supxrgelem  46457  xrlexaddrp  46472  infxr  46486  xrpnf  46603  limsupre  46759  limsuppnflem  46828  liminflelimsupuz  46903  limsupub2  46930  icccncfext  47005  fourierdlem111  47335  fouriersw  47349  sge0iunmptlemre  47533  sge0rpcpnf  47539  sge0xaddlem1  47551  meaiuninclem  47598  hoidmvlelem5  47717  ovolval5lem1  47770  pimltpnff  47821  iccpartiltu  48612