Step |
Hyp |
Ref |
Expression |
1 |
|
dfeven4 |
โข Even = { ๐ง โ โค โฃ โ ๐ โ โค ๐ง = ( 2 ยท ๐ ) } |
2 |
|
eqcom |
โข ( ๐ง = ( 2 ยท ๐ ) โ ( 2 ยท ๐ ) = ๐ง ) |
3 |
|
2cnd |
โข ( ( ๐ง โ โค โง ๐ โ โค ) โ 2 โ โ ) |
4 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
5 |
4
|
adantl |
โข ( ( ๐ง โ โค โง ๐ โ โค ) โ ๐ โ โ ) |
6 |
3 5
|
mulcomd |
โข ( ( ๐ง โ โค โง ๐ โ โค ) โ ( 2 ยท ๐ ) = ( ๐ ยท 2 ) ) |
7 |
6
|
eqeq1d |
โข ( ( ๐ง โ โค โง ๐ โ โค ) โ ( ( 2 ยท ๐ ) = ๐ง โ ( ๐ ยท 2 ) = ๐ง ) ) |
8 |
2 7
|
syl5bb |
โข ( ( ๐ง โ โค โง ๐ โ โค ) โ ( ๐ง = ( 2 ยท ๐ ) โ ( ๐ ยท 2 ) = ๐ง ) ) |
9 |
8
|
rexbidva |
โข ( ๐ง โ โค โ ( โ ๐ โ โค ๐ง = ( 2 ยท ๐ ) โ โ ๐ โ โค ( ๐ ยท 2 ) = ๐ง ) ) |
10 |
|
2z |
โข 2 โ โค |
11 |
|
divides |
โข ( ( 2 โ โค โง ๐ง โ โค ) โ ( 2 โฅ ๐ง โ โ ๐ โ โค ( ๐ ยท 2 ) = ๐ง ) ) |
12 |
10 11
|
mpan |
โข ( ๐ง โ โค โ ( 2 โฅ ๐ง โ โ ๐ โ โค ( ๐ ยท 2 ) = ๐ง ) ) |
13 |
9 12
|
bitr4d |
โข ( ๐ง โ โค โ ( โ ๐ โ โค ๐ง = ( 2 ยท ๐ ) โ 2 โฅ ๐ง ) ) |
14 |
13
|
rabbiia |
โข { ๐ง โ โค โฃ โ ๐ โ โค ๐ง = ( 2 ยท ๐ ) } = { ๐ง โ โค โฃ 2 โฅ ๐ง } |
15 |
1 14
|
eqtri |
โข Even = { ๐ง โ โค โฃ 2 โฅ ๐ง } |