Metamath Proof Explorer

Theorem opsqrlem5

Description: Lemma for opsqri . (Contributed by NM, 17-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypotheses opsqrlem2.1 ⊢ T ∈ HrmOp
opsqrlem2.2 ⊢ S = x ∈ HrmOp , y ∈ HrmOp ⟼ x + op 1 2 · op T - op x ∘ x
opsqrlem2.3 ⊢ F = seq 1 S ℕ × 0 hop
Assertion opsqrlem5 ⊢ N ∈ ℕ → F ⁡ N + 1 = F ⁡ N + op 1 2 · op T - op F ⁡ N ∘ F ⁡ N

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 ⊢ T ∈ HrmOp
2 opsqrlem2.2 ⊢ S = x ∈ HrmOp , y ∈ HrmOp ⟼ x + op 1 2 · op T - op x ∘ x
3 opsqrlem2.3 ⊢ F = seq 1 S ℕ × 0 hop
4 elnnuz ⊢ N ∈ ℕ ↔ N ∈ ℤ ≥ 1
5 seqp1 ⊢ N ∈ ℤ ≥ 1 → seq 1 S ℕ × 0 hop ⁡ N + 1 = seq 1 S ℕ × 0 hop ⁡ N S ℕ × 0 hop ⁡ N + 1
6 4 5 sylbi ⊢ N ∈ ℕ → seq 1 S ℕ × 0 hop ⁡ N + 1 = seq 1 S ℕ × 0 hop ⁡ N S ℕ × 0 hop ⁡ N + 1
7 3 fveq1i ⊢ F ⁡ N + 1 = seq 1 S ℕ × 0 hop ⁡ N + 1
8 3 fveq1i ⊢ F ⁡ N = seq 1 S ℕ × 0 hop ⁡ N
9 8 oveq1i ⊢ F ⁡ N S ℕ × 0 hop ⁡ N + 1 = seq 1 S ℕ × 0 hop ⁡ N S ℕ × 0 hop ⁡ N + 1
10 6 7 9 3eqtr4g ⊢ N ∈ ℕ → F ⁡ N + 1 = F ⁡ N S ℕ × 0 hop ⁡ N + 1
11 1 2 3 opsqrlem4 ⊢ F : ℕ ⟶ HrmOp
12 11 ffvelrni ⊢ N ∈ ℕ → F ⁡ N ∈ HrmOp
13 peano2nn ⊢ N ∈ ℕ → N + 1 ∈ ℕ
14 0hmop ⊢ 0 hop ∈ HrmOp
15 14 elexi ⊢ 0 hop ∈ V
16 15 fvconst2 ⊢ N + 1 ∈ ℕ → ℕ × 0 hop ⁡ N + 1 = 0 hop
17 13 16 syl ⊢ N ∈ ℕ → ℕ × 0 hop ⁡ N + 1 = 0 hop
18 17 14 eqeltrdi ⊢ N ∈ ℕ → ℕ × 0 hop ⁡ N + 1 ∈ HrmOp
19 1 2 3 opsqrlem3 ⊢ F ⁡ N ∈ HrmOp ∧ ℕ × 0 hop ⁡ N + 1 ∈ HrmOp → F ⁡ N S ℕ × 0 hop ⁡ N + 1 = F ⁡ N + op 1 2 · op T - op F ⁡ N ∘ F ⁡ N
20 12 18 19 syl2anc ⊢ N ∈ ℕ → F ⁡ N S ℕ × 0 hop ⁡ N + 1 = F ⁡ N + op 1 2 · op T - op F ⁡ N ∘ F ⁡ N
21 10 20 eqtrd ⊢ N ∈ ℕ → F ⁡ N + 1 = F ⁡ N + op 1 2 · op T - op F ⁡ N ∘ F ⁡ N