Theorem pnfge 12526

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2114   class class class wbr 5066  +∞cpnf 10672  ℝ^*cxr 10674   < clt 10675   ≤ cle 10676

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681

This theorem is referenced by:  xnn0n0n1ge2b  12527  0lepnf  12528  nltpnft  12558  xrre2  12564  xnn0lem1lt  12638  xleadd1a  12647  xlt2add  12654  xsubge0  12655  xlesubadd  12657  xlemul1a  12682  elicore  12790  elico2  12801  iccmax  12813  elxrge0  12846  nfile  13721  hashdom  13741  hashdomi  13742  hashge1  13751  hashss  13771  hashge2el2difr  13840  pcdvdsb  16205  pc2dvds  16215  pcaddlem  16224  xrsdsreclblem  20591  leordtvallem1  21818  lecldbas  21827  isxmet2d  22937  blssec  23045  nmoix  23338  nmoleub  23340  xrtgioo  23414  xrge0tsms  23442  metdstri  23459  nmoleub2lem  23718  ovolf  24083  ovollb2  24090  ovoliun  24106  ovolre  24126  voliunlem3  24153  volsup  24157  icombl  24165  ioombl  24166  ismbfd  24240  itg2seq  24343  dvfsumrlim  24628  dvfsumrlim2  24629  radcnvcl  25005  xrlimcnp  25546  logfacbnd3  25799  log2sumbnd  26120  tgldimor  26288  xrdifh  30503  xrge0tsmsd  30692  unitssxrge0  31143  tpr2rico  31155  lmxrge0  31195  esumle  31317  esumlef  31321  esumpinfval  31332  esumpinfsum  31336  esumcvgsum  31347  ddemeas  31495  sxbrsigalem2  31544  omssubadd  31558  carsgclctunlem3  31578  signsply0  31821  ismblfin  34948  xrgepnfd  41648  supxrgelem  41654  supxrge  41655  infrpge  41668  xrlexaddrp  41669  infleinflem1  41687  infleinf  41689  infxrpnf  41770  pnfged  41799  ge0xrre  41856  iblsplit  42300  ismbl3  42320  ovolsplit  42322  sge0cl  42712  sge0less  42723  sge0pr  42725  sge0le  42738  sge0split  42740  carageniuncl  42854  ovnsubaddlem1  42901  hspmbl  42960  pimiooltgt  43038  pgrpgt2nabl  44463