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 16341 |
. 2
          ![] ]](rbrack.gif)    |
6 | | efgcpbllem.1 |
. . . . . . 7
   
      concat
 concat    concat  concat     |
7 | 6 | relopabi 5072 |
. . . . . 6
 |
8 | 7 | a1i 11 |
. . . . 5
 
   |
9 | | efgred.d |
. . . . . . . . 9
 
      |
10 | | efgred.s |
. . . . . . . . 9
  Word           ..^                                  |
11 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 16371 |
. . . . . . . 8
  

  concat
 concat    concat  concat     |
12 | 11 | simp2bi 1004 |
. . . . . . 7
     |
13 | 12 | adantl 466 |
. . . . . 6
  

     |
14 | 11 | simp1bi 1003 |
. . . . . . 7
     |
15 | 14 | adantl 466 |
. . . . . 6
  

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

     |
18 | 11 | simp3bi 1005 |
. . . . . . . 8
     concat
 concat    concat  concat    |
19 | 18 | adantl 466 |
. . . . . . 7
  

     concat
 concat    concat  concat    |
20 | 17, 19 | ersym 7222 |
. . . . . 6
  

     concat
 concat    concat  concat    |
21 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 16371 |
. . . . . 6
  

  concat
 concat    concat  concat     |
22 | 13, 15, 20, 21 | syl3anbrc 1172 |
. . . . 5
  

       |
23 | 14 | ad2antrl 727 |
. . . . . 6
  

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

  concat
 concat    concat  concat     |
25 | 24 | simp2bi 1004 |
. . . . . . 7
     |
26 | 25 | ad2antll 728 |
. . . . . 6
  

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

      
  |
28 | 18 | ad2antrl 727 |
. . . . . . 7
  

         concat  concat
   concat  concat    |
29 | 24 | simp3bi 1005 |
. . . . . . . 8
     concat
 concat    concat  concat    |
30 | 29 | ad2antll 728 |
. . . . . . 7
  

         concat  concat
   concat  concat    |
31 | 27, 28, 30 | ertrd 7226 |
. . . . . 6
  

         concat  concat
   concat  concat    |
32 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 16371 |
. . . . . 6
  

  concat
 concat    concat  concat     |
33 | 23, 26, 31, 32 | syl3anbrc 1172 |
. . . . 5
  

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

   |
35 | | fviss 5857 |
. . . . . . . . . . . . . 14
Word    Word    |
36 | 1, 35 | eqsstri 3493 |
. . . . . . . . . . . . 13
Word    |
37 | | simpll 753 |
. . . . . . . . . . . . 13
  

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

 Word     |
39 | | simpr 461 |
. . . . . . . . . . . . 13
  

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

 Word     |
41 | | ccatcl 12391 |
. . . . . . . . . . . 12
  Word  
Word     concat
 Word     |
42 | 38, 40, 41 | syl2anc 661 |
. . . . . . . . . . 11
  

  concat  Word     |
43 | | simplr 754 |
. . . . . . . . . . . 12
  

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

 Word     |
45 | | ccatcl 12391 |
. . . . . . . . . . 11
   concat  Word  
Word      concat
 concat  Word     |
46 | 42, 44, 45 | syl2anc 661 |
. . . . . . . . . 10
  

   concat
 concat  Word     |
47 | 1 | efgrcl 16332 |
. . . . . . . . . . . 12
 
Word      |
48 | 47 | simprd 463 |
. . . . . . . . . . 11
 Word     |
49 | 48 | ad2antrr 725 |
. . . . . . . . . 10
  

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

   concat
 concat    |
51 | 34, 50 | erref 7230 |
. . . . . . . 8
  

   concat
 concat    concat  concat    |
52 | 51 | ex 434 |
. . . . . . 7
 
    concat  concat    concat
 concat     |
53 | 52 | pm4.71d 634 |
. . . . . 6
 
     concat  concat    concat
 concat      |
54 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 16371 |
. . . . . . 7
  

  concat
 concat    concat  concat     |
55 | | df-3an 967 |
. . . . . . 7
 
  concat  concat    concat
 concat  
 
   concat  concat    concat
 concat     |
56 | | anidm 644 |
. . . . . . . 8
 
   |
57 | 56 | anbi1i 695 |
. . . . . . 7
  

  concat  concat    concat  concat
     concat  concat 
  concat  concat     |
