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

Metamath Proof Explorer

Theorem seqm1

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

Ref Expression
Assertion seqm1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → seq M + ˙ F ⁡ N = seq M + ˙ F ⁡ N − 1 + ˙ F ⁡ N

Proof

Step Hyp Ref Expression
1 eluzp1m1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → N − 1 ∈ ℤ ≥ M
2 seqp1 ⊢ N − 1 ∈ ℤ ≥ M → seq M + ˙ F ⁡ N - 1 + 1 = seq M + ˙ F ⁡ N − 1 + ˙ F ⁡ N - 1 + 1
3 1 2 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → seq M + ˙ F ⁡ N - 1 + 1 = seq M + ˙ F ⁡ N − 1 + ˙ F ⁡ N - 1 + 1
4 eluzelcn ⊢ N ∈ ℤ ≥ M + 1 → N ∈ ℂ
5 ax-1cn ⊢ 1 ∈ ℂ
6 npcan ⊢ N ∈ ℂ ∧ 1 ∈ ℂ → N - 1 + 1 = N
7 4 5 6 sylancl ⊢ N ∈ ℤ ≥ M + 1 → N - 1 + 1 = N
8 7 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → N - 1 + 1 = N
9 8 fveq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → seq M + ˙ F ⁡ N - 1 + 1 = seq M + ˙ F ⁡ N
10 8 fveq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → F ⁡ N - 1 + 1 = F ⁡ N
11 10 oveq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → seq M + ˙ F ⁡ N − 1 + ˙ F ⁡ N - 1 + 1 = seq M + ˙ F ⁡ N − 1 + ˙ F ⁡ N
12 3 9 11 3eqtr3d ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → seq M + ˙ F ⁡ N = seq M + ˙ F ⁡ N − 1 + ˙ F ⁡ N