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+op12·opT-opx∘x
opsqrlem2.3 ⊢F=seq1Sℕ×0hop
Assertion opsqrlem5 ⊢N∈ℕ→F⁡N+1=F⁡N+op12·opT-opF⁡N∘F⁡N

Proof

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