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 ffvelcdmi 
 |-  ( 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 2thalfe1 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
89 88 oveq1i 
 |-  ( ( 2 x. ( 1 / 2 ) ) .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) ) = ( 1 .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) )
90 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 ) ) ) ) ) )
91 34 82 90 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 ) ) ) ) ) )
92 44 91 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 ) ) ) ) ) )
93 homullid 
 |-  ( ( 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 ) ) ) )
94 44 93 syl 
 |-  ( k e. NN -> ( 1 .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) ) = ( T -op ( ( F ` k ) o. ( F ` k ) ) ) )
95 89 92 94 3eqtr3a 
 |-  ( k e. NN -> ( 2 .op ( ( 1 / 2 ) .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) ) ) = ( T -op ( ( F ` k ) o. ( F ` k ) ) ) )
96 95 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 ) ) ) ) )
97 87 96 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 ) ) ) ) )
98 97 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 ) ) ) ) ) )
99 51 81 98 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 ) ) ) ) ) ) ) )
100 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 )
101 36 84 100 syl2anc 
 |-  ( k e. NN -> ( ( F ` k ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) ) ) : ~H --> ~H )
102 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 ) ) ) ) ) ) ) )
103 34 46 102 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 ) ) ) ) ) ) ) )
104 101 103 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 ) ) ) ) ) ) ) )
105 99 104 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 ) ) ) ) ) ) ) )
106 hosubcl 
 |-  ( ( Iop : ~H --> ~H /\ ( F ` k ) : ~H --> ~H ) -> ( Iop -op ( F ` k ) ) : ~H --> ~H )
107 46 36 106 sylancr 
 |-  ( k e. NN -> ( Iop -op ( F ` k ) ) : ~H --> ~H )
108 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 ) ) ) ) )
109 46 108 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 ) ) ) ) )
110 36 107 109 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 ) ) ) ) )
111 hmoplin 
 |-  ( Iop e. HrmOp -> Iop e. LinOp )
112 14 111 ax-mp 
 |-  Iop e. LinOp
113 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 ) ) ) )
114 112 46 113 mp3an12 
 |-  ( ( F ` k ) : ~H --> ~H -> ( Iop o. ( Iop -op ( F ` k ) ) ) = ( ( Iop o. Iop ) -op ( Iop o. ( F ` k ) ) ) )
115 36 114 syl 
 |-  ( k e. NN -> ( Iop o. ( Iop -op ( F ` k ) ) ) = ( ( Iop o. Iop ) -op ( Iop o. ( F ` k ) ) ) )
116 46 hoid1i 
 |-  ( Iop o. Iop ) = Iop
117 116 a1i 
 |-  ( k e. NN -> ( Iop o. Iop ) = Iop )
118 hoico2 
 |-  ( ( F ` k ) : ~H --> ~H -> ( Iop o. ( F ` k ) ) = ( F ` k ) )
119 36 118 syl 
 |-  ( k e. NN -> ( Iop o. ( F ` k ) ) = ( F ` k ) )
120 117 119 oveq12d 
 |-  ( k e. NN -> ( ( Iop o. Iop ) -op ( Iop o. ( F ` k ) ) ) = ( Iop -op ( F ` k ) ) )
121 115 120 eqtrd 
 |-  ( k e. NN -> ( Iop o. ( Iop -op ( F ` k ) ) ) = ( Iop -op ( F ` k ) ) )
122 hmoplin 
 |-  ( ( F ` k ) e. HrmOp -> ( F ` k ) e. LinOp )
123 16 122 syl 
 |-  ( k e. NN -> ( F ` k ) e. LinOp )
124 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 ) ) ) )
125 46 124 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 ) ) ) )
126 123 36 125 syl2anc 
 |-  ( k e. NN -> ( ( F ` k ) o. ( Iop -op ( F ` k ) ) ) = ( ( ( F ` k ) o. Iop ) -op ( ( F ` k ) o. ( F ` k ) ) ) )
127 hoico1 
 |-  ( ( F ` k ) : ~H --> ~H -> ( ( F ` k ) o. Iop ) = ( F ` k ) )
128 36 127 syl 
 |-  ( k e. NN -> ( ( F ` k ) o. Iop ) = ( F ` k ) )
129 128 oveq1d 
 |-  ( k e. NN -> ( ( ( F ` k ) o. Iop ) -op ( ( F ` k ) o. ( F ` k ) ) ) = ( ( F ` k ) -op ( ( F ` k ) o. ( F ` k ) ) ) )
130 126 129 eqtrd 
 |-  ( k e. NN -> ( ( F ` k ) o. ( Iop -op ( F ` k ) ) ) = ( ( F ` k ) -op ( ( F ` k ) o. ( F ` k ) ) ) )
131 121 130 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 ) ) ) ) )
132 36 46 jctil 
 |-  ( k e. NN -> ( Iop : ~H --> ~H /\ ( F ` k ) : ~H --> ~H ) )
133 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 ) ) ) )
134 132 36 42 133 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 ) ) ) )
135 131 134 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 ) ) ) )
136 ho2times 
 |-  ( ( F ` k ) : ~H --> ~H -> ( 2 .op ( F ` k ) ) = ( ( F ` k ) +op ( F ` k ) ) )
137 36 136 syl 
 |-  ( k e. NN -> ( 2 .op ( F ` k ) ) = ( ( F ` k ) +op ( F ` k ) ) )
138 137 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 ) ) ) )
139 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 ) ) ) ) )
140 46 139 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 ) ) ) ) )
141 42 38 140 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 ) ) ) ) )
142 135 138 141 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 ) ) ) ) )
143 110 142 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 ) ) ) ) )
144 143 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 ) ) )
145 1 2 3 opsqrlem5 
 |-  ( k e. NN -> ( F ` ( k + 1 ) ) = ( ( F ` k ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) ) ) )
