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	ffvelrni	$$⊢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		2ne0	$$⊢2\ne 0$$
89	34 88	recidi	$$⊢2\left(\frac{1}{2}\right)=1$$
90	89	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)$$
91		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)$$
92	34 82 91	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)$$
93	44 92	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)$$
94		homulid2	$$⊢\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)$$
95	44 94	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)$$
96	90 93 95	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)$$
97	96	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)$$
98	87 97	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)$$
99	98	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)$$
100	51 81 99	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)$$
101		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}$$
102	36 84 101	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}$$
103		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)$$
104	34 46 103	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)$$
105	102 104	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)$$
106	100 105	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)$$
107		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}$$
108	46 36 107	sylancr	$$⊢k\in \mathbb{N}\to \left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k\right)\right):\mathscr{H}⟶\mathscr{H}$$
109		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)$$
110	46 109	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)$$
111	36 108 110	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)$$
112		hmoplin	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}\to I_{\mathrm{op}}\in \mathrm{LinOp}$$
113	14 112	ax-mp	$$⊢I_{\mathrm{op}}\in \mathrm{LinOp}$$
114		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)$$
115	113 46 114	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)$$
116	36 115	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)$$
117	46	hoid1i	$$⊢I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}$$
118	117	a1i	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}$$
119		hoico2	$$⊢F\left(k\right):\mathscr{H}⟶\mathscr{H}\to I_{\mathrm{op}}\circ F\left(k\right)=F\left(k\right)$$
120	36 119	syl	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}\circ F\left(k\right)=F\left(k\right)$$
121	118 120	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)$$
122	116 121	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)$$
123		hmoplin	$$⊢F\left(k\right)\in \mathrm{HrmOp}\to F\left(k\right)\in \mathrm{LinOp}$$
124	16 123	syl	$$⊢k\in \mathbb{N}\to F\left(k\right)\in \mathrm{LinOp}$$
125		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)$$
126	46 125	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)$$
127	124 36 126	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)$$
128		hoico1	$$⊢F\left(k\right):\mathscr{H}⟶\mathscr{H}\to F\left(k\right)\circ I_{\mathrm{op}}=F\left(k\right)$$
129	36 128	syl	$$⊢k\in \mathbb{N}\to F\left(k\right)\circ I_{\mathrm{op}}=F\left(k\right)$$
130	129	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)$$
131	127 130	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)$$
132	122 131	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)$$
133	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)$$
134		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)$$
135	133 36 42 134	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)$$
136	132 135	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)$$
137		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)$$
138	36 137	syl	$$⊢k\in \mathbb{N}\to 2{·}_{\mathrm{op}}F\left(k\right)=F\left(k\right){+}_{\mathrm{op}}F\left(k\right)$$
139	138	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)$$
140		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)$$
141	46 140	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)$$
142	42 38 141	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)$$
143	136 139 142	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)$$
144	111 143	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)$$
145	144	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)$$
146	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)$$
147	146	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)$$
148	147	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)$$
149	106 145 148	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)$$
150	33 149	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)$$
151		peano2nn	$$⊢k\in \mathbb{N}\to k+1\in \mathbb{N}$$
152	15	ffvelrni	$$⊢k+1\in \mathbb{N}\to F\left(k+1\right)\in \mathrm{HrmOp}$$
153	151 152	syl	$$⊢k\in \mathbb{N}\to F\left(k+1\right)\in \mathrm{HrmOp}$$
154		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}$$
155	14 153 154	sylancr	$$⊢k\in \mathbb{N}\to I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\in \mathrm{HrmOp}$$
156		2re	$$⊢2\in ℝ$$
157		2pos	$$⊢0<2$$
158		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)$$
159	156 157 158	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)$$
160	155 159	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)$$
161	150 160	mpbird	$$⊢k\in \mathbb{N}\to 0_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(I_{\mathrm{op}}{-}_{\mathrm{op}}F\left(k+1\right)\right)$$
162		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)$$
163	153 14 162	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)$$
164	161 163	mpbird	$$⊢k\in \mathbb{N}\to F\left(k+1\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$
165	6 8 10 13 164	nn1suc	$$⊢N\in \mathbb{N}\to F\left(N\right){\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$