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 e. HrmOp
	opsqrlem2.2	|- S = ( x e. HrmOp , y e. HrmOp |-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
	opsqrlem2.3	|- F = seq 1 ( S , ( NN X. { 0hop } ) )
Assertion	opsqrlem2	|- ( F ` 1 ) = 0hop

Proof

Step	Hyp	Ref	Expression
1		opsqrlem2.1	|- T e. HrmOp
2		opsqrlem2.2	|- S = ( x e. HrmOp , y e. HrmOp |-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
3		opsqrlem2.3	|- F = seq 1 ( S , ( NN X. { 0hop } ) )
4	3	fveq1i	|- ( F ` 1 ) = ( seq 1 ( S , ( NN X. { 0hop } ) ) ` 1 )
5		1z	|- 1 e. ZZ
6		seq1	|- ( 1 e. ZZ -> ( seq 1 ( S , ( NN X. { 0hop } ) ) ` 1 ) = ( ( NN X. { 0hop } ) ` 1 ) )
7	5 6	ax-mp	|- ( seq 1 ( S , ( NN X. { 0hop } ) ) ` 1 ) = ( ( NN X. { 0hop } ) ` 1 )
8		1nn	|- 1 e. NN
9		0hmop	|- 0hop e. HrmOp
10	9	elexi	|- 0hop e. _V
11	10	fvconst2	|- ( 1 e. NN -> ( ( NN X. { 0hop } ) ` 1 ) = 0hop )
12	8 11	ax-mp	|- ( ( NN X. { 0hop } ) ` 1 ) = 0hop
13	4 7 12	3eqtri	|- ( F ` 1 ) = 0hop