Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℤ ) |
2 |
|
2nn |
⊢ 2 ∈ ℕ |
3 |
2
|
a1i |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 2 ∈ ℕ ) |
4 |
|
simpr |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 ) |
5 |
3 4
|
nnexpcld |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 2 ↑ 𝑀 ) ∈ ℕ ) |
6 |
1 5
|
zmodcld |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 ) |
7 |
6
|
nn0zd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ) |
8 |
7
|
biantrurd |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ) ) |
9 |
1
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ ) |
10 |
|
simplr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 ) |
11 |
|
bitsval2 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ) ) |
12 |
9 10 11
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ) ) |
13 |
|
simpr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 < 𝑀 ) |
14 |
13
|
biantrud |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) |
15 |
|
2z |
⊢ 2 ∈ ℤ |
16 |
15
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℤ ) |
17 |
9
|
zred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℝ ) |
18 |
2
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℕ ) |
19 |
18 10
|
nnexpcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℕ ) |
20 |
17 19
|
nndivred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 / ( 2 ↑ 𝑥 ) ) ∈ ℝ ) |
21 |
20
|
flcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ) |
22 |
7
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ) |
23 |
22
|
zred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ ) |
24 |
23 19
|
nndivred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ) |
25 |
24
|
flcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ) |
26 |
19
|
nnzd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℤ ) |
27 |
26 16
|
zmulcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∈ ℤ ) |
28 |
5
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℕ ) |
29 |
28
|
nnzd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℤ ) |
30 |
9 22
|
zsubcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) |
31 |
|
2cnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∈ ℂ ) |
32 |
31 10
|
expp1d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ ( 𝑥 + 1 ) ) = ( ( 2 ↑ 𝑥 ) · 2 ) ) |
33 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
34 |
33
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 1 ∈ ℕ0 ) |
35 |
10 34
|
nn0addcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ∈ ℕ0 ) |
36 |
35
|
nn0zd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ∈ ℤ ) |
37 |
|
simplr |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 ) |
38 |
37
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℕ0 ) |
39 |
38
|
nn0zd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ ) |
40 |
|
nn0ltp1le |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) ) |
41 |
10 38 40
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 < 𝑀 ↔ ( 𝑥 + 1 ) ≤ 𝑀 ) ) |
42 |
13 41
|
mpbid |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑥 + 1 ) ≤ 𝑀 ) |
43 |
|
eluz2 |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) ↔ ( ( 𝑥 + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑥 + 1 ) ≤ 𝑀 ) ) |
44 |
36 39 42 43
|
syl3anbrc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) ) |
45 |
|
dvdsexp |
⊢ ( ( 2 ∈ ℤ ∧ ( 𝑥 + 1 ) ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑥 + 1 ) ) ) → ( 2 ↑ ( 𝑥 + 1 ) ) ∥ ( 2 ↑ 𝑀 ) ) |
46 |
16 35 44 45
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ ( 𝑥 + 1 ) ) ∥ ( 2 ↑ 𝑀 ) ) |
47 |
32 46
|
eqbrtrrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( 2 ↑ 𝑀 ) ) |
48 |
28
|
nnrpd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ ) |
49 |
|
moddifz |
⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) |
50 |
17 48 49
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) |
51 |
|
2ne0 |
⊢ 2 ≠ 0 |
52 |
51
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ≠ 0 ) |
53 |
31 52 39
|
expne0d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ≠ 0 ) |
54 |
|
dvdsval2 |
⊢ ( ( ( 2 ↑ 𝑀 ) ∈ ℤ ∧ ( 2 ↑ 𝑀 ) ≠ 0 ∧ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) ) |
55 |
29 53 30 54
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑀 ) ) ∈ ℤ ) ) |
56 |
50 55
|
mpbird |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) |
57 |
27 29 30 47 56
|
dvdstrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) |
58 |
30
|
zcnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℂ ) |
59 |
19
|
nncnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℂ ) |
60 |
10
|
nn0zd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℤ ) |
61 |
31 52 60
|
expne0d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ≠ 0 ) |
62 |
58 59 61
|
divcan2d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) = ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) |
63 |
57 62
|
breqtrrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
64 |
10
|
nn0red |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ∈ ℝ ) |
65 |
38
|
nn0red |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ℝ ) |
66 |
64 65 13
|
ltled |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑥 ≤ 𝑀 ) |
67 |
|
eluz2 |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ≤ 𝑀 ) ) |
68 |
60 39 66 67
|
syl3anbrc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑥 ) ) |
69 |
|
dvdsexp |
⊢ ( ( 2 ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑥 ) ) → ( 2 ↑ 𝑥 ) ∥ ( 2 ↑ 𝑀 ) ) |
70 |
16 10 68 69
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∥ ( 2 ↑ 𝑀 ) ) |
71 |
26 29 30 70 56
|
dvdstrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) |
72 |
|
dvdsval2 |
⊢ ( ( ( 2 ↑ 𝑥 ) ∈ ℤ ∧ ( 2 ↑ 𝑥 ) ≠ 0 ∧ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) ) |
73 |
26 61 30 72
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) ∥ ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) ) |
74 |
71 73
|
mpbid |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) |
75 |
|
dvdscmulr |
⊢ ( ( 2 ∈ ℤ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ∧ ( ( 2 ↑ 𝑥 ) ∈ ℤ ∧ ( 2 ↑ 𝑥 ) ≠ 0 ) ) → ( ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
76 |
16 74 26 61 75
|
syl112anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 2 ↑ 𝑥 ) · 2 ) ∥ ( ( 2 ↑ 𝑥 ) · ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
77 |
63 76
|
mpbid |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∥ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) |
78 |
25
|
zcnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℂ ) |
79 |
74
|
zcnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℂ ) |
80 |
22
|
zcnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℂ ) |
81 |
9
|
zcnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 𝑁 ∈ ℂ ) |
82 |
80 81
|
pncan3d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) = 𝑁 ) |
83 |
82
|
oveq1d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑥 ) ) = ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) |
84 |
80 58 59 61
|
divdird |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) + ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ) / ( 2 ↑ 𝑥 ) ) = ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
85 |
83 84
|
eqtr3d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 𝑁 / ( 2 ↑ 𝑥 ) ) = ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
86 |
85
|
fveq2d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) = ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
87 |
|
fladdz |
⊢ ( ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ∧ ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℤ ) → ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
88 |
24 74 87
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
89 |
86 88
|
eqtrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) = ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) + ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
90 |
78 79 89
|
mvrladdd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) = ( ( 𝑁 − ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) / ( 2 ↑ 𝑥 ) ) ) |
91 |
77 90
|
breqtrrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → 2 ∥ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
92 |
|
dvdssub2 |
⊢ ( ( ( 2 ∈ ℤ ∧ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ∈ ℤ ) ∧ 2 ∥ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) − ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
93 |
16 21 25 91 92
|
syl31anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
94 |
93
|
notbid |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑥 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
95 |
12 14 94
|
3bitr3d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑥 < 𝑀 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
96 |
|
z0even |
⊢ 2 ∥ 0 |
97 |
1
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℤ ) |
98 |
97
|
zred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑁 ∈ ℝ ) |
99 |
|
2rp |
⊢ 2 ∈ ℝ+ |
100 |
99
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∈ ℝ+ ) |
101 |
37
|
nn0zd |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑀 ∈ ℤ ) |
102 |
101
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℤ ) |
103 |
100 102
|
rpexpcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ+ ) |
104 |
98 103
|
modcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℝ ) |
105 |
|
simplr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℕ0 ) |
106 |
105
|
nn0zd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℤ ) |
107 |
100 106
|
rpexpcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℝ+ ) |
108 |
6
|
ad2antrr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℕ0 ) |
109 |
108
|
nn0ge0d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 0 ≤ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) |
110 |
104 107 109
|
divge0d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) |
111 |
103
|
rpred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ∈ ℝ ) |
112 |
107
|
rpred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℝ ) |
113 |
|
modlt |
⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ 𝑀 ) ∈ ℝ+ ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) ) |
114 |
98 103 113
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑀 ) ) |
115 |
100
|
rpred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∈ ℝ ) |
116 |
|
1le2 |
⊢ 1 ≤ 2 |
117 |
116
|
a1i |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 1 ≤ 2 ) |
118 |
102
|
zred |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ∈ ℝ ) |
119 |
105
|
nn0red |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ℝ ) |
120 |
|
simpr |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ¬ 𝑥 < 𝑀 ) |
121 |
118 119 120
|
nltled |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑀 ≤ 𝑥 ) |
122 |
|
eluz2 |
⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥 ) ) |
123 |
102 106 121 122
|
syl3anbrc |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
124 |
115 117 123
|
leexp2ad |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑀 ) ≤ ( 2 ↑ 𝑥 ) ) |
125 |
104 111 112 114 124
|
ltletrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( 2 ↑ 𝑥 ) ) |
126 |
107
|
rpcnd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ↑ 𝑥 ) ∈ ℂ ) |
127 |
126
|
mulid1d |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 2 ↑ 𝑥 ) · 1 ) = ( 2 ↑ 𝑥 ) ) |
128 |
125 127
|
breqtrrd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( ( 2 ↑ 𝑥 ) · 1 ) ) |
129 |
|
1red |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 1 ∈ ℝ ) |
130 |
104 129 107
|
ltdivmuld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < 1 ↔ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) < ( ( 2 ↑ 𝑥 ) · 1 ) ) ) |
131 |
128 130
|
mpbird |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < 1 ) |
132 |
|
1e0p1 |
⊢ 1 = ( 0 + 1 ) |
133 |
131 132
|
breqtrdi |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) |
134 |
104 107
|
rerpdivcld |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ) |
135 |
|
0z |
⊢ 0 ∈ ℤ |
136 |
|
flbi |
⊢ ( ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ↔ ( 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∧ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) ) ) |
137 |
134 135 136
|
sylancl |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ↔ ( 0 ≤ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ∧ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) < ( 0 + 1 ) ) ) ) |
138 |
110 133 137
|
mpbir2and |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) = 0 ) |
139 |
96 138
|
breqtrrid |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) |
140 |
120
|
intnand |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ¬ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) |
141 |
139 140
|
2thd |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ¬ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) |
142 |
141
|
con2bid |
⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) ∧ ¬ 𝑥 < 𝑀 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
143 |
95 142
|
pm2.61dan |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
144 |
101
|
biantrurd |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) ) |
145 |
143 144
|
bitr3d |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ) ) |
146 |
|
an12 |
⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 < 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) |
147 |
145 146
|
bitrdi |
⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) |
148 |
147
|
pm5.32da |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) ) |
149 |
8 148
|
bitr3d |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) ) |
150 |
|
3anass |
⊢ ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ ( 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) ) |
151 |
|
elfzo2 |
⊢ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) |
152 |
|
elnn0uz |
⊢ ( 𝑥 ∈ ℕ0 ↔ 𝑥 ∈ ( ℤ≥ ‘ 0 ) ) |
153 |
152
|
3anbi1i |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) |
154 |
|
3anass |
⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) |
155 |
151 153 154
|
3bitr2i |
⊢ ( 𝑥 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) |
156 |
155
|
anbi2i |
⊢ ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) |
157 |
|
an12 |
⊢ ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑥 ∈ ℕ0 ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) |
158 |
156 157
|
bitri |
⊢ ( ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ℕ0 ∧ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑥 < 𝑀 ) ) ) ) |
159 |
149 150 158
|
3bitr4g |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ) ) |
160 |
|
bitsval |
⊢ ( 𝑥 ∈ ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ∈ ℤ ∧ 𝑥 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝑁 mod ( 2 ↑ 𝑀 ) ) / ( 2 ↑ 𝑥 ) ) ) ) ) |
161 |
|
elin |
⊢ ( 𝑥 ∈ ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ↔ ( 𝑥 ∈ ( bits ‘ 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑀 ) ) ) |
162 |
159 160 161
|
3bitr4g |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 ∈ ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) ↔ 𝑥 ∈ ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ) ) |
163 |
162
|
eqrdv |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( 𝑁 mod ( 2 ↑ 𝑀 ) ) ) = ( ( bits ‘ 𝑁 ) ∩ ( 0 ..^ 𝑀 ) ) ) |