# 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}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}$
Assertion fzen2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)\approx {{G}}^{-1}\left({N}+1-{M}\right)$

### Proof

Step Hyp Ref Expression
1 fzennn.1 ${⊢}{G}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}$
2 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
3 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
4 1z ${⊢}1\in ℤ$
5 zsubcl ${⊢}\left(1\in ℤ\wedge {M}\in ℤ\right)\to 1-{M}\in ℤ$
6 4 2 5 sylancr ${⊢}{N}\in {ℤ}_{\ge {M}}\to 1-{M}\in ℤ$
7 fzen ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge 1-{M}\in ℤ\right)\to \left({M}\dots {N}\right)\approx \left({M}+1-{M}\dots {N}+1-{M}\right)$
8 2 3 6 7 syl3anc ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)\approx \left({M}+1-{M}\dots {N}+1-{M}\right)$
9 2 zcnd ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℂ$
10 ax-1cn ${⊢}1\in ℂ$
11 pncan3 ${⊢}\left({M}\in ℂ\wedge 1\in ℂ\right)\to {M}+1-{M}=1$
12 9 10 11 sylancl ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}+1-{M}=1$
13 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
14 zcn ${⊢}{M}\in ℤ\to {M}\in ℂ$
15 addsubass ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\wedge {M}\in ℂ\right)\to {N}+1-{M}={N}+1-{M}$
16 10 15 mp3an2 ${⊢}\left({N}\in ℂ\wedge {M}\in ℂ\right)\to {N}+1-{M}={N}+1-{M}$
17 13 14 16 syl2an ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\right)\to {N}+1-{M}={N}+1-{M}$
18 3 2 17 syl2anc ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1-{M}={N}+1-{M}$
19 18 eqcomd ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1-{M}={N}+1-{M}$
20 12 19 oveq12d ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}+1-{M}\dots {N}+1-{M}\right)=\left(1\dots {N}+1-{M}\right)$
21 8 20 breqtrd ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)\approx \left(1\dots {N}+1-{M}\right)$
22 peano2uz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1\in {ℤ}_{\ge {M}}$
23 uznn0sub ${⊢}{N}+1\in {ℤ}_{\ge {M}}\to {N}+1-{M}\in {ℕ}_{0}$
24 1 fzennn ${⊢}{N}+1-{M}\in {ℕ}_{0}\to \left(1\dots {N}+1-{M}\right)\approx {{G}}^{-1}\left({N}+1-{M}\right)$
25 22 23 24 3syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left(1\dots {N}+1-{M}\right)\approx {{G}}^{-1}\left({N}+1-{M}\right)$
26 entr ${⊢}\left(\left({M}\dots {N}\right)\approx \left(1\dots {N}+1-{M}\right)\wedge \left(1\dots {N}+1-{M}\right)\approx {{G}}^{-1}\left({N}+1-{M}\right)\right)\to \left({M}\dots {N}\right)\approx {{G}}^{-1}\left({N}+1-{M}\right)$
27 21 25 26 syl2anc ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)\approx {{G}}^{-1}\left({N}+1-{M}\right)$