Natural_Numbers_are_Non_Negative_Integers
Provedintegersnatural-numbersnatural-numbers-are-non-negative-integersproofwiki
Let . Then That is, the natural numbers are precisely those integers which are greater than or equal to zero.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Natural_Numbers_are_Non_Negative_Integers (m : ℤ) : m ∈ Set.range (Int.ofNat) ↔ 0 ≤ m := by sorry
Source