This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrdi 
 |-  ( ( 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 ) )