Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
2 |
|
zesq |
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) ) |
3 |
1 2
|
syl |
|- ( N e. NN -> ( ( N / 2 ) e. ZZ <-> ( ( N ^ 2 ) / 2 ) e. ZZ ) ) |
4 |
|
nnrp |
|- ( N e. NN -> N e. RR+ ) |
5 |
4
|
rphalfcld |
|- ( N e. NN -> ( N / 2 ) e. RR+ ) |
6 |
5
|
rpgt0d |
|- ( N e. NN -> 0 < ( N / 2 ) ) |
7 |
|
nnsqcl |
|- ( N e. NN -> ( N ^ 2 ) e. NN ) |
8 |
7
|
nnrpd |
|- ( N e. NN -> ( N ^ 2 ) e. RR+ ) |
9 |
8
|
rphalfcld |
|- ( N e. NN -> ( ( N ^ 2 ) / 2 ) e. RR+ ) |
10 |
9
|
rpgt0d |
|- ( N e. NN -> 0 < ( ( N ^ 2 ) / 2 ) ) |
11 |
6 10
|
2thd |
|- ( N e. NN -> ( 0 < ( N / 2 ) <-> 0 < ( ( N ^ 2 ) / 2 ) ) ) |
12 |
3 11
|
anbi12d |
|- ( N e. NN -> ( ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) <-> ( ( ( N ^ 2 ) / 2 ) e. ZZ /\ 0 < ( ( N ^ 2 ) / 2 ) ) ) ) |
13 |
|
elnnz |
|- ( ( N / 2 ) e. NN <-> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) ) |
14 |
|
elnnz |
|- ( ( ( N ^ 2 ) / 2 ) e. NN <-> ( ( ( N ^ 2 ) / 2 ) e. ZZ /\ 0 < ( ( N ^ 2 ) / 2 ) ) ) |
15 |
12 13 14
|
3bitr4g |
|- ( N e. NN -> ( ( N / 2 ) e. NN <-> ( ( N ^ 2 ) / 2 ) e. NN ) ) |