Description: The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018) (Revised by Alexander van der Vekens, 9-Jun-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fz0addcom | |- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( A + B ) = ( B + A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfznn0 | |- ( A e. ( 0 ... N ) -> A e. NN0 ) |
|
| 2 | 1 | nn0cnd | |- ( A e. ( 0 ... N ) -> A e. CC ) |
| 3 | elfznn0 | |- ( B e. ( 0 ... N ) -> B e. NN0 ) |
|
| 4 | 3 | nn0cnd | |- ( B e. ( 0 ... N ) -> B e. CC ) |
| 5 | addcom | |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) ) |
|
| 6 | 2 4 5 | syl2an | |- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( A + B ) = ( B + A ) ) |