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