Theorem ltpnf 13122

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 2762	. . . 4 ⊢ +∞ = +∞
2		orc 878	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 701	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 885	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11228	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11236	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13117	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 595	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 259	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1560   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072   <_ℝ cltrr 11077  +∞cpnf 11213  -∞cmnf 11214  ℝ^*cxr 11215   < clt 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-pnf 11218  df-xr 11220  df-ltxr 11221

This theorem is referenced by:  ltpnfd  13123  0ltpnf  13124  xrlttri  13141  xrlttr  13142  xrrebnd  13171  xrre  13172  qbtwnxr  13203  xnn0lem1lt  13247  xrinfmsslem  13311  xrub  13315  supxrunb1  13322  supxrunb2  13323  dfrp2  13398  elioc2  13413  elicc2  13415  ioomax  13426  ioopos  13428  elioopnf  13447  elicopnf  13449  difreicc  13488  hashbnd  14349  hashv01gt1  14358  fprodge0  16023  fprodge1  16025  pcadd  16925  ramubcl  17054  rge0srg  21487  mnfnei  23278  icopnfcld  24824  iocmnfcld  24825  xrtgioo  24864  xrge0tsms  24892  ioombl1lem4  25620  icombl1  25622  mbfmax  25708  upgrfi  29289  topnfbey  30668  isblo3i  31001  htthlem  31117  xlt2addrd  32958  fsumrp0cl  33196  xrge0tsmsd  33250  pnfinf  33360  xrge0slmod  33531  xrge0iifcnv  34227  xrge0iifiso  34229  xrge0iifhom  34231  lmxrge0  34246  esumcst  34357  esumcvgre  34385  voliune  34523  volfiniune  34524  sxbrsigalem0  34565  orvcgteel  34762  dstfrvclim1  34772  itg2addnclem2  38168  asindmre  38199  dvasin  38200  dvacos  38201  rfcnpre3  45610  supxrgere  45906  supxrgelem  45910  xrlexaddrp  45925  infxr  45939  xrpnf  46056  limsupre  46212  limsuppnflem  46281  liminflelimsupuz  46356  limsupub2  46383  icccncfext  46458  fourierdlem111  46788  fouriersw  46802  sge0iunmptlemre  46986  sge0rpcpnf  46992  sge0xaddlem1  47004  meaiuninclem  47051  hoidmvlelem5  47170  ovolval5lem1  47223  pimltpnff  47274  iccpartiltu  48025  itscnhlinecirc02p  49404