Theorem ltpnf 13183

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 2740	. . . 4 ⊢ +∞ = +∞
2		orc 866	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 690	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 873	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11336	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11344	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13178	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 585	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   <_ℝ cltrr 11188  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-pnf 11326  df-xr 11328  df-ltxr 11329

This theorem is referenced by:  ltpnfd  13184  0ltpnf  13185  xrlttri  13201  xrlttr  13202  xrrebnd  13230  xrre  13231  qbtwnxr  13262  xnn0lem1lt  13306  xrinfmsslem  13370  xrub  13374  supxrunb1  13381  supxrunb2  13382  dfrp2  13456  elioc2  13470  elicc2  13472  ioomax  13482  ioopos  13484  elioopnf  13503  elicopnf  13505  difreicc  13544  hashbnd  14385  hashv01gt1  14394  fprodge0  16041  fprodge1  16043  pcadd  16936  ramubcl  17065  rge0srg  21479  mnfnei  23250  icopnfcld  24809  iocmnfcld  24810  xrtgioo  24847  xrge0tsms  24875  ioombl1lem4  25615  icombl1  25617  mbfmax  25703  upgrfi  29126  topnfbey  30501  isblo3i  30833  htthlem  30949  xlt2addrd  32765  fsumrp0cl  33007  xrge0tsmsd  33041  pnfinf  33163  xrge0slmod  33341  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  lmxrge0  33898  esumcst  34027  esumcvgre  34055  voliune  34193  volfiniune  34194  sxbrsigalem0  34236  orvcgteel  34432  dstfrvclim1  34442  itg2addnclem2  37632  asindmre  37663  dvasin  37664  dvacos  37665  rfcnpre3  44933  supxrgere  45248  supxrgelem  45252  xrlexaddrp  45267  infxr  45282  xrpnf  45401  limsupre  45562  limsuppnflem  45631  liminflelimsupuz  45706  limsupub2  45733  icccncfext  45808  fourierdlem111  46138  fourierdlem113  46140  fouriersw  46152  sge0iunmptlemre  46336  sge0rpcpnf  46342  sge0xaddlem1  46354  meaiuninclem  46401  hoidmvlelem5  46520  ovolval5lem1  46573  pimltpnff  46624  iccpartiltu  47296  itscnhlinecirc02p  48519