58 | 54, 55, 57 | 3bitri 271 |
. . . . . 6
  

  concat
 concat    concat  concat     |
59 | 53, 58 | syl6bbr 263 |
. . . . 5
 
       |
60 | 8, 22, 33, 59 | iserd 7236 |
. . . 4
 
   |
61 | 1, 2, 3, 4 | efgtf 16339 |
. . . . . . . . . 10
                 
 splice                                       |
62 | 61 | simprd 463 |
. . . . . . . . 9
                       |
63 | 62 | adantl 466 |
. . . . . . . 8
  

                       |
64 | | ffn 5666 |
. . . . . . . 8
                                       |
65 | | ovelrn 6348 |
. . . . . . . 8
                
    
                         |
66 | 63, 64, 65 | 3syl 20 |
. . . . . . 7
  

                               |
67 | | simplr 754 |
. . . . . . . . . 10
                     |
68 | 62 | ad2antlr 726 |
. . . . . . . . . . 11
                                         |
69 | | simprl 755 |
. . . . . . . . . . 11
                             |
70 | | simprr 756 |
. . . . . . . . . . 11
                  
    |
71 | 68, 69, 70 | fovrnd 6344 |
. . . . . . . . . 10
                             |
72 | 50 | adantr 465 |
. . . . . . . . . . 11
                     concat  concat    |
73 | 37 | adantr 465 |
. . . . . . . . . . . . . . . . 17
                  
  |
74 | 36, 73 | sseldi 3461 |
. . . . . . . . . . . . . . . 16
                  
Word     |
75 | 40 | adantr 465 |
. . . . . . . . . . . . . . . . 17
                   Word
    |
76 | | swrdcl 12432 |
. . . . . . . . . . . . . . . . 17
 Word  
 substr     Word
    |
77 | 75, 76 | syl 16 |
. . . . . . . . . . . . . . . 16
                    substr
    Word     |
78 | | ccatcl 12391 |
. . . . . . . . . . . . . . . 16
  Word   
substr     Word   
 concat  substr      Word     |
79 | 74, 77, 78 | syl2anc 661 |
. . . . . . . . . . . . . . 15
                    concat
 substr      Word     |
80 | 3 | efgmf 16330 |
. . . . . . . . . . . . . . . . . 18
         |
81 | 80 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . 17
  
        |
82 | 81 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
                           |
83 | 70, 82 | s2cld 12613 |
. . . . . . . . . . . . . . 15
                            Word
    |
84 | | ccatcl 12391 |
. . . . . . . . . . . . . . 15
   concat  substr      Word            Word   
  concat  substr      concat           Word     |
85 | 79, 83, 84 | syl2anc 661 |
. . . . . . . . . . . . . 14
                     concat  substr      concat           Word     |
86 | | swrdcl 12432 |
. . . . . . . . . . . . . . 15
 Word  
 substr         Word     |
87 | 75, 86 | syl 16 |
. . . . . . . . . . . . . 14
                    substr
        Word     |
88 | 44 | adantr 465 |
. . . . . . . . . . . . . 14
                  
Word     |
89 | | ccatass 12403 |
. . . . . . . . . . . . . 14
    concat  substr      concat           Word    substr         Word   Word   
    concat  substr      concat           concat  substr          concat     concat  substr  
   concat           concat   substr
        concat
    |
90 | 85, 87, 88, 89 | syl3anc 1219 |
. . . . . . . . . . . . 13
                       concat  substr  
   concat           concat  substr          concat     concat  substr  
   concat           concat   substr
        concat
    |
91 | | ccatcl 12391 |
. . . . . . . . . . . . . . . . 17
   substr     Word            Word   
  substr    
concat           Word     |
92 | 77, 83, 91 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
                     substr  
  concat           Word     |
93 | | ccatass 12403 |
. . . . . . . . . . . . . . . 16
  Word     substr  
  concat           Word    substr         Word   
  concat   substr  
  concat            concat  substr           concat    substr    
concat           concat  substr             |
94 | 74, 92, 87, 93 | syl3anc 1219 |
. . . . . . . . . . . . . . 15
                     concat   substr
    concat
           concat  substr           concat    substr     concat           concat
 substr             |
95 | | ccatass 12403 |
. . . . . . . . . . . . . . . . 17
  Word   
substr     Word            Word   
  concat  substr      concat            concat   substr    
