Metamath Proof Explorer

Theorem ruclem7

Description: Lemma for ruc . Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 ⊢ φ → F : ℕ ⟶ ℝ
ruc.2 ⊢ φ → D = x ∈ ℝ 2 , y ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ x
ruc.4 ⊢ C = 0 0 1 ∪ F
ruc.5 ⊢ G = seq 0 D C
Assertion ruclem7 ⊢ φ ∧ N ∈ ℕ 0 → G ⁡ N + 1 = G ⁡ N D F ⁡ N + 1

Proof

Step Hyp Ref Expression
1 ruc.1 ⊢ φ → F : ℕ ⟶ ℝ
2 ruc.2 ⊢ φ → D = x ∈ ℝ 2 , y ∈ ℝ ⟼ ⦋ 1 st ⁡ x + 2 nd ⁡ x 2 / m⦌ if m < y 1 st ⁡ x m m + 2 nd ⁡ x 2 2 nd ⁡ x
3 ruc.4 ⊢ C = 0 0 1 ∪ F
4 ruc.5 ⊢ G = seq 0 D C
5 simpr ⊢ φ ∧ N ∈ ℕ 0 → N ∈ ℕ 0
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 5 6 eleqtrdi ⊢ φ ∧ N ∈ ℕ 0 → N ∈ ℤ ≥ 0
8 seqp1 ⊢ N ∈ ℤ ≥ 0 → seq 0 D C ⁡ N + 1 = seq 0 D C ⁡ N D C ⁡ N + 1
9 7 8 syl ⊢ φ ∧ N ∈ ℕ 0 → seq 0 D C ⁡ N + 1 = seq 0 D C ⁡ N D C ⁡ N + 1
10 4 fveq1i ⊢ G ⁡ N + 1 = seq 0 D C ⁡ N + 1
11 4 fveq1i ⊢ G ⁡ N = seq 0 D C ⁡ N
12 11 oveq1i ⊢ G ⁡ N D C ⁡ N + 1 = seq 0 D C ⁡ N D C ⁡ N + 1
13 9 10 12 3eqtr4g ⊢ φ ∧ N ∈ ℕ 0 → G ⁡ N + 1 = G ⁡ N D C ⁡ N + 1
14 nn0p1nn ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ
15 14 adantl ⊢ φ ∧ N ∈ ℕ 0 → N + 1 ∈ ℕ
16 15 nnne0d ⊢ φ ∧ N ∈ ℕ 0 → N + 1 ≠ 0
17 16 necomd ⊢ φ ∧ N ∈ ℕ 0 → 0 ≠ N + 1
18 3 equncomi ⊢ C = F ∪ 0 0 1
19 18 fveq1i ⊢ C ⁡ N + 1 = F ∪ 0 0 1 ⁡ N + 1
20 fvunsn ⊢ 0 ≠ N + 1 → F ∪ 0 0 1 ⁡ N + 1 = F ⁡ N + 1
21 19 20 eqtrid ⊢ 0 ≠ N + 1 → C ⁡ N + 1 = F ⁡ N + 1
22 17 21 syl ⊢ φ ∧ N ∈ ℕ 0 → C ⁡ N + 1 = F ⁡ N + 1
23 22 oveq2d ⊢ φ ∧ N ∈ ℕ 0 → G ⁡ N D C ⁡ N + 1 = G ⁡ N D F ⁡ N + 1
24 13 23 eqtrd ⊢ φ ∧ N ∈ ℕ 0 → G ⁡ N + 1 = G ⁡ N D F ⁡ N + 1