Theorem pnfge 11840

Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)

Assertion

Ref	Expression
pnfge	⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Proof of Theorem pnfge

Step	Hyp	Ref	Expression
1		pnfnlt 11838	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 9971	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 9982	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 703	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 246	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∈ wcel 1977   class class class wbr 4583  +∞cpnf 9950  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  xnn0n0n1ge2b  11841  0lepnf  11842  nltpnft  11871  xrre2  11875  xleadd1a  11955  xlt2add  11962  xsubge0  11963  xlesubadd  11965  xlemul1a  11990  elicore  12097  elico2  12108  iccmax  12120  elxrge0  12152  hashdom  13029  hashdomi  13030  hashge1  13039  hashss  13058  hashge2el2difr  13118  pcdvdsb  15411  pc2dvds  15421  pcaddlem  15430  xrsdsreclblem  19611  leordtvallem1  20824  lecldbas  20833  isxmet2d  21942  blssec  22050  nmoix  22343  nmoleub  22345  xrtgioo  22417  xrge0tsms  22445  metdstri  22462  nmoleub2lem  22722  ovolf  23057  ovollb2  23064  ovoliun  23080  ovolre  23100  voliunlem3  23127  volsup  23131  icombl  23139  ioombl  23140  ismbfd  23213  itg2seq  23315  dvfsumrlim  23598  dvfsumrlim2  23599  radcnvcl  23975  xrlimcnp  24495  logfacbnd3  24748  log2sumbnd  25033  tgldimor  25197  sizeusglecusg  26014  vdgfrgragt2  26554  xrdifh  28932  xrge0tsmsd  29116  unitssxrge0  29274  tpr2rico  29286  lmxrge0  29326  esumle  29447  esumlef  29451  esumpinfval  29462  esumpinfsum  29466  esumcvgsum  29477  ddemeas  29626  sxbrsigalem2  29675  omssubadd  29689  carsgclctunlem3  29709  signsply0  29954  ismblfin  32620  xrgepnfd  38488  supxrgelem  38494  supxrge  38495  infrpge  38508  xrlexaddrp  38509  infleinflem1  38527  infleinf  38529  ge0xrre  38605  iblsplit  38858  ismbl3  38879  ovolsplit  38881  sge0cl  39274  sge0less  39285  sge0pr  39287  sge0le  39300  sge0split  39302  carageniuncl  39413  ovnsubaddlem1  39460  hspmbl  39519  pimiooltgt  39598  nfile  40369  pgrpgt2nabl  41941