Theorem pnfge 13035

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2111   class class class wbr 5093  +∞cpnf 11149  ℝ^*cxr 11151   < clt 11152   ≤ cle 11153

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11068  ax-resscn 11069

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-pnf 11154  df-mnf 11155  df-xr 11156  df-ltxr 11157  df-le 11158

This theorem is referenced by:  pnfged  13036  xnn0n0n1ge2b  13037  0lepnf  13038  nltpnft  13069  xrre2  13075  xnn0lem1lt  13149  xleadd1a  13158  xlt2add  13165  xsubge0  13166  xlesubadd  13168  xlemul1a  13193  elicore  13304  elico2  13316  iccmax  13329  elxrge0  13363  nfile  14272  hashdom  14292  hashdomi  14293  hashge1  14302  hashss  14322  hashge2el2difr  14394  pcdvdsb  16787  pc2dvds  16797  pcaddlem  16806  xrsdsreclblem  21355  leordtvallem1  23131  lecldbas  23140  isxmet2d  24248  blssec  24356  nmoix  24650  nmoleub  24652  xrtgioo  24728  xrge0tsms  24756  metdstri  24773  nmoleub2lem  25047  ovolf  25416  ovollb2  25423  ovoliun  25439  ovolre  25459  voliunlem3  25486  volsup  25490  icombl  25498  ioombl  25499  ismbfd  25573  itg2seq  25676  dvfsumrlim  25971  dvfsumrlim2  25972  radcnvcl  26359  logfacbnd3  27167  log2sumbnd  27488  tgldimor  28486  xrdifh  32770  xrge0tsmsd  33049  unitssxrge0  33920  tpr2rico  33932  lmxrge0  33972  esumle  34078  esumlef  34082  esumpinfval  34093  esumpinfsum  34097  esumcvgsum  34108  ddemeas  34256  sxbrsigalem2  34306  omssubadd  34320  carsgclctunlem3  34340  signsply0  34571  ismblfin  37707  xrgepnfd  45435  supxrgelem  45441  supxrge  45442  infrpge  45455  xrlexaddrp  45456  infleinflem1  45473  infleinf  45475  infxrpnf  45549  ge0xrre  45636  iblsplit  46069  ismbl3  46089  ovolsplit  46091  sge0cl  46484  sge0less  46495  sge0pr  46497  sge0le  46510  sge0split  46512  carageniuncl  46626  ovnsubaddlem1  46673  hspmbl  46732  pgrpgt2nabl  48471