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<2m
7 1 3 5 6 syl3anc ⊢N∈ℕ0→∃m∈ℕN<2m
8 fzofi ⊢0..^m∈Fin
9 simpl ⊢N∈ℕ0∧m∈ℕ∧N<2m→N∈ℕ0
10 nn0uz ⊢ℕ0=ℤ≥0
11 9 10 eleqtrdi ⊢N∈ℕ0∧m∈ℕ∧N<2m→N∈ℤ≥0
12 2nn ⊢2∈ℕ
13 12 a1i ⊢N∈ℕ0∧m∈ℕ∧N<2m→2∈ℕ
14 simprl ⊢N∈ℕ0∧m∈ℕ∧N<2m→m∈ℕ
15 14 nnnn0d ⊢N∈ℕ0∧m∈ℕ∧N<2m→m∈ℕ0
16 13 15 nnexpcld ⊢N∈ℕ0∧m∈ℕ∧N<2m→2m∈ℕ
17 16 nnzd ⊢N∈ℕ0∧m∈ℕ∧N<2m→2m∈ℤ
18 simprr ⊢N∈ℕ0∧m∈ℕ∧N<2m→N<2m
19 elfzo2 ⊢N∈0..^2m↔N∈ℤ≥0∧2m∈ℤ∧N<2m
20 11 17 18 19 syl3anbrc ⊢N∈ℕ0∧m∈ℕ∧N<2m→N∈0..^2m
21 9 nn0zd ⊢N∈ℕ0∧m∈ℕ∧N<2m→N∈ℤ
22 bitsfzo ⊢N∈ℤ∧m∈ℕ0→N∈0..^2m↔bits⁡N⊆0..^m
23 21 15 22 syl2anc ⊢N∈ℕ0∧m∈ℕ∧N<2m→N∈0..^2m↔bits⁡N⊆0..^m
24 20 23 mpbid ⊢N∈ℕ0∧m∈ℕ∧N<2m→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<2m→bits⁡N∈Fin
27 7 26 rexlimddv ⊢N∈ℕ0→bits⁡N∈Fin