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

---

Theorem sl0 517

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 515	1 sumti li 0

Colors of variables: sumti selbri bridi

Syntax hints:  li sli 515  0 p0 516

This theorem is referenced by:  succ-zero-ref  524  nat-indi  537  nat-indii  538  nat-ind-cur  539  sumji-no  547  pilji-no  554  gt-zero-ref  558

Copyright terms: Public domain

W3C validator