Description: 6 is an even number. (Contributed by AV, 20-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 6even | |- 6 e. Even |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 6nn | |- 6 e. NN |
|
| 2 | 1 | nnzi | |- 6 e. ZZ |
| 3 | 3t2e6 | |- ( 3 x. 2 ) = 6 |
|
| 4 | 3 | eqcomi | |- 6 = ( 3 x. 2 ) |
| 5 | 4 | oveq1i | |- ( 6 / 2 ) = ( ( 3 x. 2 ) / 2 ) |
| 6 | 3cn | |- 3 e. CC |
|
| 7 | 2cn | |- 2 e. CC |
|
| 8 | 2ne0 | |- 2 =/= 0 |
|
| 9 | 6 7 8 | divcan4i | |- ( ( 3 x. 2 ) / 2 ) = 3 |
| 10 | 5 9 | eqtri | |- ( 6 / 2 ) = 3 |
| 11 | 3z | |- 3 e. ZZ |
|
| 12 | 10 11 | eqeltri | |- ( 6 / 2 ) e. ZZ |
| 13 | iseven | |- ( 6 e. Even <-> ( 6 e. ZZ /\ ( 6 / 2 ) e. ZZ ) ) |
|
| 14 | 2 12 13 | mpbir2an | |- 6 e. Even |