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  21354  leordtvallem1  23130  lecldbas  23139  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  xrlimcnp  26911  logfacbnd3  27167  log2sumbnd  27488  tgldimor  28482  xrdifh  32753  xrge0tsmsd  33045  unitssxrge0  33883  tpr2rico  33895  lmxrge0  33935  esumle  34041  esumlef  34045  esumpinfval  34056  esumpinfsum  34060  esumcvgsum  34071  ddemeas  34219  sxbrsigalem2  34270  omssubadd  34284  carsgclctunlem3  34304  signsply0  34535  ismblfin  37648  xrgepnfd  45320  supxrgelem  45326  supxrge  45327  infrpge  45340  xrlexaddrp  45341  infleinflem1  45359  infleinf  45361  infxrpnf  45435  ge0xrre  45522  iblsplit  45957  ismbl3  45977  ovolsplit  45979  sge0cl  46372  sge0less  46383  sge0pr  46385  sge0le  46398  sge0split  46400  carageniuncl  46514  ovnsubaddlem1  46561  hspmbl  46620  pimiooltgt  46701  pgrpgt2nabl  48347