Metamath Proof Explorer

Theorem odd2np1

Description: An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion odd2np1 ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 divides ⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
3 1 2 mpan ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
4 3 notbid ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
5 elznn0 ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )
6 odd2np1lem ⊢ ( 𝑁 ∈ ℕ0 → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
7 6 adantl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
8 peano2z ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 + 1 ) ∈ ℤ )
9 znegcl ⊢ ( ( 𝑥 + 1 ) ∈ ℤ → - ( 𝑥 + 1 ) ∈ ℤ )
10 8 9 syl ⊢ ( 𝑥 ∈ ℤ → - ( 𝑥 + 1 ) ∈ ℤ )
11 10 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ) → - ( 𝑥 + 1 ) ∈ ℤ )
12 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
13 2cn ⊢ 2 ∈ ℂ
14 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ ℂ )
15 13 14 mpan ⊢ ( 𝑥 ∈ ℂ → ( 2 · 𝑥 ) ∈ ℂ )
16 peano2cn ⊢ ( ( 2 · 𝑥 ) ∈ ℂ → ( ( 2 · 𝑥 ) + 1 ) ∈ ℂ )
17 15 16 syl ⊢ ( 𝑥 ∈ ℂ → ( ( 2 · 𝑥 ) + 1 ) ∈ ℂ )
18 12 17 syl ⊢ ( 𝑥 ∈ ℤ → ( ( 2 · 𝑥 ) + 1 ) ∈ ℂ )
19 18 adantl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( ( 2 · 𝑥 ) + 1 ) ∈ ℂ )
20 simpl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℝ )
21 20 recnd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → 𝑁 ∈ ℂ )
22 negcon2 ⊢ ( ( ( ( 2 · 𝑥 ) + 1 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ↔ 𝑁 = - ( ( 2 · 𝑥 ) + 1 ) ) )
23 19 21 22 syl2anc ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ↔ 𝑁 = - ( ( 2 · 𝑥 ) + 1 ) ) )
24 eqcom ⊢ ( 𝑁 = - ( ( 2 · 𝑥 ) + 1 ) ↔ - ( ( 2 · 𝑥 ) + 1 ) = 𝑁 )
25 13 12 14 sylancr ⊢ ( 𝑥 ∈ ℤ → ( 2 · 𝑥 ) ∈ ℂ )
26 ax-1cn ⊢ 1 ∈ ℂ
27 13 26 mulcli ⊢ ( 2 · 1 ) ∈ ℂ
28 addsubass ⊢ ( ( ( 2 · 𝑥 ) ∈ ℂ ∧ ( 2 · 1 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) − 1 ) = ( ( 2 · 𝑥 ) + ( ( 2 · 1 ) − 1 ) ) )
29 27 26 28 mp3an23 ⊢ ( ( 2 · 𝑥 ) ∈ ℂ → ( ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) − 1 ) = ( ( 2 · 𝑥 ) + ( ( 2 · 1 ) − 1 ) ) )
30 25 29 syl ⊢ ( 𝑥 ∈ ℤ → ( ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) − 1 ) = ( ( 2 · 𝑥 ) + ( ( 2 · 1 ) − 1 ) ) )
31 2t1e2 ⊢ ( 2 · 1 ) = 2
32 31 oveq1i ⊢ ( ( 2 · 1 ) − 1 ) = ( 2 − 1 )
33 2m1e1 ⊢ ( 2 − 1 ) = 1
34 32 33 eqtri ⊢ ( ( 2 · 1 ) − 1 ) = 1
35 34 oveq2i ⊢ ( ( 2 · 𝑥 ) + ( ( 2 · 1 ) − 1 ) ) = ( ( 2 · 𝑥 ) + 1 )
36 30 35 eqtr2di ⊢ ( 𝑥 ∈ ℤ → ( ( 2 · 𝑥 ) + 1 ) = ( ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) − 1 ) )
37 adddi ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 2 · ( 𝑥 + 1 ) ) = ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) )
38 13 26 37 mp3an13 ⊢ ( 𝑥 ∈ ℂ → ( 2 · ( 𝑥 + 1 ) ) = ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) )
39 12 38 syl ⊢ ( 𝑥 ∈ ℤ → ( 2 · ( 𝑥 + 1 ) ) = ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) )
40 39 oveq1d ⊢ ( 𝑥 ∈ ℤ → ( ( 2 · ( 𝑥 + 1 ) ) − 1 ) = ( ( ( 2 · 𝑥 ) + ( 2 · 1 ) ) − 1 ) )
41 36 40 eqtr4d ⊢ ( 𝑥 ∈ ℤ → ( ( 2 · 𝑥 ) + 1 ) = ( ( 2 · ( 𝑥 + 1 ) ) − 1 ) )
42 41 negeqd ⊢ ( 𝑥 ∈ ℤ → - ( ( 2 · 𝑥 ) + 1 ) = - ( ( 2 · ( 𝑥 + 1 ) ) − 1 ) )
43 8 zcnd ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 + 1 ) ∈ ℂ )
44 mulneg2 ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑥 + 1 ) ∈ ℂ ) → ( 2 · - ( 𝑥 + 1 ) ) = - ( 2 · ( 𝑥 + 1 ) ) )
45 13 43 44 sylancr ⊢ ( 𝑥 ∈ ℤ → ( 2 · - ( 𝑥 + 1 ) ) = - ( 2 · ( 𝑥 + 1 ) ) )
46 45 oveq1d ⊢ ( 𝑥 ∈ ℤ → ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = ( - ( 2 · ( 𝑥 + 1 ) ) + 1 ) )
47 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑥 + 1 ) ∈ ℂ ) → ( 2 · ( 𝑥 + 1 ) ) ∈ ℂ )
48 13 43 47 sylancr ⊢ ( 𝑥 ∈ ℤ → ( 2 · ( 𝑥 + 1 ) ) ∈ ℂ )
49 negsubdi ⊢ ( ( ( 2 · ( 𝑥 + 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( 2 · ( 𝑥 + 1 ) ) − 1 ) = ( - ( 2 · ( 𝑥 + 1 ) ) + 1 ) )
50 48 26 49 sylancl ⊢ ( 𝑥 ∈ ℤ → - ( ( 2 · ( 𝑥 + 1 ) ) − 1 ) = ( - ( 2 · ( 𝑥 + 1 ) ) + 1 ) )
51 46 50 eqtr4d ⊢ ( 𝑥 ∈ ℤ → ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = - ( ( 2 · ( 𝑥 + 1 ) ) − 1 ) )
52 42 51 eqtr4d ⊢ ( 𝑥 ∈ ℤ → - ( ( 2 · 𝑥 ) + 1 ) = ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) )
53 52 adantl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → - ( ( 2 · 𝑥 ) + 1 ) = ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) )
54 53 eqeq1d ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( - ( ( 2 · 𝑥 ) + 1 ) = 𝑁 ↔ ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = 𝑁 ) )
55 24 54 bitrid ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( 𝑁 = - ( ( 2 · 𝑥 ) + 1 ) ↔ ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = 𝑁 ) )
56 23 55 bitrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) → ( ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ↔ ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = 𝑁 ) )
57 56 biimpa ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ) → ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = 𝑁 )
58 oveq2 ⊢ ( 𝑛 = - ( 𝑥 + 1 ) → ( 2 · 𝑛 ) = ( 2 · - ( 𝑥 + 1 ) ) )
59 58 oveq1d ⊢ ( 𝑛 = - ( 𝑥 + 1 ) → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) )
60 59 eqeq1d ⊢ ( 𝑛 = - ( 𝑥 + 1 ) → ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = 𝑁 ) )
61 60 rspcev ⊢ ( ( - ( 𝑥 + 1 ) ∈ ℤ ∧ ( ( 2 · - ( 𝑥 + 1 ) ) + 1 ) = 𝑁 ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
62 11 57 61 syl2anc ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ ) ∧ ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
63 62 rexlimdva2 ⊢ ( 𝑁 ∈ ℝ → ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
64 znegcl ⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
65 64 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑦 · 2 ) = - 𝑁 ) → - 𝑦 ∈ ℤ )
66 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
67 mulcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 2 ∈ ℂ ) → ( 𝑦 · 2 ) ∈ ℂ )
68 66 13 67 sylancl ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 · 2 ) ∈ ℂ )
69 recn ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
70 negcon2 ⊢ ( ( ( 𝑦 · 2 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑦 · 2 ) = - 𝑁 ↔ 𝑁 = - ( 𝑦 · 2 ) ) )
71 68 69 70 syl2anr ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 · 2 ) = - 𝑁 ↔ 𝑁 = - ( 𝑦 · 2 ) ) )
72 eqcom ⊢ ( 𝑁 = - ( 𝑦 · 2 ) ↔ - ( 𝑦 · 2 ) = 𝑁 )
73 mulneg1 ⊢ ( ( 𝑦 ∈ ℂ ∧ 2 ∈ ℂ ) → ( - 𝑦 · 2 ) = - ( 𝑦 · 2 ) )
74 66 13 73 sylancl ⊢ ( 𝑦 ∈ ℤ → ( - 𝑦 · 2 ) = - ( 𝑦 · 2 ) )
75 74 adantl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( - 𝑦 · 2 ) = - ( 𝑦 · 2 ) )
76 75 eqeq1d ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( ( - 𝑦 · 2 ) = 𝑁 ↔ - ( 𝑦 · 2 ) = 𝑁 ) )
77 72 76 bitr4id ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( 𝑁 = - ( 𝑦 · 2 ) ↔ ( - 𝑦 · 2 ) = 𝑁 ) )
78 71 77 bitrd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 · 2 ) = - 𝑁 ↔ ( - 𝑦 · 2 ) = 𝑁 ) )
79 78 biimpa ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑦 · 2 ) = - 𝑁 ) → ( - 𝑦 · 2 ) = 𝑁 )
80 oveq1 ⊢ ( 𝑘 = - 𝑦 → ( 𝑘 · 2 ) = ( - 𝑦 · 2 ) )
81 80 eqeq1d ⊢ ( 𝑘 = - 𝑦 → ( ( 𝑘 · 2 ) = 𝑁 ↔ ( - 𝑦 · 2 ) = 𝑁 ) )
82 81 rspcev ⊢ ( ( - 𝑦 ∈ ℤ ∧ ( - 𝑦 · 2 ) = 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 )
83 65 79 82 syl2anc ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑦 · 2 ) = - 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 )
84 83 rexlimdva2 ⊢ ( 𝑁 ∈ ℝ → ( ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = - 𝑁 → ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
85 63 84 orim12d ⊢ ( 𝑁 ∈ ℝ → ( ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ∨ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = - 𝑁 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ) )
86 odd2np1lem ⊢ ( - 𝑁 ∈ ℕ0 → ( ∃ 𝑥 ∈ ℤ ( ( 2 · 𝑥 ) + 1 ) = - 𝑁 ∨ ∃ 𝑦 ∈ ℤ ( 𝑦 · 2 ) = - 𝑁 ) )
87 85 86 impel ⊢ ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ0 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
88 7 87 jaodan ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
89 5 88 sylbi ⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
90 halfnz ⊢ ¬ ( 1 / 2 ) ∈ ℤ
91 reeanv ⊢ ( ∃ 𝑛 ∈ ℤ ∃ 𝑘 ∈ ℤ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ( 𝑘 · 2 ) = 𝑁 ) ↔ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
92 eqtr3 ⊢ ( ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ( 𝑘 · 2 ) = 𝑁 ) → ( ( 2 · 𝑛 ) + 1 ) = ( 𝑘 · 2 ) )
93 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
94 mulcom ⊢ ( ( 𝑘 ∈ ℂ ∧ 2 ∈ ℂ ) → ( 𝑘 · 2 ) = ( 2 · 𝑘 ) )
95 93 13 94 sylancl ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 · 2 ) = ( 2 · 𝑘 ) )
96 95 eqeq2d ⊢ ( 𝑘 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = ( 𝑘 · 2 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 2 · 𝑘 ) ) )
97 96 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = ( 𝑘 · 2 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 2 · 𝑘 ) ) )
98 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 2 · 𝑘 ) ∈ ℂ )
99 13 93 98 sylancr ⊢ ( 𝑘 ∈ ℤ → ( 2 · 𝑘 ) ∈ ℂ )
100 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
101 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 · 𝑛 ) ∈ ℂ )
102 13 100 101 sylancr ⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℂ )
103 subadd ⊢ ( ( ( 2 · 𝑘 ) ∈ ℂ ∧ ( 2 · 𝑛 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 2 · 𝑘 ) ) )
104 26 103 mp3an3 ⊢ ( ( ( 2 · 𝑘 ) ∈ ℂ ∧ ( 2 · 𝑛 ) ∈ ℂ ) → ( ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 2 · 𝑘 ) ) )
105 99 102 104 syl2anr ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 ↔ ( ( 2 · 𝑛 ) + 1 ) = ( 2 · 𝑘 ) ) )
106 subcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑘 − 𝑛 ) ∈ ℂ )
107 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
108 eqcom ⊢ ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( 1 / 2 ) = ( 𝑘 − 𝑛 ) )
109 divmul ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑘 − 𝑛 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 1 / 2 ) = ( 𝑘 − 𝑛 ) ↔ ( 2 · ( 𝑘 − 𝑛 ) ) = 1 ) )
110 108 109 bitrid ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑘 − 𝑛 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( 2 · ( 𝑘 − 𝑛 ) ) = 1 ) )
111 26 107 110 mp3an13 ⊢ ( ( 𝑘 − 𝑛 ) ∈ ℂ → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( 2 · ( 𝑘 − 𝑛 ) ) = 1 ) )
112 106 111 syl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( 2 · ( 𝑘 − 𝑛 ) ) = 1 ) )
113 112 ancoms ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( 2 · ( 𝑘 − 𝑛 ) ) = 1 ) )
114 subdi ⊢ ( ( 2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 · ( 𝑘 − 𝑛 ) ) = ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) )
115 13 114 mp3an1 ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 · ( 𝑘 − 𝑛 ) ) = ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) )
116 115 ancoms ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 2 · ( 𝑘 − 𝑛 ) ) = ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) )
117 116 eqeq1d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 2 · ( 𝑘 − 𝑛 ) ) = 1 ↔ ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 ) )
118 113 117 bitrd ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 ) )
119 100 93 118 syl2an ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) ↔ ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 ) )
120 zsubcl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑘 − 𝑛 ) ∈ ℤ )
121 eleq1 ⊢ ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) → ( ( 𝑘 − 𝑛 ) ∈ ℤ ↔ ( 1 / 2 ) ∈ ℤ ) )
122 120 121 syl5ibcom ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) → ( 1 / 2 ) ∈ ℤ ) )
123 122 ancoms ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 − 𝑛 ) = ( 1 / 2 ) → ( 1 / 2 ) ∈ ℤ ) )
124 119 123 sylbird ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) = 1 → ( 1 / 2 ) ∈ ℤ ) )
125 105 124 sylbird ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = ( 2 · 𝑘 ) → ( 1 / 2 ) ∈ ℤ ) )
126 97 125 sylbid ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑛 ) + 1 ) = ( 𝑘 · 2 ) → ( 1 / 2 ) ∈ ℤ ) )
127 92 126 syl5 ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ( 𝑘 · 2 ) = 𝑁 ) → ( 1 / 2 ) ∈ ℤ ) )
128 127 rexlimivv ⊢ ( ∃ 𝑛 ∈ ℤ ∃ 𝑘 ∈ ℤ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ( 𝑘 · 2 ) = 𝑁 ) → ( 1 / 2 ) ∈ ℤ )
129 91 128 sylbir ⊢ ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) → ( 1 / 2 ) ∈ ℤ )
130 90 129 mto ⊢ ¬ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 )
131 pm5.17 ⊢ ( ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ∧ ¬ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ) ↔ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) )
132 bicom ⊢ ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ↔ ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ↔ ( ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
133 131 132 bitri ⊢ ( ( ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∨ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ∧ ¬ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ∧ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ) ) ↔ ( ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
134 89 130 133 sylanblc ⊢ ( 𝑁 ∈ ℤ → ( ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 · 2 ) = 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
135 4 134 bitrd ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )