Metamath Proof Explorer

Theorem nneo

Description: A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006) (Proof shortened by Mario Carneiro, 18-May-2014)

Ref Expression
Assertion nneo 
|- ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( N e. NN -> N e. CC )
2 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
3 1 2 syl 
 |-  ( N e. NN -> ( N + 1 ) e. CC )
4 2cn 
 |-  2 e. CC
5 4 a1i 
 |-  ( N e. NN -> 2 e. CC )
6 2ne0 
 |-  2 =/= 0
7 6 a1i 
 |-  ( N e. NN -> 2 =/= 0 )
8 3 5 7 divcan2d 
 |-  ( N e. NN -> ( 2 x. ( ( N + 1 ) / 2 ) ) = ( N + 1 ) )
9 1 5 7 divcan2d 
 |-  ( N e. NN -> ( 2 x. ( N / 2 ) ) = N )
10 9 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. ( N / 2 ) ) + 1 ) = ( N + 1 ) )
11 8 10 eqtr4d 
 |-  ( N e. NN -> ( 2 x. ( ( N + 1 ) / 2 ) ) = ( ( 2 x. ( N / 2 ) ) + 1 ) )
12 nnz 
 |-  ( ( ( N + 1 ) / 2 ) e. NN -> ( ( N + 1 ) / 2 ) e. ZZ )
13 nnz 
 |-  ( ( N / 2 ) e. NN -> ( N / 2 ) e. ZZ )
14 zneo 
 |-  ( ( ( ( N + 1 ) / 2 ) e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) )
15 12 13 14 syl2an 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ ( N / 2 ) e. NN ) -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) )
16 15 expcom 
 |-  ( ( N / 2 ) e. NN -> ( ( ( N + 1 ) / 2 ) e. NN -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) ) )
17 16 necon2bd 
 |-  ( ( N / 2 ) e. NN -> ( ( 2 x. ( ( N + 1 ) / 2 ) ) = ( ( 2 x. ( N / 2 ) ) + 1 ) -> -. ( ( N + 1 ) / 2 ) e. NN ) )
18 11 17 syl5com 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN -> -. ( ( N + 1 ) / 2 ) e. NN ) )
19 oveq1 
 |-  ( j = 1 -> ( j + 1 ) = ( 1 + 1 ) )
20 19 oveq1d 
 |-  ( j = 1 -> ( ( j + 1 ) / 2 ) = ( ( 1 + 1 ) / 2 ) )
21 20 eleq1d 
 |-  ( j = 1 -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( 1 + 1 ) / 2 ) e. NN ) )
22 oveq1 
 |-  ( j = 1 -> ( j / 2 ) = ( 1 / 2 ) )
23 22 eleq1d 
 |-  ( j = 1 -> ( ( j / 2 ) e. NN <-> ( 1 / 2 ) e. NN ) )
24 21 23 orbi12d 
 |-  ( j = 1 -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( 1 + 1 ) / 2 ) e. NN \/ ( 1 / 2 ) e. NN ) ) )
25 oveq1 
 |-  ( j = k -> ( j + 1 ) = ( k + 1 ) )
26 25 oveq1d 
 |-  ( j = k -> ( ( j + 1 ) / 2 ) = ( ( k + 1 ) / 2 ) )
27 26 eleq1d 
 |-  ( j = k -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( k + 1 ) / 2 ) e. NN ) )
28 oveq1 
 |-  ( j = k -> ( j / 2 ) = ( k / 2 ) )
29 28 eleq1d 
 |-  ( j = k -> ( ( j / 2 ) e. NN <-> ( k / 2 ) e. NN ) )
30 27 29 orbi12d 
 |-  ( j = k -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( k + 1 ) / 2 ) e. NN \/ ( k / 2 ) e. NN ) ) )
31 oveq1 
 |-  ( j = ( k + 1 ) -> ( j + 1 ) = ( ( k + 1 ) + 1 ) )
32 31 oveq1d 
 |-  ( j = ( k + 1 ) -> ( ( j + 1 ) / 2 ) = ( ( ( k + 1 ) + 1 ) / 2 ) )
33 32 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) )
34 oveq1 
 |-  ( j = ( k + 1 ) -> ( j / 2 ) = ( ( k + 1 ) / 2 ) )
35 34 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( j / 2 ) e. NN <-> ( ( k + 1 ) / 2 ) e. NN ) )
36 33 35 orbi12d 
 |-  ( j = ( k + 1 ) -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN \/ ( ( k + 1 ) / 2 ) e. NN ) ) )
