Theorem ltpnf 13140

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 2763	. . . 4 ⊢ +∞ = +∞
2		orc 880	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 703	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 887	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11250	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11258	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13135	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 597	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1570   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   <_ℝ cltrr 11099  +∞cpnf 11235  -∞cmnf 11236  ℝ^*cxr 11237   < clt 11238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-pnf 11240  df-xr 11242  df-ltxr 11243

This theorem is referenced by:  ltpnfd  13141  0ltpnf  13142  xrlttri  13159  xrlttr  13160  xrrebnd  13189  xrre  13190  qbtwnxr  13221  xnn0lem1lt  13265  xrinfmsslem  13329  xrub  13333  supxrunb1  13340  supxrunb2  13341  dfrp2  13416  elioc2  13431  elicc2  13433  ioomax  13444  ioopos  13446  elioopnf  13465  elicopnf  13467  difreicc  13506  hashbnd  14368  hashv01gt1  14377  fprodge0  16043  fprodge1  16045  pcadd  16944  ramubcl  17073  rge0srg  21588  mnfnei  23378  icopnfcld  24924  iocmnfcld  24925  xrtgioo  24964  xrge0tsms  24992  ioombl1lem4  25720  icombl1  25722  mbfmax  25808  upgrfi  29441  topnfbey  30820  isblo3i  31153  htthlem  31269  xlt2addrd  33104  fsumrp0cl  33341  xrge0tsmsd  33393  pnfinf  33503  xrge0slmod  33668  xrge0iifcnv  34323  xrge0iifiso  34325  xrge0iifhom  34327  lmxrge0  34342  esumcst  34453  esumcvgre  34481  voliune  34619  volfiniune  34620  sxbrsigalem0  34661  orvcgteel  34858  dstfrvclim1  34868  itg2addnclem2  38323  asindmre  38354  dvasin  38355  dvacos  38356  rfcnpre3  45753  supxrgere  46049  supxrgelem  46053  xrlexaddrp  46068  infxr  46082  xrpnf  46199  limsupre  46355  limsuppnflem  46424  liminflelimsupuz  46499  limsupub2  46526  icccncfext  46601  fourierdlem111  46931  fouriersw  46945  sge0iunmptlemre  47129  sge0rpcpnf  47135  sge0xaddlem1  47147  meaiuninclem  47194  hoidmvlelem5  47313  ovolval5lem1  47366  pimltpnff  47417  iccpartiltu  48171  itscnhlinecirc02p  49565