Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . 8
Word     |
2 | | efgval.r |
. . . . . . . 8
~FG    |
3 | | efgval2.m |
. . . . . . . 8
 
       |
4 | | efgval2.t |
. . . . . . . 8
              splice                  |
5 | | efgred.d |
. . . . . . . 8
 
      |
6 | | efgred.s |
. . . . . . . 8
  Word           ..^                                  |
7 | 1, 2, 3, 4, 5, 6 | efgsdm 17380 |
. . . . . . 7

 Word       
  ..^                       |
8 | 7 | simp1bi 1023 |
. . . . . 6

Word      |
9 | 8 | adantr 467 |
. . . . 5
 
        
Word      |
10 | 9 | eldifad 3416 |
. . . 4
 
        
Word   |
11 | 1, 2, 3, 4, 5, 6 | efgsf 17379 |
. . . . . . . . . . . 12
   Word
          ..^                         |
12 | 11 | fdmi 5734 |
. . . . . . . . . . . . 13
 Word
          ..^                       |
13 | 12 | feq2i 5721 |
. . . . . . . . . . . 12
    
   Word
          ..^                          |
14 | 11, 13 | mpbir 213 |
. . . . . . . . . . 11
     |
15 | 14 | ffvelrni 6021 |
. . . . . . . . . 10
       |
16 | 15 | adantr 467 |
. . . . . . . . 9
 
        
      |
17 | 1, 2, 3, 4 | efgtf 17372 |
. . . . . . . . 9
                             
     splice                                               |
18 | 16, 17 | syl 17 |
. . . . . . . 8
 
        
                              splice               
                               |
19 | 18 | simprd 465 |
. . . . . . 7
 
        
                              |
20 | | frn 5735 |
. . . . . . 7
                                       |
21 | 19, 20 | syl 17 |
. . . . . 6
 
        
          |
22 | | simpr 463 |
. . . . . 6
 
        
          |
23 | 21, 22 | sseldd 3433 |
. . . . 5
 
        
  |
24 | 23 | s1cld 12742 |
. . . 4
 
        
    Word
  |
25 | | ccatcl 12720 |
. . . 4
  Word     Word   ++     
Word   |
26 | 10, 24, 25 | syl2anc 667 |
. . 3
 
        
 ++     
Word   |
27 | | ccatlen 12721 |
. . . . . . 7
  Word     Word      ++                       |
28 | 10, 24, 27 | syl2anc 667 |
. . . . . 6
 
        
    ++                       |
29 | | s1len 12744 |
. . . . . . 7
       
 |
30 | 29 | oveq2i 6301 |
. . . . . 6
                     |
31 | 28, 30 | syl6eq 2501 |
. . . . 5
 
        
    ++               |
32 | | lencl 12687 |
. . . . . 6
 Word       |
33 | | nn0p1nn 10909 |
. . . . . 6
    
        |
34 | 10, 32, 33 | 3syl 18 |
. . . . 5
 
        
        |
35 | 31, 34 | eqeltrd 2529 |
. . . 4
 
        
    ++         |
36 | | wrdfin 12686 |
. . . . 5
  ++     
Word  ++        |
37 | | hashnncl 12547 |
. . . . 5
  ++     
     ++        ++     
   |
38 | 26, 36, 37 | 3syl 18 |
. . . 4
 
        
     ++      
 ++         |
39 | 35, 38 | mpbid 214 |
. . 3
 
        
 ++        |
40 | | eldifsn 4097 |
. . 3
  ++     
Word      ++      Word  ++         |
41 | 26, 39, 40 | sylanbrc 670 |
. 2
 
        
 ++     
Word      |
42 | | eldifsni 4098 |
. . . . . . 7
 Word      |
43 | 9, 42 | syl 17 |
. . . . . 6
 
        
  |
44 | | wrdfin 12686 |
. . . . . . 7
 Word   |
45 | | hashnncl 12547 |
. . . . . . 7
     
   |
46 | 10, 44, 45 | 3syl 18 |
. . . . . 6
 
        
    
   |
47 | 43, 46 | mpbird 236 |
. . . . 5
 
        
      |
48 | | lbfzo0 11955 |
. . . . 5
  ..^           |
49 | 47, 48 | sylibr 216 |
. . . 4
 
        
 ..^       |
50 | | ccatval1 12722 |
. . . 4
  Word     Word  ..^        ++               |
51 | 10, 24, 49, 50 | syl3anc 1268 |
. . 3
 
        
  ++               |
52 | 7 | simp2bi 1024 |
. . . 4
       |
53 | 52 | adantr 467 |
. . 3
 
        
      |
54 | 51, 53 | eqeltrd 2529 |
. 2
 
        
  ++           |
55 | 7 | simp3bi 1025 |
. . . . . 6
 
 ..^                      |
56 | 55 | adantr 467 |
. . . . 5
 
        
  ..^                      |
57 | | fzo0ss1 11948 |
. . . . . . . . . . 11
 ..^      ..^      |
58 | 57 | sseli 3428 |
. . . . . . . . . 10
  ..^    
 ..^       |
59 | | ccatval1 12722 |
. . . . . . . . . 10
  Word     Word  ..^        ++               |
60 | 58, 59 | syl3an3 1303 |
. . . . . . . . 9
  Word     Word  ..^        ++               |
61 | | elfzoel2 11919 |
. . . . . . . . . . . . . . . 16
  ..^    
      |
62 | | peano2zm 10980 |
. . . . . . . . . . . . . . . 16
    
        |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
  ..^    
        |
64 | 61 | zred 11040 |
. . . . . . . . . . . . . . . 16
  ..^    
      |
65 | 64 | lem1d 10540 |
. . . . . . . . . . . . . . 15
  ..^    
            |
66 | | eluz2 11165 |
. . . . . . . . . . . . . . 15
              
                        |
67 | 63, 61, 65, 66 | syl3anbrc 1192 |
. . . . . . . . . . . . . 14
  ..^    
                |
68 | | fzoss2 11946 |
. . . . . . . . . . . . . 14
                ..^        ..^       |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
  ..^    
 ..^      
 ..^       |
70 | | elfzoelz 11920 |
. . . . . . . . . . . . . . 15
  ..^    
  |
71 | | elfzom1b 12010 |
. . . . . . . . . . . . . . 15
         ..^    
   ..^          |
72 | 70, 61, 71 | syl2anc 667 |
. . . . . . . . . . . . . 14
  ..^    
  ..^    
   ..^          |
73 | 72 | ibi 245 |
. . . . . . . . . . . . 13
  ..^    
   ..^         |
74 | 69, 73 | sseldd 3433 |
. . . . . . . . . . . 12
  ..^    
   ..^       |
75 | | ccatval1 12722 |
. . . . . . . . . . . 12
  Word     Word    ..^        ++                   |
76 | 74, 75 | syl3an3 1303 |
. . . . . . . . . . 11
  Word     Word  ..^        ++                   |
77 | 76 | fveq2d 5869 |
. . . . . . . . . 10
  Word     Word  ..^           ++                        |
78 | 77 | rneqd 5062 |
. . . . . . . . 9
  Word     Word  ..^     
     ++                        |
79 | 60, 78 | eleq12d 2523 |
. . . . . . . 8
  Word     Word  ..^         ++              ++                             |
80 | 79 | 3expa 1208 |
. . . . . . 7
   Word     Word 
 ..^         ++              ++           
                 |
81 | 80 | ralbidva 2824 |
. . . . . 6
  Word     Word   
 ..^        ++              ++              ..^                       |
82 | 10, 24, 81 | syl2anc 667 |
. . . . 5
 
        
 
 ..^        ++              ++              ..^                       |
83 | 56, 82 | mpbird 236 |
. . . 4
 
        
  ..^        ++              ++              |
84 | 10, 32 | syl 17 |
. . . . . . . . . 10
 
        
      |
85 | 84 | nn0cnd 10927 |
. . . . . . . . 9
 
        
      |
86 | 85 | addid2d 9834 |
. . . . . . . 8
 
        
            |
87 | 86 | fveq2d 5869 |
. . . . . . 7
 
        
  ++                 ++               |
88 | | 1nn 10620 |
. . . . . . . . . . 11
 |
89 | 29, 88 | eqeltri 2525 |
. . . . . . . . . 10
       
 |
90 | 89 | a1i 11 |
. . . . . . . . 9
 
        
          |
91 | | lbfzo0 11955 |
. . . . . . . . 9
  ..^        
          |
92 | 90, 91 | sylibr 216 |
. . . . . . . 8
 
        
 ..^           |
93 | | ccatval3 12724 |
. . . . . . . 8
  Word     Word  ..^            ++                         |
94 | 10, 24, 92, 93 | syl3anc 1268 |
. . . . . . 7
 
        
  ++                         |
95 | 87, 94 | eqtr3d 2487 |
. . . . . 6
 
        
  ++                       |
96 | | s1fv 12748 |
. . . . . . . 8
                   |
97 | 96 | adantl 468 |
. . . . . . 7
 
        
          |
98 | | fzo0end 12003 |
. . . . . . . . . . . 12
    
       ..^       |
99 | 47, 98 | syl 17 |
. . . . . . . . . . 11
 
        
       ..^       |
100 | | ccatval1 12722 |
. . . . . . . . . . 11
  Word     Word        ..^        ++                           |
101 | 10, 24, 99, 100 | syl3anc 1268 |
. . . . . . . . . 10
 
        
  ++                           |
102 | 1, 2, 3, 4, 5, 6 | efgsval 17381 |
. . . . . . . . . . 11
                 |
103 | 102 | adantr 467 |
. . . . . . . . . 10
 
        
                |
104 | 101, 103 | eqtr4d 2488 |
. . . . . . . . 9
 
        
  ++                     |
105 | 104 | fveq2d 5869 |
. . . . . . . 8
 
        
     ++                          |
106 | 105 | rneqd 5062 |
. . . . . . 7
 
        
     ++                          |
107 | 22, 97, 106 | 3eltr4d 2544 |
. . . . . 6
 
        
             ++                  |
108 | 95, 107 | eqeltrd 2529 |
. . . . 5
 
        
  ++                  ++                  |
109 | | fvex 5875 |
. . . . . 6
     |
110 | | fveq2 5865 |
. . . . . . 7
    
  ++           ++               |
111 | | oveq1 6297 |
. . . . . . . . . 10
    
          |
112 | 111 | fveq2d 5869 |
. . . . . . . . 9
    
  ++             ++                 |
113 | 112 | fveq2d 5869 |
. . . . . . . 8
    
     ++                 ++                  |
114 | 113 | rneqd 5062 |
. . . . . . 7
    
     ++                 ++                  |
115 | 110, 114 | eleq12d 2523 |
. . . . . 6
    
   ++              ++              ++                  ++                   |
116 | 109, 115 | ralsn 4010 |
. . . . 5
 
        ++              ++              ++                  ++                  |
117 | 108, 116 | sylibr 216 |
. . . 4
 
        
         ++              ++              |
118 | | ralunb 3615 |
. . . 4
 
  ..^               ++              ++               ..^        ++              ++                     ++              ++               |
119 | 83, 117, 118 | sylanbrc 670 |
. . 3
 
        
   ..^               ++              ++              |
120 | 31 | oveq2d 6306 |
. . . . 5
 
        
 ..^    ++         ..^         |
121 | | nnuz 11194 |
. . . . . . 7
     |
122 | 47, 121 | syl6eleq 2539 |
. . . . . 6
 
        
          |
123 | | fzosplitsn 12017 |
. . . . . 6
          ..^         ..^              |
124 | 122, 123 | syl 17 |
. . . . 5
 
        
 ..^         ..^              |
125 | 120, 124 | eqtrd 2485 |
. . . 4
 
        
 ..^    ++          ..^              |
126 | 125 | raleqdv 2993 |
. . 3
 
        
 
 ..^    ++           ++              ++               ..^               ++              ++               |
127 | 119, 126 | mpbird 236 |
. 2
 
        
  ..^    ++           ++              ++              |
128 | 1, 2, 3, 4, 5, 6 | efgsdm 17380 |
. 2
  ++     
  ++      Word      ++           ..^    ++           ++              ++               |
129 | 41, 54, 127, 128 | syl3anbrc 1192 |
1
 
        
 ++     
  |