Theorem pnfge 13269

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2146   class class class wbr 5105  +∞cpnf 11350  ℝ^*cxr 11352   < clt 11353   ≤ cle 11354

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-xp 5660  df-cnv 5662  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359

This theorem is used by:  pnfged  13270  xnn0n0n1ge2b  13271  0lepnf  13272  nltpnft  13304  xrre2  13310  xnn0lem1lt  13384  xleadd1a  13393  xlt2add  13400  xsubge0  13401  xlesubadd  13403  xlemul1a  13428  elicore  13539  elico2  13551  iccmax  13564  elxrge0  13598  nfile  14513  hashdom  14533  hashdomi  14534  hashge1  14543  hashss  14563  hashge2el2difr  14636  pcdvdsb  17059  pc2dvds  17069  pcaddlem  17078  xrsdsreclblem  21731  leordtvallem1  23540  lecldbas  23549  isxmet2d  24658  blssec  24766  nmoix  25060  nmoleub  25062  xrtgioo  25138  xrge0tsms  25166  metdstri  25183  nmoleub2lem  25447  ovolf  25815  ovollb2  25822  ovoliun  25838  ovolre  25858  voliunlem3  25885  volsup  25889  icombl  25897  ioombl  25898  ismbfd  25972  itg2seq  26075  dvfsumrlim  26363  dvfsumrlim2  26364  radcnvcl  26756  logfacbnd3  27562  log2sumbnd  27883  tgldimor  28977  xrdifh  33425  xrge0tsmsd  33687  unitssxrge0  34585  tpr2rico  34597  lmxrge0  34637  esumle  34743  esumlef  34747  esumpinfval  34758  esumpinfsum  34762  esumcvgsum  34773  ddemeas  34922  sxbrsigalem2  34971  carsgclctunlem3  35005  signsply0  35233  ismblfin  38719  xrgepnfd  46482  supxrgelem  46488  supxrge  46489  infrpge  46502  xrlexaddrp  46503  infleinflem1  46520  infleinf  46522  infxrpnf  46595  ge0xrre  46682  iblsplit  47115  ismbl3  47135  ovolsplit  47137  sge0cl  47530  sge0less  47541  sge0pr  47543  sge0le  47556  sge0split  47558  carageniuncl  47672  ovnsubaddlem1  47719  hspmbl  47778  pgrpgt2nabl  49617