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