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 ∈ ℕ → N 2 ∈ ℕ ↔ ¬ N + 1 2 ∈ ℕ

Proof

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