Metamath Proof Explorer

Theorem bitsfi

Description: Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsfi ⊢ N ∈ ℕ 0 → bits ⁡ N ∈ Fin

Proof

Step Hyp Ref Expression
1 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
2 2re ⊢ 2 ∈ ℝ
3 2 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ
4 1lt2 ⊢ 1 < 2
5 4 a1i ⊢ N ∈ ℕ 0 → 1 < 2
6 expnbnd ⊢ N ∈ ℝ ∧ 2 ∈ ℝ ∧ 1 < 2 → ∃ m ∈ ℕ N < 2 m
7 1 3 5 6 syl3anc ⊢ N ∈ ℕ 0 → ∃ m ∈ ℕ N < 2 m
8 fzofi ⊢ 0 ..^ m ∈ Fin
9 simpl ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → N ∈ ℕ 0
10 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
11 9 10 eleqtrdi ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → N ∈ ℤ ≥ 0
12 2nn ⊢ 2 ∈ ℕ
13 12 a1i ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → 2 ∈ ℕ
14 simprl ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → m ∈ ℕ
15 14 nnnn0d ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → m ∈ ℕ 0
16 13 15 nnexpcld ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → 2 m ∈ ℕ
17 16 nnzd ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → 2 m ∈ ℤ
18 simprr ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → N < 2 m
19 elfzo2 ⊢ N ∈ 0 ..^ 2 m ↔ N ∈ ℤ ≥ 0 ∧ 2 m ∈ ℤ ∧ N < 2 m
20 11 17 18 19 syl3anbrc ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → N ∈ 0 ..^ 2 m
21 9 nn0zd ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → N ∈ ℤ
22 bitsfzo ⊢ N ∈ ℤ ∧ m ∈ ℕ 0 → N ∈ 0 ..^ 2 m ↔ bits ⁡ N ⊆ 0 ..^ m
23 21 15 22 syl2anc ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → N ∈ 0 ..^ 2 m ↔ bits ⁡ N ⊆ 0 ..^ m
24 20 23 mpbid ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → bits ⁡ N ⊆ 0 ..^ m
25 ssfi ⊢ 0 ..^ m ∈ Fin ∧ bits ⁡ N ⊆ 0 ..^ m → bits ⁡ N ∈ Fin
26 8 24 25 sylancr ⊢ N ∈ ℕ 0 ∧ m ∈ ℕ ∧ N < 2 m → bits ⁡ N ∈ Fin
27 7 26 rexlimddv ⊢ N ∈ ℕ 0 → bits ⁡ N ∈ Fin