Metamath Proof Explorer

Theorem peano2fzor

Description: A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion peano2fzor ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → K ∈ M ..^ N

Proof

Step Hyp Ref Expression
1 simpr ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → K + 1 ∈ M ..^ N
2 elfzoel2 ⊢ K + 1 ∈ M ..^ N → N ∈ ℤ
3 2 adantl ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → N ∈ ℤ
4 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
5 3 4 syl ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → M ..^ N = M … N − 1
6 1 5 eleqtrd ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → K + 1 ∈ M … N − 1
7 peano2fzr ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M … N − 1 → K ∈ M … N − 1
8 6 7 syldan ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → K ∈ M … N − 1
9 8 5 eleqtrrd ⊢ K ∈ ℤ ≥ M ∧ K + 1 ∈ M ..^ N → K ∈ M ..^ N