Theorem pnfge 12078

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 12076	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 10205	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 10216	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 709	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 247	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∈ wcel 2103   class class class wbr 4760  +∞cpnf 10184  ℝ^*cxr 10186   < clt 10187   ≤ cle 10188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-xp 5224  df-cnv 5226  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193

This theorem is referenced by:  xnn0n0n1ge2b  12079  0lepnf  12080  nltpnft  12109  xrre2  12115  xleadd1a  12197  xlt2add  12204  xsubge0  12205  xlesubadd  12207  xlemul1a  12232  elicore  12340  elico2  12351  iccmax  12363  elxrge0  12395  nfile  13263  hashdom  13281  hashdomi  13282  hashge1  13291  hashss  13310  hashge2el2difr  13376  pcdvdsb  15696  pc2dvds  15706  pcaddlem  15715  xrsdsreclblem  19915  leordtvallem1  21137  lecldbas  21146  isxmet2d  22254  blssec  22362  nmoix  22655  nmoleub  22657  xrtgioo  22731  xrge0tsms  22759  metdstri  22776  nmoleub2lem  23035  ovolf  23371  ovollb2  23378  ovoliun  23394  ovolre  23414  voliunlem3  23441  volsup  23445  icombl  23453  ioombl  23454  ismbfd  23527  itg2seq  23629  dvfsumrlim  23914  dvfsumrlim2  23915  radcnvcl  24291  xrlimcnp  24815  logfacbnd3  25068  log2sumbnd  25353  tgldimor  25517  xrdifh  29772  xrge0tsmsd  30015  unitssxrge0  30176  tpr2rico  30188  lmxrge0  30228  esumle  30350  esumlef  30354  esumpinfval  30365  esumpinfsum  30369  esumcvgsum  30380  ddemeas  30529  sxbrsigalem2  30578  omssubadd  30592  carsgclctunlem3  30612  signsply0  30858  ismblfin  33682  xrgepnfd  39962  supxrgelem  39968  supxrge  39969  infrpge  39982  xrlexaddrp  39983  infleinflem1  40001  infleinf  40003  infxrpnf  40089  pnfged  40119  ge0xrre  40178  iblsplit  40602  ismbl3  40623  ovolsplit  40625  sge0cl  41018  sge0less  41029  sge0pr  41031  sge0le  41044  sge0split  41046  carageniuncl  41160  ovnsubaddlem1  41207  hspmbl  41266  pimiooltgt  41344  pgrpgt2nabl  42574