Step | Hyp | Ref
| Expression |
1 | | ccatws1len 13398 |
. . . . . . . . 9
Word
++ |
2 | 1 | 3ad2ant1 1082 |
. . . . . . . 8
Word
Word ++ |
3 | 2 | oveq2d 6666 |
. . . . . . 7
Word
Word ..^ ++ ..^ |
4 | | lencl 13324 |
. . . . . . . . . . 11
Word |
5 | | elnn0uz 11725 |
. . . . . . . . . . 11
|
6 | 4, 5 | sylib 208 |
. . . . . . . . . 10
Word |
7 | 6 | adantr 481 |
. . . . . . . . 9
Word
|
8 | | fzosplitsn 12576 |
. . . . . . . . 9
..^ ..^ |
9 | 7, 8 | syl 17 |
. . . . . . . 8
Word
..^ ..^ |
10 | 9 | 3ad2ant1 1082 |
. . . . . . 7
Word
Word ..^ ..^ |
11 | 3, 10 | eqtrd 2656 |
. . . . . 6
Word
Word ..^ ++ ..^ |
12 | 11 | raleqdv 3144 |
. . . . 5
Word
Word
..^ ++
++ ++ ..^
++ ++ |
13 | 4 | adantr 481 |
. . . . . . 7
Word
|
14 | 13 | 3ad2ant1 1082 |
. . . . . 6
Word
Word |
15 | | fveq2 6191 |
. . . . . . . . . 10
++ ++ |
16 | 15 | fveq1d 6193 |
. . . . . . . . 9
++ ++ |
17 | | fveq2 6191 |
. . . . . . . . . 10
++ ++ |
18 | 17 | fveq1d 6193 |
. . . . . . . . 9
++ ++ |
19 | 16, 18 | eqeq12d 2637 |
. . . . . . . 8
++ ++ ++ ++ |
20 | 19 | ralbidv 2986 |
. . . . . . 7
++ ++ ++ ++ |
21 | 20 | ralunsn 4422 |
. . . . . 6
..^
++ ++
..^
++ ++ ++ ++ |
22 | 14, 21 | syl 17 |
. . . . 5
Word
Word
..^
++ ++ ..^
++ ++ ++ ++ |
23 | | simpl 473 |
. . . . . . . . . . . . 13
Word
Word |
24 | 23 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
Word
Word Word |
25 | 24 | adantr 481 |
. . . . . . . . . . 11
Word
Word ..^ Word |
26 | | simpr 477 |
. . . . . . . . . . . . 13
Word
|
27 | 26 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
Word
Word |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
Word
Word ..^ |
29 | | simpr 477 |
. . . . . . . . . . 11
Word
Word ..^ ..^ |
30 | | ccats1val1 13403 |
. . . . . . . . . . 11
Word
..^ ++ |
31 | 25, 28, 29, 30 | syl3anc 1326 |
. . . . . . . . . 10
Word
Word ..^ ++ |
32 | 31 | fveq1d 6193 |
. . . . . . . . 9
Word
Word ..^ ++ |
33 | | simpl2l 1114 |
. . . . . . . . . . 11
Word
Word ..^ Word |
34 | | simpl2r 1115 |
. . . . . . . . . . 11
Word
Word ..^ |
35 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
..^ ..^ |
36 | 35 | eleq2d 2687 |
. . . . . . . . . . . . . 14
..^
..^ |
37 | 36 | biimpd 219 |
. . . . . . . . . . . . 13
..^ ..^ |
38 | 37 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
Word
Word ..^ ..^ |
39 | 38 | imp 445 |
. . . . . . . . . . 11
Word
Word ..^ ..^ |
40 | | ccats1val1 13403 |
. . . . . . . . . . 11
Word
..^ ++ |
41 | 33, 34, 39, 40 | syl3anc 1326 |
. . . . . . . . . 10
Word
Word ..^ ++ |
42 | 41 | fveq1d 6193 |
. . . . . . . . 9
Word
Word ..^ ++ |
43 | 32, 42 | eqeq12d 2637 |
. . . . . . . 8
Word
Word ..^ ++ ++
|
44 | 43 | ralbidv 2986 |
. . . . . . 7
Word
Word ..^
++ ++
|
45 | 44 | ralbidva 2985 |
. . . . . 6
Word
Word
..^
++ ++
..^
|
46 | | eqidd 2623 |
. . . . . . . . . . . 12
Word
|
47 | 23, 26, 46 | 3jca 1242 |
. . . . . . . . . . 11
Word
Word
|
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . 10
Word
Word
Word
|
49 | | ccats1val2 13404 |
. . . . . . . . . 10
Word
++ |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
Word
Word ++ |
51 | 50 | fveq1d 6193 |
. . . . . . . 8
Word
Word ++ |
52 | | df-3an 1039 |
. . . . . . . . . . 11
Word
Word |
53 | 52 | biimpri 218 |
. . . . . . . . . 10
Word
Word
|
54 | 53 | 3adant1 1079 |
. . . . . . . . 9
Word
Word
Word
|
55 | | ccats1val2 13404 |
. . . . . . . . . 10
Word
++ |
56 | 55 | fveq1d 6193 |
. . . . . . . . 9
Word
++ |
57 | 54, 56 | syl 17 |
. . . . . . . 8
Word
Word ++ |
58 | 51, 57 | eqeq12d 2637 |
. . . . . . 7
Word
Word ++ ++
|
59 | 58 | ralbidv 2986 |
. . . . . 6
Word
Word
++ ++
|
60 | 45, 59 | anbi12d 747 |
. . . . 5
Word
Word ..^
++ ++ ++ ++ ..^
|
61 | 12, 22, 60 | 3bitrd 294 |
. . . 4
Word
Word
..^ ++
++ ++ ..^
|
62 | 61 | ad2antlr 763 |
. . 3
Word
Word ..^
g g
..^ ++
++ ++ ..^
|
63 | | pm3.35 611 |
. . . . . . 7
..^
..^
g g
g g |
64 | | fveq2 6191 |
. . . . . . . . . . 11
g g |
65 | | fveq2 6191 |
. . . . . . . . . . 11
g g |
66 | 64, 65 | eqeq12d 2637 |
. . . . . . . . . 10
g g
g g |
67 | 66 | cbvralv 3171 |
. . . . . . . . 9
g g g g |
68 | | simp-4l 806 |
. . . . . . . . . . . . . . 15
Word
Word g g |
69 | | simp-4r 807 |
. . . . . . . . . . . . . . 15
Word
Word g g |
70 | | simpr 477 |
. . . . . . . . . . . . . . 15
Word
Word g g |
71 | 68, 69, 70 | 3jca 1242 |
. . . . . . . . . . . . . 14
Word
Word g g
|
72 | 71 | adantr 481 |
. . . . . . . . . . . . 13
Word
Word g g
|
73 | | simp-4r 807 |
. . . . . . . . . . . . 13
Word
Word g g Word
Word |
74 | | simpr 477 |
. . . . . . . . . . . . . . 15
Word
Word g g
g g |
75 | 74 | adantr 481 |
. . . . . . . . . . . . . 14
Word
Word g g
g g |
76 | 75 | anim1i 592 |
. . . . . . . . . . . . 13
Word
Word g g g g
|
77 | | gsmsymgrfix.s |
. . . . . . . . . . . . . . 15
|
78 | | gsmsymgrfix.b |
. . . . . . . . . . . . . . 15
|
79 | | gsmsymgreq.z |
. . . . . . . . . . . . . . 15
|
80 | | gsmsymgreq.p |
. . . . . . . . . . . . . . 15
|
81 | | gsmsymgreq.i |
. . . . . . . . . . . . . . 15
|
82 | 77, 78, 79, 80, 81 | gsmsymgreqlem1 17850 |
. . . . . . . . . . . . . 14
Word
Word
g g
g ++ g ++ |
83 | 82 | imp 445 |
. . . . . . . . . . . . 13
Word
Word g g g ++
g ++ |
84 | 72, 73, 76, 83 | syl21anc 1325 |
. . . . . . . . . . . 12
Word
Word g g g ++ g ++ |
85 | 84 | ex 450 |
. . . . . . . . . . 11
Word
Word g g g ++ g ++ |
86 | 85 | ralimdva 2962 |
. . . . . . . . . 10
Word
Word g g
g ++ g ++ |
87 | 86 | expcom 451 |
. . . . . . . . 9
g g
Word
Word g ++ g ++ |
88 | 67, 87 | sylbi 207 |
. . . . . . . 8
g g
Word
Word g ++ g ++ |
89 | 88 | com23 86 |
. . . . . . 7
g g
Word
Word
g ++ g ++ |
90 | 63, 89 | syl 17 |
. . . . . 6
..^
..^
g g
Word
Word
g ++ g ++ |
91 | 90 | impancom 456 |
. . . . 5
..^
..^
g g
Word
Word
g ++ g ++ |
92 | 91 | com13 88 |
. . . 4
Word
Word ..^
g g ..^
g ++ g ++ |
93 | 92 | imp 445 |
. . 3
Word
Word ..^
g g
..^
g ++ g ++ |
94 | 62, 93 | sylbid 230 |
. 2
Word
Word ..^
g g
..^ ++
++ ++ g ++ g ++ |
95 | 94 | ex 450 |
1
Word
Word ..^
g g
..^ ++
++ ++ g ++ g ++ |