Metamath Proof Explorer


Theorem dfeven2

Description: Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion dfeven2 Even = { ๐‘ง โˆˆ โ„ค โˆฃ 2 โˆฅ ๐‘ง }

Proof

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 โˆฅ ๐‘ง }