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 ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
2 1 nncnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℂ )
3 2cn ⊢ 2 ∈ ℂ
4 3 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
5 2ne0 ⊢ 2 ≠ 0
6 5 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
7 2 4 6 divcan2d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( 𝑁 + 1 ) )
8 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
9 8 4 6 divcan2d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
10 9 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) = ( 𝑁 + 1 ) )
11 7 10 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
12 nnz ⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
13 nnz ⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℤ )
14 zneo ⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
15 12 13 14 syl2an ⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ ) → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
16 15 expcom ⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) )
17 16 necon2bd ⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
18 11 17 syl5com ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
19 oveq1 ⊢ ( 𝑗 = 1 → ( 𝑗 + 1 ) = ( 1 + 1 ) )
20 19 oveq1d ⊢ ( 𝑗 = 1 → ( ( 𝑗 + 1 ) / 2 ) = ( ( 1 + 1 ) / 2 ) )
21 20 eleq1d ⊢ ( 𝑗 = 1 → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( 1 + 1 ) / 2 ) ∈ ℕ ) )
22 oveq1 ⊢ ( 𝑗 = 1 → ( 𝑗 / 2 ) = ( 1 / 2 ) )
23 22 eleq1d ⊢ ( 𝑗 = 1 → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( 1 / 2 ) ∈ ℕ ) )
24 21 23 orbi12d ⊢ ( 𝑗 = 1 → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( 1 + 1 ) / 2 ) ∈ ℕ ∨ ( 1 / 2 ) ∈ ℕ ) ) )
25 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 + 1 ) = ( 𝑘 + 1 ) )
26 25 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 + 1 ) / 2 ) = ( ( 𝑘 + 1 ) / 2 ) )
27 26 eleq1d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) )
28 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 / 2 ) = ( 𝑘 / 2 ) )
29 28 eleq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( 𝑘 / 2 ) ∈ ℕ ) )
30 27 29 orbi12d ⊢ ( 𝑗 = 𝑘 → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑘 / 2 ) ∈ ℕ ) ) )
31 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑘 + 1 ) + 1 ) )
32 31 oveq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑗 + 1 ) / 2 ) = ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) )
33 32 eleq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) )
34 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 / 2 ) = ( ( 𝑘 + 1 ) / 2 ) )
35 34 eleq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) )
36 33 35 orbi12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ∨ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) )
37 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 + 1 ) = ( 𝑁 + 1 ) )
38 37 oveq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 + 1 ) / 2 ) = ( ( 𝑁 + 1 ) / 2 ) )
39 38 eleq1d ⊢ ( 𝑗 = 𝑁 → ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
40 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 / 2 ) = ( 𝑁 / 2 ) )
41 40 eleq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 / 2 ) ∈ ℕ ↔ ( 𝑁 / 2 ) ∈ ℕ ) )
42 39 41 orbi12d ⊢ ( 𝑗 = 𝑁 → ( ( ( ( 𝑗 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑗 / 2 ) ∈ ℕ ) ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑁 / 2 ) ∈ ℕ ) ) )
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 ∈ ℕ
48 46 47 eqeltri ⊢ ( ( 1 + 1 ) / 2 ) ∈ ℕ
49 48 orci ⊢ ( ( ( 1 + 1 ) / 2 ) ∈ ℕ ∨ ( 1 / 2 ) ∈ ℕ )
50 peano2nn ⊢ ( ( 𝑘 / 2 ) ∈ ℕ → ( ( 𝑘 / 2 ) + 1 ) ∈ ℕ )
51 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
52 add1p1 ⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 + 1 ) + 1 ) = ( 𝑘 + 2 ) )
53 52 oveq1d ⊢ ( 𝑘 ∈ ℂ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) = ( ( 𝑘 + 2 ) / 2 ) )
54 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
55 divdir ⊢ ( ( 𝑘 ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑘 + 2 ) / 2 ) = ( ( 𝑘 / 2 ) + ( 2 / 2 ) ) )
56 3 54 55 mp3an23 ⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 + 2 ) / 2 ) = ( ( 𝑘 / 2 ) + ( 2 / 2 ) ) )
57 45 oveq2i ⊢ ( ( 𝑘 / 2 ) + ( 2 / 2 ) ) = ( ( 𝑘 / 2 ) + 1 )
58 56 57 eqtrdi ⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 + 2 ) / 2 ) = ( ( 𝑘 / 2 ) + 1 ) )
59 53 58 eqtrd ⊢ ( 𝑘 ∈ ℂ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) = ( ( 𝑘 / 2 ) + 1 ) )
60 51 59 syl ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) = ( ( 𝑘 / 2 ) + 1 ) )
61 60 eleq1d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ↔ ( ( 𝑘 / 2 ) + 1 ) ∈ ℕ ) )
62 50 61 imbitrrid ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 / 2 ) ∈ ℕ → ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) )
63 62 orim2d ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑘 / 2 ) ∈ ℕ ) → ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) ) )
64 orcom ⊢ ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ) ↔ ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ∨ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) )
65 63 64 imbitrdi ⊢ ( 𝑘 ∈ ℕ → ( ( ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑘 / 2 ) ∈ ℕ ) → ( ( ( ( 𝑘 + 1 ) + 1 ) / 2 ) ∈ ℕ ∨ ( ( 𝑘 + 1 ) / 2 ) ∈ ℕ ) ) )
66 24 30 36 42 49 65 nnind ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∨ ( 𝑁 / 2 ) ∈ ℕ ) )
67 66 ord ⊢ ( 𝑁 ∈ ℕ → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ ) )
68 18 67 impbid ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )