Metamath Proof Explorer


Theorem opsqrlem2

Description: Lemma for opsqri . FN is the recursive function A_n (starting at n=1 instead of 0) of Theorem 9.4-2 of Kreyszig p. 476. (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 opsqrlem2 F 1 = 0 hop

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 3 fveq1i F 1 = seq 1 S × 0 hop 1
5 1z 1
6 seq1 1 seq 1 S × 0 hop 1 = × 0 hop 1
7 5 6 ax-mp seq 1 S × 0 hop 1 = × 0 hop 1
8 1nn 1
9 0hmop 0 hop HrmOp
10 9 elexi 0 hop V
11 10 fvconst2 1 × 0 hop 1 = 0 hop
12 8 11 ax-mp × 0 hop 1 = 0 hop
13 4 7 12 3eqtri F 1 = 0 hop