Step | Hyp | Ref
| Expression |
1 | | eqwrd 12708 |
. . 3
  Word
Word            
 ..^                  |
2 | 1 | 3adant3 1028 |
. 2
  Word
Word  ..^                  ..^                  |
3 | | elfzofz 11935 |
. . . . . . . . 9
  ..^    
          |
4 | | fzosplit 11951 |
. . . . . . . . 9
          ..^       ..^  ..^        |
5 | 3, 4 | syl 17 |
. . . . . . . 8
  ..^    
 ..^       ..^  ..^        |
6 | 5 | 3ad2ant3 1031 |
. . . . . . 7
  Word
Word  ..^       ..^       ..^  ..^        |
7 | 6 | adantr 467 |
. . . . . 6
   Word
Word
 ..^                ..^       ..^  ..^        |
8 | 7 | raleqdv 2993 |
. . . . 5
   Word
Word
 ..^                
 ..^                 ..^  ..^                  |
9 | | ralunb 3615 |
. . . . 5
 
  ..^  ..^              
 
 ..^         
  ..^                 |
10 | 8, 9 | syl6bb 265 |
. . . 4
   Word
Word
 ..^                
 ..^                 ..^            ..^                  |
11 | | 3simpa 1005 |
. . . . . . 7
  Word
Word  ..^       Word Word    |
12 | 11 | adantr 467 |
. . . . . 6
   Word
Word
 ..^               
Word Word    |
13 | | elfzonn0 11960 |
. . . . . . . . 9
  ..^    
  |
14 | 13 | 3ad2ant3 1031 |
. . . . . . . 8
  Word
Word  ..^        |
15 | 14 | adantr 467 |
. . . . . . 7
   Word
Word
 ..^                 |
16 | | 0nn0 10884 |
. . . . . . 7
 |
17 | 15, 16 | jctil 540 |
. . . . . 6
   Word
Word
 ..^               
   |
18 | | elfzo0le 11959 |
. . . . . . . 8
  ..^    
      |
19 | 18 | 3ad2ant3 1031 |
. . . . . . 7
  Word
Word  ..^            |
20 | 19 | adantr 467 |
. . . . . 6
   Word
Word
 ..^                     |
21 | | breq2 4406 |
. . . . . . . 8
        
    
       |
22 | 21 | adantl 468 |
. . . . . . 7
   Word
Word
 ..^               
   
       |
23 | 20, 22 | mpbid 214 |
. . . . . 6
   Word
Word
 ..^                     |
24 | | swrdspsleq 12805 |
. . . . . . 7
   Word
Word  
     
        substr
     substr       ..^             |
25 | 24 | bicomd 205 |
. . . . . 6
   Word
Word  
     
       
 ..^         
 substr      substr        |
26 | 12, 17, 20, 23, 25 | syl112anc 1272 |
. . . . 5
   Word
Word
 ..^                
 ..^         
 substr      substr        |
27 | | lencl 12687 |
. . . . . . . . 9
 Word       |
28 | 27 | 3ad2ant1 1029 |
. . . . . . . 8
  Word
Word  ..^            |
29 | 14, 28 | jca 535 |
. . . . . . 7
  Word
Word  ..^      
       |
30 | 29 | adantr 467 |
. . . . . 6
   Word
Word
 ..^                       |
31 | | nn0re 10878 |
. . . . . . . . . 10
    
      |
32 | 31 | leidd 10180 |
. . . . . . . . 9
    
   
      |
33 | 27, 32 | syl 17 |
. . . . . . . 8
 Word           |
34 | 33 | 3ad2ant1 1029 |
. . . . . . 7
  Word
Word  ..^         
      |
35 | 34 | adantr 467 |
. . . . . 6
   Word
Word
 ..^                         |
36 | | breq2 4406 |
. . . . . . . 8
        
                    |
37 | 36 | adantl 468 |
. . . . . . 7
   Word
Word
 ..^                           
       |
38 | 35, 37 | mpbid 214 |
. . . . . 6
   Word
Word
 ..^                         |
39 | | swrdspsleq 12805 |
. . . . . . 7
   Word
Word  
         
   
   
        substr          substr           ..^                 |
40 | 39 | bicomd 205 |
. . . . . 6
   Word
Word  
         
   
   
         ..^             
 substr          substr            |
41 | 12, 30, 35, 38, 40 | syl112anc 1272 |
. . . . 5
   Word
Word
 ..^                
 ..^               substr          substr            |
42 | 26, 41 | anbi12d 717 |
. . . 4
   Word
Word
 ..^                   ..^            ..^              
  substr      substr      substr          substr             |
43 | 10, 42 | bitrd 257 |
. . 3
   Word
Word
 ..^                
 ..^                substr      substr      substr          substr             |
44 | 43 | pm5.32da 647 |
. 2
  Word
Word  ..^               
  ..^              
        
  substr      substr      substr          substr              |
45 | 2, 44 | bitrd 257 |
1
  Word
Word  ..^                  substr      substr      substr          substr              |