Theorem ltpnf 13022

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 2729	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11161	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11169	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13017	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 586	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   <_ℝ cltrr 11013  +∞cpnf 11146  -∞cmnf 11147  ℝ^*cxr 11148   < clt 11149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-pnf 11151  df-xr 11153  df-ltxr 11154

This theorem is referenced by:  ltpnfd  13023  0ltpnf  13024  xrlttri  13041  xrlttr  13042  xrrebnd  13070  xrre  13071  qbtwnxr  13102  xnn0lem1lt  13146  xrinfmsslem  13210  xrub  13214  supxrunb1  13221  supxrunb2  13222  dfrp2  13297  elioc2  13312  elicc2  13314  ioomax  13325  ioopos  13327  elioopnf  13346  elicopnf  13348  difreicc  13387  hashbnd  14243  hashv01gt1  14252  fprodge0  15900  fprodge1  15902  pcadd  16801  ramubcl  16930  rge0srg  21345  mnfnei  23106  icopnfcld  24653  iocmnfcld  24654  xrtgioo  24693  xrge0tsms  24721  ioombl1lem4  25460  icombl1  25462  mbfmax  25548  upgrfi  29036  topnfbey  30413  isblo3i  30745  htthlem  30861  xlt2addrd  32703  fsumrp0cl  32976  xrge0tsmsd  33016  pnfinf  33126  xrge0slmod  33286  xrge0iifcnv  33906  xrge0iifiso  33908  xrge0iifhom  33910  lmxrge0  33925  esumcst  34036  esumcvgre  34064  voliune  34202  volfiniune  34203  sxbrsigalem0  34245  orvcgteel  34442  dstfrvclim1  34452  itg2addnclem2  37662  asindmre  37693  dvasin  37694  dvacos  37695  rfcnpre3  45021  supxrgere  45323  supxrgelem  45327  xrlexaddrp  45342  infxr  45356  xrpnf  45474  limsupre  45632  limsuppnflem  45701  liminflelimsupuz  45776  limsupub2  45803  icccncfext  45878  fourierdlem111  46208  fourierdlem113  46210  fouriersw  46222  sge0iunmptlemre  46406  sge0rpcpnf  46412  sge0xaddlem1  46424  meaiuninclem  46471  hoidmvlelem5  46590  ovolval5lem1  46643  pimltpnff  46694  iccpartiltu  47416  itscnhlinecirc02p  48780