Proof of Theorem swrdccat
Step | Hyp | Ref
| Expression |
1 | | swrdccatin12.l |
. . . . 5
     |
2 | 1 | swrdccat3 12902 |
. . . 4
  Word
Word       
   
         ++  substr         substr       
  substr
           substr     ++  substr             |
3 | 2 | imp 436 |
. . 3
   Word
Word      
   
       
  ++  substr         substr       
  substr
           substr     ++  substr            |
4 | | lencl 12737 |
. . . . . 6
 Word       |
5 | 4 | adantr 472 |
. . . . 5
  Word
Word        |
6 | 1 | eqcomi 2480 |
. . . . . . 7
     |
7 | 6 | eleq1i 2540 |
. . . . . 6
    
  |
8 | | elfz2nn0 11911 |
. . . . . . . . 9
    

   |
9 | | iftrue 3878 |
. . . . . . . . . . . . . . . . . 18
  
 
   |
10 | 9 | adantl 473 |
. . . . . . . . . . . . . . . . 17
    Word Word 
 
           |
11 | 10 | opeq2d 4165 |
. . . . . . . . . . . . . . . 16
    Word Word 
 
       
 
       |
12 | 11 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
    Word Word 
 
     substr
        
 substr       |
13 | | iftrue 3878 |
. . . . . . . . . . . . . . . . . . . 20
     
          |
14 | 13 | opeq1d 4164 |
. . . . . . . . . . . . . . . . . . 19
     
            
       |
15 | 14 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
    substr                 substr           |
16 | 15 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
     Word Word 
 
      substr   
             substr           |
17 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . 21
  Word
Word  Word   |
18 | | nn0z 10984 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
19 | | nn0z 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
20 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
21 | | zsubcl 11003 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
22 | 20, 21 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
     |
23 | | nn0z 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
24 | 23 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
25 | | zsubcl 11003 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
26 | 24, 25 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
     |
27 | 22, 26 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         |
28 | 18, 27 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . 21
   
         |
29 | 17, 28 | anim12i 576 |
. . . . . . . . . . . . . . . . . . . 20
   Word
Word   
    Word          |
30 | | 3anass 1011 |
. . . . . . . . . . . . . . . . . . . 20
  Word 
 
   Word          |
31 | 29, 30 | sylibr 217 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   
    Word   
    |
32 | 31 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . 18
 
     Word Word 
 
      Word        |
33 | | nn0re 10902 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
34 | | nn0re 10902 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
35 | 33, 34 | anim12i 576 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
36 | | nn0re 10902 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
37 | | subge0 10148 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
    |
38 | 37 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
   |
39 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
40 | 39 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
41 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
42 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
   |
43 | 42 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
44 | 40, 41, 43 | 3jca 1210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
45 | | letr 9745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
    |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
47 | 46 | expcomd 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
48 | 38, 47 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       

    |
49 | 48 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
    |
50 | 35, 36, 49 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
    |
51 | 50 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
   Word
Word   
     

    |
52 | 51 | imp 436 |
. . . . . . . . . . . . . . . . . . . 20
    Word Word 
 
     

   |
53 | 52 | impcom 437 |
. . . . . . . . . . . . . . . . . . 19
 
     Word Word 
 
       |
54 | 34 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
55 | 54 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
   |
56 | 33 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
   |
58 | 36 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
   |
59 | 55, 57, 58 | 3jca 1210 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     |
60 | 59 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . 21
   Word
Word   
   
   |
61 | 60 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . 20
 
     Word Word 
 
         |
62 | | lesub1 10129 |
. . . . . . . . . . . . . . . . . . . 20
 
 
  
    |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
     Word Word 
 
       
     |
64 | 53, 63 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
 
     Word Word 
 
       
   |
65 | | swrdlend 12841 |
. . . . . . . . . . . . . . . . . 18
  Word 
 
      
 substr            |
66 | 32, 64, 65 | sylc 61 |
. . . . . . . . . . . . . . . . 17
 
     Word Word 
 
      substr  
        |
