Metamath Proof Explorer

Theorem 0dig2nn0o

Description: The last bit of an odd integer is 1. (Contributed by AV, 3-Jun-2010)

Ref Expression
Assertion 0dig2nn0o 
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 0 ( digit ` 2 ) N ) = 1 )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 1 a1i 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> 2 e. NN )
3 0nn0 
 |-  0 e. NN0
4 3 a1i 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> 0 e. NN0 )
5 nn0rp0 
 |-  ( N e. NN0 -> N e. ( 0 [,) +oo ) )
6 5 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> N e. ( 0 [,) +oo ) )
7 nn0digval 
 |-  ( ( 2 e. NN /\ 0 e. NN0 /\ N e. ( 0 [,) +oo ) ) -> ( 0 ( digit ` 2 ) N ) = ( ( |_ ` ( N / ( 2 ^ 0 ) ) ) mod 2 ) )
8 2 4 6 7 syl3anc 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 0 ( digit ` 2 ) N ) = ( ( |_ ` ( N / ( 2 ^ 0 ) ) ) mod 2 ) )
9 2cn 
 |-  2 e. CC
10 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
11 9 10 mp1i 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 2 ^ 0 ) = 1 )
12 11 oveq2d 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N / ( 2 ^ 0 ) ) = ( N / 1 ) )
13 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
14 13 div1d 
 |-  ( N e. NN0 -> ( N / 1 ) = N )
15 14 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N / 1 ) = N )
16 12 15 eqtrd 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N / ( 2 ^ 0 ) ) = N )
17 16 fveq2d 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / ( 2 ^ 0 ) ) ) = ( |_ ` N ) )
18 17 oveq1d 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` ( N / ( 2 ^ 0 ) ) ) mod 2 ) = ( ( |_ ` N ) mod 2 ) )
19 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
20 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
21 19 20 syl 
 |-  ( N e. NN0 -> ( |_ ` N ) = N )
22 21 oveq1d 
 |-  ( N e. NN0 -> ( ( |_ ` N ) mod 2 ) = ( N mod 2 ) )
23 22 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` N ) mod 2 ) = ( N mod 2 ) )
24 nn0z 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N + 1 ) / 2 ) e. ZZ )
25 24 adantl 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N + 1 ) / 2 ) e. ZZ )
26 2z 
 |-  2 e. ZZ
27 26 a1i 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> 2 e. ZZ )
28 2ne0 
 |-  2 =/= 0
29 28 a1i 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> 2 =/= 0 )
30 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
31 30 nn0zd 
 |-  ( N e. NN0 -> ( N + 1 ) e. ZZ )
32 31 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N + 1 ) e. ZZ )
33 dvdsval2 
 |-  ( ( 2 e. ZZ /\ 2 =/= 0 /\ ( N + 1 ) e. ZZ ) -> ( 2 || ( N + 1 ) <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
34 27 29 32 33 syl3anc 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 2 || ( N + 1 ) <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
35 25 34 mpbird 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> 2 || ( N + 1 ) )
36 oddp1even 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )
37 19 36 syl 
 |-  ( N e. NN0 -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )
38 37 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )
39 35 38 mpbird 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> -. 2 || N )
40 19 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> N e. ZZ )
41 mod2eq1n2dvds 
 |-  ( N e. ZZ -> ( ( N mod 2 ) = 1 <-> -. 2 || N ) )
42 40 41 syl 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N mod 2 ) = 1 <-> -. 2 || N ) )
43 39 42 mpbird 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N mod 2 ) = 1 )
44 23 43 eqtrd 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` N ) mod 2 ) = 1 )
45 18 44 eqtrd 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` ( N / ( 2 ^ 0 ) ) ) mod 2 ) = 1 )
46 8 45 eqtrd 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 0 ( digit ` 2 ) N ) = 1 )