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 \in V ⟼ x + 1), 0) ↾}_{ω}$
	Assertion	fzen2	$⊢ N \in ℤ_{\geq M} \to (M \dots N) \approx G^{-1} (N + 1 - M)$

Proof

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

Metamath Proof Explorer

Theorem fzen2

Proof