Theorem pnfge 13060

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 13058	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11218	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11229	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 689	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 256	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2106   class class class wbr 5110  +∞cpnf 11195  ℝ^*cxr 11197   < clt 11198   ≤ cle 11199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204

This theorem is referenced by:  xnn0n0n1ge2b  13061  0lepnf  13062  nltpnft  13093  xrre2  13099  xnn0lem1lt  13173  xleadd1a  13182  xlt2add  13189  xsubge0  13190  xlesubadd  13192  xlemul1a  13217  elicore  13326  elico2  13338  iccmax  13350  elxrge0  13384  nfile  14269  hashdom  14289  hashdomi  14290  hashge1  14299  hashss  14319  hashge2el2difr  14392  pcdvdsb  16752  pc2dvds  16762  pcaddlem  16771  xrsdsreclblem  20880  leordtvallem1  22598  lecldbas  22607  isxmet2d  23717  blssec  23825  nmoix  24130  nmoleub  24132  xrtgioo  24206  xrge0tsms  24234  metdstri  24251  nmoleub2lem  24514  ovolf  24883  ovollb2  24890  ovoliun  24906  ovolre  24926  voliunlem3  24953  volsup  24957  icombl  24965  ioombl  24966  ismbfd  25040  itg2seq  25144  dvfsumrlim  25432  dvfsumrlim2  25433  radcnvcl  25813  xrlimcnp  26355  logfacbnd3  26608  log2sumbnd  26929  tgldimor  27507  xrdifh  31751  xrge0tsmsd  31969  unitssxrge0  32570  tpr2rico  32582  lmxrge0  32622  esumle  32746  esumlef  32750  esumpinfval  32761  esumpinfsum  32765  esumcvgsum  32776  ddemeas  32924  sxbrsigalem2  32975  omssubadd  32989  carsgclctunlem3  33009  signsply0  33252  ismblfin  36192  xrgepnfd  43686  supxrgelem  43692  supxrge  43693  infrpge  43706  xrlexaddrp  43707  infleinflem1  43725  infleinf  43727  infxrpnf  43801  pnfged  43829  ge0xrre  43889  iblsplit  44327  ismbl3  44347  ovolsplit  44349  sge0cl  44742  sge0less  44753  sge0pr  44755  sge0le  44768  sge0split  44770  carageniuncl  44884  ovnsubaddlem1  44931  hspmbl  44990  pimiooltgt  45071  pgrpgt2nabl  46562