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 V x + 1 0 ω
Assertion fzen2 N M M N G -1 N + 1 - M

Proof

Step Hyp Ref Expression
1 fzennn.1 G = rec x V x + 1 0 ω
2 eluzel2 N M M
3 eluzelz N M N
4 1z 1
5 zsubcl 1 M 1 M
6 4 2 5 sylancr N M 1 M
7 fzen M N 1 M M N M + 1 - M N + 1 - M
8 2 3 6 7 syl3anc N M M N M + 1 - M N + 1 - M
9 2 zcnd N M M
10 ax-1cn 1
11 pncan3 M 1 M + 1 - M = 1
12 9 10 11 sylancl N M M + 1 - M = 1
13 zcn N N
14 zcn M M
15 addsubass N 1 M N + 1 - M = N + 1 - M
16 10 15 mp3an2 N M N + 1 - M = N + 1 - M
17 13 14 16 syl2an N M N + 1 - M = N + 1 - M
18 3 2 17 syl2anc N M N + 1 - M = N + 1 - M
19 18 eqcomd N M N + 1 - M = N + 1 - M
20 12 19 oveq12d N M M + 1 - M N + 1 - M = 1 N + 1 - M
21 8 20 breqtrd N M M N 1 N + 1 - M
22 peano2uz N M N + 1 M
23 uznn0sub N + 1 M N + 1 - M 0
24 1 fzennn N + 1 - M 0 1 N + 1 - M G -1 N + 1 - M
25 22 23 24 3syl N M 1 N + 1 - M G -1 N + 1 - M
26 entr M N 1 N + 1 - M 1 N + 1 - M G -1 N + 1 - M M N G -1 N + 1 - M
27 21 25 26 syl2anc N M M N G -1 N + 1 - M