Nat.evenOddRec.proof_1
theorem Nat.evenOddRec.proof_1 : ∀ (i : ℕ), 2 * i = bit0 i
This theorem states that for any natural number `i`, multiplying `i` by 2 is the same as applying the `bit0` function to `i`. The `bit0` function takes a number and adds it to itself, which is the definition of multiplication by two. Therefore, it is true for all natural numbers `i` that `2 * i` is equivalent to `bit0 i`.
More concisely: For all natural numbers `i`, `2 * i` is equivalent to `bit0 i`. In other words, multiplying a natural number by 2 is the same as applying the `bit0` function.
|
Nat.evenOddRec.proof_2
theorem Nat.evenOddRec.proof_2 : ∀ (i : ℕ), 2 * i + 1 = bit1 i
This theorem states that for every natural number `i`, the result of multiplying `i` by 2 and then adding 1 is equal to the application of the `bit1` function to `i`. In other words, the value of `2*i + 1` and `bit1 i` are the same for any natural number `i`. The `bit1` function in this context effectively doubles its input and then adds one, which mirrors the operation on the left side of the equation.
More concisely: For all natural numbers `i`, `2 * i + 1` equals `bit1 i`.
|