Theorem ltpnf 12147

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 399	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 709	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 407	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10277	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10284	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 12142	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 697	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 247	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1632   ∈ wcel 2139   class class class wbr 4804  ℝcr 10127   <_ℝ cltrr 10132  +∞cpnf 10263  -∞cmnf 10264  ℝ^*cxr 10265   < clt 10266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-pnf 10268  df-xr 10270  df-ltxr 10271

This theorem is referenced by:  ltpnfd  12148  0ltpnf  12149  xrlttri  12165  xrlttr  12166  xrrebnd  12192  xrre  12193  qbtwnxr  12224  xltnegi  12240  xrinfmsslem  12331  xrub  12335  supxrunb1  12342  supxrunb2  12343  elioc2  12429  elicc2  12431  ioomax  12441  ioopos  12443  elioopnf  12460  elicopnf  12462  difreicc  12497  hashbnd  13317  hashnnn0genn0  13325  hashv01gt1  13327  fprodge0  14923  fprodge1  14925  pcadd  15795  ramubcl  15924  rge0srg  20019  mnfnei  21227  xblss2ps  22407  icopnfcld  22772  iocmnfcld  22773  blcvx  22802  xrtgioo  22810  reconnlem1  22830  xrge0tsms  22838  iccpnfhmeo  22945  ioombl1lem4  23529  icombl1  23531  uniioombllem1  23549  mbfmax  23615  ismbf3d  23620  itg2seq  23708  lhop2  23977  dvfsumlem2  23989  logccv  24608  xrlimcnp  24894  pntleme  25496  upgrfi  26185  topnfbey  27636  isblo3i  27965  htthlem  28083  xlt2addrd  29832  dfrp2  29841  fsumrp0cl  30004  pnfinf  30046  xrge0tsmsd  30094  xrge0slmod  30153  xrge0iifcnv  30288  xrge0iifiso  30290  xrge0iifhom  30292  lmxrge0  30307  esumcst  30434  esumcvgre  30462  voliune  30601  volfiniune  30602  sxbrsigalem0  30642  orvcgteel  30838  dstfrvclim1  30848  itg2addnclem2  33775  asindmre  33808  dvasin  33809  dvacos  33810  rfcnpre3  39691  supxrgere  40047  supxrgelem  40051  xrlexaddrp  40066  infxr  40081  xrpnf  40214  limsupre  40376  limsuppnfdlem  40436  limsuppnflem  40445  liminflelimsupuz  40520  icccncfext  40603  fourierdlem111  40937  fourierdlem113  40939  fouriersw  40951  sge0iunmptlemre  41135  sge0rpcpnf  41141  sge0xaddlem1  41153  meaiuninclem  41200  hoidmvlelem5  41319  ovolval5lem1  41372  pimltpnf  41422  iccpartiltu  41868