Theorem pnfge 13173

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 13171	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11280	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11291	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 704	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 260	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2146   class class class wbr 5111  +∞cpnf 11257  ℝ^*cxr 11259   < clt 11260   ≤ cle 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11173  ax-resscn 11174

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266

This theorem is used by:  pnfged  13174  xnn0n0n1ge2b  13175  0lepnf  13176  nltpnft  13208  xrre2  13214  xnn0lem1lt  13288  xleadd1a  13297  xlt2add  13304  xsubge0  13305  xlesubadd  13307  xlemul1a  13332  elicore  13443  elico2  13455  iccmax  13468  elxrge0  13502  nfile  14415  hashdom  14435  hashdomi  14436  hashge1  14445  hashss  14465  hashge2el2difr  14538  pcdvdsb  16953  pc2dvds  16963  pcaddlem  16972  xrsdsreclblem  21615  leordtvallem1  23419  lecldbas  23428  isxmet2d  24537  blssec  24645  nmoix  24939  nmoleub  24941  xrtgioo  25017  xrge0tsms  25045  metdstri  25062  nmoleub2lem  25326  ovolf  25694  ovollb2  25701  ovoliun  25717  ovolre  25737  voliunlem3  25764  volsup  25768  icombl  25776  ioombl  25777  ismbfd  25851  itg2seq  25954  dvfsumrlim  26243  dvfsumrlim2  26244  radcnvcl  26633  logfacbnd3  27440  log2sumbnd  27761  tgldimor  28824  xrdifh  33197  xrge0tsmsd  33459  unitssxrge0  34356  tpr2rico  34368  lmxrge0  34408  esumle  34514  esumlef  34518  esumpinfval  34529  esumpinfsum  34533  esumcvgsum  34544  ddemeas  34693  sxbrsigalem2  34743  omssubadd  34757  carsgclctunlem3  34777  signsply0  35005  ismblfin  38371  xrgepnfd  46107  supxrgelem  46113  supxrge  46114  infrpge  46127  xrlexaddrp  46128  infleinflem1  46145  infleinf  46147  infxrpnf  46220  ge0xrre  46307  iblsplit  46740  ismbl3  46760  ovolsplit  46762  sge0cl  47155  sge0less  47166  sge0pr  47168  sge0le  47181  sge0split  47183  carageniuncl  47297  ovnsubaddlem1  47344  hspmbl  47403  pgrpgt2nabl  49205