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

Metamath Proof Explorer

Theorem fzofzp1

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzofzp1 
|- ( C e. ( A ..^ B ) -> ( C + 1 ) e. ( A ... B ) )

Proof

Step Hyp Ref Expression
1 elfzoel1 
 |-  ( C e. ( A ..^ B ) -> A e. ZZ )
2 uzid 
 |-  ( A e. ZZ -> A e. ( ZZ>= ` A ) )
3 peano2uz 
 |-  ( A e. ( ZZ>= ` A ) -> ( A + 1 ) e. ( ZZ>= ` A ) )
4 fzoss1 
 |-  ( ( A + 1 ) e. ( ZZ>= ` A ) -> ( ( A + 1 ) ..^ ( B + 1 ) ) C_ ( A ..^ ( B + 1 ) ) )
5 1 2 3 4 4syl 
 |-  ( C e. ( A ..^ B ) -> ( ( A + 1 ) ..^ ( B + 1 ) ) C_ ( A ..^ ( B + 1 ) ) )
6 1z 
 |-  1 e. ZZ
7 fzoaddel 
 |-  ( ( C e. ( A ..^ B ) /\ 1 e. ZZ ) -> ( C + 1 ) e. ( ( A + 1 ) ..^ ( B + 1 ) ) )
8 6 7 mpan2 
 |-  ( C e. ( A ..^ B ) -> ( C + 1 ) e. ( ( A + 1 ) ..^ ( B + 1 ) ) )
9 5 8 sseldd 
 |-  ( C e. ( A ..^ B ) -> ( C + 1 ) e. ( A ..^ ( B + 1 ) ) )
10 elfzoel2 
 |-  ( C e. ( A ..^ B ) -> B e. ZZ )
11 fzval3 
 |-  ( B e. ZZ -> ( A ... B ) = ( A ..^ ( B + 1 ) ) )
12 10 11 syl 
 |-  ( C e. ( A ..^ B ) -> ( A ... B ) = ( A ..^ ( B + 1 ) ) )
13 9 12 eleqtrrd 
 |-  ( C e. ( A ..^ B ) -> ( C + 1 ) e. ( A ... B ) )