Theorem pnfge 13172

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5143  +∞cpnf 11292  ℝ^*cxr 11294   < clt 11295   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301

This theorem is referenced by:  pnfged  13173  xnn0n0n1ge2b  13174  0lepnf  13175  nltpnft  13206  xrre2  13212  xnn0lem1lt  13286  xleadd1a  13295  xlt2add  13302  xsubge0  13303  xlesubadd  13305  xlemul1a  13330  elicore  13439  elico2  13451  iccmax  13463  elxrge0  13497  nfile  14398  hashdom  14418  hashdomi  14419  hashge1  14428  hashss  14448  hashge2el2difr  14520  pcdvdsb  16907  pc2dvds  16917  pcaddlem  16926  xrsdsreclblem  21430  leordtvallem1  23218  lecldbas  23227  isxmet2d  24337  blssec  24445  nmoix  24750  nmoleub  24752  xrtgioo  24828  xrge0tsms  24856  metdstri  24873  nmoleub2lem  25147  ovolf  25517  ovollb2  25524  ovoliun  25540  ovolre  25560  voliunlem3  25587  volsup  25591  icombl  25599  ioombl  25600  ismbfd  25674  itg2seq  25777  dvfsumrlim  26072  dvfsumrlim2  26073  radcnvcl  26460  xrlimcnp  27011  logfacbnd3  27267  log2sumbnd  27588  tgldimor  28510  xrdifh  32782  xrge0tsmsd  33065  unitssxrge0  33899  tpr2rico  33911  lmxrge0  33951  esumle  34059  esumlef  34063  esumpinfval  34074  esumpinfsum  34078  esumcvgsum  34089  ddemeas  34237  sxbrsigalem2  34288  omssubadd  34302  carsgclctunlem3  34322  signsply0  34566  ismblfin  37668  xrgepnfd  45342  supxrgelem  45348  supxrge  45349  infrpge  45362  xrlexaddrp  45363  infleinflem1  45381  infleinf  45383  infxrpnf  45457  ge0xrre  45544  iblsplit  45981  ismbl3  46001  ovolsplit  46003  sge0cl  46396  sge0less  46407  sge0pr  46409  sge0le  46422  sge0split  46424  carageniuncl  46538  ovnsubaddlem1  46585  hspmbl  46644  pimiooltgt  46725  pgrpgt2nabl  48282