This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fseq1hash

Description: The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 12-Mar-2015)

		Ref	Expression
	Assertion	fseq1hash	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to \|F\| = N$

Proof

Step	Hyp	Ref	Expression
1		hashfn	$⊢ F Fn (1 \dots N) \to \|F\| = \|(1 \dots N)\|$
2		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
3	1 2	sylan9eqr	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to \|F\| = N$