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	⊢ 𝑇 ∈ HrmOp
	opsqrlem2.2	⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
	opsqrlem2.3	⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
Assertion	opsqrlem2	⊢ ( 𝐹 ‘ 1 ) = 0hop

Proof

Step	Hyp	Ref	Expression
1		opsqrlem2.1	⊢ 𝑇 ∈ HrmOp
2		opsqrlem2.2	⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
3		opsqrlem2.3	⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
4	3	fveq1i	⊢ ( 𝐹 ‘ 1 ) = ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 1 )
5		1z	⊢ 1 ∈ ℤ
6		seq1	⊢ ( 1 ∈ ℤ → ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 1 ) = ( ( ℕ × { 0hop } ) ‘ 1 ) )
7	5 6	ax-mp	⊢ ( seq 1 ( 𝑆 , ( ℕ × { 0hop } ) ) ‘ 1 ) = ( ( ℕ × { 0hop } ) ‘ 1 )
8		1nn	⊢ 1 ∈ ℕ
9		0hmop	⊢ 0hop ∈ HrmOp
10	9	elexi	⊢ 0hop ∈ V
11	10	fvconst2	⊢ ( 1 ∈ ℕ → ( ( ℕ × { 0hop } ) ‘ 1 ) = 0hop )
12	8 11	ax-mp	⊢ ( ( ℕ × { 0hop } ) ‘ 1 ) = 0hop
13	4 7 12	3eqtri	⊢ ( 𝐹 ‘ 1 ) = 0hop