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

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