Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002)
Ref | Expression | ||
---|---|---|---|
Assertion | 0nn0 | ⊢ 0 ∈ ℕ_{0} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ 0 = 0 | |
2 | elnn0 | ⊢ ( 0 ∈ ℕ_{0} ↔ ( 0 ∈ ℕ ∨ 0 = 0 ) ) | |
3 | 2 | biimpri | ⊢ ( ( 0 ∈ ℕ ∨ 0 = 0 ) → 0 ∈ ℕ_{0} ) |
4 | 3 | olcs | ⊢ ( 0 = 0 → 0 ∈ ℕ_{0} ) |
5 | 1 4 | ax-mp | ⊢ 0 ∈ ℕ_{0} |