ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Collection of sets
Set union
Successor set
Inductive set
Set of inductive sets
Set of natural numbers
Set of integers
Integer
Integer base-2 representation
N-bit integer
Definition D6267
32-bit integer
Formulation 0
An D995: Integer $a \in \mathbb{Z}$ is a 32-bit integer if and only if \begin{equation} \exists \, r_0, r_1, \ldots, r_{31} \in \{ 0, 1 \} : a = - r_{31} 2^{31} + \sum_{n = 0}^{30} r_n 2^n \end{equation}
Formulation 1
An D995: Integer $a \in \mathbb{Z}$ is a 32-bit integer if and only if \begin{equation} \begin{split} \exists \, r_0, r_1, \ldots, r_{31} \in \{ 0, 1 \} : a & = r_0 + 2 r_1 + 4 r_2 + 8 r_3 + 16 r_4 + 32 r_5 + 64 r_6 + 128 r_7 \\ & \quad + 256 r_8 + 512 r_9 + 1024 r_{10} + 2048 r_{11} + 4096 r_{12} \\ & \quad + 8192 r_{13} + 16384 r_{14} + 32768 r_{15} + 65536 r_{16} \\ & \quad + 131072 r_{17} + 262144 r_{18} + 524288 r_{19} \\ & \quad + 1048576 r_{20} + 2097152 r_{21} + 4194304 r_{22} \\ & \quad + 8388608 r_{23} + 16777216 r_{24} + 33554432 r_{25} \\ & \quad + 67108864 r_{26} + 134217728 r_{27} + 268435456 r_{28} \\ & \quad + 536870912 r_{29} + 1073741824 r_{30} - 2147483648 r_{31} \end{split} \end{equation}