Theorem ltpnf 12265

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 2778	. . . 4 ⊢ +∞ = +∞
2		orc 856	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 681	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 863	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10422	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10430	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 12260	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 580	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 249	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   = wceq 1601   ∈ wcel 2107   class class class wbr 4886  ℝcr 10271   <_ℝ cltrr 10276  +∞cpnf 10408  -∞cmnf 10409  ℝ^*cxr 10410   < clt 10411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-xp 5361  df-pnf 10413  df-xr 10415  df-ltxr 10416

This theorem is referenced by:  ltpnfd  12266  0ltpnf  12267  xrlttri  12282  xrlttr  12283  xrrebnd  12311  xrre  12312  qbtwnxr  12343  xrinfmsslem  12450  xrub  12454  supxrunb1  12461  supxrunb2  12462  elioc2  12548  elicc2  12550  ioomax  12560  ioopos  12562  elioopnf  12580  elicopnf  12582  difreicc  12621  hashbnd  13441  hashv01gt1  13450  fprodge0  15126  fprodge1  15128  pcadd  15997  ramubcl  16126  rge0srg  20213  mnfnei  21433  xblss2ps  22614  icopnfcld  22979  iocmnfcld  22980  blcvx  23009  xrtgioo  23017  reconnlem1  23037  xrge0tsms  23045  iccpnfhmeo  23152  ioombl1lem4  23765  icombl1  23767  uniioombllem1  23785  mbfmax  23853  ismbf3d  23858  itg2seq  23946  lhop2  24215  dvfsumlem2  24227  logccv  24846  xrlimcnp  25147  pntleme  25749  upgrfi  26439  topnfbey  27900  isblo3i  28228  htthlem  28346  xlt2addrd  30088  dfrp2  30097  fsumrp0cl  30257  pnfinf  30299  xrge0tsmsd  30347  xrge0slmod  30406  xrge0iifcnv  30577  xrge0iifiso  30579  xrge0iifhom  30581  lmxrge0  30596  esumcst  30723  esumcvgre  30751  voliune  30890  volfiniune  30891  sxbrsigalem0  30931  orvcgteel  31128  dstfrvclim1  31138  itg2addnclem2  34087  asindmre  34120  dvasin  34121  dvacos  34122  rfcnpre3  40125  supxrgere  40457  supxrgelem  40461  xrlexaddrp  40476  infxr  40491  xrpnf  40621  limsupre  40781  limsuppnfdlem  40841  limsuppnflem  40850  liminflelimsupuz  40925  limsupub2  40952  icccncfext  41028  fourierdlem111  41361  fourierdlem113  41363  fouriersw  41375  sge0iunmptlemre  41556  sge0rpcpnf  41562  sge0xaddlem1  41574  meaiuninclem  41621  hoidmvlelem5  41740  ovolval5lem1  41793  pimltpnf  41843  iccpartiltu  42390  itscnhlinecirc02p  43521