fvffz0

Description: The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021)

		Ref	Expression
	Assertion	fvffz0	$⊢ ((N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \land P : (0 \dots N) ⟶ V) \to P (I) \in V$

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \land P : (0 \dots N) ⟶ V) \to P : (0 \dots N) ⟶ V$
2		simp2	$⊢ (N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \to I \in ℕ_{0}$
3		simp1	$⊢ (N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \to N \in ℕ_{0}$
4		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
5		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
6		ltle	$⊢ (I \in ℝ \land N \in ℝ) \to (I < N \to I \leq N)$
7	4 5 6	syl2anr	$⊢ (N \in ℕ_{0} \land I \in ℕ_{0}) \to (I < N \to I \leq N)$
8	7	3impia	$⊢ (N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \to I \leq N$
9		elfz2nn0	$⊢ I \in (0 \dots N) \leftrightarrow (I \in ℕ_{0} \land N \in ℕ_{0} \land I \leq N)$
10	2 3 8 9	syl3anbrc	$⊢ (N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \to I \in (0 \dots N)$
11	10	adantr	$⊢ ((N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \land P : (0 \dots N) ⟶ V) \to I \in (0 \dots N)$
12	1 11	ffvelrnd	$⊢ ((N \in ℕ_{0} \land I \in ℕ_{0} \land I < N) \land P : (0 \dots N) ⟶ V) \to P (I) \in V$

Metamath Proof Explorer