Description: Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | zred.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℤ ) | |
Assertion | peano2zd | ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℤ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zred.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℤ ) | |
2 | peano2z | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 + 1 ) ∈ ℤ ) | |
3 | 1 2 | syl | ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℤ ) |