Metamath Proof Explorer


Theorem 6even

Description: 6 is an even number. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion 6even
|- 6 e. Even

Proof

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