Theorem ltpnf 13062

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 2739	. . . 4 ⊢ +∞ = +∞
2		orc 873	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 697	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 880	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11182	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11190	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13057	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 592	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 258	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   <_ℝ cltrr 11033  +∞cpnf 11167  -∞cmnf 11168  ℝ^*cxr 11169   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-pnf 11172  df-xr 11174  df-ltxr 11175

This theorem is referenced by:  ltpnfd  13063  0ltpnf  13064  xrlttri  13081  xrlttr  13082  xrrebnd  13111  xrre  13112  qbtwnxr  13143  xnn0lem1lt  13187  xrinfmsslem  13251  xrub  13255  supxrunb1  13262  supxrunb2  13263  dfrp2  13338  elioc2  13353  elicc2  13355  ioomax  13366  ioopos  13368  elioopnf  13387  elicopnf  13389  difreicc  13428  hashbnd  14289  hashv01gt1  14298  fprodge0  15949  fprodge1  15951  pcadd  16851  ramubcl  16980  rge0srg  21413  mnfnei  23204  icopnfcld  24750  iocmnfcld  24751  xrtgioo  24790  xrge0tsms  24818  ioombl1lem4  25546  icombl1  25548  mbfmax  25634  upgrfi  29178  topnfbey  30557  isblo3i  30890  htthlem  31006  xlt2addrd  32851  fsumrp0cl  33100  xrge0tsmsd  33154  pnfinf  33264  xrge0slmod  33431  xrge0iifcnv  34117  xrge0iifiso  34119  xrge0iifhom  34121  lmxrge0  34136  esumcst  34247  esumcvgre  34275  voliune  34413  volfiniune  34414  sxbrsigalem0  34455  orvcgteel  34652  dstfrvclim1  34662  itg2addnclem2  38039  asindmre  38070  dvasin  38071  dvacos  38072  rfcnpre3  45481  supxrgere  45778  supxrgelem  45782  xrlexaddrp  45797  infxr  45811  xrpnf  45928  limsupre  46084  limsuppnflem  46153  liminflelimsupuz  46228  limsupub2  46255  icccncfext  46330  fourierdlem111  46660  fourierdlem113  46662  fouriersw  46674  sge0iunmptlemre  46858  sge0rpcpnf  46864  sge0xaddlem1  46876  meaiuninclem  46923  hoidmvlelem5  47042  ovolval5lem1  47095  pimltpnff  47146  iccpartiltu  47897  itscnhlinecirc02p  49276