146 145 oveq2d 
 |-  ( k e. NN -> ( Iop -op ( F ` ( k + 1 ) ) ) = ( Iop -op ( ( F ` k ) +op ( ( 1 / 2 ) .op ( T -op ( ( F ` k ) o. ( F ` k ) ) ) ) ) ) )
147 146 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 ) ) ) ) ) ) ) )
148 105 144 147 3eqtr4d 
 |-  ( k e. NN -> ( ( ( Iop -op ( F ` k ) ) o. ( Iop -op ( F ` k ) ) ) +op ( Iop -op T ) ) = ( 2 .op ( Iop -op ( F ` ( k + 1 ) ) ) ) )
149 33 148 breqtrd 
 |-  ( k e. NN -> 0hop <_op ( 2 .op ( Iop -op ( F ` ( k + 1 ) ) ) ) )
150 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
151 15 ffvelcdmi 
 |-  ( ( k + 1 ) e. NN -> ( F ` ( k + 1 ) ) e. HrmOp )
152 150 151 syl 
 |-  ( k e. NN -> ( F ` ( k + 1 ) ) e. HrmOp )
153 hmopd 
 |-  ( ( Iop e. HrmOp /\ ( F ` ( k + 1 ) ) e. HrmOp ) -> ( Iop -op ( F ` ( k + 1 ) ) ) e. HrmOp )
154 14 152 153 sylancr 
 |-  ( k e. NN -> ( Iop -op ( F ` ( k + 1 ) ) ) e. HrmOp )
155 2re 
 |-  2 e. RR
156 2pos 
 |-  0 < 2
157 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 ) ) ) ) ) )
158 155 156 157 mp3an13 
 |-  ( ( Iop -op ( F ` ( k + 1 ) ) ) e. HrmOp -> ( 0hop <_op ( Iop -op ( F ` ( k + 1 ) ) ) <-> 0hop <_op ( 2 .op ( Iop -op ( F ` ( k + 1 ) ) ) ) ) )
159 154 158 syl 
 |-  ( k e. NN -> ( 0hop <_op ( Iop -op ( F ` ( k + 1 ) ) ) <-> 0hop <_op ( 2 .op ( Iop -op ( F ` ( k + 1 ) ) ) ) ) )
160 149 159 mpbird 
 |-  ( k e. NN -> 0hop <_op ( Iop -op ( F ` ( k + 1 ) ) ) )
161 leop3 
 |-  ( ( ( F ` ( k + 1 ) ) e. HrmOp /\ Iop e. HrmOp ) -> ( ( F ` ( k + 1 ) ) <_op Iop <-> 0hop <_op ( Iop -op ( F ` ( k + 1 ) ) ) ) )
162 152 14 161 sylancl 
 |-  ( k e. NN -> ( ( F ` ( k + 1 ) ) <_op Iop <-> 0hop <_op ( Iop -op ( F ` ( k + 1 ) ) ) ) )
163 160 162 mpbird 
 |-  ( k e. NN -> ( F ` ( k + 1 ) ) <_op Iop )
164 6 8 10 13 163 nn1suc 
 |-  ( N e. NN -> ( F ` N ) <_op Iop )