Theorem opsqrlem6

Description: Lemma for opsqri . (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	opsqrlem2.1	⊢ 𝑇 ∈ HrmOp
	opsqrlem2.2	⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
	opsqrlem2.3	⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
	opsqrlem6.4	⊢ 𝑇 ≤op Iop
Assertion	opsqrlem6	⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ≤op Iop )

Proof

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