# Metamath Proof Explorer

## Theorem bitsfzo

Description: The bits of a number are all less than M iff the number is nonnegative and less than 2 ^ M . (Contributed by Mario Carneiro, 5-Sep-2016) (Proof shortened by AV, 1-Oct-2020)

Ref Expression
Assertion bitsfzo ${⊢}\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to \left({N}\in \left(0..^{2}^{{M}}\right)↔\mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)$

### Proof

Step Hyp Ref Expression
1 bitsval ${⊢}{m}\in \mathrm{bits}\left({N}\right)↔\left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)$
2 simp32 ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {m}\in {ℕ}_{0}$
3 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
4 2 3 eleqtrdi ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {m}\in {ℤ}_{\ge 0}$
5 simp1r ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {M}\in {ℕ}_{0}$
6 5 nn0zd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {M}\in ℤ$
7 2re ${⊢}2\in ℝ$
8 7 a1i ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 2\in ℝ$
9 8 2 reexpcld ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {2}^{{m}}\in ℝ$
10 simp1l ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {N}\in ℤ$
11 10 zred ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {N}\in ℝ$
12 8 5 reexpcld ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {2}^{{M}}\in ℝ$
13 9 recnd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {2}^{{m}}\in ℂ$
14 13 mulid2d ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 1{2}^{{m}}={2}^{{m}}$
15 simp33 ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋$
16 2rp ${⊢}2\in {ℝ}^{+}$
17 16 a1i ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 2\in {ℝ}^{+}$
18 2 nn0zd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {m}\in ℤ$
19 17 18 rpexpcld ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {2}^{{m}}\in {ℝ}^{+}$
20 11 19 rerpdivcld ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \frac{{N}}{{2}^{{m}}}\in ℝ$
21 1red ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 1\in ℝ$
22 20 21 ltnled ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(\frac{{N}}{{2}^{{m}}}<1↔¬1\le \frac{{N}}{{2}^{{m}}}\right)$
23 0p1e1 ${⊢}0+1=1$
24 23 breq2i ${⊢}\frac{{N}}{{2}^{{m}}}<0+1↔\frac{{N}}{{2}^{{m}}}<1$
25 elfzole1 ${⊢}{N}\in \left(0..^{2}^{{M}}\right)\to 0\le {N}$
26 25 3ad2ant2 ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 0\le {N}$
27 11 19 26 divge0d ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 0\le \frac{{N}}{{2}^{{m}}}$
28 0z ${⊢}0\in ℤ$
29 flbi ${⊢}\left(\frac{{N}}{{2}^{{m}}}\in ℝ\wedge 0\in ℤ\right)\to \left(⌊\frac{{N}}{{2}^{{m}}}⌋=0↔\left(0\le \frac{{N}}{{2}^{{m}}}\wedge \frac{{N}}{{2}^{{m}}}<0+1\right)\right)$
30 20 28 29 sylancl ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(⌊\frac{{N}}{{2}^{{m}}}⌋=0↔\left(0\le \frac{{N}}{{2}^{{m}}}\wedge \frac{{N}}{{2}^{{m}}}<0+1\right)\right)$
31 z0even ${⊢}2\parallel 0$
32 id ${⊢}⌊\frac{{N}}{{2}^{{m}}}⌋=0\to ⌊\frac{{N}}{{2}^{{m}}}⌋=0$
33 31 32 breqtrrid ${⊢}⌊\frac{{N}}{{2}^{{m}}}⌋=0\to 2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋$
34 30 33 syl6bir ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(\left(0\le \frac{{N}}{{2}^{{m}}}\wedge \frac{{N}}{{2}^{{m}}}<0+1\right)\to 2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)$
35 27 34 mpand ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(\frac{{N}}{{2}^{{m}}}<0+1\to 2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)$
36 24 35 syl5bir ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(\frac{{N}}{{2}^{{m}}}<1\to 2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)$
37 22 36 sylbird ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(¬1\le \frac{{N}}{{2}^{{m}}}\to 2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)$
38 15 37 mt3d ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 1\le \frac{{N}}{{2}^{{m}}}$
39 21 11 19 lemuldivd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left(1{2}^{{m}}\le {N}↔1\le \frac{{N}}{{2}^{{m}}}\right)$
40 38 39 mpbird ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 1{2}^{{m}}\le {N}$
41 14 40 eqbrtrrd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {2}^{{m}}\le {N}$
42 elfzolt2 ${⊢}{N}\in \left(0..^{2}^{{M}}\right)\to {N}<{2}^{{M}}$
43 42 3ad2ant2 ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {N}<{2}^{{M}}$
44 9 11 12 41 43 lelttrd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {2}^{{m}}<{2}^{{M}}$
45 1lt2 ${⊢}1<2$
46 45 a1i ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to 1<2$
47 8 18 6 46 ltexp2d ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to \left({m}<{M}↔{2}^{{m}}<{2}^{{M}}\right)$
48 44 47 mpbird ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {m}<{M}$
49 elfzo2 ${⊢}{m}\in \left(0..^{M}\right)↔\left({m}\in {ℤ}_{\ge 0}\wedge {M}\in ℤ\wedge {m}<{M}\right)$
50 4 6 48 49 syl3anbrc ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\wedge \left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\right)\to {m}\in \left(0..^{M}\right)$
51 50 3expia ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\right)\to \left(\left({N}\in ℤ\wedge {m}\in {ℕ}_{0}\wedge ¬2\parallel ⌊\frac{{N}}{{2}^{{m}}}⌋\right)\to {m}\in \left(0..^{M}\right)\right)$
52 1 51 syl5bi ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\right)\to \left({m}\in \mathrm{bits}\left({N}\right)\to {m}\in \left(0..^{M}\right)\right)$
53 52 ssrdv ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge {N}\in \left(0..^{2}^{{M}}\right)\right)\to \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)$
54 simpr ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -{N}\in ℕ$
55 54 nnred ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -{N}\in ℝ$
56 simpllr ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {M}\in {ℕ}_{0}$
57 56 nn0red ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {M}\in ℝ$
58 max2 ${⊢}\left(-{N}\in ℝ\wedge {M}\in ℝ\right)\to {M}\le if\left(-{N}\le {M},{M},-{N}\right)$
59 55 57 58 syl2anc ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {M}\le if\left(-{N}\le {M},{M},-{N}\right)$
60 simplr ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)$
61 n2dvdsm1 ${⊢}¬2\parallel -1$
62 simplll ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {N}\in ℤ$
63 62 zred ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {N}\in ℝ$
64 2nn ${⊢}2\in ℕ$
65 64 a1i ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 2\in ℕ$
66 54 nnnn0d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -{N}\in {ℕ}_{0}$
67 56 66 ifcld ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)\in {ℕ}_{0}$
68 65 67 nnexpcld ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\in ℕ$
69 63 68 nndivred ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\in ℝ$
70 1red ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 1\in ℝ$
71 62 zcnd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {N}\in ℂ$
72 68 nncnd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\in ℂ$
73 2cnd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 2\in ℂ$
74 2ne0 ${⊢}2\ne 0$
75 74 a1i ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 2\ne 0$
76 67 nn0zd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)\in ℤ$
77 73 75 76 expne0d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\ne 0$
78 71 72 77 divnegd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}=\frac{-{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}$
79 67 nn0red ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)\in ℝ$
80 68 nnred ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\in ℝ$
81 max1 ${⊢}\left(-{N}\in ℝ\wedge {M}\in ℝ\right)\to -{N}\le if\left(-{N}\le {M},{M},-{N}\right)$
82 55 57 81 syl2anc ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -{N}\le if\left(-{N}\le {M},{M},-{N}\right)$
83 2z ${⊢}2\in ℤ$
84 uzid ${⊢}2\in ℤ\to 2\in {ℤ}_{\ge 2}$
85 83 84 ax-mp ${⊢}2\in {ℤ}_{\ge 2}$
86 bernneq3 ${⊢}\left(2\in {ℤ}_{\ge 2}\wedge if\left(-{N}\le {M},{M},-{N}\right)\in {ℕ}_{0}\right)\to if\left(-{N}\le {M},{M},-{N}\right)<{2}^{if\left(-{N}\le {M},{M},-{N}\right)}$
87 85 67 86 sylancr ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)<{2}^{if\left(-{N}\le {M},{M},-{N}\right)}$
88 79 80 87 ltled ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)\le {2}^{if\left(-{N}\le {M},{M},-{N}\right)}$
89 55 79 80 82 88 letrd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -{N}\le {2}^{if\left(-{N}\le {M},{M},-{N}\right)}$
90 72 mulid1d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\cdot 1={2}^{if\left(-{N}\le {M},{M},-{N}\right)}$
91 89 90 breqtrrd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -{N}\le {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\cdot 1$
92 68 nnrpd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\in {ℝ}^{+}$
93 55 70 92 ledivmuld ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \left(\frac{-{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\le 1↔-{N}\le {2}^{if\left(-{N}\le {M},{M},-{N}\right)}\cdot 1\right)$
94 91 93 mpbird ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \frac{-{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\le 1$
95 78 94 eqbrtrd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\le 1$
96 69 70 95 lenegcon1d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to -1\le \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}$
97 54 nngt0d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 0<-{N}$
98 68 nngt0d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 0<{2}^{if\left(-{N}\le {M},{M},-{N}\right)}$
99 55 80 97 98 divgt0d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 0<\frac{-{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}$
100 99 78 breqtrrd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to 0<-\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}$
101 69 lt0neg1d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \left(\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}<0↔0<-\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\right)$
102 100 101 mpbird ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}<0$
103 ax-1cn ${⊢}1\in ℂ$
104 neg1cn ${⊢}-1\in ℂ$
105 1pneg1e0 ${⊢}1+-1=0$
106 103 104 105 addcomli ${⊢}-1+1=0$
107 102 106 breqtrrdi ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}<-1+1$
108 neg1z ${⊢}-1\in ℤ$
109 flbi ${⊢}\left(\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\in ℝ\wedge -1\in ℤ\right)\to \left(⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋=-1↔\left(-1\le \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\wedge \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}<-1+1\right)\right)$
110 69 108 109 sylancl ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \left(⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋=-1↔\left(-1\le \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}\wedge \frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}<-1+1\right)\right)$
111 96 107 110 mpbir2and ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to ⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋=-1$
112 111 breq2d ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \left(2\parallel ⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋↔2\parallel -1\right)$
113 61 112 mtbiri ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to ¬2\parallel ⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋$
114 bitsval2 ${⊢}\left({N}\in ℤ\wedge if\left(-{N}\le {M},{M},-{N}\right)\in {ℕ}_{0}\right)\to \left(if\left(-{N}\le {M},{M},-{N}\right)\in \mathrm{bits}\left({N}\right)↔¬2\parallel ⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋\right)$
115 62 67 114 syl2anc ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \left(if\left(-{N}\le {M},{M},-{N}\right)\in \mathrm{bits}\left({N}\right)↔¬2\parallel ⌊\frac{{N}}{{2}^{if\left(-{N}\le {M},{M},-{N}\right)}}⌋\right)$
116 113 115 mpbird ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)\in \mathrm{bits}\left({N}\right)$
117 60 116 sseldd ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)\in \left(0..^{M}\right)$
118 elfzolt2 ${⊢}if\left(-{N}\le {M},{M},-{N}\right)\in \left(0..^{M}\right)\to if\left(-{N}\le {M},{M},-{N}\right)<{M}$
119 117 118 syl ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to if\left(-{N}\le {M},{M},-{N}\right)<{M}$
120 79 57 ltnled ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to \left(if\left(-{N}\le {M},{M},-{N}\right)<{M}↔¬{M}\le if\left(-{N}\le {M},{M},-{N}\right)\right)$
121 119 120 mpbid ${⊢}\left(\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\wedge -{N}\in ℕ\right)\to ¬{M}\le if\left(-{N}\le {M},{M},-{N}\right)$
122 59 121 pm2.65da ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to ¬-{N}\in ℕ$
123 122 intnand ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to ¬\left({N}\in ℝ\wedge -{N}\in ℕ\right)$
124 simpll ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to {N}\in ℤ$
125 elznn0nn ${⊢}{N}\in ℤ↔\left({N}\in {ℕ}_{0}\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$
126 124 125 sylib ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to \left({N}\in {ℕ}_{0}\vee \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$
127 126 ord ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to \left(¬{N}\in {ℕ}_{0}\to \left({N}\in ℝ\wedge -{N}\in ℕ\right)\right)$
128 123 127 mt3d ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to {N}\in {ℕ}_{0}$
129 simplr ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to {M}\in {ℕ}_{0}$
130 simpr ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)$
131 eqid ${⊢}sup\left(\left\{{n}\in {ℕ}_{0}|{N}<{2}^{{n}}\right\},ℝ,<\right)=sup\left(\left\{{n}\in {ℕ}_{0}|{N}<{2}^{{n}}\right\},ℝ,<\right)$
132 128 129 130 131 bitsfzolem ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\wedge \mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)\to {N}\in \left(0..^{2}^{{M}}\right)$
133 53 132 impbida ${⊢}\left({N}\in ℤ\wedge {M}\in {ℕ}_{0}\right)\to \left({N}\in \left(0..^{2}^{{M}}\right)↔\mathrm{bits}\left({N}\right)\subseteq \left(0..^{M}\right)\right)$