Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
Word     |
2 | | efgval.r |
. . 3
~FG    |
3 | | efgval2.m |
. . 3
 
       |
4 | | efgval2.t |
. . 3
              splice                  |
5 | 1, 2, 3, 4 | efgval2 17374 |
. 2
          ![] ]](rbrack.gif)    |
6 | | efgcpbllem.1 |
. . . . . . 7
   
      ++  ++    ++  ++     |
7 | 6 | relopabi 4959 |
. . . . . 6
 |
8 | 7 | a1i 11 |
. . . . 5
 
   |
9 | | efgred.d |
. . . . . . . . 9
 
      |
10 | | efgred.s |
. . . . . . . . 9
  Word           ..^                                  |
11 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 17404 |
. . . . . . . 8
  

  ++  ++    ++  ++     |
12 | 11 | simp2bi 1024 |
. . . . . . 7
     |
13 | 12 | adantl 468 |
. . . . . 6
  

     |
14 | 11 | simp1bi 1023 |
. . . . . . 7
     |
15 | 14 | adantl 468 |
. . . . . 6
  

     |
16 | 1, 2 | efger 17368 |
. . . . . . . 8
 |
17 | 16 | a1i 11 |
. . . . . . 7
  

     |
18 | 11 | simp3bi 1025 |
. . . . . . . 8
     ++  ++    ++  ++    |
19 | 18 | adantl 468 |
. . . . . . 7
  

     ++  ++    ++  ++    |
20 | 17, 19 | ersym 7375 |
. . . . . 6
  

     ++  ++    ++  ++    |
21 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 17404 |
. . . . . 6
  

  ++  ++    ++  ++     |
22 | 13, 15, 20, 21 | syl3anbrc 1192 |
. . . . 5
  

       |
23 | 14 | ad2antrl 734 |
. . . . . 6
  

         |
24 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 17404 |
. . . . . . . 8
  

  ++  ++    ++  ++     |
25 | 24 | simp2bi 1024 |
. . . . . . 7
     |
26 | 25 | ad2antll 735 |
. . . . . 6
  

         |
27 | 16 | a1i 11 |
. . . . . . 7
  

      
  |
28 | 18 | ad2antrl 734 |
. . . . . . 7
  

         ++  ++    ++  ++    |
29 | 24 | simp3bi 1025 |
. . . . . . . 8
     ++  ++    ++  ++    |
30 | 29 | ad2antll 735 |
. . . . . . 7
  

         ++  ++    ++  ++    |
31 | 27, 28, 30 | ertrd 7379 |
. . . . . 6
  

         ++  ++    ++  ++    |
32 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 17404 |
. . . . . 6
  

  ++  ++    ++  ++     |
33 | 23, 26, 31, 32 | syl3anbrc 1192 |
. . . . 5
  

           |
34 | 16 | a1i 11 |
. . . . . . . . 9
  

   |
35 | | fviss 5923 |
. . . . . . . . . . . . . 14
Word    Word    |
36 | 1, 35 | eqsstri 3462 |
. . . . . . . . . . . . 13
Word    |
37 | | simpll 760 |
. . . . . . . . . . . . 13
  

   |
38 | 36, 37 | sseldi 3430 |
. . . . . . . . . . . 12
  

 Word     |
39 | | simpr 463 |
. . . . . . . . . . . . 13
  

   |
40 | 36, 39 | sseldi 3430 |
. . . . . . . . . . . 12
  

 Word     |
41 | | ccatcl 12720 |
. . . . . . . . . . . 12
  Word  
Word     ++  Word     |
42 | 38, 40, 41 | syl2anc 667 |
. . . . . . . . . . 11
  

  ++  Word     |
43 | | simplr 762 |
. . . . . . . . . . . 12
  

   |
44 | 36, 43 | sseldi 3430 |
. . . . . . . . . . 11
  

 Word     |
45 | | ccatcl 12720 |
. . . . . . . . . . 11
   ++  Word  
Word      ++  ++  Word     |
46 | 42, 44, 45 | syl2anc 667 |
. . . . . . . . . 10
  

   ++  ++  Word     |
47 | 1 | efgrcl 17365 |
. . . . . . . . . . . 12
 
Word      |
48 | 47 | simprd 465 |
. . . . . . . . . . 11
 Word     |
