Metamath Proof Explorer

Theorem bitsuz

Description: The bits of a number are all at least N iff the number is divisible by 2 ^ N . (Contributed by Mario Carneiro, 21-Sep-2016)

Ref Expression
Assertion bitsuz 
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( 2 ^ N ) || A <-> ( bits ` A ) C_ ( ZZ>= ` N ) ) )

Proof

Step Hyp Ref Expression
1 bitsres 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) )
2 1 eqeq1d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` A ) <-> ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) = ( bits ` A ) ) )
3 simpl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. ZZ )
4 3 zred 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. RR )
5 2nn 
 |-  2 e. NN
6 5 a1i 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> 2 e. NN )
7 simpr 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> N e. NN0 )
8 6 7 nnexpcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. NN )
9 4 8 nndivred 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A / ( 2 ^ N ) ) e. RR )
10 9 flcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( |_ ` ( A / ( 2 ^ N ) ) ) e. ZZ )
11 8 nnzd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. ZZ )
12 10 11 zmulcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) e. ZZ )
13 bitsf1 
 |-  bits : ZZ -1-1-> ~P NN0
14 f1fveq 
 |-  ( ( bits : ZZ -1-1-> ~P NN0 /\ ( ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) e. ZZ /\ A e. ZZ ) ) -> ( ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) = ( bits ` A ) <-> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A ) )
15 13 14 mpan 
 |-  ( ( ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) e. ZZ /\ A e. ZZ ) -> ( ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) = ( bits ` A ) <-> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A ) )
16 12 3 15 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) = ( bits ` A ) <-> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A ) )
17 dvdsmul2 
 |-  ( ( ( |_ ` ( A / ( 2 ^ N ) ) ) e. ZZ /\ ( 2 ^ N ) e. ZZ ) -> ( 2 ^ N ) || ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) )
18 10 11 17 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) || ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) )
19 breq2 
 |-  ( ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A -> ( ( 2 ^ N ) || ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) <-> ( 2 ^ N ) || A ) )
20 18 19 syl5ibcom 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A -> ( 2 ^ N ) || A ) )
21 8 nnne0d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) =/= 0 )
22 dvdsval2 
 |-  ( ( ( 2 ^ N ) e. ZZ /\ ( 2 ^ N ) =/= 0 /\ A e. ZZ ) -> ( ( 2 ^ N ) || A <-> ( A / ( 2 ^ N ) ) e. ZZ ) )
23 11 21 3 22 syl3anc 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( 2 ^ N ) || A <-> ( A / ( 2 ^ N ) ) e. ZZ ) )
24 23 biimpa 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( A / ( 2 ^ N ) ) e. ZZ )
25 flid 
 |-  ( ( A / ( 2 ^ N ) ) e. ZZ -> ( |_ ` ( A / ( 2 ^ N ) ) ) = ( A / ( 2 ^ N ) ) )
26 24 25 syl 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( |_ ` ( A / ( 2 ^ N ) ) ) = ( A / ( 2 ^ N ) ) )
27 26 oveq1d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = ( ( A / ( 2 ^ N ) ) x. ( 2 ^ N ) ) )
28 3 zcnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. CC )
29 28 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> A e. CC )
30 8 nncnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. CC )
31 30 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( 2 ^ N ) e. CC )
32 2cnd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> 2 e. CC )
33 2ne0 
 |-  2 =/= 0
34 33 a1i 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> 2 =/= 0 )
35 7 nn0zd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> N e. ZZ )
36 35 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> N e. ZZ )
37 32 34 36 expne0d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( 2 ^ N ) =/= 0 )
38 29 31 37 divcan1d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( ( A / ( 2 ^ N ) ) x. ( 2 ^ N ) ) = A )
39 27 38 eqtrd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( 2 ^ N ) || A ) -> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A )
40 39 ex 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( 2 ^ N ) || A -> ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A ) )
41 20 40 impbid 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) = A <-> ( 2 ^ N ) || A ) )
42 2 16 41 3bitrrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( 2 ^ N ) || A <-> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` A ) ) )
43 df-ss 
 |-  ( ( bits ` A ) C_ ( ZZ>= ` N ) <-> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` A ) )
44 42 43 bitr4di 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( 2 ^ N ) || A <-> ( bits ` A ) C_ ( ZZ>= ` N ) ) )