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

Metamath Proof Explorer

Theorem evennn02n

Description: A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion evennn02n 
|- ( N e. NN0 -> ( 2 || N <-> E. n e. NN0 ( 2 x. n ) = N ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( 2 x. n ) = N -> ( ( 2 x. n ) e. NN0 <-> N e. NN0 ) )
2 simpr 
 |-  ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> n e. ZZ )
3 2rp 
 |-  2 e. RR+
4 3 a1i 
 |-  ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> 2 e. RR+ )
5 zre 
 |-  ( n e. ZZ -> n e. RR )
6 5 adantl 
 |-  ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> n e. RR )
7 nn0ge0 
 |-  ( ( 2 x. n ) e. NN0 -> 0 <_ ( 2 x. n ) )
8 7 adantr 
 |-  ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> 0 <_ ( 2 x. n ) )
9 4 6 8 prodge0rd 
 |-  ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> 0 <_ n )
10 elnn0z 
 |-  ( n e. NN0 <-> ( n e. ZZ /\ 0 <_ n ) )
11 2 9 10 sylanbrc 
 |-  ( ( ( 2 x. n ) e. NN0 /\ n e. ZZ ) -> n e. NN0 )
12 11 ex 
 |-  ( ( 2 x. n ) e. NN0 -> ( n e. ZZ -> n e. NN0 ) )
13 1 12 biimtrrdi 
 |-  ( ( 2 x. n ) = N -> ( N e. NN0 -> ( n e. ZZ -> n e. NN0 ) ) )
14 13 com13 
 |-  ( n e. ZZ -> ( N e. NN0 -> ( ( 2 x. n ) = N -> n e. NN0 ) ) )
15 14 impcom 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( 2 x. n ) = N -> n e. NN0 ) )
16 15 pm4.71rd 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( 2 x. n ) = N <-> ( n e. NN0 /\ ( 2 x. n ) = N ) ) )
17 16 bicomd 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( n e. NN0 /\ ( 2 x. n ) = N ) <-> ( 2 x. n ) = N ) )
18 17 rexbidva 
 |-  ( N e. NN0 -> ( E. n e. ZZ ( n e. NN0 /\ ( 2 x. n ) = N ) <-> E. n e. ZZ ( 2 x. n ) = N ) )
19 nn0ssz 
 |-  NN0 C_ ZZ
20 rexss 
 |-  ( NN0 C_ ZZ -> ( E. n e. NN0 ( 2 x. n ) = N <-> E. n e. ZZ ( n e. NN0 /\ ( 2 x. n ) = N ) ) )
21 19 20 mp1i 
 |-  ( N e. NN0 -> ( E. n e. NN0 ( 2 x. n ) = N <-> E. n e. ZZ ( n e. NN0 /\ ( 2 x. n ) = N ) ) )
22 even2n 
 |-  ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N )
23 22 a1i 
 |-  ( N e. NN0 -> ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N ) )
24 18 21 23 3bitr4rd 
 |-  ( N e. NN0 -> ( 2 || N <-> E. n e. NN0 ( 2 x. n ) = N ) )