# Metamath Proof Explorer

## Theorem 0bits

Description: The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016)

Ref Expression
Assertion 0bits ${⊢}\mathrm{bits}\left(0\right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 c0ex ${⊢}0\in \mathrm{V}$
2 1 snid ${⊢}0\in \left\{0\right\}$
3 fzo01 ${⊢}\left(0..^1\right)=\left\{0\right\}$
4 2 3 eleqtrri ${⊢}0\in \left(0..^1\right)$
5 2cn ${⊢}2\in ℂ$
6 exp0 ${⊢}2\in ℂ\to {2}^{0}=1$
7 5 6 ax-mp ${⊢}{2}^{0}=1$
8 7 oveq2i ${⊢}\left(0..^{2}^{0}\right)=\left(0..^1\right)$
9 4 8 eleqtrri ${⊢}0\in \left(0..^{2}^{0}\right)$
10 0z ${⊢}0\in ℤ$
11 0nn0 ${⊢}0\in {ℕ}_{0}$
12 bitsfzo ${⊢}\left(0\in ℤ\wedge 0\in {ℕ}_{0}\right)\to \left(0\in \left(0..^{2}^{0}\right)↔\mathrm{bits}\left(0\right)\subseteq \left(0..^0\right)\right)$
13 10 11 12 mp2an ${⊢}0\in \left(0..^{2}^{0}\right)↔\mathrm{bits}\left(0\right)\subseteq \left(0..^0\right)$
14 9 13 mpbi ${⊢}\mathrm{bits}\left(0\right)\subseteq \left(0..^0\right)$
15 fzo0 ${⊢}\left(0..^0\right)=\varnothing$
16 14 15 sseqtri ${⊢}\mathrm{bits}\left(0\right)\subseteq \varnothing$
17 0ss ${⊢}\varnothing \subseteq \mathrm{bits}\left(0\right)$
18 16 17 eqssi ${⊢}\mathrm{bits}\left(0\right)=\varnothing$