Step | Hyp | Ref
| Expression |
1 | | tgcgrxfr.p |
. . 3
|
2 | | tgcgrxfr.m |
. . 3
|
3 | | tgcgrxfr.r |
. . 3
cgrG |
4 | | tgcgrxfr.g |
. . 3
TarskiG |
5 | | fzo0ssnn0 12548 |
. . . . 5
..^ |
6 | | nn0ssre 11296 |
. . . . 5
|
7 | 5, 6 | sstri 3612 |
. . . 4
..^ |
8 | 7 | a1i 11 |
. . 3
..^ |
9 | | tgcgr4.a |
. . . . . 6
|
10 | | tgcgr4.b |
. . . . . 6
|
11 | | tgcgr4.c |
. . . . . 6
|
12 | | tgcgr4.d |
. . . . . 6
|
13 | 9, 10, 11, 12 | s4cld 13618 |
. . . . 5
Word |
14 | | wrdf 13310 |
. . . . 5
Word ..^ |
15 | 13, 14 | syl 17 |
. . . 4
..^ |
16 | | s4len 13644 |
. . . . . 6
|
17 | 16 | oveq2i 6661 |
. . . . 5
..^ ..^ |
18 | 17 | feq2i 6037 |
. . . 4
..^
..^ |
19 | 15, 18 | sylib 208 |
. . 3
..^ |
20 | | tgcgr4.w |
. . . . . 6
|
21 | | tgcgr4.x |
. . . . . 6
|
22 | | tgcgr4.y |
. . . . . 6
|
23 | | tgcgr4.z |
. . . . . 6
|
24 | 20, 21, 22, 23 | s4cld 13618 |
. . . . 5
Word |
25 | | wrdf 13310 |
. . . . 5
Word ..^ |
26 | 24, 25 | syl 17 |
. . . 4
..^ |
27 | | s4len 13644 |
. . . . . 6
|
28 | 27 | oveq2i 6661 |
. . . . 5
..^ ..^ |
29 | 28 | feq2i 6037 |
. . . 4
..^
..^ |
30 | 26, 29 | sylib 208 |
. . 3
..^ |
31 | 1, 2, 3, 4, 8, 19,
30 | iscgrglt 25409 |
. 2
|
32 | | fdm 6051 |
. . . . . . . 8
..^
..^ |
33 | 19, 32 | syl 17 |
. . . . . . 7
..^ |
34 | | 3p1e4 11153 |
. . . . . . . . 9
|
35 | 34 | oveq2i 6661 |
. . . . . . . 8
..^ ..^ |
36 | | 3nn0 11310 |
. . . . . . . . . 10
|
37 | | nn0uz 11722 |
. . . . . . . . . 10
|
38 | 36, 37 | eleqtri 2699 |
. . . . . . . . 9
|
39 | | fzosplitsn 12576 |
. . . . . . . . 9
..^ ..^ |
40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
..^ ..^ |
41 | 35, 40 | eqtr3i 2646 |
. . . . . . 7
..^ ..^ |
42 | 33, 41 | syl6eq 2672 |
. . . . . 6
..^ |
43 | 42 | raleqdv 3144 |
. . . . 5
..^ |
44 | | breq2 4657 |
. . . . . . . 8
|
45 | | fveq2 6191 |
. . . . . . . . . 10
|
46 | 45 | oveq2d 6666 |
. . . . . . . . 9
|
47 | | fveq2 6191 |
. . . . . . . . . 10
|
48 | 47 | oveq2d 6666 |
. . . . . . . . 9
|
49 | 46, 48 | eqeq12d 2637 |
. . . . . . . 8
|
50 | 44, 49 | imbi12d 334 |
. . . . . . 7
|
51 | 50 | ralunsn 4422 |
. . . . . 6
..^
..^ |
52 | 36, 51 | ax-mp 5 |
. . . . 5
..^
..^ |
53 | 43, 52 | syl6bb 276 |
. . . 4
..^ |
54 | 53 | ralbidv 2986 |
. . 3
..^ |
55 | 42 | raleqdv 3144 |
. . . 4
..^
..^ ..^ |
56 | | fzo0ssnn0 12548 |
. . . . . . . . . . . . . . . 16
..^ |
57 | 56, 6 | sstri 3612 |
. . . . . . . . . . . . . . 15
..^ |
58 | | simpr 477 |
. . . . . . . . . . . . . . 15
..^ ..^ |
59 | 57, 58 | sseldi 3601 |
. . . . . . . . . . . . . 14
..^ |
60 | | simpl 473 |
. . . . . . . . . . . . . . 15
..^ |
61 | 6, 36 | sselii 3600 |
. . . . . . . . . . . . . . 15
|
62 | 60, 61 | syl6eqel 2709 |
. . . . . . . . . . . . . 14
..^ |
63 | | elfzolt2 12479 |
. . . . . . . . . . . . . . . 16
..^
|
64 | 63 | adantl 482 |
. . . . . . . . . . . . . . 15
..^
|
65 | 64, 60 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
..^
|
66 | | ltnsym 10135 |
. . . . . . . . . . . . . . 15
|
67 | 66 | imp 445 |
. . . . . . . . . . . . . 14
|
68 | 59, 62, 65, 67 | syl21anc 1325 |
. . . . . . . . . . . . 13
..^
|
69 | 68 | pm2.21d 118 |
. . . . . . . . . . . 12
..^ |
70 | | tbtru 1494 |
. . . . . . . . . . . 12
|
71 | 69, 70 | sylib 208 |
. . . . . . . . . . 11
..^
|
72 | 71 | ralbidva 2985 |
. . . . . . . . . 10
..^
..^ |
73 | | 3nn 11186 |
. . . . . . . . . . . . 13
|
74 | | lbfzo0 12507 |
. . . . . . . . . . . . 13
..^ |
75 | 73, 74 | mpbir 221 |
. . . . . . . . . . . 12
..^ |
76 | 75 | ne0ii 3923 |
. . . . . . . . . . 11
..^ |
77 | | r19.3rzv 4064 |
. . . . . . . . . . 11
..^
..^ |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . 10
..^ |
79 | 72, 78 | syl6bbr 278 |
. . . . . . . . 9
..^
|
80 | | breq1 4656 |
. . . . . . . . . . . 12
|
81 | 61 | ltnri 10146 |
. . . . . . . . . . . . 13
|
82 | 81 | bifal 1497 |
. . . . . . . . . . . 12
|
83 | 80, 82 | syl6bb 276 |
. . . . . . . . . . 11
|
84 | 83 | imbi1d 331 |
. . . . . . . . . 10
|
85 | | falim 1498 |
. . . . . . . . . . 11
|
86 | 85 | bitru 1496 |
. . . . . . . . . 10
|
87 | 84, 86 | syl6bb 276 |
. . . . . . . . 9
|
88 | 79, 87 | anbi12d 747 |
. . . . . . . 8
..^ |
89 | | anidm 676 |
. . . . . . . 8
|
90 | 88, 89 | syl6bb 276 |
. . . . . . 7
..^ |
91 | 90 | ralunsn 4422 |
. . . . . 6
..^ ..^ ..^ ..^ |
92 | 36, 91 | ax-mp 5 |
. . . . 5
..^ ..^ ..^ ..^ |
93 | | ancom 466 |
. . . . 5
..^ ..^
..^ ..^ |
94 | | truan 1501 |
. . . . 5
..^ ..^ ..^ ..^ |
95 | 92, 93, 94 | 3bitri 286 |
. . . 4
..^ ..^
..^ ..^ |
96 | 55, 95 | syl6bb 276 |
. . 3
..^
..^ ..^ |
97 | 54, 96 | bitrd 268 |
. 2
..^ ..^ |
98 | | r19.26 3064 |
. . 3
..^
..^ ..^ ..^ ..^ |
99 | 9, 10, 11 | s3cld 13617 |
. . . . . . . . 9
Word |
100 | | wrdf 13310 |
. . . . . . . . 9
Word ..^ |
101 | 99, 100 | syl 17 |
. . . . . . . 8
..^ |
102 | | s3len 13639 |
. . . . . . . . . 10
|
103 | 102 | oveq2i 6661 |
. . . . . . . . 9
..^ ..^ |
104 | 103 | feq2i 6037 |
. . . . . . . 8
..^
..^ |
105 | 101, 104 | sylib 208 |
. . . . . . 7
..^ |
106 | | fdm 6051 |
. . . . . . 7
..^
..^ |
107 | 105, 106 | syl 17 |
. . . . . 6
..^ |
108 | | raleq 3138 |
. . . . . . 7
..^
..^
|
109 | 105, 106,
108 | 3syl 18 |
. . . . . 6
..^
|
110 | 107, 109 | raleqbidv 3152 |
. . . . 5
..^
..^
|
111 | 57 | a1i 11 |
. . . . . 6
..^ |
112 | 20, 21, 22 | s3cld 13617 |
. . . . . . . 8
Word |
113 | | wrdf 13310 |
. . . . . . . 8
Word ..^ |
114 | 112, 113 | syl 17 |
. . . . . . 7
..^ |
115 | | s3len 13639 |
. . . . . . . . 9
|
116 | 115 | oveq2i 6661 |
. . . . . . . 8
..^ ..^ |
117 | 116 | feq2i 6037 |
. . . . . . 7
..^
..^ |
118 | 114, 117 | sylib 208 |
. . . . . 6
..^ |
119 | 1, 2, 3, 4, 111, 105, 118 | iscgrglt 25409 |
. . . . 5
|
120 | | df-s4 13595 |
. . . . . . . . . . 11
++ |
121 | 120 | fveq1i 6192 |
. . . . . . . . . 10
++
|
122 | 9 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
123 | 10 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
124 | 11 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
125 | 122, 123,
124 | s3cld 13617 |
. . . . . . . . . . 11
..^ ..^
Word |
126 | 12 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
127 | 126 | s1cld 13383 |
. . . . . . . . . . 11
..^ ..^
Word
|
128 | | simprl 794 |
. . . . . . . . . . . 12
..^ ..^
..^ |
129 | 128, 103 | syl6eleqr 2712 |
. . . . . . . . . . 11
..^ ..^
..^ |
130 | | ccatval1 13361 |
. . . . . . . . . . 11
Word Word ..^ ++ |
131 | 125, 127,
129, 130 | syl3anc 1326 |
. . . . . . . . . 10
..^ ..^
++
|
132 | 121, 131 | syl5eq 2668 |
. . . . . . . . 9
..^ ..^
|
133 | 120 | fveq1i 6192 |
. . . . . . . . . 10
++
|
134 | | simprr 796 |
. . . . . . . . . . . 12
..^ ..^
..^ |
135 | 134, 103 | syl6eleqr 2712 |
. . . . . . . . . . 11
..^ ..^
..^ |
136 | | ccatval1 13361 |
. . . . . . . . . . 11
Word Word ..^ ++ |
137 | 125, 127,
135, 136 | syl3anc 1326 |
. . . . . . . . . 10
..^ ..^
++
|
138 | 133, 137 | syl5eq 2668 |
. . . . . . . . 9
..^ ..^
|
139 | 132, 138 | oveq12d 6668 |
. . . . . . . 8
..^ ..^
|
140 | | df-s4 13595 |
. . . . . . . . . . 11
++ |
141 | 140 | fveq1i 6192 |
. . . . . . . . . 10
++
|
142 | 20 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
143 | 21 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
144 | 22 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
145 | 142, 143,
144 | s3cld 13617 |
. . . . . . . . . . 11
..^ ..^
Word |
146 | 23 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
|
147 | 146 | s1cld 13383 |
. . . . . . . . . . 11
..^ ..^
Word
|
148 | 128, 116 | syl6eleqr 2712 |
. . . . . . . . . . 11
..^ ..^
..^ |
149 | | ccatval1 13361 |
. . . . . . . . . . 11
Word Word ..^ ++ |
150 | 145, 147,
148, 149 | syl3anc 1326 |
. . . . . . . . . 10
..^ ..^
++
|
151 | 141, 150 | syl5eq 2668 |
. . . . . . . . 9
..^ ..^
|
152 | 140 | fveq1i 6192 |
. . . . . . . . . 10
++
|
153 | 134, 116 | syl6eleqr 2712 |
. . . . . . . . . . 11
..^ ..^
..^ |
154 | | ccatval1 13361 |
. . . . . . . . . . 11
Word Word ..^ ++ |
155 | 145, 147,
153, 154 | syl3anc 1326 |
. . . . . . . . . 10
..^ ..^
++
|
156 | 152, 155 | syl5eq 2668 |
. . . . . . . . 9
..^ ..^
|
157 | 151, 156 | oveq12d 6668 |
. . . . . . . 8
..^ ..^
|
158 | 139, 157 | eqeq12d 2637 |
. . . . . . 7
..^ ..^
|
159 | 158 | imbi2d 330 |
. . . . . 6
..^ ..^
|
160 | 159 | 2ralbidva 2988 |
. . . . 5
..^ ..^
..^ ..^
|
161 | 110, 119,
160 | 3bitr4rd 301 |
. . . 4
..^ ..^
|
162 | | fzo0to3tp 12554 |
. . . . . 6
..^ |
163 | | raleq 3138 |
. . . . . 6
..^ ..^
|
164 | 162, 163 | mp1i 13 |
. . . . 5
..^
|
165 | | 3pos 11114 |
. . . . . . . . . 10
|
166 | | breq1 4656 |
. . . . . . . . . 10
|
167 | 165, 166 | mpbiri 248 |
. . . . . . . . 9
|
168 | 167 | adantl 482 |
. . . . . . . 8
|
169 | | biimt 350 |
. . . . . . . 8
|
170 | 168, 169 | syl 17 |
. . . . . . 7
|
171 | | simpr 477 |
. . . . . . . . . . 11
|
172 | 171 | fveq2d 6195 |
. . . . . . . . . 10
|
173 | | s4fv0 13640 |
. . . . . . . . . . . 12
|
174 | 9, 173 | syl 17 |
. . . . . . . . . . 11
|
175 | 174 | adantr 481 |
. . . . . . . . . 10
|
176 | 172, 175 | eqtrd 2656 |
. . . . . . . . 9
|
177 | | s4fv3 13643 |
. . . . . . . . . . 11
|
178 | 12, 177 | syl 17 |
. . . . . . . . . 10
|
179 | 178 | adantr 481 |
. . . . . . . . 9
|
180 | 176, 179 | oveq12d 6668 |
. . . . . . . 8
|
181 | 171 | fveq2d 6195 |
. . . . . . . . . 10
|
182 | | s4fv0 13640 |
. . . . . . . . . . . 12
|
183 | 20, 182 | syl 17 |
. . . . . . . . . . 11
|
184 | 183 | adantr 481 |
. . . . . . . . . 10
|
185 | 181, 184 | eqtrd 2656 |
. . . . . . . . 9
|
186 | | s4fv3 13643 |
. . . . . . . . . . 11
|
187 | 23, 186 | syl 17 |
. . . . . . . . . 10
|
188 | 187 | adantr 481 |
. . . . . . . . 9
|
189 | 185, 188 | oveq12d 6668 |
. . . . . . . 8
|
190 | 180, 189 | eqeq12d 2637 |
. . . . . . 7
|
191 | 170, 190 | bitr3d 270 |
. . . . . 6
|
192 | | 1lt3 11196 |
. . . . . . . . . 10
|
193 | | breq1 4656 |
. . . . . . . . . 10
|
194 | 192, 193 | mpbiri 248 |
. . . . . . . . 9
|
195 | 194 | adantl 482 |
. . . . . . . 8
|
196 | 195, 169 | syl 17 |
. . . . . . 7
|
197 | | simpr 477 |
. . . . . . . . . . 11
|
198 | 197 | fveq2d 6195 |
. . . . . . . . . 10
|
199 | | s4fv1 13641 |
. . . . . . . . . . . 12
|
200 | 10, 199 | syl 17 |
. . . . . . . . . . 11
|
201 | 200 | adantr 481 |
. . . . . . . . . 10
|
202 | 198, 201 | eqtrd 2656 |
. . . . . . . . 9
|
203 | 178 | adantr 481 |
. . . . . . . . 9
|
204 | 202, 203 | oveq12d 6668 |
. . . . . . . 8
|
205 | 197 | fveq2d 6195 |
. . . . . . . . . 10
|
206 | | s4fv1 13641 |
. . . . . . . . . . . 12
|
207 | 21, 206 | syl 17 |
. . . . . . . . . . 11
|
208 | 207 | adantr 481 |
. . . . . . . . . 10
|
209 | 205, 208 | eqtrd 2656 |
. . . . . . . . 9
|
210 | 187 | adantr 481 |
. . . . . . . . 9
|
211 | 209, 210 | oveq12d 6668 |
. . . . . . . 8
|
212 | 204, 211 | eqeq12d 2637 |
. . . . . . 7
|
213 | 196, 212 | bitr3d 270 |
. . . . . 6
|
214 | | 2lt3 11195 |
. . . . . . . . . 10
|
215 | | breq1 4656 |
. . . . . . . . . 10
|
216 | 214, 215 | mpbiri 248 |
. . . . . . . . 9
|
217 | 216 | adantl 482 |
. . . . . . . 8
|
218 | 217, 169 | syl 17 |
. . . . . . 7
|
219 | | simpr 477 |
. . . . . . . . . . 11
|
220 | 219 | fveq2d 6195 |
. . . . . . . . . 10
|
221 | | s4fv2 13642 |
. . . . . . . . . . . 12
|
222 | 11, 221 | syl 17 |
. . . . . . . . . . 11
|
223 | 222 | adantr 481 |
. . . . . . . . . 10
|
224 | 220, 223 | eqtrd 2656 |
. . . . . . . . 9
|
225 | 178 | adantr 481 |
. . . . . . . . 9
|
226 | 224, 225 | oveq12d 6668 |
. . . . . . . 8
|
227 | 219 | fveq2d 6195 |
. . . . . . . . . 10
|
228 | | s4fv2 13642 |
. . . . . . . . . . . 12
|
229 | 22, 228 | syl 17 |
. . . . . . . . . . 11
|
230 | 229 | adantr 481 |
. . . . . . . . . 10
|
231 | 227, 230 | eqtrd 2656 |
. . . . . . . . 9
|
232 | 187 | adantr 481 |
. . . . . . . . 9
|
233 | 231, 232 | oveq12d 6668 |
. . . . . . . 8
|
234 | 226, 233 | eqeq12d 2637 |
. . . . . . 7
|
235 | 218, 234 | bitr3d 270 |
. . . . . 6
|
236 | | 0red 10041 |
. . . . . 6
|
237 | | 1red 10055 |
. . . . . 6
|
238 | | 2re 11090 |
. . . . . . 7
|
239 | 238 | a1i 11 |
. . . . . 6
|
240 | 191, 213,
235, 236, 237, 239 | raltpd 4315 |
. . . . 5
|
241 | 164, 240 | bitrd 268 |
. . . 4
..^
|
242 | 161, 241 | anbi12d 747 |
. . 3
..^ ..^ ..^
|
243 | 98, 242 | syl5bb 272 |
. 2
..^ ..^
|
244 | 31, 97, 243 | 3bitrd 294 |
1
|