49 | 48 | ad2antrr 732 |
. . . . . . . . . 10
  

 Word     |
50 | 46, 49 | eleqtrrd 2532 |
. . . . . . . . 9
  

   ++  ++    |
51 | 34, 50 | erref 7383 |
. . . . . . . 8
  

   ++  ++    ++  ++    |
52 | 51 | ex 436 |
. . . . . . 7
 
    ++  ++    ++  ++     |
53 | 52 | pm4.71d 640 |
. . . . . 6
 
     ++  ++    ++  ++      |
54 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 17404 |
. . . . . . 7
  

  ++  ++    ++  ++     |
55 | | df-3an 987 |
. . . . . . 7
 
  ++  ++    ++  ++        ++  ++    ++  ++     |
56 | | anidm 650 |
. . . . . . . 8
 
   |
57 | 56 | anbi1i 701 |
. . . . . . 7
  

  ++  ++    ++  ++      ++  ++ 
  ++  ++     |
58 | 54, 55, 57 | 3bitri 275 |
. . . . . 6
  

  ++  ++    ++  ++     |
59 | 53, 58 | syl6bbr 267 |
. . . . 5
 
       |
60 | 8, 22, 33, 59 | iserd 7389 |
. . . 4
 
   |
61 | 1, 2, 3, 4 | efgtf 17372 |
. . . . . . . . . 10
                 
 splice                                       |
62 | 61 | simprd 465 |
. . . . . . . . 9
                       |
63 | 62 | adantl 468 |
. . . . . . . 8
  

                       |
64 | | ffn 5728 |
. . . . . . . 8
                                       |
65 | | ovelrn 6445 |
. . . . . . . 8
                
    
                         |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . 7
  

                               |
67 | | simplr 762 |
. . . . . . . . . 10
                     |
68 | 62 | ad2antlr 733 |
. . . . . . . . . . 11
                                         |
69 | | simprl 764 |
. . . . . . . . . . 11
                             |
70 | | simprr 766 |
. . . . . . . . . . 11
                  
    |
71 | 68, 69, 70 | fovrnd 6441 |
. . . . . . . . . 10
                             |
72 | 50 | adantr 467 |
. . . . . . . . . . 11
                     ++  ++    |
73 | 37 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                  
  |
74 | 36, 73 | sseldi 3430 |
. . . . . . . . . . . . . . . 16
                  
Word     |
75 | 40 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                   Word
    |
76 | | swrdcl 12775 |
. . . . . . . . . . . . . . . . 17
 Word  
 substr     Word
    |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
                    substr
    Word     |
78 | | ccatcl 12720 |
. . . . . . . . . . . . . . . 16
  Word   
substr     Word   
 ++ 
substr      Word     |
79 | 74, 77, 78 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                    ++  substr      Word     |
80 | 3 | efgmf 17363 |
. . . . . . . . . . . . . . . . . 18
         |
81 | 80 | ffvelrni 6021 |
. . . . . . . . . . . . . . . . 17
  
        |
82 | 81 | ad2antll 735 |
. . . . . . . . . . . . . . . 16
                           |
83 | 70, 82 | s2cld 12965 |
. . . . . . . . . . . . . . 15
                            Word
    |
84 | | ccatcl 12720 |
. . . . . . . . . . . . . . 15
   ++  substr      Word            Word   
  ++  substr      ++           Word     |
85 | 79, 83, 84 | syl2anc 667 |
. . . . . . . . . . . . . 14
                     ++  substr      ++           Word     |
86 | | swrdcl 12775 |
. . . . . . . . . . . . . . 15
 Word  
 substr         Word     |
87 | 75, 86 | syl 17 |
. . . . . . . . . . . . . 14
                    substr
        Word     |
88 | 44 | adantr 467 |
. . . . . . . . . . . . . 14
                  
Word     |
89 | | ccatass 12732 |
. . . . . . . . . . . . . 14
    ++  substr      ++           Word    substr         Word   Word   
    ++  substr      ++           ++ 
substr          ++     ++  substr      ++           ++   substr         ++     |
90 | 85, 87, 88, 89 | syl3anc 1268 |
. . . . . . . . . . . . 13
                       ++  substr  
   ++           ++  substr          ++     ++  substr  
   ++           ++   substr         ++     |
