This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )