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\in \mathrm{HrmOp}$$
	opsqrlem2.2	$$⊢S=\left(x\in \mathrm{HrmOp},y\in \mathrm{HrmOp}⟼x{+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(x\circ x\right)\right)\right)\right)$$
	opsqrlem2.3	$$⊢F=seq1\left(S,\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\right)$$
Assertion	opsqrlem2	$$⊢F\left(1\right)=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		opsqrlem2.1	$$⊢T\in \mathrm{HrmOp}$$
2		opsqrlem2.2	$$⊢S=\left(x\in \mathrm{HrmOp},y\in \mathrm{HrmOp}⟼x{+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(x\circ x\right)\right)\right)\right)$$
3		opsqrlem2.3	$$⊢F=seq1\left(S,\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\right)$$
4	3	fveq1i	$$⊢F\left(1\right)=seq1\left(S,\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\right)\left(1\right)$$
5		1z	$$⊢1\in \mathbb{Z}$$
6		seq1	$$⊢1\in \mathbb{Z}\to seq1\left(S,\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\right)\left(1\right)=\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\left(1\right)$$
7	5 6	ax-mp	$$⊢seq1\left(S,\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\right)\left(1\right)=\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\left(1\right)$$
8		1nn	$$⊢1\in \mathbb{N}$$
9		0hmop	$$⊢0_{\mathrm{hop}}\in \mathrm{HrmOp}$$
10	9	elexi	$$⊢0_{\mathrm{hop}}\in \mathrm{V}$$
11	10	fvconst2	$$⊢1\in \mathbb{N}\to \left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\left(1\right)=0_{\mathrm{hop}}$$
12	8 11	ax-mp	$$⊢\left(\mathbb{N}\times \left\{0_{\mathrm{hop}}\right\}\right)\left(1\right)=0_{\mathrm{hop}}$$
13	4 7 12	3eqtri	$$⊢F\left(1\right)=0_{\mathrm{hop}}$$