91 | | ccatcl 12720 |
. . . . . . . . . . . . . . . . 17
   substr     Word            Word   
  substr     ++
          Word     |
92 | 77, 83, 91 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                     substr  
  ++           Word     |
93 | | ccatass 12732 |
. . . . . . . . . . . . . . . 16
  Word     substr  
  ++           Word    substr         Word   
  ++   substr  
  ++            ++  substr           ++    substr     ++
          ++ 
substr             |
94 | 74, 92, 87, 93 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
                     ++   substr
    ++            ++  substr           ++    substr     ++           ++  substr             |
95 | | ccatass 12732 |
. . . . . . . . . . . . . . . . 17
  Word   
substr     Word            Word   
  ++  substr      ++            ++   substr     ++
             |
96 | 74, 77, 83, 95 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                     ++  substr      ++            ++   substr
    ++              |
97 | 96 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                      ++  substr      ++           ++  substr            ++   substr     ++
           ++  substr            |
98 | 1, 2, 3, 4 | efgtval 17373 |
. . . . . . . . . . . . . . . . . 18
 
                    splice                 |
99 | 67, 69, 70, 98 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
                            splice                 |
100 | | splval 12858 |
. . . . . . . . . . . . . . . . . 18
          
                 Word      splice
                 substr     ++
          ++ 
substr            |
101 | 67, 69, 69, 83, 100 | syl13anc 1270 |
. . . . . . . . . . . . . . . . 17
                    splice
                 substr     ++
          ++ 
substr            |
102 | 99, 101 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
                              substr     ++           ++  substr            |
103 | 102 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                    ++           ++    substr  
  ++           ++  substr             |
104 | 94, 97, 103 | 3eqtr4rd 2496 |
. . . . . . . . . . . . . 14
                    ++             ++  substr  
   ++           ++  substr            |
105 | 104 | oveq1d 6305 |
. . . . . . . . . . . . 13
                     ++          ++      ++  substr  
   ++           ++  substr          ++    |
106 | | lencl 12687 |
. . . . . . . . . . . . . . . . . . 19
 Word  
      |
107 | 74, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                         |
108 | | nn0uz 11193 |
. . . . . . . . . . . . . . . . . 18
     |
109 | 107, 108 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . 17
                             |
110 | | elfznn0 11887 |
. . . . . . . . . . . . . . . . . 18
           |
111 | 110 | ad2antrl 734 |
. . . . . . . . . . . . . . . . 17
                     |
112 | | uzaddcl 11215 |
. . . . . . . . . . . . . . . . 17
                       |
113 | 109, 111,
112 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                               |
114 | 42 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                    ++  Word     |
115 | | ccatlen 12721 |
. . . . . . . . . . . . . . . . . 18
   ++  Word  
Word         ++  ++        ++          |
116 | 114, 88, 115 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
                        ++  ++        ++          |
117 | | ccatlen 12721 |
. . . . . . . . . . . . . . . . . . . 20
  Word  
Word        ++               |
118 | 74, 75, 117 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
                       ++               |
119 | | elfzuz3 11797 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
120 | 119 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . 21
                             |
121 | 107 | nn0zd 11038 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
122 | | eluzadd 11187 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
123 | 120, 121,
122 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
124 | | lencl 12687 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Word  
      |
125 | 75, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
126 | 125 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
127 | 107 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
128 | 126, 127 | addcomd 9835 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
129 | 111 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
130 | 129, 127 | addcomd 9835 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
131 | 130 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
132 | 123, 128,
131 | 3eltr3d 2543 |
. . . . . . . . . . . . . . . . . . 19
                                         |
133 | 118, 132 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . 18
                       ++               |
134 | | lencl 12687 |
. . . . . . . . . . . . . . . . . . 19
 Word  
      |
135 | 88, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                         |
136 | | uzaddcl 11215 |
. . . . . . . . . . . . . . . . . 18
      ++                       ++                    |
137 | 133, 135,
136 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
                        ++                    |
138 | 116, 137 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
                        ++  ++               |
139 | | elfzuzb 11794 |
. . . . . . . . . . . . . . . 16
               ++  ++                    ++  ++                |
140 | 113, 138,
139 | sylanbrc 670 |
. . . . . . . . . . . . . . 15
                                 ++  ++      |
141 | 1, 2, 3, 4 | efgtval 17373 |
. . . . . . . . . . . . . . 15
    ++  ++                ++  ++                    ++  ++        ++  ++  splice                             |
