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	ffvelrni	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ 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		2ne0	⊢ 2 ≠ 0
89	34 88	recidi	⊢ ( 2 · ( 1 / 2 ) ) = 1
90	89	oveq1i	⊢ ( ( 2 · ( 1 / 2 ) ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 1 ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
91		homulass	⊢ ( ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) : ℋ ⟶ ℋ ) → ( ( 2 · ( 1 / 2 ) ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 2 ·op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
92	34 82 91	mp3an12	⊢ ( ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) : ℋ ⟶ ℋ → ( ( 2 · ( 1 / 2 ) ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 2 ·op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
93	44 92	syl	⊢ ( 𝑘 ∈ ℕ → ( ( 2 · ( 1 / 2 ) ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 2 ·op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
94		homulid2	⊢ ( ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) : ℋ ⟶ ℋ → ( 1 ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
95	44 94	syl	⊢ ( 𝑘 ∈ ℕ → ( 1 ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
96	90 93 95	3eqtr3a	⊢ ( 𝑘 ∈ ℕ → ( 2 ·op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) = ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
97	96	oveq2d	⊢ ( 𝑘 ∈ ℕ → ( ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) +op ( 2 ·op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) = ( ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) +op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
98	87 97	eqtrd	⊢ ( 𝑘 ∈ ℕ → ( 2 ·op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) = ( ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) +op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
99	98	oveq2d	⊢ ( 𝑘 ∈ ℕ → ( ( 2 ·op Iop ) −op ( 2 ·op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) = ( ( 2 ·op Iop ) −op ( ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) +op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
100	51 81 99	3eqtr4d	⊢ ( 𝑘 ∈ ℕ → ( ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) +op ( Iop −op 𝑇 ) ) = ( ( 2 ·op Iop ) −op ( 2 ·op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
101		hoaddcl	⊢ ( ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ∧ ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) : ℋ ⟶ ℋ ) → ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) : ℋ ⟶ ℋ )
102	36 84 101	syl2anc	⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) : ℋ ⟶ ℋ )
103		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 ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
104	34 46 103	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 ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
105	102 104	syl	⊢ ( 𝑘 ∈ ℕ → ( 2 ·op ( Iop −op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) = ( ( 2 ·op Iop ) −op ( 2 ·op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
106	100 105	eqtr4d	⊢ ( 𝑘 ∈ ℕ → ( ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) +op ( Iop −op 𝑇 ) ) = ( 2 ·op ( Iop −op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
107		hosubcl	⊢ ( ( Iop : ℋ ⟶ ℋ ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ) → ( Iop −op ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ )
108	46 36 107	sylancr	⊢ ( 𝑘 ∈ ℕ → ( Iop −op ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ )
109		hocsubdir	⊢ ( ( Iop : ℋ ⟶ ℋ ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ∧ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ) → ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) ) )
110	46 109	mp3an1	⊢ ( ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ∧ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ) → ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) ) )
111	36 108 110	syl2anc	⊢ ( 𝑘 ∈ ℕ → ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) ) )
112		hmoplin	⊢ ( Iop ∈ HrmOp → Iop ∈ LinOp )
113	14 112	ax-mp	⊢ Iop ∈ LinOp
114		hoddi	⊢ ( ( Iop ∈ LinOp ∧ Iop : ℋ ⟶ ℋ ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ) → ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop ∘ Iop ) −op ( Iop ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
115	113 46 114	mp3an12	⊢ ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ → ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop ∘ Iop ) −op ( Iop ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
116	36 115	syl	⊢ ( 𝑘 ∈ ℕ → ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop ∘ Iop ) −op ( Iop ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
117	46	hoid1i	⊢ ( Iop ∘ Iop ) = Iop
118	117	a1i	⊢ ( 𝑘 ∈ ℕ → ( Iop ∘ Iop ) = Iop )
119		hoico2	⊢ ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ → ( Iop ∘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
120	36 119	syl	⊢ ( 𝑘 ∈ ℕ → ( Iop ∘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
121	118 120	oveq12d	⊢ ( 𝑘 ∈ ℕ → ( ( Iop ∘ Iop ) −op ( Iop ∘ ( 𝐹 ‘ 𝑘 ) ) ) = ( Iop −op ( 𝐹 ‘ 𝑘 ) ) )
122	116 121	eqtrd	⊢ ( 𝑘 ∈ ℕ → ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( Iop −op ( 𝐹 ‘ 𝑘 ) ) )
123		hmoplin	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ HrmOp → ( 𝐹 ‘ 𝑘 ) ∈ LinOp )
124	16 123	syl	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ LinOp )
125		hoddi	⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ LinOp ∧ Iop : ℋ ⟶ ℋ ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ) → ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ∘ Iop ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
126	46 125	mp3an2	⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ LinOp ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ) → ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ∘ Iop ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
127	124 36 126	syl2anc	⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ∘ Iop ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
128		hoico1	⊢ ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ → ( ( 𝐹 ‘ 𝑘 ) ∘ Iop ) = ( 𝐹 ‘ 𝑘 ) )
129	36 128	syl	⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ 𝑘 ) ∘ Iop ) = ( 𝐹 ‘ 𝑘 ) )
130	129	oveq1d	⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝐹 ‘ 𝑘 ) ∘ Iop ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
131	127 130	eqtrd	⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) )
132	122 131	oveq12d	⊢ ( 𝑘 ∈ ℕ → ( ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) −op ( ( 𝐹 ‘ 𝑘 ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
133	36 46	jctil	⊢ ( 𝑘 ∈ ℕ → ( Iop : ℋ ⟶ ℋ ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ) )
134		hosubadd4	⊢ ( ( ( Iop : ℋ ⟶ ℋ ∧ ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ) ∧ ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ ∧ ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ) ) → ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) −op ( ( 𝐹 ‘ 𝑘 ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) +op ( 𝐹 ‘ 𝑘 ) ) ) )
135	133 36 42 134	syl12anc	⊢ ( 𝑘 ∈ ℕ → ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) −op ( ( 𝐹 ‘ 𝑘 ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) +op ( 𝐹 ‘ 𝑘 ) ) ) )
136	132 135	eqtrd	⊢ ( 𝑘 ∈ ℕ → ( ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) +op ( 𝐹 ‘ 𝑘 ) ) ) )
137		ho2times	⊢ ( ( 𝐹 ‘ 𝑘 ) : ℋ ⟶ ℋ → ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) +op ( 𝐹 ‘ 𝑘 ) ) )
138	36 137	syl	⊢ ( 𝑘 ∈ ℕ → ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) +op ( 𝐹 ‘ 𝑘 ) ) )
139	138	oveq2d	⊢ ( 𝑘 ∈ ℕ → ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) = ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) +op ( 𝐹 ‘ 𝑘 ) ) ) )
140		hoaddsubass	⊢ ( ( Iop : ℋ ⟶ ℋ ∧ ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ∧ ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ) → ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) = ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) )
141	46 140	mp3an1	⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ∧ ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) : ℋ ⟶ ℋ ) → ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) = ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) )
142	42 38 141	syl2anc	⊢ ( 𝑘 ∈ ℕ → ( ( Iop +op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) = ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) )
143	136 139 142	3eqtr2d	⊢ ( 𝑘 ∈ ℕ → ( ( Iop ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) ) = ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) )
144	111 143	eqtrd	⊢ ( 𝑘 ∈ ℕ → ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) = ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) )
145	144	oveq1d	⊢ ( 𝑘 ∈ ℕ → ( ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) +op ( Iop −op 𝑇 ) ) = ( ( Iop +op ( ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) −op ( 2 ·op ( 𝐹 ‘ 𝑘 ) ) ) ) +op ( Iop −op 𝑇 ) ) )
146	1 2 3	opsqrlem5	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
147	146	oveq2d	⊢ ( 𝑘 ∈ ℕ → ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( Iop −op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
148	147	oveq2d	⊢ ( 𝑘 ∈ ℕ → ( 2 ·op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) = ( 2 ·op ( Iop −op ( ( 𝐹 ‘ 𝑘 ) +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( ( 𝐹 ‘ 𝑘 ) ∘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) ) )
149	106 145 148	3eqtr4d	⊢ ( 𝑘 ∈ ℕ → ( ( ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ∘ ( Iop −op ( 𝐹 ‘ 𝑘 ) ) ) +op ( Iop −op 𝑇 ) ) = ( 2 ·op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
150	33 149	breqtrd	⊢ ( 𝑘 ∈ ℕ → 0hop ≤op ( 2 ·op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
151		peano2nn	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
152	15	ffvelrni	⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ HrmOp )
153	151 152	syl	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ HrmOp )
154		hmopd	⊢ ( ( Iop ∈ HrmOp ∧ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ HrmOp ) → ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ HrmOp )
155	14 153 154	sylancr	⊢ ( 𝑘 ∈ ℕ → ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ HrmOp )
156		2re	⊢ 2 ∈ ℝ
157		2pos	⊢ 0 < 2
158		leopmul	⊢ ( ( 2 ∈ ℝ ∧ ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ HrmOp ∧ 0 < 2 ) → ( 0hop ≤op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ 0hop ≤op ( 2 ·op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
159	156 157 158	mp3an13	⊢ ( ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ HrmOp → ( 0hop ≤op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ 0hop ≤op ( 2 ·op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
160	155 159	syl	⊢ ( 𝑘 ∈ ℕ → ( 0hop ≤op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ 0hop ≤op ( 2 ·op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
161	150 160	mpbird	⊢ ( 𝑘 ∈ ℕ → 0hop ≤op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
162		leop3	⊢ ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ HrmOp ∧ Iop ∈ HrmOp ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤op Iop ↔ 0hop ≤op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
163	153 14 162	sylancl	⊢ ( 𝑘 ∈ ℕ → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤op Iop ↔ 0hop ≤op ( Iop −op ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
164	161 163	mpbird	⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤op Iop )
165	6 8 10 13 164	nn1suc	⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) ≤op Iop )