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