142 | 72, 140, 70, 141 | syl3anc 1268 |
. . . . . . . . . . . . . 14
                                ++  ++        ++  ++  splice                             |
143 | | wrd0 12691 |
. . . . . . . . . . . . . . . 16
Word    |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
                   Word     |
145 | | ccatcl 12720 |
. . . . . . . . . . . . . . . 16
   substr         Word   Word   
  substr         ++  Word     |
146 | 87, 88, 145 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                     substr         ++  Word     |
147 | | ccatrid 12731 |
. . . . . . . . . . . . . . . . . 18
  ++  substr  
   Word     ++  substr      ++   ++  substr        |
148 | 79, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
                     ++  substr      ++   ++  substr        |
149 | 148 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                      ++  substr      ++  ++   substr         ++     ++  substr      ++   substr         ++     |
150 | | ccatass 12732 |
. . . . . . . . . . . . . . . . 17
   ++  substr      Word    substr         Word   Word   
   ++  substr      ++  substr          ++    ++  substr      ++   substr         ++     |
151 | 79, 87, 88, 150 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                      ++  substr      ++  substr          ++    ++  substr  
   ++   substr         ++     |
152 | | ccatass 12732 |
. . . . . . . . . . . . . . . . . . 19
  Word   
substr     Word    substr         Word   
  ++  substr      ++  substr           ++   substr     ++
 substr             |
153 | 74, 77, 87, 152 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . 18
                     ++  substr      ++  substr           ++   substr  
  ++  substr             |
154 | 111, 108 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
155 | | eluzfz1 11806 |
. . . . . . . . . . . . . . . . . . . . . 22
    
      |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
157 | 125, 108 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
158 | | eluzfz2 11807 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
160 | | ccatswrd 12812 |
. . . . . . . . . . . . . . . . . . . . 21
  Word                                substr     ++  substr           substr           |
161 | 75, 156, 69, 159, 160 | syl13anc 1270 |
. . . . . . . . . . . . . . . . . . . 20
                     substr  
  ++  substr           substr           |
162 | | swrdid 12784 |
. . . . . . . . . . . . . . . . . . . . 21
 Word  
 substr           |
163 | 75, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                    substr
          |
164 | 161, 163 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19
                     substr  
  ++  substr            |
165 | 164 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
                    ++   substr     ++
 substr            ++    |
166 | 153, 165 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
                     ++  substr      ++  substr           ++    |
167 | 166 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                      ++  substr      ++  substr          ++    ++  ++    |
168 | 149, 151,
167 | 3eqtr2rd 2492 |
. . . . . . . . . . . . . . 15
                     ++  ++     ++  substr      ++  ++   substr         ++     |
169 | | ccatlen 12721 |
. . . . . . . . . . . . . . . . 17
  Word   
substr     Word   
    ++  substr                substr         |
170 | 74, 77, 169 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                       ++  substr                substr         |
171 | | swrd0len 12778 |
. . . . . . . . . . . . . . . . . 18
  Word  
             substr        |
172 | 75, 69, 171 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
                       substr        |
173 | 172 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
                            substr               |
174 | 170, 173 | eqtr2d 2486 |
. . . . . . . . . . . . . . 15
                             ++  substr         |
175 | | hash0 12548 |
. . . . . . . . . . . . . . . . 17
     |
176 | 175 | oveq2i 6301 |
. . . . . . . . . . . . . . . 16
                     |
177 | 107, 111 | nn0addcld 10929 |
. . . . . . . . . . . . . . . . . 18
                           |
178 | 177 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . 17
                           |
179 | 178 | addid1d 9833 |
. . . . . . . . . . . . . . . 16
                                   |
180 | 176, 179 | syl5req 2498 |
. . . . . . . . . . . . . . 15
                                       |
181 | 79, 144, 146, 83, 168, 174, 180 | splval2 12864 |
. . . . . . . . . . . . . 14
                      ++  ++  splice                              ++  substr  
   ++           ++   substr         ++     |
182 | 142, 181 | eqtrd 2485 |
. . . . . . . . . . . . 13
                                ++  ++        ++  substr      ++           ++   substr         ++     |
183 | 90, 105, 182 | 3eqtr4d 2495 |
. . . . . . . . . . . 12
                     ++          ++               ++  ++       |
