Theorem opsqrlem6

Description: Lemma for opsqri . (Contributed by NM, 23-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)$$
	opsqrlem6.4	$$⊢T{\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$
Assertion	opsqrlem6	$$⊢N\in \mathbb{N}\to F\left(N\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$

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		opsqrlem6.4	$$⊢T{\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$
5		fveq2	$$⊢j=1\to F\left(j\right)=F\left(1\right)$$
6	5	breq1d	$$⊢j=1\to \left(F\left(j\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow F\left(1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\right)$$
7		fveq2	$$⊢j=k+1\to F\left(j\right)=F\left(k+1\right)$$
8	7	breq1d	$$⊢j=k+1\to \left(F\left(j\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow F\left(k+1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\right)$$
9		fveq2	$$⊢j=N\to F\left(j\right)=F\left(N\right)$$
10	9	breq1d	$$⊢j=N\to \left(F\left(j\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow F\left(N\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\right)$$
11	1 2 3	opsqrlem2	$$⊢F\left(1\right)=0_{\mathrm{hop}}$$
12		idleop	$$⊢0_{\mathrm{hop}}{\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$
13	11 12	eqbrtri	$$⊢F\left(1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$
14		idhmop	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}$$
15	1 2 3	opsqrlem4	$$⊢F:\mathbb{N}⟶\mathrm{HrmOp}$$
16	15	ffvelcdmi	$$⊢k\in \mathbb{N}\to F\left(k\right)\in \mathrm{HrmOp}$$
17		hmopd	$$⊢\left(I_{\mathrm{op}}\in \mathrm{HrmOp}\wedge F\left(k\right)\in \mathrm{HrmOp}\right)\to I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}$$
18	14 16 17	sylancr	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}$$
19		eqid	$$⊢\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)$$
20		hmopco	$$⊢\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}\wedge \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\in \mathrm{HrmOp}$$
21	19 20	mp3an3	$$⊢\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}\right)\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\in \mathrm{HrmOp}$$
22	18 18 21	syl2anc	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\in \mathrm{HrmOp}$$
23		leopsq	$$⊢I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\in \mathrm{HrmOp}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)$$
24	18 23	syl	$$⊢k\in \mathbb{N}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)$$
25		leop3	$$⊢\left(T\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}\in \mathrm{HrmOp}\right)\to \left(T{\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)$$
26	1 14 25	mp2an	$$⊢T{\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)$$
27	4 26	mpbi	$$⊢0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)$$
28		hmopd	$$⊢\left(I_{\mathrm{op}}\in \mathrm{HrmOp}\wedge T\in \mathrm{HrmOp}\right)\to I_{\mathrm{op}}{-}_{\mathrm{op}}T\in \mathrm{HrmOp}$$
29	14 1 28	mp2an	$$⊢I_{\mathrm{op}}{-}_{\mathrm{op}}T\in \mathrm{HrmOp}$$
30		leopadd	$$⊢\left(\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}{-}_{\mathrm{op}}T\in \mathrm{HrmOp}\right)\wedge \left(0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)\wedge 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)\right)\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)$$
31	29 30	mpanl2	$$⊢\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\in \mathrm{HrmOp}\wedge \left(0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)\wedge 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)\right)\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)$$
32	27 31	mpanr2	$$⊢\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\in \mathrm{HrmOp}\wedge 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)\right)\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)$$
33	22 24 32	syl2anc	$$⊢k\in \mathbb{N}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)\right)$$
34		2cn	$$⊢2\in ℂ$$
35		hmopf	$$⊢F\left(k\right)\in \mathrm{HrmOp}\to F\left(k\right):\mathscr{H}⟶\mathscr{H}$$
36	16 35	syl	$$⊢k\in \mathbb{N}\to F\left(k\right):\mathscr{H}⟶\mathscr{H}$$
37		homulcl	$$⊢\left(2\in ℂ\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
38	34 36 37	sylancr	$$⊢k\in \mathbb{N}\to \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
39		hmopf	$$⊢T\in \mathrm{HrmOp}\to T:\mathscr{H}⟶\mathscr{H}$$
40	1 39	ax-mp	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
41		fco	$$⊢\left(F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
42	36 36 41	syl2anc	$$⊢k\in \mathbb{N}\to \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
43		hosubcl	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
44	40 42 43	sylancr	$$⊢k\in \mathbb{N}\to \left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
45		hmopf	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}\to I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}$$
46	14 45	ax-mp	$$⊢I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}$$
47		homulcl	$$⊢\left(2\in ℂ\wedge I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\right)\to \left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}$$
48	34 46 47	mp2an	$$⊢\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}$$
49		hosubsub4	$$⊢\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
50	48 49	mp3an1	$$⊢\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
51	38 44 50	syl2anc	$$⊢k\in \mathbb{N}\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
52		hosubcl	$$⊢\left(\left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
53	42 38 52	syl2anc	$$⊢k\in \mathbb{N}\to \left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
54		hoadd32	$$⊢\left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge \left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\wedge I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
55	46 46 54	mp3an13	$$⊢\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
56	53 55	syl	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
57		ho2times	$$⊢I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\to 2{·}_{\mathrm{op}}{I}_{\mathrm{op}}=I_{\mathrm{op}}{+}_{\mathrm{op}}{I}_{\mathrm{op}}$$
58	46 57	ax-mp	$$⊢2{·}_{\mathrm{op}}{I}_{\mathrm{op}}=I_{\mathrm{op}}{+}_{\mathrm{op}}{I}_{\mathrm{op}}$$
59	58	oveq1i	$$⊢\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
60	56 59	eqtr4di	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
61		hoaddsubass	$$⊢\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
62	48 61	mp3an1	$$⊢\left(\left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
63	42 38 62	syl2anc	$$⊢k\in \mathbb{N}\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
64	60 63	eqtr4d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)$$
65	64	oveq1d	$$⊢k\in \mathbb{N}\to \left(\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}T=\left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}T$$
66		hoaddcl	$$⊢\left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge \left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
67	46 53 66	sylancr	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
68		hoaddsubass	$$⊢\left(\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\wedge I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}T=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)$$
69	46 40 68	mp3an23	$$⊢\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\to \left(\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}T=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)$$
70	67 69	syl	$$⊢k\in \mathbb{N}\to \left(\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}T=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)$$
71		hoaddcl	$$⊢\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
72	48 42 71	sylancr	$$⊢k\in \mathbb{N}\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
73		hosubsub4	$$⊢\left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}T=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
74	40 73	mp3an3	$$⊢\left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}T=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
75	72 38 74	syl2anc	$$⊢k\in \mathbb{N}\to \left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}T=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
76	65 70 75	3eqtr3d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
77		hosubadd4	$$⊢\left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
78	40 77	mpanr1	$$⊢\left(\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
79	48 78	mpanl1	$$⊢\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
80	38 42 79	syl2anc	$$⊢k\in \mathbb{N}\to \left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}T\right)$$
81	76 80	eqtr4d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)=\left(\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)$$
82		halfcn	$$⊢\frac{1}{2}\in ℂ$$
83		homulcl	$$⊢\left(\frac{1}{2}\in ℂ\wedge \left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
84	82 44 83	sylancr	$$⊢k\in \mathbb{N}\to \left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
85		hoadddi	$$⊢\left(2\in ℂ\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge \left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to 2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)$$
86	34 85	mp3an1	$$⊢\left(F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge \left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to 2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)$$
87	36 84 86	syl2anc	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)$$
88		2thalfe1	$$⊢2\left(\frac{1}{2}\right)=1$$
89	88	oveq1i	$$⊢2\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)$$
90		homulass	$$⊢\left(2\in ℂ\wedge \frac{1}{2}\in ℂ\wedge \left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to 2\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
91	34 82 90	mp3an12	$$⊢\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\to 2\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
92	44 91	syl	$$⊢k\in \mathbb{N}\to 2\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
93		homullid	$$⊢\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right):\mathscr{H}⟶\mathscr{H}\to 1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
94	44 93	syl	$$⊢k\in \mathbb{N}\to 1{·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
95	89 92 94	3eqtr3a	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)=T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
96	95	oveq2d	$$⊢k\in \mathbb{N}\to \left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)$$
97	87 96	eqtrd	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)$$
98	97	oveq2d	$$⊢k\in \mathbb{N}\to \left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(\left(2{·}_{\mathrm{op}}F\left(k\right)\right){+}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
99	51 81 98	3eqtr4d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)$$
100		hoaddcl	$$⊢\left(F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge \left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
101	36 84 100	syl2anc	$$⊢k\in \mathbb{N}\to \left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
102		hosubdi	$$⊢\left(2\in ℂ\wedge I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to 2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)$$
103	34 46 102	mp3an12	$$⊢\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right):\mathscr{H}⟶\mathscr{H}\to 2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)$$
104	101 103	syl	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)=\left(2{·}_{\mathrm{op}}{I}_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)$$
105	99 104	eqtr4d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)=2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)$$
106		hosubcl	$$⊢\left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
107	46 36 106	sylancr	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
108		hocsubdir	$$⊢\left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)$$
109	46 108	mp3an1	$$⊢\left(F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)$$
110	36 107 109	syl2anc	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)$$
111		hmoplin	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}\to I_{\mathrm{op}}\in \mathrm{LinOp}$$
112	14 111	ax-mp	$$⊢I_{\mathrm{op}}\in \mathrm{LinOp}$$
113		hoddi	$$⊢\left(I_{\mathrm{op}}\in \mathrm{LinOp}\wedge I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\to I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(I_{\mathrm{op}}\circ F\left(k\right)\right)$$
114	112 46 113	mp3an12	$$⊢F\left(k\right):\mathscr{H}⟶\mathscr{H}\to I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(I_{\mathrm{op}}\circ F\left(k\right)\right)$$
115	36 114	syl	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(I_{\mathrm{op}}\circ F\left(k\right)\right)$$
116	46	hoid1i	$$⊢I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}$$
117	116	a1i	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}$$
118		hoico2	$$⊢F\left(k\right):\mathscr{H}⟶\mathscr{H}\to I_{\mathrm{op}}\circ F\left(k\right)=F\left(k\right)$$
119	36 118	syl	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}\circ F\left(k\right)=F\left(k\right)$$
120	117 119	oveq12d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(I_{\mathrm{op}}\circ F\left(k\right)\right)=I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)$$
121	115 120	eqtrd	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)$$
122		hmoplin	$$⊢F\left(k\right)\in \mathrm{HrmOp}\to F\left(k\right)\in \mathrm{LinOp}$$
123	16 122	syl	$$⊢k\in \mathbb{N}\to F\left(k\right)\in \mathrm{LinOp}$$
124		hoddi	$$⊢\left(F\left(k\right)\in \mathrm{LinOp}\wedge I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\to F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(F\left(k\right)\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
125	46 124	mp3an2	$$⊢\left(F\left(k\right)\in \mathrm{LinOp}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\to F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(F\left(k\right)\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
126	123 36 125	syl2anc	$$⊢k\in \mathbb{N}\to F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=\left(F\left(k\right)\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
127		hoico1	$$⊢F\left(k\right):\mathscr{H}⟶\mathscr{H}\to F\left(k\right)\circ I_{\mathrm{op}}=F\left(k\right)$$
128	36 127	syl	$$⊢k\in \mathbb{N}\to F\left(k\right)\circ I_{\mathrm{op}}=F\left(k\right)$$
129	128	oveq1d	$$⊢k\in \mathbb{N}\to \left(F\left(k\right)\circ I_{\mathrm{op}}\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)=F\left(k\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
130	126 129	eqtrd	$$⊢k\in \mathbb{N}\to F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=F\left(k\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)$$
131	121 130	oveq12d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)=\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)$$
132	36 46	jctil	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)$$
133		hosubadd4	$$⊢\left(\left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge F\left(k\right):\mathscr{H}⟶\mathscr{H}\right)\wedge \left(F\left(k\right):\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}F\left(k\right)\right)$$
134	132 36 42 133	syl12anc	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}F\left(k\right)\right)$$
135	131 134	eqtrd	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}F\left(k\right)\right)$$
136		ho2times	$$⊢F\left(k\right):\mathscr{H}⟶\mathscr{H}\to 2{·}_{\mathrm{op}}F\left(k\right)=F\left(k\right){+}_{\mathrm{op}}F\left(k\right)$$
137	36 136	syl	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}F\left(k\right)=F\left(k\right){+}_{\mathrm{op}}F\left(k\right)$$
138	137	oveq2d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}F\left(k\right)\right)$$
139		hoaddsubass	$$⊢\left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge \left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
140	46 139	mp3an1	$$⊢\left(\left(F\left(k\right)\circ F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\wedge \left(2{·}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}\right)\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
141	42 38 140	syl2anc	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)=I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
142	135 138 141	3eqtr2d	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){-}_{\mathrm{op}}\left(F\left(k\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right)=I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
143	110 142	eqtrd	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)=I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)$$
144	143	oveq1d	$$⊢k\in \mathbb{N}\to \left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)=\left(I_{\mathrm{op}}{+}_{\mathrm{op}}\left(\left(F\left(k\right)\circ F\left(k\right)\right){-}_{\mathrm{op}}\left(2{·}_{\mathrm{op}}F\left(k\right)\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)$$
145	1 2 3	opsqrlem5	$$⊢k\in \mathbb{N}\to F\left(k+1\right)=F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)$$
146	145	oveq2d	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)=I_{\mathrm{op}}{-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)$$
147	146	oveq2d	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)=2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}\left(F\left(k\right){+}_{\mathrm{op}}\left(\left(\frac{1}{2}\right){·}_{\mathrm{op}}\left(T{-}_{\mathrm{op}}\left(F\left(k\right)\circ F\left(k\right)\right)\right)\right)\right)\right)$$
148	105 144 147	3eqtr4d	$$⊢k\in \mathbb{N}\to \left(\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\circ \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right)\right){+}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}T\right)=2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)$$
149	33 148	breqtrd	$$⊢k\in \mathbb{N}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\right)$$
150		peano2nn	$$⊢k\in \mathbb{N}\to k+1\in \mathbb{N}$$
151	15	ffvelcdmi	$$⊢k+1\in \mathbb{N}\to F\left(k+1\right)\in \mathrm{HrmOp}$$
152	150 151	syl	$$⊢k\in \mathbb{N}\to F\left(k+1\right)\in \mathrm{HrmOp}$$
153		hmopd	$$⊢\left(I_{\mathrm{op}}\in \mathrm{HrmOp}\wedge F\left(k+1\right)\in \mathrm{HrmOp}\right)\to I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\in \mathrm{HrmOp}$$
154	14 152 153	sylancr	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\in \mathrm{HrmOp}$$
155		2re	$$⊢2\in ℝ$$
156		2pos	$$⊢0<2$$
157		leopmul	$$⊢\left(2\in ℝ\wedge I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\in \mathrm{HrmOp}\wedge 0<2\right)\to \left(0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\right)\right)$$
158	155 156 157	mp3an13	$$⊢I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\in \mathrm{HrmOp}\to \left(0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\right)\right)$$
159	154 158	syl	$$⊢k\in \mathbb{N}\to \left(0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(2{·}_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\right)\right)$$
160	149 159	mpbird	$$⊢k\in \mathbb{N}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)$$
161		leop3	$$⊢\left(F\left(k+1\right)\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}\in \mathrm{HrmOp}\right)\to \left(F\left(k+1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\right)$$
162	152 14 161	sylancl	$$⊢k\in \mathbb{N}\to \left(F\left(k+1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)\right)$$
163	160 162	mpbird	$$⊢k\in \mathbb{N}\to F\left(k+1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$
164	6 8 10 13 163	nn1suc	$$⊢N\in \mathbb{N}\to F\left(N\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$