Theorem bitsval2

Description: Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bitsval2	|- ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bitsval	|- ( M e. ( bits ` N ) <-> ( N e. ZZ /\ M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
2		df-3an	|- ( ( N e. ZZ /\ M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) <-> ( ( N e. ZZ /\ M e. NN0 ) /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
3	1 2	bitri	|- ( M e. ( bits ` N ) <-> ( ( N e. ZZ /\ M e. NN0 ) /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
4	3	baib	|- ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )