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 N ¬ 2 N n 2 n + 1 = N

Proof

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