brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  sl0

---

Theorem sl0 471

Description: Syntax for zero. (Contributed by la korvo, 31-Jul-2024.)

Assertion

Ref	Expression
sl0	sumti li 0

---

Proof of Theorem sl0

Step	Hyp	Ref	Expression
1		sli 469	1 sumti li 0

Colors of variables: sumti selbri bridi

Syntax hints:  li sli 469  0 p0 470

This theorem is referenced by:  succ-zero-ref  478  nat-indi  491  nat-indii  492  nat-ind-cur  493  sumji-no  501  pilji-no  508  gt-zero-ref  512

Copyright terms: Public domain

W3C validator