seqm1

Description: Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013)

		Ref	Expression
	Assertion	seqm1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N)$

Step	Hyp	Ref	Expression
1		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
2		seqp1	$⊢ N - 1 \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (N - 1 + 1) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N - 1 + 1)$
3	1 2	syl	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N - 1 + 1) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N - 1 + 1)$
4		eluzelcn	$⊢ N \in ℤ_{\geq (M + 1)} \to N \in ℂ$
5		ax-1cn	$⊢ 1 \in ℂ$
6		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
7	4 5 6	sylancl	$⊢ N \in ℤ_{\geq (M + 1)} \to N - 1 + 1 = N$
8	7	adantl	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 + 1 = N$
9	8	fveq2d	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N - 1 + 1) = seq M (\underset{˙}{+}, F) (N)$
10	8	fveq2d	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to F (N - 1 + 1) = F (N)$
11	10	oveq2d	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N - 1 + 1) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N)$
12	3 9 11	3eqtr3d	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N)$

Metamath Proof Explorer