Metamath Proof Explorer

Theorem 0dig2nn0e

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

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

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 1 a1i 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> 2 e. NN )
3 0nn0 
 |-  0 e. NN0
4 3 a1i 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> 0 e. NN0 )
5 nn0rp0 
 |-  ( N e. NN0 -> N e. ( 0 [,) +oo ) )
6 5 adantr 
 |-  ( ( N e. NN0 /\ ( N / 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 / 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 / 2 ) e. NN0 ) -> ( 2 ^ 0 ) = 1 )
12 11 oveq2d 
 |-  ( ( N e. NN0 /\ ( N / 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 / 2 ) e. NN0 ) -> ( N / 1 ) = N )
16 12 15 eqtrd 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( N / ( 2 ^ 0 ) ) = N )
17 16 fveq2d 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( |_ ` ( N / ( 2 ^ 0 ) ) ) = ( |_ ` N ) )
18 17 oveq1d 
 |-  ( ( N e. NN0 /\ ( N / 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 adantr 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( |_ ` N ) = N )
23 22 oveq1d 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( ( |_ ` N ) mod 2 ) = ( N mod 2 ) )
24 nn0z 
 |-  ( ( N / 2 ) e. NN0 -> ( N / 2 ) e. ZZ )
25 24 adantl 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( N / 2 ) e. ZZ )
26 nn0re 
 |-  ( N e. NN0 -> N e. RR )
27 26 adantr 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> N e. RR )
28 2rp 
 |-  2 e. RR+
29 mod0 
 |-  ( ( N e. RR /\ 2 e. RR+ ) -> ( ( N mod 2 ) = 0 <-> ( N / 2 ) e. ZZ ) )
30 27 28 29 sylancl 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( ( N mod 2 ) = 0 <-> ( N / 2 ) e. ZZ ) )
31 25 30 mpbird 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( N mod 2 ) = 0 )
32 23 31 eqtrd 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( ( |_ ` N ) mod 2 ) = 0 )
33 18 32 eqtrd 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( ( |_ ` ( N / ( 2 ^ 0 ) ) ) mod 2 ) = 0 )
34 8 33 eqtrd 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( 0 ( digit ` 2 ) N ) = 0 )