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

Theorem sl0 575
Description: Syntax for zero. (Contributed by la korvo, 31-Jul-2024.)
Assertion
Ref Expression
sl0 sumti li no

Proof of Theorem sl0
StepHypRef Expression
1 sli 573 1 sumti li no
Colors of variables: sumti selbri bridi
Syntax hints:   li sli 573   no p0 574
This theorem is referenced by:  succ-zero-ref  582  nat-indi  595  nat-indii  596  nat-ind-cur  597  sumji-no  605  pilji-no  612  gt-zero-ref  616
  Copyright terms: Public domain W3C validator