Theorem pnfge 13193

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5166  +∞cpnf 11321  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330

This theorem is referenced by:  xnn0n0n1ge2b  13194  0lepnf  13195  nltpnft  13226  xrre2  13232  xnn0lem1lt  13306  xleadd1a  13315  xlt2add  13322  xsubge0  13323  xlesubadd  13325  xlemul1a  13350  elicore  13459  elico2  13471  iccmax  13483  elxrge0  13517  nfile  14408  hashdom  14428  hashdomi  14429  hashge1  14438  hashss  14458  hashge2el2difr  14530  pcdvdsb  16916  pc2dvds  16926  pcaddlem  16935  xrsdsreclblem  21453  leordtvallem1  23239  lecldbas  23248  isxmet2d  24358  blssec  24466  nmoix  24771  nmoleub  24773  xrtgioo  24847  xrge0tsms  24875  metdstri  24892  nmoleub2lem  25166  ovolf  25536  ovollb2  25543  ovoliun  25559  ovolre  25579  voliunlem3  25606  volsup  25610  icombl  25618  ioombl  25619  ismbfd  25693  itg2seq  25797  dvfsumrlim  26092  dvfsumrlim2  26093  radcnvcl  26478  xrlimcnp  27029  logfacbnd3  27285  log2sumbnd  27606  tgldimor  28528  xrdifh  32785  xrge0tsmsd  33041  unitssxrge0  33846  tpr2rico  33858  lmxrge0  33898  esumle  34022  esumlef  34026  esumpinfval  34037  esumpinfsum  34041  esumcvgsum  34052  ddemeas  34200  sxbrsigalem2  34251  omssubadd  34265  carsgclctunlem3  34285  signsply0  34528  ismblfin  37621  xrgepnfd  45246  supxrgelem  45252  supxrge  45253  infrpge  45266  xrlexaddrp  45267  infleinflem1  45285  infleinf  45287  infxrpnf  45361  pnfged  45389  ge0xrre  45449  iblsplit  45887  ismbl3  45907  ovolsplit  45909  sge0cl  46302  sge0less  46313  sge0pr  46315  sge0le  46328  sge0split  46330  carageniuncl  46444  ovnsubaddlem1  46491  hspmbl  46550  pimiooltgt  46631  pgrpgt2nabl  48091