hashfz

Description: Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014) (Proof shortened by Mario Carneiro, 15-Apr-2015)

		Ref	Expression
	Assertion	hashfz	$⊢ B \in ℤ_{\geq A} \to \|(A \dots B)\| = B - A + 1$

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ B \in ℤ_{\geq A} \to A \in ℤ$
2		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
3		1z	$⊢ 1 \in ℤ$
4		zsubcl	$⊢ (1 \in ℤ \land A \in ℤ) \to 1 - A \in ℤ$
5	3 1 4	sylancr	$⊢ B \in ℤ_{\geq A} \to 1 - A \in ℤ$
6		fzen	$⊢ (A \in ℤ \land B \in ℤ \land 1 - A \in ℤ) \to (A \dots B) \approx (A + 1 - A \dots B + 1 - A)$
7	1 2 5 6	syl3anc	$⊢ B \in ℤ_{\geq A} \to (A \dots B) \approx (A + 1 - A \dots B + 1 - A)$
8	1	zcnd	$⊢ B \in ℤ_{\geq A} \to A \in ℂ$
9		ax-1cn	$⊢ 1 \in ℂ$
10		pncan3	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 - A = 1$
11	8 9 10	sylancl	$⊢ B \in ℤ_{\geq A} \to A + 1 - A = 1$
12		1cnd	$⊢ B \in ℤ_{\geq A} \to 1 \in ℂ$
13	2	zcnd	$⊢ B \in ℤ_{\geq A} \to B \in ℂ$
14	13 8	subcld	$⊢ B \in ℤ_{\geq A} \to B - A \in ℂ$
15	13 12 8	addsub12d	$⊢ B \in ℤ_{\geq A} \to B + 1 - A = 1 + B - A$
16	12 14 15	comraddd	$⊢ B \in ℤ_{\geq A} \to B + 1 - A = B - A + 1$
17	11 16	oveq12d	$⊢ B \in ℤ_{\geq A} \to (A + 1 - A \dots B + 1 - A) = (1 \dots B - A + 1)$
18	7 17	breqtrd	$⊢ B \in ℤ_{\geq A} \to (A \dots B) \approx (1 \dots B - A + 1)$
19		hasheni	$⊢ (A \dots B) \approx (1 \dots B - A + 1) \to \|(A \dots B)\| = \|(1 \dots B - A + 1)\|$
20	18 19	syl	$⊢ B \in ℤ_{\geq A} \to \|(A \dots B)\| = \|(1 \dots B - A + 1)\|$
21		uznn0sub	$⊢ B \in ℤ_{\geq A} \to B - A \in ℕ_{0}$
22		peano2nn0	$⊢ B - A \in ℕ_{0} \to B - A + 1 \in ℕ_{0}$
23		hashfz1	$⊢ B - A + 1 \in ℕ_{0} \to \|(1 \dots B - A + 1)\| = B - A + 1$
24	21 22 23	3syl	$⊢ B \in ℤ_{\geq A} \to \|(1 \dots B - A + 1)\| = B - A + 1$
25	20 24	eqtrd	$⊢ B \in ℤ_{\geq A} \to \|(A \dots B)\| = B - A + 1$

Metamath Proof Explorer

Theorem hashfz

Proof