Theorem peano2fzr

Description: A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014)

	Ref	Expression
Assertion	peano2fzr	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
3		elfzuz3	⊢ ( ( 𝐾 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
4		peano2uzr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
5	2 3 4	syl2an	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
6		elfzuzb	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
7	1 5 6	sylanbrc	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐾 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )