Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . . 8
++ ++ |
2 | 1 | fveq2d 6195 |
. . . . . . 7
++ ++ |
3 | 2 | fveq1d 6193 |
. . . . . 6
++ ++ |
4 | 3 | eqeq1d 2624 |
. . . . 5
++ ++ |
5 | 4 | imbi2d 330 |
. . . 4
Word ..^ ++
Word ..^ ++ |
6 | | oveq2 6658 |
. . . . . . . 8
++ ++ |
7 | 6 | fveq2d 6195 |
. . . . . . 7
++ ++ |
8 | 7 | fveq1d 6193 |
. . . . . 6
++ ++ |
9 | 8 | eqeq1d 2624 |
. . . . 5
++
++ |
10 | 9 | imbi2d 330 |
. . . 4
Word ..^ ++
Word ..^ ++ |
11 | | oveq2 6658 |
. . . . . . . 8
++ ++ ++ ++ |
12 | 11 | fveq2d 6195 |
. . . . . . 7
++ ++ ++ ++ |
13 | 12 | fveq1d 6193 |
. . . . . 6
++ ++
++ ++ |
14 | 13 | eqeq1d 2624 |
. . . . 5
++ ++
++ ++
|
15 | 14 | imbi2d 330 |
. . . 4
++ Word
..^ ++ Word ..^ ++
++ |
16 | | oveq2 6658 |
. . . . . . . 8
++ ++ |
17 | 16 | fveq2d 6195 |
. . . . . . 7
++ ++ |
18 | 17 | fveq1d 6193 |
. . . . . 6
++ ++ |
19 | 18 | eqeq1d 2624 |
. . . . 5
++
++ |
20 | 19 | imbi2d 330 |
. . . 4
Word ..^ ++
Word ..^ ++ |
21 | | ccatrid 13370 |
. . . . . . 7
Word
++
|
22 | 21 | fveq2d 6195 |
. . . . . 6
Word
++ |
23 | 22 | fveq1d 6193 |
. . . . 5
Word
++ |
24 | 23 | adantr 481 |
. . . 4
Word
..^ ++
|
25 | | simprl 794 |
. . . . . . . . . . . 12
Word Word ..^ Word |
26 | | simpll 790 |
. . . . . . . . . . . 12
Word Word ..^ Word |
27 | | simplr 792 |
. . . . . . . . . . . . 13
Word Word ..^ |
28 | 27 | s1cld 13383 |
. . . . . . . . . . . 12
Word Word ..^ Word
|
29 | | ccatass 13371 |
. . . . . . . . . . . 12
Word
Word Word
++ ++ ++ ++ |
30 | 25, 26, 28, 29 | syl3anc 1326 |
. . . . . . . . . . 11
Word Word ..^ ++ ++ ++ ++ |
31 | 30 | fveq2d 6195 |
. . . . . . . . . 10
Word Word ..^ ++ ++ ++ ++ |
32 | 31 | fveq1d 6193 |
. . . . . . . . 9
Word Word ..^ ++ ++ ++ ++ |
33 | | ccatcl 13359 |
. . . . . . . . . . 11
Word
Word ++ Word |
34 | 25, 26, 33 | syl2anc 693 |
. . . . . . . . . 10
Word Word ..^ ++ Word
|
35 | | lencl 13324 |
. . . . . . . . . . . . . . 15
Word
|
36 | 25, 35 | syl 17 |
. . . . . . . . . . . . . 14
Word Word ..^ |
37 | 36 | nn0zd 11480 |
. . . . . . . . . . . . 13
Word Word ..^ |
38 | | lencl 13324 |
. . . . . . . . . . . . . . 15
++ Word ++ |
39 | 34, 38 | syl 17 |
. . . . . . . . . . . . . 14
Word Word ..^ ++ |
40 | 39 | nn0zd 11480 |
. . . . . . . . . . . . 13
Word Word ..^ ++ |
41 | 36 | nn0red 11352 |
. . . . . . . . . . . . . . 15
Word Word ..^ |
42 | | lencl 13324 |
. . . . . . . . . . . . . . . 16
Word
|
43 | 26, 42 | syl 17 |
. . . . . . . . . . . . . . 15
Word Word ..^ |
44 | | nn0addge1 11339 |
. . . . . . . . . . . . . . 15
|
45 | 41, 43, 44 | syl2anc 693 |
. . . . . . . . . . . . . 14
Word Word ..^
|
46 | | ccatlen 13360 |
. . . . . . . . . . . . . . 15
Word
Word ++ |
47 | 25, 26, 46 | syl2anc 693 |
. . . . . . . . . . . . . 14
Word Word ..^ ++ |
48 | 45, 47 | breqtrrd 4681 |
. . . . . . . . . . . . 13
Word Word ..^
++ |
49 | | eluz2 11693 |
. . . . . . . . . . . . 13
++
++ ++ |
50 | 37, 40, 48, 49 | syl3anbrc 1246 |
. . . . . . . . . . . 12
Word Word ..^ ++ |
51 | | fzoss2 12496 |
. . . . . . . . . . . 12
++ ..^ ..^ ++ |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
Word Word ..^ ..^
..^ ++ |
53 | | simprr 796 |
. . . . . . . . . . 11
Word Word ..^ ..^ |
54 | 52, 53 | sseldd 3604 |
. . . . . . . . . 10
Word Word ..^ ..^ ++ |
55 | | signsv.p |
. . . . . . . . . . 11
|
56 | | signsv.w |
. . . . . . . . . . 11
|
57 | | signsv.t |
. . . . . . . . . . 11
Word
..^ g sgn |
58 | | signsv.v |
. . . . . . . . . . 11
Word ..^ |
59 | 55, 56, 57, 58 | signstfvp 30648 |
. . . . . . . . . 10
++ Word
..^ ++ ++ ++ ++ |
60 | 34, 27, 54, 59 | syl3anc 1326 |
. . . . . . . . 9
Word Word ..^ ++ ++ ++ |
61 | 32, 60 | eqtr3d 2658 |
. . . . . . . 8
Word Word ..^ ++ ++ ++
|
62 | 61 | adantr 481 |
. . . . . . 7
Word Word ..^ ++ ++ ++ ++
|
63 | | simpr 477 |
. . . . . . 7
Word Word ..^ ++ ++ |
64 | 62, 63 | eqtrd 2656 |
. . . . . 6
Word Word ..^ ++ ++ ++ |
65 | 64 | exp31 630 |
. . . . 5
Word
Word ..^ ++ ++
++ |
66 | 65 | a2d 29 |
. . . 4
Word
Word
..^ ++ Word
..^ ++ ++ |
67 | 5, 10, 15, 20, 24, 66 | wrdind 13476 |
. . 3
Word
Word
..^ ++
|
68 | 67 | 3impib 1262 |
. 2
Word
Word ..^ ++ |
69 | 68 | 3com12 1269 |
1
Word
Word ..^ ++ |