concat              |
96 | 74, 77, 83, 95 | syl3anc 1219 |
. . . . . . . . . . . . . . . 16
                     concat  substr      concat            concat   substr
    concat
             |
97 | 96 | oveq1d 6214 |
. . . . . . . . . . . . . . 15
                      concat  substr
     concat           concat  substr            concat   substr
    concat
           concat  substr            |
98 | 1, 2, 3, 4 | efgtval 16340 |
. . . . . . . . . . . . . . . . . 18
 
                    splice                 |
99 | 67, 69, 70, 98 | syl3anc 1219 |
. . . . . . . . . . . . . . . . 17
                            splice                 |
100 | | splval 12510 |
. . . . . . . . . . . . . . . . . 18
          
                 Word      splice
                 substr    
concat           concat  substr            |
101 | 67, 69, 69, 83, 100 | syl13anc 1221 |
. . . . . . . . . . . . . . . . 17
                    splice
                 substr    
concat           concat  substr            |
102 | 99, 101 | eqtrd 2495 |
. . . . . . . . . . . . . . . 16
                              substr     concat           concat
 substr            |
103 | 102 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
                    concat
          concat    substr  
  concat           concat
 substr             |
104 | 94, 97, 103 | 3eqtr4rd 2506 |
. . . . . . . . . . . . . 14
                    concat
            concat  substr  
   concat           concat  substr            |
105 | 104 | oveq1d 6214 |
. . . . . . . . . . . . 13
                     concat          concat      concat  substr  
   concat           concat  substr          concat    |
106 | | lencl 12366 |
. . . . . . . . . . . . . . . . . . 19
 Word  
      |
107 | 74, 106 | syl 16 |
. . . . . . . . . . . . . . . . . 18
                         |
108 | | nn0uz 11005 |
. . . . . . . . . . . . . . . . . 18
     |
109 | 107, 108 | syl6eleq 2552 |
. . . . . . . . . . . . . . . . 17
                             |
110 | | elfznn0 11597 |
. . . . . . . . . . . . . . . . . 18
           |
111 | 110 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
                     |
112 | | uzaddcl 11021 |
. . . . . . . . . . . . . . . . 17
                       |
113 | 109, 111,
112 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
                               |
114 | 42 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
                    concat
 Word     |
115 | | ccatlen 12392 |
. . . . . . . . . . . . . . . . . 18
   concat  Word  
Word         concat  concat
       concat          |
116 | 114, 88, 115 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
                        concat  concat        concat          |
117 | | ccatlen 12392 |
. . . . . . . . . . . . . . . . . . . 20
  Word  
Word        concat               |
118 | 74, 75, 117 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . 19
                       concat               |
119 | | elfzuz3 11566 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
120 | 119 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
                             |
121 | 107 | nn0zd 10855 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
122 | | eluzadd 10999 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
123 | 120, 121,
122 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
124 | | lencl 12366 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Word  
      |
125 | 75, 124 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
126 | 125 | nn0cnd 10748 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
127 | 107 | nn0cnd 10748 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
128 | 126, 127 | addcomd 9681 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
129 | 111 | nn0cnd 10748 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
130 | 129, 127 | addcomd 9681 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
131 | 130 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
132 | 123, 128,
131 | 3eltr3d 2556 |
. . . . . . . . . . . . . . . . . . 19
                                         |
133 | 118, 132 | eqeltrd 2542 |
. . . . . . . . . . . . . . . . . 18
                       concat               |
134 | | lencl 12366 |
. . . . . . . . . . . . . . . . . . 19
 Word  
      |
135 | 88, 134 | syl 16 |
. . . . . . . . . . . . . . . . . 18
                         |
136 | | uzaddcl 11021 |
. . . . . . . . . . . . . . . . . 18
      concat                       concat                    |
137 | 133, 135,
136 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
                        concat                    |
138 | 116, 137 | eqeltrd 2542 |
. . . . . . . . . . . . . . . 16
                        concat  concat               |
139 | | elfzuzb 11563 |
. . . . . . . . . . . . . . . 16
               concat
 concat   
                concat
 concat                |
140 | 113, 138,
139 | sylanbrc 664 |
. . . . . . . . . . . . . . 15
                                 concat
 concat      |
141 | 1, 2, 3, 4 | efgtval 16340 |
. . . . . . . . . . . . . . 15
    concat  concat                concat
 concat   
                concat  concat        concat  concat 
