Theorem ltpnf 13163

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 2736	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11308	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11316	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13158	. . 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 1539   ∈ wcel 2107   class class class wbr 5142  ℝcr 11155   <_ℝ cltrr 11160  +∞cpnf 11293  -∞cmnf 11294  ℝ^*cxr 11295   < clt 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-xp 5690  df-pnf 11298  df-xr 11300  df-ltxr 11301

This theorem is referenced by:  ltpnfd  13164  0ltpnf  13165  xrlttri  13182  xrlttr  13183  xrrebnd  13211  xrre  13212  qbtwnxr  13243  xnn0lem1lt  13287  xrinfmsslem  13351  xrub  13355  supxrunb1  13362  supxrunb2  13363  dfrp2  13437  elioc2  13451  elicc2  13453  ioomax  13463  ioopos  13465  elioopnf  13484  elicopnf  13486  difreicc  13525  hashbnd  14376  hashv01gt1  14385  fprodge0  16030  fprodge1  16032  pcadd  16928  ramubcl  17057  rge0srg  21457  mnfnei  23230  icopnfcld  24789  iocmnfcld  24790  xrtgioo  24829  xrge0tsms  24857  ioombl1lem4  25597  icombl1  25599  mbfmax  25685  upgrfi  29109  topnfbey  30489  isblo3i  30821  htthlem  30937  xlt2addrd  32763  fsumrp0cl  33027  xrge0tsmsd  33066  pnfinf  33191  xrge0slmod  33377  xrge0iifcnv  33933  xrge0iifiso  33935  xrge0iifhom  33937  lmxrge0  33952  esumcst  34065  esumcvgre  34093  voliune  34231  volfiniune  34232  sxbrsigalem0  34274  orvcgteel  34471  dstfrvclim1  34481  itg2addnclem2  37680  asindmre  37711  dvasin  37712  dvacos  37713  rfcnpre3  45043  supxrgere  45349  supxrgelem  45353  xrlexaddrp  45368  infxr  45383  xrpnf  45501  limsupre  45661  limsuppnflem  45730  liminflelimsupuz  45805  limsupub2  45832  icccncfext  45907  fourierdlem111  46237  fourierdlem113  46239  fouriersw  46251  sge0iunmptlemre  46435  sge0rpcpnf  46441  sge0xaddlem1  46453  meaiuninclem  46500  hoidmvlelem5  46619  ovolval5lem1  46672  pimltpnff  46723  iccpartiltu  47414  itscnhlinecirc02p  48711