67 | 16, 66 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
 
     Word Word 
 
      substr   
              |
68 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . 19

    
        |
69 | 68 | opeq1d 4164 |
. . . . . . . . . . . . . . . . . 18

    
                  |
70 | 69 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17

   substr                 substr         |
71 | 17 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
   Word
Word   
  
Word   |
72 | 71 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
    Word Word 
 
   
Word   |
73 | | 0zd 10973 |
. . . . . . . . . . . . . . . . . . 19
    Word Word 
 
      |
74 | 24, 18, 25 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
75 | 74 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
   Word
Word   
       |
76 | 75 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
    Word Word 
 
        |
77 | 72, 73, 76 | 3jca 1210 |
. . . . . . . . . . . . . . . . . 18
    Word Word 
 
     Word
     |
78 | 54, 36 | anim12i 576 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
79 | 78 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
   Word
Word   
       |
80 | | suble0 10149 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   
         |
82 | 81 | biimpar 493 |
. . . . . . . . . . . . . . . . . 18
    Word Word 
 
     
  |
83 | | swrdlend 12841 |
. . . . . . . . . . . . . . . . . 18
  Word

    
 substr      
   |
84 | 77, 82, 83 | sylc 61 |
. . . . . . . . . . . . . . . . 17
    Word Word 
 
     substr
        |
85 | 70, 84 | sylan9eq 2525 |
. . . . . . . . . . . . . . . 16
  
    Word Word    
     substr
  
              |
86 | 67, 85 | pm2.61ian 807 |
. . . . . . . . . . . . . . 15
    Word Word 
 
     substr
  
              |
87 | 12, 86 | oveq12d 6326 |
. . . . . . . . . . . . . 14
    Word Word 
 
      substr          ++
 substr    
              substr     ++    |
88 | | swrdcl 12829 |
. . . . . . . . . . . . . . . . . 18
 Word  substr     Word   |
89 | | ccatrid 12782 |
. . . . . . . . . . . . . . . . . 18
  substr     Word   substr     ++   substr       |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
 Word   substr
    ++   substr       |
91 | 90 | adantr 472 |
. . . . . . . . . . . . . . . 16
  Word
Word    substr     ++   substr       |
92 | 91 | adantr 472 |
. . . . . . . . . . . . . . 15
   Word
Word   
     substr     ++   substr       |
93 | 92 | adantr 472 |
. . . . . . . . . . . . . 14
    Word Word 
 
      substr     ++   substr       |
94 | 87, 93 | eqtrd 2505 |
. . . . . . . . . . . . 13
    Word Word 
 
      substr          ++
 substr    
             substr       |
95 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . 19

       |
96 | 95 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . 18
    Word Word 
 
  
        |
97 | 96 | opeq2d 4165 |
. . . . . . . . . . . . . . . . 17
    Word Word 
 
  
    
 
       |
98 | 97 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
    Word Word 
 
  
  substr
        
 substr       |
99 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . 21
  Word
Word  Word   |
100 | 99, 20, 18 | 3anim123i 1215 |
. . . . . . . . . . . . . . . . . . . 20
   Word
Word  
  
Word    |
101 | 100 | 3expb 1232 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   
    Word
   |
102 | | swrdlend 12841 |
. . . . . . . . . . . . . . . . . . 19
  Word
   substr        |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   Word
Word   
     substr        |
104 | 103 | imp 436 |
. . . . . . . . . . . . . . . . 17
    Word Word 
 
     substr
      |
105 | 104 | 3adant2 1049 |
. . . . . . . . . . . . . . . 16
    Word Word 
 
  
  substr
      |
106 | 98, 105 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
    Word Word 
 
  
  substr
        
  |
107 | 56, 36, 37 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
   |
108 | 107 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . 20
   
  
    |
109 | 108 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   
   
     |
110 | 109 | imp 436 |
. . . . . . . . . . . . . . . . . 18
    Word Word 
 
   
    |
