Metamath Proof Explorer

Theorem seqp1

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

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

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
2 fveq2 ⊢ M = if M ∈ ℤ M 0 → ℤ ≥ M = ℤ ≥ if M ∈ ℤ M 0
3 2 eleq2d ⊢ M = if M ∈ ℤ M 0 → N ∈ ℤ ≥ M ↔ N ∈ ℤ ≥ if M ∈ ℤ M 0
4 seqeq1 ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F = seq if M ∈ ℤ M 0 + ˙ F
5 4 fveq1d ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F ⁡ N + 1 = seq if M ∈ ℤ M 0 + ˙ F ⁡ N + 1
6 4 fveq1d ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F ⁡ N = seq if M ∈ ℤ M 0 + ˙ F ⁡ N
7 6 oveq2d ⊢ M = if M ∈ ℤ M 0 → N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq if M ∈ ℤ M 0 + ˙ F ⁡ N
8 5 7 eqeq12d ⊢ M = if M ∈ ℤ M 0 → seq M + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N ↔ seq if M ∈ ℤ M 0 + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq if M ∈ ℤ M 0 + ˙ F ⁡ N
9 3 8 imbi12d ⊢ M = if M ∈ ℤ M 0 → N ∈ ℤ ≥ M → seq M + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N ↔ N ∈ ℤ ≥ if M ∈ ℤ M 0 → seq if M ∈ ℤ M 0 + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq if M ∈ ℤ M 0 + ˙ F ⁡ N
10 0z ⊢ 0 ∈ ℤ
11 10 elimel ⊢ if M ∈ ℤ M 0 ∈ ℤ
12 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω
13 fvex ⊢ F ⁡ if M ∈ ℤ M 0 ∈ V
14 eqid ⊢ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 x z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 y if M ∈ ℤ M 0 F ⁡ if M ∈ ℤ M 0 ↾ ω = rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 x z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 y if M ∈ ℤ M 0 F ⁡ if M ∈ ℤ M 0 ↾ ω
15 14 seqval ⊢ seq if M ∈ ℤ M 0 + ˙ F = ran ⁡ rec ⁡ x ∈ V , y ∈ V ⟼ x + 1 x z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 y if M ∈ ℤ M 0 F ⁡ if M ∈ ℤ M 0 ↾ ω
16 11 12 13 14 15 uzrdgsuci ⊢ N ∈ ℤ ≥ if M ∈ ℤ M 0 → seq if M ∈ ℤ M 0 + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq if M ∈ ℤ M 0 + ˙ F ⁡ N
17 9 16 dedth ⊢ M ∈ ℤ → N ∈ ℤ ≥ M → seq M + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N
18 1 17 mpcom ⊢ N ∈ ℤ ≥ M → seq M + ˙ F ⁡ N + 1 = N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N
19 elex ⊢ N ∈ ℤ ≥ M → N ∈ V
20 fvex ⊢ seq M + ˙ F ⁡ N ∈ V
21 fvoveq1 ⊢ z = N → F ⁡ z + 1 = F ⁡ N + 1
22 21 oveq2d ⊢ z = N → w + ˙ F ⁡ z + 1 = w + ˙ F ⁡ N + 1
23 oveq1 ⊢ w = seq M + ˙ F ⁡ N → w + ˙ F ⁡ N + 1 = seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1
24 eqid ⊢ z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 = z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1
25 ovex ⊢ seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1 ∈ V
26 22 23 24 25 ovmpo ⊢ N ∈ V ∧ seq M + ˙ F ⁡ N ∈ V → N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N = seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1
27 19 20 26 sylancl ⊢ N ∈ ℤ ≥ M → N z ∈ V , w ∈ V ⟼ w + ˙ F ⁡ z + 1 seq M + ˙ F ⁡ N = seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1
28 18 27 eqtrd ⊢ N ∈ ℤ ≥ M → seq M + ˙ F ⁡ N + 1 = seq M + ˙ F ⁡ N + ˙ F ⁡ N + 1