splice                             |
142 | 72, 140, 70, 141 | syl3anc 1219 |
. . . . . . . . . . . . . 14
                                concat  concat        concat  concat 
splice                             |
143 | | wrd0 12369 |
. . . . . . . . . . . . . . . 16
Word    |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
                   Word     |
145 | | ccatcl 12391 |
. . . . . . . . . . . . . . . 16
   substr         Word   Word   
  substr         concat  Word     |
146 | 87, 88, 145 | syl2anc 661 |
. . . . . . . . . . . . . . 15
                     substr         concat
 Word     |
147 | | ccatrid 12402 |
. . . . . . . . . . . . . . . . . 18
  concat  substr  
   Word     concat  substr      concat   concat  substr        |
148 | 79, 147 | syl 16 |
. . . . . . . . . . . . . . . . 17
                     concat  substr      concat   concat  substr        |
149 | 148 | oveq1d 6214 |
. . . . . . . . . . . . . . . 16
                      concat  substr
     concat  concat   substr
        concat
    concat  substr  
   concat   substr         concat     |
150 | | ccatass 12403 |
. . . . . . . . . . . . . . . . 17
   concat  substr      Word    substr         Word   Word   
   concat
 substr      concat
 substr          concat    concat  substr      concat
  substr         concat     |
151 | 79, 87, 88, 150 | syl3anc 1219 |
. . . . . . . . . . . . . . . 16
                      concat  substr
     concat  substr          concat    concat  substr
     concat   substr
        concat
    |
152 | | ccatass 12403 |
. . . . . . . . . . . . . . . . . . 19
  Word   
substr     Word    substr         Word   
  concat  substr      concat  substr           concat   substr    
concat  substr             |
153 | 74, 77, 87, 152 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . 18
                     concat  substr      concat  substr           concat   substr  
  concat  substr
            |
154 | 111, 108 | syl6eleq 2552 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
155 | | eluzfz1 11574 |
. . . . . . . . . . . . . . . . . . . . . 22
    
      |
156 | 154, 155 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
157 | 125, 108 | syl6eleq 2552 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
158 | | eluzfz2 11575 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
159 | 157, 158 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
160 | | ccatswrd 12467 |
. . . . . . . . . . . . . . . . . . . . 21
  Word                                substr     concat  substr           substr           |
161 | 75, 156, 69, 159, 160 | syl13anc 1221 |
. . . . . . . . . . . . . . . . . . . 20
                     substr  
  concat  substr
          substr           |
162 | | swrdid 12438 |
. . . . . . . . . . . . . . . . . . . . 21
 Word  
 substr           |
163 | 75, 162 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
                    substr
          |
164 | 161, 163 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . 19
                     substr  
  concat  substr
           |
165 | 164 | oveq2d 6215 |
. . . . . . . . . . . . . . . . . 18
                    concat
  substr    
concat  substr            concat    |
166 | 153, 165 | eqtrd 2495 |
. . . . . . . . . . . . . . . . 17
                     concat  substr      concat  substr           concat    |
167 | 166 | oveq1d 6214 |
. . . . . . . . . . . . . . . 16
                      concat  substr
     concat  substr          concat    concat  concat
   |
168 | 149, 151,
167 | 3eqtr2rd 2502 |
. . . . . . . . . . . . . . 15
                     concat  concat     concat  substr      concat  concat   substr
        concat
    |
169 | | ccatlen 12392 |
. . . . . . . . . . . . . . . . 17
  Word   
substr     Word   
    concat  substr                substr         |
170 | 74, 77, 169 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
                       concat  substr
               substr         |
171 | | swrd0len 12435 |
. . . . . . . . . . . . . . . . . 18
  Word  
             substr        |
172 | 75, 69, 171 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
                       substr        |
173 | 172 | oveq2d 6215 |
. . . . . . . . . . . . . . . 16
                            substr               |
174 | 170, 173 | eqtr2d 2496 |
. . . . . . . . . . . . . . 15
                             concat  substr         |
175 | | hash0 12251 |
. . . . . . . . . . . . . . . . 17
     |
176 | 175 | oveq2i 6210 |
. . . . . . . . . . . . . . . 16
                     |
177 | 107, 111 | nn0addcld 10750 |
. . . . . . . . . . . . . . . . . 18
                           |
178 | 177 | nn0cnd 10748 |
. . . . . . . . . . . . . . . . 17
                           |
