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
|- ( N e. NN -> ( 2 || N <-> E. n e. NN ( 2 x. n ) = N ) )

Proof

Step Hyp Ref Expression
1 eleq1
 |-  ( ( 2 x. n ) = N -> ( ( 2 x. n ) e. NN <-> N e. NN ) )
2 simpr
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> n e. ZZ )
3 2re
 |-  2 e. RR
4 3 a1i
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> 2 e. RR )
5 zre
 |-  ( n e. ZZ -> n e. RR )
6 5 adantl
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> n e. RR )
7 0le2
 |-  0 <_ 2
8 7 a1i
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> 0 <_ 2 )
9 nngt0
 |-  ( ( 2 x. n ) e. NN -> 0 < ( 2 x. n ) )
10 9 adantr
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> 0 < ( 2 x. n ) )
11 prodgt0
 |-  ( ( ( 2 e. RR /\ n e. RR ) /\ ( 0 <_ 2 /\ 0 < ( 2 x. n ) ) ) -> 0 < n )
12 4 6 8 10 11 syl22anc
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> 0 < n )
13 elnnz
 |-  ( n e. NN <-> ( n e. ZZ /\ 0 < n ) )
14 2 12 13 sylanbrc
 |-  ( ( ( 2 x. n ) e. NN /\ n e. ZZ ) -> n e. NN )
15 14 ex
 |-  ( ( 2 x. n ) e. NN -> ( n e. ZZ -> n e. NN ) )
16 1 15 syl6bir
 |-  ( ( 2 x. n ) = N -> ( N e. NN -> ( n e. ZZ -> n e. NN ) ) )
17 16 com13
 |-  ( n e. ZZ -> ( N e. NN -> ( ( 2 x. n ) = N -> n e. NN ) ) )
18 17 impcom
 |-  ( ( N e. NN /\ n e. ZZ ) -> ( ( 2 x. n ) = N -> n e. NN ) )
19 18 pm4.71rd
 |-  ( ( N e. NN /\ n e. ZZ ) -> ( ( 2 x. n ) = N <-> ( n e. NN /\ ( 2 x. n ) = N ) ) )
20 19 bicomd
 |-  ( ( N e. NN /\ n e. ZZ ) -> ( ( n e. NN /\ ( 2 x. n ) = N ) <-> ( 2 x. n ) = N ) )
21 20 rexbidva
 |-  ( N e. NN -> ( E. n e. ZZ ( n e. NN /\ ( 2 x. n ) = N ) <-> E. n e. ZZ ( 2 x. n ) = N ) )
22 nnssz
 |-  NN C_ ZZ
23 rexss
 |-  ( NN C_ ZZ -> ( E. n e. NN ( 2 x. n ) = N <-> E. n e. ZZ ( n e. NN /\ ( 2 x. n ) = N ) ) )
24 22 23 mp1i
 |-  ( N e. NN -> ( E. n e. NN ( 2 x. n ) = N <-> E. n e. ZZ ( n e. NN /\ ( 2 x. n ) = N ) ) )
25 even2n
 |-  ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N )
26 25 a1i
 |-  ( N e. NN -> ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N ) )
27 21 24 26 3bitr4rd
 |-  ( N e. NN -> ( 2 || N <-> E. n e. NN ( 2 x. n ) = N ) )