184 | 1, 2, 3, 4 | efgtf 17372 |
. . . . . . . . . . . . . . 15
   ++  ++        ++  ++            ++  ++      
   ++  ++  splice                     ++  ++              ++  ++            |
185 | 184 | simprd 465 |
. . . . . . . . . . . . . 14
   ++  ++       ++  ++              ++  ++           |
186 | | ffn 5728 |
. . . . . . . . . . . . . 14
      ++  ++              ++  ++              ++  ++            ++  ++         |
187 | 72, 185, 186 | 3syl 18 |
. . . . . . . . . . . . 13
                        ++  ++            ++  ++         |
188 | | fnovrn 6444 |
. . . . . . . . . . . . 13
       ++  ++            ++  ++                     ++  ++                    ++  ++          ++  ++     |
189 | 187, 140,
70, 188 | syl3anc 1268 |
. . . . . . . . . . . 12
                                ++  ++          ++  ++     |
190 | 183, 189 | eqeltrd 2529 |
. . . . . . . . . . 11
                     ++          ++       ++  ++     |
191 | 1, 2, 3, 4 | efgi2 17375 |
. . . . . . . . . . 11
    ++  ++    ++          ++       ++  ++      ++  ++    ++          ++    |
192 | 72, 190, 191 | syl2anc 667 |
. . . . . . . . . 10
                     ++  ++    ++          ++    |
193 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 17404 |
. . . . . . . . . 10
          

          ++  ++    ++          ++     |
194 | 67, 71, 192, 193 | syl3anbrc 1192 |
. . . . . . . . 9
                               |
195 | | vex 3048 |
. . . . . . . . . . 11
 |
196 | | vex 3048 |
. . . . . . . . . . 11
 |
197 | 195, 196 | elec 7403 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)     |
198 | | breq2 4406 |
. . . . . . . . . 10
           
             |
199 | 197, 198 | syl5bb 261 |
. . . . . . . . 9
            ![] ]](rbrack.gif)
             |
200 | 194, 199 | syl5ibrcom 226 |
. . . . . . . 8
                              ![] ]](rbrack.gif)    |
201 | 200 | rexlimdvva 2886 |
. . . . . . 7
  

  
                       ![] ]](rbrack.gif)    |
202 | 66, 201 | sylbid 219 |
. . . . . 6
  

        ![] ]](rbrack.gif)    |
203 | 202 | ssrdv 3438 |
. . . . 5
  

       ![] ]](rbrack.gif)   |
204 | 203 | ralrimiva 2802 |
. . . 4
 
     
  ![] ]](rbrack.gif)   |
205 | | fvex 5875 |
. . . . . . 7
Word     |
206 | 1, 205 | eqeltri 2525 |
. . . . . 6
 |
207 | | erex 7387 |
. . . . . 6
 
   |
208 | 60, 206, 207 | mpisyl 21 |
. . . . 5
 
   |
209 | | ereq1 7370 |
. . . . . . 7
 
   |
210 | | eceq2 7401 |
. . . . . . . . 9
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
211 | 210 | sseq2d 3460 |
. . . . . . . 8
     
  ![] ]](rbrack.gif)
      ![] ]](rbrack.gif)    |
212 | 211 | ralbidv 2827 |
. . . . . . 7
  
   
  ![] ]](rbrack.gif)

      ![] ]](rbrack.gif)    |
213 | 209, 212 | anbi12d 717 |
. . . . . 6
       
  ![] ]](rbrack.gif) 


      ![] ]](rbrack.gif)     |
214 | 213 | elabg 3186 |
. . . . 5
 
  
      ![] ]](rbrack.gif)           ![] ]](rbrack.gif)     |
215 | 208, 214 | syl 17 |
. . . 4
 
    
      ![] ]](rbrack.gif)  


      ![] ]](rbrack.gif)     |
216 | 60, 204, 215 | mpbir2and 933 |
. . 3
 
   
      ![] ]](rbrack.gif)     |
217 | | intss1 4249 |
. . 3
       
  ![] ]](rbrack.gif)          
  ![] ]](rbrack.gif)     |
218 | 216, 217 | syl 17 |
. 2
 
        
  ![] ]](rbrack.gif)     |
219 | 5, 218 | syl5eqss 3476 |
1
 

  |