Theorem pnfge 13154

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 13152	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11262	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11273	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 703	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 260	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2149   class class class wbr 5113  +∞cpnf 11239  ℝ^*cxr 11241   < clt 11242   ≤ cle 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248

This theorem is referenced by:  pnfged  13155  xnn0n0n1ge2b  13156  0lepnf  13157  nltpnft  13189  xrre2  13195  xnn0lem1lt  13269  xleadd1a  13278  xlt2add  13285  xsubge0  13286  xlesubadd  13288  xlemul1a  13313  elicore  13424  elico2  13436  iccmax  13449  elxrge0  13483  nfile  14394  hashdom  14414  hashdomi  14415  hashge1  14424  hashss  14444  hashge2el2difr  14517  pcdvdsb  16928  pc2dvds  16938  pcaddlem  16947  xrsdsreclblem  21531  leordtvallem1  23335  lecldbas  23344  isxmet2d  24452  blssec  24560  nmoix  24854  nmoleub  24856  xrtgioo  24932  xrge0tsms  24960  metdstri  24977  nmoleub2lem  25241  ovolf  25609  ovollb2  25616  ovoliun  25632  ovolre  25652  voliunlem3  25679  volsup  25683  icombl  25691  ioombl  25692  ismbfd  25766  itg2seq  25869  dvfsumrlim  26158  dvfsumrlim2  26159  radcnvcl  26545  logfacbnd3  27352  log2sumbnd  27673  tgldimor  28736  xrdifh  33065  xrge0tsmsd  33333  unitssxrge0  34234  tpr2rico  34246  lmxrge0  34286  esumle  34392  esumlef  34396  esumpinfval  34407  esumpinfsum  34411  esumcvgsum  34422  ddemeas  34570  sxbrsigalem2  34620  omssubadd  34634  carsgclctunlem3  34654  signsply0  34882  ismblfin  38199  xrgepnfd  45938  supxrgelem  45944  supxrge  45945  infrpge  45958  xrlexaddrp  45959  infleinflem1  45976  infleinf  45978  infxrpnf  46051  ge0xrre  46138  iblsplit  46571  ismbl3  46591  ovolsplit  46593  sge0cl  46986  sge0less  46997  sge0pr  46999  sge0le  47012  sge0split  47014  carageniuncl  47128  ovnsubaddlem1  47175  hspmbl  47234  pgrpgt2nabl  49030