Metamath Proof Explorer

Theorem fzen2

Description: The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Mario Carneiro, 13-Feb-2014)

Ref Expression
Hypothesis fzennn.1 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
Assertion fzen2 
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) )

Proof

Step Hyp Ref Expression
1 fzennn.1 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
3 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
4 1z 
 |-  1 e. ZZ
5 zsubcl 
 |-  ( ( 1 e. ZZ /\ M e. ZZ ) -> ( 1 - M ) e. ZZ )
6 4 2 5 sylancr 
 |-  ( N e. ( ZZ>= ` M ) -> ( 1 - M ) e. ZZ )
7 fzen 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( 1 - M ) e. ZZ ) -> ( M ... N ) ~~ ( ( M + ( 1 - M ) ) ... ( N + ( 1 - M ) ) ) )
8 2 3 6 7 syl3anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) ~~ ( ( M + ( 1 - M ) ) ... ( N + ( 1 - M ) ) ) )
9 2 zcnd 
 |-  ( N e. ( ZZ>= ` M ) -> M e. CC )
10 ax-1cn 
 |-  1 e. CC
11 pncan3 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( M + ( 1 - M ) ) = 1 )
12 9 10 11 sylancl 
 |-  ( N e. ( ZZ>= ` M ) -> ( M + ( 1 - M ) ) = 1 )
13 zcn 
 |-  ( N e. ZZ -> N e. CC )
14 zcn 
 |-  ( M e. ZZ -> M e. CC )
15 addsubass 
 |-  ( ( N e. CC /\ 1 e. CC /\ M e. CC ) -> ( ( N + 1 ) - M ) = ( N + ( 1 - M ) ) )
16 10 15 mp3an2 
 |-  ( ( N e. CC /\ M e. CC ) -> ( ( N + 1 ) - M ) = ( N + ( 1 - M ) ) )
17 13 14 16 syl2an 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N + 1 ) - M ) = ( N + ( 1 - M ) ) )
18 3 2 17 syl2anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N + 1 ) - M ) = ( N + ( 1 - M ) ) )
19 18 eqcomd 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + ( 1 - M ) ) = ( ( N + 1 ) - M ) )
20 12 19 oveq12d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M + ( 1 - M ) ) ... ( N + ( 1 - M ) ) ) = ( 1 ... ( ( N + 1 ) - M ) ) )
21 8 20 breqtrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) ~~ ( 1 ... ( ( N + 1 ) - M ) ) )
22 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
23 uznn0sub 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( ( N + 1 ) - M ) e. NN0 )
24 1 fzennn 
 |-  ( ( ( N + 1 ) - M ) e. NN0 -> ( 1 ... ( ( N + 1 ) - M ) ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) )
25 22 23 24 3syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( 1 ... ( ( N + 1 ) - M ) ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) )
26 entr 
 |-  ( ( ( M ... N ) ~~ ( 1 ... ( ( N + 1 ) - M ) ) /\ ( 1 ... ( ( N + 1 ) - M ) ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) ) -> ( M ... N ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) )
27 21 25 26 syl2anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) )