111 | 110 | 3adant2 1049 |
. . . . . . . . . . . . . . . . 17
    Word Word 
 
  

    |
112 | 111, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
    Word Word 
 
  
              
         |
113 | 112 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
    Word Word 
 
  
  substr
  
             substr           |
114 | 106, 113 | oveq12d 6326 |
. . . . . . . . . . . . . 14
    Word Word 
 
  
   substr          ++
 substr    
             ++  substr  
         |
115 | | swrdcl 12829 |
. . . . . . . . . . . . . . . . . 18
 Word  substr        
Word   |
116 | 115 | adantl 473 |
. . . . . . . . . . . . . . . . 17
  Word
Word   substr  
      Word   |
117 | | ccatlid 12781 |
. . . . . . . . . . . . . . . . 17
  substr        
Word  ++  substr  
        substr           |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
  Word
Word  
++  substr           substr           |
119 | 118 | adantr 472 |
. . . . . . . . . . . . . . 15
   Word
Word   
    ++  substr  
        substr           |
120 | 119 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
    Word Word 
 
  
  ++  substr  
        substr           |
121 | 114, 120 | eqtrd 2505 |
. . . . . . . . . . . . 13
    Word Word 
 
  
   substr          ++
 substr    
             substr           |
122 | 95 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . 16
    Word Word 
 
  
        |
123 | 122 | opeq2d 4165 |
. . . . . . . . . . . . . . 15
    Word Word 
 
  
    
 
       |
124 | 123 | oveq2d 6324 |
. . . . . . . . . . . . . 14
    Word Word 
 
  
  substr         
 substr       |
125 | 33, 36, 37 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
    |
126 | 125 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
   |
127 | 126 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
   Word
Word   
    
    |
128 | 127 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
   Word
Word   
    

   |
129 | 128 | con3dimp 448 |
. . . . . . . . . . . . . . . . . 18
    Word Word 
 
  

    |
130 | 129 | 3adant2 1049 |
. . . . . . . . . . . . . . . . 17
    Word Word 
 
  

    |
131 | 130, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
    Word Word 
 
  
            |
132 | 131 | opeq1d 4164 |
. . . . . . . . . . . . . . 15
    Word Word 
 
  
                      |
133 | 132 | oveq2d 6324 |
. . . . . . . . . . . . . 14
    Word Word 
 
  
  substr   
             substr         |
134 | 124, 133 | oveq12d 6326 |
. . . . . . . . . . . . 13
    Word Word 
 
  
   substr    
 
   ++  substr   
               substr     ++  substr          |
135 | 94, 121, 134 | 2if2 3920 |
. . . . . . . . . . . 12
   Word
Word   
     substr          ++
 substr    
                substr       
  substr
           substr     ++  substr            |
136 | 135 | exp32 616 |
. . . . . . . . . . 11
  Word
Word   


  substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
137 | 136 | com12 31 |
. . . . . . . . . 10
 
   Word Word 

  substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
138 | 137 | 3adant3 1050 |
. . . . . . . . 9
 
   Word
Word     substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
139 | 8, 138 | sylbi 200 |
. . . . . . . 8
       Word
Word     substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
140 | 139 | adantr 472 |
. . . . . . 7
     
             Word Word 

  substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
141 | 140 | com13 82 |
. . . . . 6

  Word
Word       
   
         substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
142 | 7, 141 | sylbi 200 |
. . . . 5
    
 
Word Word                     substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr              |
143 | 5, 142 | mpcom 36 |
. . . 4
  Word
Word       
   
         substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr             |
144 | 143 | imp 436 |
. . 3
   Word
Word      
   
       
  substr    
 
   ++  substr   
               
 substr  
       substr            substr     ++  substr            |
145 | 3, 144 | eqtr4d 2508 |
. 2
   Word
Word      
   
       
  ++  substr       substr          ++
 substr    
              |
146 | 145 | ex 441 |
1
  Word
Word       
   
         ++  substr       substr          ++
 substr    
               |