Theorem pnfge 13066

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5102  +∞cpnf 11181  ℝ^*cxr 11183   < clt 11184   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  pnfged  13067  xnn0n0n1ge2b  13068  0lepnf  13069  nltpnft  13100  xrre2  13106  xnn0lem1lt  13180  xleadd1a  13189  xlt2add  13196  xsubge0  13197  xlesubadd  13199  xlemul1a  13224  elicore  13335  elico2  13347  iccmax  13360  elxrge0  13394  nfile  14300  hashdom  14320  hashdomi  14321  hashge1  14330  hashss  14350  hashge2el2difr  14422  pcdvdsb  16816  pc2dvds  16826  pcaddlem  16835  xrsdsreclblem  21305  leordtvallem1  23073  lecldbas  23082  isxmet2d  24191  blssec  24299  nmoix  24593  nmoleub  24595  xrtgioo  24671  xrge0tsms  24699  metdstri  24716  nmoleub2lem  24990  ovolf  25359  ovollb2  25366  ovoliun  25382  ovolre  25402  voliunlem3  25429  volsup  25433  icombl  25441  ioombl  25442  ismbfd  25516  itg2seq  25619  dvfsumrlim  25914  dvfsumrlim2  25915  radcnvcl  26302  xrlimcnp  26854  logfacbnd3  27110  log2sumbnd  27431  tgldimor  28405  xrdifh  32676  xrge0tsmsd  32975  unitssxrge0  33863  tpr2rico  33875  lmxrge0  33915  esumle  34021  esumlef  34025  esumpinfval  34036  esumpinfsum  34040  esumcvgsum  34051  ddemeas  34199  sxbrsigalem2  34250  omssubadd  34264  carsgclctunlem3  34284  signsply0  34515  ismblfin  37628  xrgepnfd  45300  supxrgelem  45306  supxrge  45307  infrpge  45320  xrlexaddrp  45321  infleinflem1  45339  infleinf  45341  infxrpnf  45415  ge0xrre  45502  iblsplit  45937  ismbl3  45957  ovolsplit  45959  sge0cl  46352  sge0less  46363  sge0pr  46365  sge0le  46378  sge0split  46380  carageniuncl  46494  ovnsubaddlem1  46541  hspmbl  46600  pimiooltgt  46681  pgrpgt2nabl  48327