Description: A number that sums to itself is zero. Compare addid0 , readdid1addid2d . (Contributed by SN, 5-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sn-addid0.a | ||
sn-addid0.1 | |||
Assertion | sn-addid0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sn-addid0.a | ||
2 | sn-addid0.1 | ||
3 | sn-addid1 | ||
4 | 1 3 | syl | |
5 | 2 4 | eqtr4d | |
6 | 0cnd | ||
7 | 1 1 6 | sn-addcand | |
8 | 5 7 | mpbid |