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 |