179 | 178 | addid1d 9679 |
. . . . . . . . . . . . . . . 16
                                   |
180 | 176, 179 | syl5req 2508 |
. . . . . . . . . . . . . . 15
                                       |
181 | 79, 144, 146, 83, 168, 174, 180 | splval2 12516 |
. . . . . . . . . . . . . 14
                      concat  concat
 splice                              concat  substr  
   concat           concat   substr
        concat
    |
182 | 142, 181 | eqtrd 2495 |
. . . . . . . . . . . . 13
                                concat  concat        concat  substr      concat
          concat   substr         concat
    |
183 | 90, 105, 182 | 3eqtr4d 2505 |
. . . . . . . . . . . 12
                     concat          concat               concat  concat       |
184 | 1, 2, 3, 4 | efgtf 16339 |
. . . . . . . . . . . . . . 15
   concat  concat        concat  concat            concat  concat          concat  concat
 splice                     concat  concat              concat  concat
           |
185 | 184 | simprd 463 |
. . . . . . . . . . . . . 14
   concat  concat       concat
 concat              concat  concat
          |
186 | | ffn 5666 |
. . . . . . . . . . . . . 14
      concat  concat              concat  concat
             concat  concat            concat  concat         |
187 | 72, 185, 186 | 3syl 20 |
. . . . . . . . . . . . 13
                        concat
 concat            concat  concat
        |
188 | | fnovrn 6347 |
. . . . . . . . . . . . 13
       concat
 concat            concat  concat
                    concat  concat
                   concat
 concat          concat  concat
    |
189 | 187, 140,
70, 188 | syl3anc 1219 |
. . . . . . . . . . . 12
                                concat  concat          concat  concat     |
190 | 183, 189 | eqeltrd 2542 |
. . . . . . . . . . 11
                     concat          concat       concat  concat     |
191 | 1, 2, 3, 4 | efgi2 16342 |
. . . . . . . . . . 11
    concat  concat    concat          concat       concat  concat      concat  concat
   concat          concat    |
192 | 72, 190, 191 | syl2anc 661 |
. . . . . . . . . 10
                     concat  concat    concat
         concat    |
193 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 16371 |
. . . . . . . . . 10
          

          concat
 concat    concat          concat     |
194 | 67, 71, 192, 193 | syl3anbrc 1172 |
. . . . . . . . 9
                               |
195 | | vex 3079 |
. . . . . . . . . . 11
 |
196 | | vex 3079 |
. . . . . . . . . . 11
 |
197 | 195, 196 | elec 7249 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)     |
198 | | breq2 4403 |
. . . . . . . . . 10
           
             |
199 | 197, 198 | syl5bb 257 |
. . . . . . . . 9
            ![] ]](rbrack.gif)
             |
200 | 194, 199 | syl5ibrcom 222 |
. . . . . . . 8
                              ![] ]](rbrack.gif)    |
201 | 200 | rexlimdvva 2952 |
. . . . . . 7
  

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

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

       ![] ]](rbrack.gif)   |
204 | 203 | ralrimiva 2829 |
. . . 4
 
     
  ![] ]](rbrack.gif)   |
205 | | fvex 5808 |
. . . . . . 7
Word     |
206 | 1, 205 | eqeltri 2538 |
. . . . . 6
 |
207 | | erex 7234 |
. . . . . 6
 
   |
208 | 60, 206, 207 | mpisyl 18 |
. . . . 5
 
   |
209 | | ereq1 7217 |
. . . . . . 7
 
   |
210 | | eceq2 7247 |
. . . . . . . . 9
   ![] ]](rbrack.gif)   ![] ]](rbrack.gif)   |
211 | 210 | sseq2d 3491 |
. . . . . . . 8
     
  ![] ]](rbrack.gif)
      ![] ]](rbrack.gif)    |
212 | 211 | ralbidv 2845 |
. . . . . . 7
  
   
  ![] ]](rbrack.gif)

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


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


      ![] ]](rbrack.gif)     |
216 | 60, 204, 215 | mpbir2and 913 |
. . 3
 
   
      ![] ]](rbrack.gif)     |
217 | | intss1 4250 |
. . 3
       
  ![] ]](rbrack.gif)          
  ![] ]](rbrack.gif)     |
218 | 216, 217 | syl 16 |
. 2
 
        
  ![] ]](rbrack.gif)     |
219 | 5, 218 | syl5eqss 3507 |
1
 

  |