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

Metamath Proof Explorer

Theorem fzoend

Description: The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzoend 
|- ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( A ..^ B ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. ( A ..^ B ) -> A e. ( A ..^ B ) )
2 elfzoel2 
 |-  ( A e. ( A ..^ B ) -> B e. ZZ )
3 fzoval 
 |-  ( B e. ZZ -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
4 2 3 syl 
 |-  ( A e. ( A ..^ B ) -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
5 1 4 eleqtrd 
 |-  ( A e. ( A ..^ B ) -> A e. ( A ... ( B - 1 ) ) )
6 elfzuz3 
 |-  ( A e. ( A ... ( B - 1 ) ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
7 5 6 syl 
 |-  ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
8 eluzfz2 
 |-  ( ( B - 1 ) e. ( ZZ>= ` A ) -> ( B - 1 ) e. ( A ... ( B - 1 ) ) )
9 7 8 syl 
 |-  ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( A ... ( B - 1 ) ) )
10 9 4 eleqtrrd 
 |-  ( A e. ( A ..^ B ) -> ( B - 1 ) e. ( A ..^ B ) )