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