Metamath Proof Explorer

Theorem opsqrlem6

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

Ref Expression
Hypotheses opsqrlem2.1 
|- T e. HrmOp
opsqrlem2.2 
|- S = ( x e. HrmOp , y e. HrmOp |-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
opsqrlem2.3 
|- F = seq 1 ( S , ( NN X. { 0hop } ) )
opsqrlem6.4 
|- T <_op Iop
Assertion opsqrlem6 
|- ( N e. NN -> ( F ` N ) <_op Iop )

Proof

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