Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . 3
|
2 | 1 | breq1d 4663 |
. 2
|
3 | | fveq2 6191 |
. . 3
|
4 | 3 | breq1d 4663 |
. 2
|
5 | | fveq2 6191 |
. . 3
|
6 | 5 | breq1d 4663 |
. 2
|
7 | | opsqrlem2.1 |
. . . 4
|
8 | | opsqrlem2.2 |
. . . 4
|
9 | | opsqrlem2.3 |
. . . 4
|
10 | 7, 8, 9 | opsqrlem2 29000 |
. . 3
|
11 | | idleop 28990 |
. . 3
|
12 | 10, 11 | eqbrtri 4674 |
. 2
|
13 | | idhmop 28841 |
. . . . . . . 8
|
14 | 7, 8, 9 | opsqrlem4 29002 |
. . . . . . . . 9
|
15 | 14 | ffvelrni 6358 |
. . . . . . . 8
|
16 | | hmopd 28881 |
. . . . . . . 8
|
17 | 13, 15, 16 | sylancr 695 |
. . . . . . 7
|
18 | | eqid 2622 |
. . . . . . . 8
|
19 | | hmopco 28882 |
. . . . . . . 8
|
20 | 18, 19 | mp3an3 1413 |
. . . . . . 7
|
21 | 17, 17, 20 | syl2anc 693 |
. . . . . 6
|
22 | | leopsq 28988 |
. . . . . . 7
|
23 | 17, 22 | syl 17 |
. . . . . 6
|
24 | | opsqrlem6.4 |
. . . . . . . 8
|
25 | | leop3 28984 |
. . . . . . . . 9
|
26 | 7, 13, 25 | mp2an 708 |
. . . . . . . 8
|
27 | 24, 26 | mpbi 220 |
. . . . . . 7
|
28 | | hmopd 28881 |
. . . . . . . . 9
|
29 | 13, 7, 28 | mp2an 708 |
. . . . . . . 8
|
30 | | leopadd 28991 |
. . . . . . . 8
|
31 | 29, 30 | mpanl2 717 |
. . . . . . 7
|
32 | 27, 31 | mpanr2 720 |
. . . . . 6
|
33 | 21, 23, 32 | syl2anc 693 |
. . . . 5
|
34 | | 2cn 11091 |
. . . . . . . . . 10
|
35 | | hmopf 28733 |
. . . . . . . . . . 11
|
36 | 15, 35 | syl 17 |
. . . . . . . . . 10
|
37 | | homulcl 28618 |
. . . . . . . . . 10
|
38 | 34, 36, 37 | sylancr 695 |
. . . . . . . . 9
|
39 | | hmopf 28733 |
. . . . . . . . . . 11
|
40 | 7, 39 | ax-mp 5 |
. . . . . . . . . 10
|
41 | | fco 6058 |
. . . . . . . . . . 11
|
42 | 36, 36, 41 | syl2anc 693 |
. . . . . . . . . 10
|
43 | | hosubcl 28632 |
. . . . . . . . . 10
|
44 | 40, 42, 43 | sylancr 695 |
. . . . . . . . 9
|
45 | | hmopf 28733 |
. . . . . . . . . . . 12
|
46 | 13, 45 | ax-mp 5 |
. . . . . . . . . . 11
|
47 | | homulcl 28618 |
. . . . . . . . . . 11
|
48 | 34, 46, 47 | mp2an 708 |
. . . . . . . . . 10
|
49 | | hosubsub4 28677 |
. . . . . . . . . 10
|
50 | 48, 49 | mp3an1 1411 |
. . . . . . . . 9
|
51 | 38, 44, 50 | syl2anc 693 |
. . . . . . . 8
|
52 | | hosubcl 28632 |
. . . . . . . . . . . . . . 15
|
53 | 42, 38, 52 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
54 | | hoadd32 28642 |
. . . . . . . . . . . . . . 15
|
55 | 46, 46, 54 | mp3an13 1415 |
. . . . . . . . . . . . . 14
|
56 | 53, 55 | syl 17 |
. . . . . . . . . . . . 13
|
57 | | ho2times 28678 |
. . . . . . . . . . . . . . 15
|
58 | 46, 57 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
59 | 58 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
60 | 56, 59 | syl6eqr 2674 |
. . . . . . . . . . . 12
|
61 | | hoaddsubass 28674 |
. . . . . . . . . . . . . 14
|
62 | 48, 61 | mp3an1 1411 |
. . . . . . . . . . . . 13
|
63 | 42, 38, 62 | syl2anc 693 |
. . . . . . . . . . . 12
|
64 | 60, 63 | eqtr4d 2659 |
. . . . . . . . . . 11
|
65 | 64 | oveq1d 6665 |
. . . . . . . . . 10
|
66 | | hoaddcl 28617 |
. . . . . . . . . . . 12
|
67 | 46, 53, 66 | sylancr 695 |
. . . . . . . . . . 11
|
68 | | hoaddsubass 28674 |
. . . . . . . . . . . 12
|
69 | 46, 40, 68 | mp3an23 1416 |
. . . . . . . . . . 11
|
70 | 67, 69 | syl 17 |
. . . . . . . . . 10
|
71 | | hoaddcl 28617 |
. . . . . . . . . . . 12
|
72 | 48, 42, 71 | sylancr 695 |
. . . . . . . . . . 11
|
73 | | hosubsub4 28677 |
. . . . . . . . . . . 12
|
74 | 40, 73 | mp3an3 1413 |
. . . . . . . . . . 11
|
75 | 72, 38, 74 | syl2anc 693 |
. . . . . . . . . 10
|
76 | 65, 70, 75 | 3eqtr3d 2664 |
. . . . . . . . 9
|
77 | | hosubadd4 28673 |
. . . . . . . . . . . 12
|
78 | 40, 77 | mpanr1 719 |
. . . . . . . . . . 11
|
79 | 48, 78 | mpanl1 716 |
. . . . . . . . . 10
|
80 | 38, 42, 79 | syl2anc 693 |
. . . . . . . . 9
|
81 | 76, 80 | eqtr4d 2659 |
. . . . . . . 8
|
82 | | halfcn 11247 |
. . . . . . . . . . . 12
|
83 | | homulcl 28618 |
. . . . . . . . . . . 12
|
84 | 82, 44, 83 | sylancr 695 |
. . . . . . . . . . 11
|
85 | | hoadddi 28662 |
. . . . . . . . . . . 12
|
86 | 34, 85 | mp3an1 1411 |
. . . . . . . . . . 11
|
87 | 36, 84, 86 | syl2anc 693 |
. . . . . . . . . 10
|
88 | | 2ne0 11113 |
. . . . . . . . . . . . . 14
|
89 | 34, 88 | recidi 10756 |
. . . . . . . . . . . . 13
|
90 | 89 | oveq1i 6660 |
. . . . . . . . . . . 12
|
91 | | homulass 28661 |
. . . . . . . . . . . . . 14
|
92 | 34, 82, 91 | mp3an12 1414 |
. . . . . . . . . . . . 13
|
93 | 44, 92 | syl 17 |
. . . . . . . . . . . 12
|
94 | | homulid2 28659 |
. . . . . . . . . . . . 13
|
95 | 44, 94 | syl 17 |
. . . . . . . . . . . 12
|
96 | 90, 93, 95 | 3eqtr3a 2680 |
. . . . . . . . . . 11
|
97 | 96 | oveq2d 6666 |
. . . . . . . . . 10
|
98 | 87, 97 | eqtrd 2656 |
. . . . . . . . 9
|
99 | 98 | oveq2d 6666 |
. . . . . . . 8
|
100 | 51, 81, 99 | 3eqtr4d 2666 |
. . . . . . 7
|
101 | | hoaddcl 28617 |
. . . . . . . . 9
|
102 | 36, 84, 101 | syl2anc 693 |
. . . . . . . 8
|
103 | | hosubdi 28667 |
. . . . . . . . 9
|
104 | 34, 46, 103 | mp3an12 1414 |
. . . . . . . 8
|
105 | 102, 104 | syl 17 |
. . . . . . 7
|
106 | 100, 105 | eqtr4d 2659 |
. . . . . 6
|
107 | | hosubcl 28632 |
. . . . . . . . . 10
|
108 | 46, 36, 107 | sylancr 695 |
. . . . . . . . 9
|
109 | | hocsubdir 28644 |
. . . . . . . . . 10
|
110 | 46, 109 | mp3an1 1411 |
. . . . . . . . 9
|
111 | 36, 108, 110 | syl2anc 693 |
. . . . . . . 8
|
112 | | hmoplin 28801 |
. . . . . . . . . . . . . . 15
|
113 | 13, 112 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
114 | | hoddi 28849 |
. . . . . . . . . . . . . 14
|
115 | 113, 46, 114 | mp3an12 1414 |
. . . . . . . . . . . . 13
|
116 | 36, 115 | syl 17 |
. . . . . . . . . . . 12
|
117 | 46 | hoid1i 28648 |
. . . . . . . . . . . . . 14
|
118 | 117 | a1i 11 |
. . . . . . . . . . . . 13
|
119 | | hoico2 28616 |
. . . . . . . . . . . . . 14
|
120 | 36, 119 | syl 17 |
. . . . . . . . . . . . 13
|
121 | 118, 120 | oveq12d 6668 |
. . . . . . . . . . . 12
|
122 | 116, 121 | eqtrd 2656 |
. . . . . . . . . . 11
|
123 | | hmoplin 28801 |
. . . . . . . . . . . . . 14
|
124 | 15, 123 | syl 17 |
. . . . . . . . . . . . 13
|
125 | | hoddi 28849 |
. . . . . . . . . . . . . 14
|
126 | 46, 125 | mp3an2 1412 |
. . . . . . . . . . . . 13
|
127 | 124, 36, 126 | syl2anc 693 |
. . . . . . . . . . . 12
|
128 | | hoico1 28615 |
. . . . . . . . . . . . . 14
|
129 | 36, 128 | syl 17 |
. . . . . . . . . . . . 13
|
130 | 129 | oveq1d 6665 |
. . . . . . . . . . . 12
|
131 | 127, 130 | eqtrd 2656 |
. . . . . . . . . . 11
|
132 | 122, 131 | oveq12d 6668 |
. . . . . . . . . 10
|
133 | 36, 46 | jctil 560 |
. . . . . . . . . . 11
|
134 | | hosubadd4 28673 |
. . . . . . . . . . 11
|
135 | 133, 36, 42, 134 | syl12anc 1324 |
. . . . . . . . . 10
|
136 | 132, 135 | eqtrd 2656 |
. . . . . . . . 9
|
137 | | ho2times 28678 |
. . . . . . . . . . 11
|
138 | 36, 137 | syl 17 |
. . . . . . . . . 10
|
139 | 138 | oveq2d 6666 |
. . . . . . . . 9
|
140 | | hoaddsubass 28674 |
. . . . . . . . . . 11
|
141 | 46, 140 | mp3an1 1411 |
. . . . . . . . . 10
|
142 | 42, 38, 141 | syl2anc 693 |
. . . . . . . . 9
|
143 | 136, 139,
142 | 3eqtr2d 2662 |
. . . . . . . 8
|
144 | 111, 143 | eqtrd 2656 |
. . . . . . 7
|
145 | 144 | oveq1d 6665 |
. . . . . 6
|
146 | 7, 8, 9 | opsqrlem5 29003 |
. . . . . . . 8
|
147 | 146 | oveq2d 6666 |
. . . . . . 7
|
148 | 147 | oveq2d 6666 |
. . . . . 6
|
149 | 106, 145,
148 | 3eqtr4d 2666 |
. . . . 5
|
150 | 33, 149 | breqtrd 4679 |
. . . 4
|
151 | | peano2nn 11032 |
. . . . . . 7
|
152 | 14 | ffvelrni 6358 |
. . . . . . 7
|
153 | 151, 152 | syl 17 |
. . . . . 6
|
154 | | hmopd 28881 |
. . . . . 6
|
155 | 13, 153, 154 | sylancr 695 |
. . . . 5
|
156 | | 2re 11090 |
. . . . . 6
|
157 | | 2pos 11112 |
. . . . . 6
|
158 | | leopmul 28993 |
. . . . . 6
|
159 | 156, 157,
158 | mp3an13 1415 |
. . . . 5
|
160 | 155, 159 | syl 17 |
. . . 4
|
161 | 150, 160 | mpbird 247 |
. . 3
|
162 | | leop3 28984 |
. . . 4
|
163 | 153, 13, 162 | sylancl 694 |
. . 3
|
164 | 161, 163 | mpbird 247 |
. 2
|
165 | 2, 4, 6, 12, 164 | nn1suc 11041 |
1
|