37 oveq1 
 |-  ( j = N -> ( j + 1 ) = ( N + 1 ) )
38 37 oveq1d 
 |-  ( j = N -> ( ( j + 1 ) / 2 ) = ( ( N + 1 ) / 2 ) )
39 38 eleq1d 
 |-  ( j = N -> ( ( ( j + 1 ) / 2 ) e. NN <-> ( ( N + 1 ) / 2 ) e. NN ) )
40 oveq1 
 |-  ( j = N -> ( j / 2 ) = ( N / 2 ) )
41 40 eleq1d 
 |-  ( j = N -> ( ( j / 2 ) e. NN <-> ( N / 2 ) e. NN ) )
42 39 41 orbi12d 
 |-  ( j = N -> ( ( ( ( j + 1 ) / 2 ) e. NN \/ ( j / 2 ) e. NN ) <-> ( ( ( N + 1 ) / 2 ) e. NN \/ ( N / 2 ) e. NN ) ) )
43 df-2 
 |-  2 = ( 1 + 1 )
44 43 oveq1i 
 |-  ( 2 / 2 ) = ( ( 1 + 1 ) / 2 )
45 2div2e1 
 |-  ( 2 / 2 ) = 1
46 44 45 eqtr3i 
 |-  ( ( 1 + 1 ) / 2 ) = 1
47 1nn 
 |-  1 e. NN
48 46 47 eqeltri 
 |-  ( ( 1 + 1 ) / 2 ) e. NN
49 48 orci 
 |-  ( ( ( 1 + 1 ) / 2 ) e. NN \/ ( 1 / 2 ) e. NN )
50 peano2nn 
 |-  ( ( k / 2 ) e. NN -> ( ( k / 2 ) + 1 ) e. NN )
51 nncn 
 |-  ( k e. NN -> k e. CC )
52 add1p1 
 |-  ( k e. CC -> ( ( k + 1 ) + 1 ) = ( k + 2 ) )
53 52 oveq1d 
 |-  ( k e. CC -> ( ( ( k + 1 ) + 1 ) / 2 ) = ( ( k + 2 ) / 2 ) )
54 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
55 divdir 
 |-  ( ( k e. CC /\ 2 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( k + 2 ) / 2 ) = ( ( k / 2 ) + ( 2 / 2 ) ) )
56 4 54 55 mp3an23 
 |-  ( k e. CC -> ( ( k + 2 ) / 2 ) = ( ( k / 2 ) + ( 2 / 2 ) ) )
57 45 oveq2i 
 |-  ( ( k / 2 ) + ( 2 / 2 ) ) = ( ( k / 2 ) + 1 )
58 56 57 eqtrdi 
 |-  ( k e. CC -> ( ( k + 2 ) / 2 ) = ( ( k / 2 ) + 1 ) )
59 53 58 eqtrd 
 |-  ( k e. CC -> ( ( ( k + 1 ) + 1 ) / 2 ) = ( ( k / 2 ) + 1 ) )
60 51 59 syl 
 |-  ( k e. NN -> ( ( ( k + 1 ) + 1 ) / 2 ) = ( ( k / 2 ) + 1 ) )
61 60 eleq1d 
 |-  ( k e. NN -> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN <-> ( ( k / 2 ) + 1 ) e. NN ) )
62 50 61 syl5ibr 
 |-  ( k e. NN -> ( ( k / 2 ) e. NN -> ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) )
63 62 orim2d 
 |-  ( k e. NN -> ( ( ( ( k + 1 ) / 2 ) e. NN \/ ( k / 2 ) e. NN ) -> ( ( ( k + 1 ) / 2 ) e. NN \/ ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) ) )
64 orcom 
 |-  ( ( ( ( k + 1 ) / 2 ) e. NN \/ ( ( ( k + 1 ) + 1 ) / 2 ) e. NN ) <-> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN \/ ( ( k + 1 ) / 2 ) e. NN ) )
65 63 64 syl6ib 
 |-  ( k e. NN -> ( ( ( ( k + 1 ) / 2 ) e. NN \/ ( k / 2 ) e. NN ) -> ( ( ( ( k + 1 ) + 1 ) / 2 ) e. NN \/ ( ( k + 1 ) / 2 ) e. NN ) ) )
66 24 30 36 42 49 65 nnind 
 |-  ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. NN \/ ( N / 2 ) e. NN ) )
67 66 ord 
 |-  ( N e. NN -> ( -. ( ( N + 1 ) / 2 ) e. NN -> ( N / 2 ) e. NN ) )
68 18 67 impbid 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) )