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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ 𝐴 ↔ ( bits ‘ 𝐴 ) ⊆ ( ℤ≥ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 bitsres ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) )
2 1 eqeq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( bits ‘ 𝐴 ) ↔ ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) ) )
3 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
4 3 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
5 2nn ⊢ 2 ∈ ℕ
6 5 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℕ )
7 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
8 6 7 nnexpcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
9 4 8 nndivred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
10 9 flcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ )
11 8 nnzd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℤ )
12 10 11 zmulcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ∈ ℤ )
13 bitsf1 ⊢ bits : ℤ –1-1→ 𝒫 ℕ0
14 f1fveq ⊢ ( ( bits : ℤ –1-1→ 𝒫 ℕ0 ∧ ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ) → ( ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) ↔ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 ) )
15 13 14 mpan ⊢ ( ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) ↔ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 ) )
16 12 3 15 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) ↔ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 ) )
17 dvdsmul2 ⊢ ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℤ ) → ( 2 ↑ 𝑁 ) ∥ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) )
18 10 11 17 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∥ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) )
19 breq2 ⊢ ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 → ( ( 2 ↑ 𝑁 ) ∥ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ↔ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) )
20 18 19 syl5ibcom ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 → ( 2 ↑ 𝑁 ) ∥ 𝐴 ) )
21 8 nnne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ≠ 0 )
22 dvdsval2 ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ∧ 𝐴 ∈ ℤ ) → ( ( 2 ↑ 𝑁 ) ∥ 𝐴 ↔ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
23 11 21 3 22 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ 𝐴 ↔ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
24 23 biimpa ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
25 flid ⊢ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 / ( 2 ↑ 𝑁 ) ) )
26 24 25 syl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 / ( 2 ↑ 𝑁 ) ) )
27 26 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) · ( 2 ↑ 𝑁 ) ) )
28 3 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → 𝐴 ∈ ℂ )
30 8 nncnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
31 30 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
32 2cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → 2 ∈ ℂ )
33 2ne0 ⊢ 2 ≠ 0
34 33 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → 2 ≠ 0 )
35 7 nn0zd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → 𝑁 ∈ ℤ )
37 32 34 36 expne0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( 2 ↑ 𝑁 ) ≠ 0 )
38 29 31 37 divcan1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 )
39 27 38 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 )
40 39 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ 𝐴 → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 ) )
41 20 40 impbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) = 𝐴 ↔ ( 2 ↑ 𝑁 ) ∥ 𝐴 ) )
42 2 16 41 3bitrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ 𝐴 ↔ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( bits ‘ 𝐴 ) ) )
43 df-ss ⊢ ( ( bits ‘ 𝐴 ) ⊆ ( ℤ≥ ‘ 𝑁 ) ↔ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( bits ‘ 𝐴 ) )
44 42 43 bitr4di ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ 𝐴 ↔ ( bits ‘ 𝐴 ) ⊆ ( ℤ≥ ‘ 𝑁 ) ) )