Metamath Proof Explorer


Theorem bits0ALTV

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

Ref Expression
Assertion bits0ALTV N 0 bits N N Odd

Proof

Step Hyp Ref Expression
1 0nn0 0 0
2 bitsval2 N 0 0 0 bits N ¬ 2 N 2 0
3 1 2 mpan2 N 0 bits N ¬ 2 N 2 0
4 2cn 2
5 exp0 2 2 0 = 1
6 4 5 ax-mp 2 0 = 1
7 6 oveq2i N 2 0 = N 1
8 zcn N N
9 8 div1d N N 1 = N
10 7 9 syl5eq N N 2 0 = N
11 10 fveq2d N N 2 0 = N
12 flid N N = N
13 11 12 eqtrd N N 2 0 = N
14 13 breq2d N 2 N 2 0 2 N
15 14 notbid N ¬ 2 N 2 0 ¬ 2 N
16 isodd3 N Odd N ¬ 2 N
17 16 baibr N ¬ 2 N N Odd
18 3 15 17 3bitrd N 0 bits N N Odd