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	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) )
2		elfzoel2	⊢ ( ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
3	2	adantl	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℤ )
4		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
5	3 4	syl	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
6	1 5	eleqtrd	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾 + 1 ) ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
7		peano2fzr	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
8	6 7	syldan	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
9	8 5	eleqtrrd	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) )