Metamath Proof Explorer

Theorem fzofzp1b

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion fzofzp1b 
|- ( C e. ( ZZ>= ` A ) -> ( C e. ( A ..^ B ) <-> ( C + 1 ) e. ( A ... B ) ) )

Proof

Step Hyp Ref Expression
1 fzofzp1 
 |-  ( C e. ( A ..^ B ) -> ( C + 1 ) e. ( A ... B ) )
2 simpl 
 |-  ( ( C e. ( ZZ>= ` A ) /\ ( C + 1 ) e. ( A ... B ) ) -> C e. ( ZZ>= ` A ) )
3 eluzelz 
 |-  ( C e. ( ZZ>= ` A ) -> C e. ZZ )
4 elfzuz3 
 |-  ( ( C + 1 ) e. ( A ... B ) -> B e. ( ZZ>= ` ( C + 1 ) ) )
5 eluzp1m1 
 |-  ( ( C e. ZZ /\ B e. ( ZZ>= ` ( C + 1 ) ) ) -> ( B - 1 ) e. ( ZZ>= ` C ) )
6 3 4 5 syl2an 
 |-  ( ( C e. ( ZZ>= ` A ) /\ ( C + 1 ) e. ( A ... B ) ) -> ( B - 1 ) e. ( ZZ>= ` C ) )
7 elfzuzb 
 |-  ( C e. ( A ... ( B - 1 ) ) <-> ( C e. ( ZZ>= ` A ) /\ ( B - 1 ) e. ( ZZ>= ` C ) ) )
8 2 6 7 sylanbrc 
 |-  ( ( C e. ( ZZ>= ` A ) /\ ( C + 1 ) e. ( A ... B ) ) -> C e. ( A ... ( B - 1 ) ) )
9 elfzel2 
 |-  ( ( C + 1 ) e. ( A ... B ) -> B e. ZZ )
10 9 adantl 
 |-  ( ( C e. ( ZZ>= ` A ) /\ ( C + 1 ) e. ( A ... B ) ) -> B e. ZZ )
11 fzoval 
 |-  ( B e. ZZ -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
12 10 11 syl 
 |-  ( ( C e. ( ZZ>= ` A ) /\ ( C + 1 ) e. ( A ... B ) ) -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
13 8 12 eleqtrrd 
 |-  ( ( C e. ( ZZ>= ` A ) /\ ( C + 1 ) e. ( A ... B ) ) -> C e. ( A ..^ B ) )
14 13 ex 
 |-  ( C e. ( ZZ>= ` A ) -> ( ( C + 1 ) e. ( A ... B ) -> C e. ( A ..^ B ) ) )
15 1 14 impbid2 
 |-  ( C e. ( ZZ>= ` A ) -> ( C e. ( A ..^ B ) <-> ( C + 1 ) e. ( A ... B ) ) )