Theorem pnfge 13042

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 13040	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11184	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11195	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 691	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 257	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2113   class class class wbr 5096  +∞cpnf 11161  ℝ^*cxr 11163   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170

This theorem is referenced by:  pnfged  13043  xnn0n0n1ge2b  13044  0lepnf  13045  nltpnft  13077  xrre2  13083  xnn0lem1lt  13157  xleadd1a  13166  xlt2add  13173  xsubge0  13174  xlesubadd  13176  xlemul1a  13201  elicore  13312  elico2  13324  iccmax  13337  elxrge0  13371  nfile  14280  hashdom  14300  hashdomi  14301  hashge1  14310  hashss  14330  hashge2el2difr  14402  pcdvdsb  16795  pc2dvds  16805  pcaddlem  16814  xrsdsreclblem  21365  leordtvallem1  23152  lecldbas  23161  isxmet2d  24269  blssec  24377  nmoix  24671  nmoleub  24673  xrtgioo  24749  xrge0tsms  24777  metdstri  24794  nmoleub2lem  25068  ovolf  25437  ovollb2  25444  ovoliun  25460  ovolre  25480  voliunlem3  25507  volsup  25511  icombl  25519  ioombl  25520  ismbfd  25594  itg2seq  25697  dvfsumrlim  25992  dvfsumrlim2  25993  radcnvcl  26380  logfacbnd3  27188  log2sumbnd  27509  tgldimor  28523  xrdifh  32809  xrge0tsmsd  33104  unitssxrge0  34006  tpr2rico  34018  lmxrge0  34058  esumle  34164  esumlef  34168  esumpinfval  34179  esumpinfsum  34183  esumcvgsum  34194  ddemeas  34342  sxbrsigalem2  34392  omssubadd  34406  carsgclctunlem3  34426  signsply0  34657  ismblfin  37801  xrgepnfd  45518  supxrgelem  45524  supxrge  45525  infrpge  45538  xrlexaddrp  45539  infleinflem1  45556  infleinf  45558  infxrpnf  45632  ge0xrre  45719  iblsplit  46152  ismbl3  46172  ovolsplit  46174  sge0cl  46567  sge0less  46578  sge0pr  46580  sge0le  46593  sge0split  46595  carageniuncl  46709  ovnsubaddlem1  46756  hspmbl  46815  pgrpgt2nabl  48554