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 e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> K e. ( M ..^ N ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> ( K + 1 ) e. ( M ..^ N ) )
2 elfzoel2 
 |-  ( ( K + 1 ) e. ( M ..^ N ) -> N e. ZZ )
3 2 adantl 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> N e. ZZ )
4 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
5 3 4 syl 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
6 1 5 eleqtrd 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> ( K + 1 ) e. ( M ... ( N - 1 ) ) )
7 peano2fzr 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ... ( N - 1 ) ) ) -> K e. ( M ... ( N - 1 ) ) )
8 6 7 syldan 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> K e. ( M ... ( N - 1 ) ) )
9 8 5 eleqtrrd 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ..^ N ) ) -> K e. ( M ..^ N ) )