Metamath Proof Explorer


Theorem evennn2n

Description: A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021)

Ref Expression
Assertion evennn2n ( ๐‘ โˆˆ โ„• โ†’ ( 2 โˆฅ ๐‘ โ†” โˆƒ ๐‘› โˆˆ โ„• ( 2 ยท ๐‘› ) = ๐‘ ) )

Proof

Step Hyp Ref Expression
1 eleq1 โŠข ( ( 2 ยท ๐‘› ) = ๐‘ โ†’ ( ( 2 ยท ๐‘› ) โˆˆ โ„• โ†” ๐‘ โˆˆ โ„• ) )
2 simpr โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ ๐‘› โˆˆ โ„ค )
3 2re โŠข 2 โˆˆ โ„
4 3 a1i โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ 2 โˆˆ โ„ )
5 zre โŠข ( ๐‘› โˆˆ โ„ค โ†’ ๐‘› โˆˆ โ„ )
6 5 adantl โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ ๐‘› โˆˆ โ„ )
7 0le2 โŠข 0 โ‰ค 2
8 7 a1i โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ 0 โ‰ค 2 )
9 nngt0 โŠข ( ( 2 ยท ๐‘› ) โˆˆ โ„• โ†’ 0 < ( 2 ยท ๐‘› ) )
10 9 adantr โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ 0 < ( 2 ยท ๐‘› ) )
11 prodgt0 โŠข ( ( ( 2 โˆˆ โ„ โˆง ๐‘› โˆˆ โ„ ) โˆง ( 0 โ‰ค 2 โˆง 0 < ( 2 ยท ๐‘› ) ) ) โ†’ 0 < ๐‘› )
12 4 6 8 10 11 syl22anc โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ 0 < ๐‘› )
13 elnnz โŠข ( ๐‘› โˆˆ โ„• โ†” ( ๐‘› โˆˆ โ„ค โˆง 0 < ๐‘› ) )
14 2 12 13 sylanbrc โŠข ( ( ( 2 ยท ๐‘› ) โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ ๐‘› โˆˆ โ„• )
15 14 ex โŠข ( ( 2 ยท ๐‘› ) โˆˆ โ„• โ†’ ( ๐‘› โˆˆ โ„ค โ†’ ๐‘› โˆˆ โ„• ) )
16 1 15 syl6bir โŠข ( ( 2 ยท ๐‘› ) = ๐‘ โ†’ ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘› โˆˆ โ„ค โ†’ ๐‘› โˆˆ โ„• ) ) )
17 16 com13 โŠข ( ๐‘› โˆˆ โ„ค โ†’ ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 ยท ๐‘› ) = ๐‘ โ†’ ๐‘› โˆˆ โ„• ) ) )
18 17 impcom โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ ( ( 2 ยท ๐‘› ) = ๐‘ โ†’ ๐‘› โˆˆ โ„• ) )
19 18 pm4.71rd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ ( ( 2 ยท ๐‘› ) = ๐‘ โ†” ( ๐‘› โˆˆ โ„• โˆง ( 2 ยท ๐‘› ) = ๐‘ ) ) )
20 19 bicomd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐‘› โˆˆ โ„ค ) โ†’ ( ( ๐‘› โˆˆ โ„• โˆง ( 2 ยท ๐‘› ) = ๐‘ ) โ†” ( 2 ยท ๐‘› ) = ๐‘ ) )
21 20 rexbidva โŠข ( ๐‘ โˆˆ โ„• โ†’ ( โˆƒ ๐‘› โˆˆ โ„ค ( ๐‘› โˆˆ โ„• โˆง ( 2 ยท ๐‘› ) = ๐‘ ) โ†” โˆƒ ๐‘› โˆˆ โ„ค ( 2 ยท ๐‘› ) = ๐‘ ) )
22 nnssz โŠข โ„• โŠ† โ„ค
23 rexss โŠข ( โ„• โŠ† โ„ค โ†’ ( โˆƒ ๐‘› โˆˆ โ„• ( 2 ยท ๐‘› ) = ๐‘ โ†” โˆƒ ๐‘› โˆˆ โ„ค ( ๐‘› โˆˆ โ„• โˆง ( 2 ยท ๐‘› ) = ๐‘ ) ) )
24 22 23 mp1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( โˆƒ ๐‘› โˆˆ โ„• ( 2 ยท ๐‘› ) = ๐‘ โ†” โˆƒ ๐‘› โˆˆ โ„ค ( ๐‘› โˆˆ โ„• โˆง ( 2 ยท ๐‘› ) = ๐‘ ) ) )
25 even2n โŠข ( 2 โˆฅ ๐‘ โ†” โˆƒ ๐‘› โˆˆ โ„ค ( 2 ยท ๐‘› ) = ๐‘ )
26 25 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โˆฅ ๐‘ โ†” โˆƒ ๐‘› โˆˆ โ„ค ( 2 ยท ๐‘› ) = ๐‘ ) )
27 21 24 26 3bitr4rd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โˆฅ ๐‘ โ†” โˆƒ ๐‘› โˆˆ โ„• ( 2 ยท ๐‘› ) = ๐‘ ) )