Step | Hyp | Ref
| Expression |
1 | | opelxp 4869 |
. . . 4
          
         |
2 | | opelxp 4869 |
. . . . 5
  
       |
3 | | swrdval 12827 |
. . . . . . 7
 
  substr  
     ..^    ..^              |
4 | | fzonlt0 11968 |
. . . . . . . . . . . . . . 15
 
   ..^    |
5 | 4 | biimprd 231 |
. . . . . . . . . . . . . 14
 
   ..^    |
6 | 5 | con2d 119 |
. . . . . . . . . . . . 13
 
   ..^    |
7 | 6 | impcom 437 |
. . . . . . . . . . . 12
  
 
 ..^   |
8 | | ss0 3768 |
. . . . . . . . . . . 12
  ..^  ..^   |
9 | 7, 8 | nsyl 125 |
. . . . . . . . . . 11
  
 
 ..^   |
10 | | dm0 5054 |
. . . . . . . . . . . . 13
 |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
  
 
  |
12 | 11 | sseq2d 3446 |
. . . . . . . . . . 11
  
 
  ..^  ..^    |
13 | 9, 12 | mtbird 308 |
. . . . . . . . . 10
  
 
 ..^   |
14 | 13 | iffalsed 3883 |
. . . . . . . . 9
  
 
   ..^
   ..^           
  |
15 | | 0ss 3766 |
. . . . . . . . . . . . 13
 |
16 | 15 | a1i 11 |
. . . . . . . . . . . 12
    
  |
17 | 4 | biimpac 494 |
. . . . . . . . . . . 12
    
 ..^   |
18 | 10 | a1i 11 |
. . . . . . . . . . . 12
    
  |
19 | 16, 17, 18 | 3sstr4d 3461 |
. . . . . . . . . . 11
    
 ..^   |
20 | 19 | iftrued 3880 |
. . . . . . . . . 10
    
   ..^
   ..^           
  ..^            |
21 | | zre 10965 |
. . . . . . . . . . . . . . . . 17
   |
22 | | zre 10965 |
. . . . . . . . . . . . . . . . 17
   |
23 | | lenlt 9730 |
. . . . . . . . . . . . . . . . . 18
 
     |
24 | 23 | bicomd 206 |
. . . . . . . . . . . . . . . . 17
 
 
   |
25 | 21, 22, 24 | syl2anr 486 |
. . . . . . . . . . . . . . . 16
 
 
   |
26 | | fzo0n 11967 |
. . . . . . . . . . . . . . . 16
 
   ..^      |
27 | 25, 26 | bitrd 261 |
. . . . . . . . . . . . . . 15
 
   ..^      |
28 | 27 | biimpac 494 |
. . . . . . . . . . . . . 14
    
 ..^     |
29 | 28 | mpteq1d 4477 |
. . . . . . . . . . . . 13
    
  ..^                    |
30 | 29 | dmeqd 5042 |
. . . . . . . . . . . 12
    
  ..^          
         |
31 | | ral0 3865 |
. . . . . . . . . . . . 13
        |
32 | | dmmptg 5339 |
. . . . . . . . . . . . 13
 
                |
33 | 31, 32 | mp1i 13 |
. . . . . . . . . . . 12
    
          |
34 | 30, 33 | eqtrd 2505 |
. . . . . . . . . . 11
    
  ..^            |
35 | | mptrel 4966 |
. . . . . . . . . . . 12
  ..^           |
36 | | reldm0 5058 |
. . . . . . . . . . . 12
   ..^             ..^          
 ..^             |
37 | 35, 36 | mp1i 13 |
. . . . . . . . . . 11
    
   ..^            ..^             |
38 | 34, 37 | mpbird 240 |
. . . . . . . . . 10
    
  ..^            |
39 | 20, 38 | eqtrd 2505 |
. . . . . . . . 9
    
   ..^
   ..^           
  |
40 | 14, 39 | pm2.61ian 807 |
. . . . . . . 8
 
    ..^    ..^              |
41 | 40 | 3adant1 1048 |
. . . . . . 7
 
    ..^
   ..^           
  |
42 | 3, 41 | eqtrd 2505 |
. . . . . 6
 
  substr  
    |
43 | 42 | 3expb 1232 |
. . . . 5
 

   substr       |
44 | 2, 43 | sylan2b 483 |
. . . 4
 
     
 substr       |
45 | 1, 44 | sylbi 200 |
. . 3
            substr  
    |
46 | | df-substr 12715 |
. . . 4
substr            ..^        ..^                          |
47 | | ovex 6336 |
. . . . . 6
 ..^            |
48 | 47 | mptex 6152 |
. . . . 5
  ..^                       |
49 | | 0ex 4528 |
. . . . 5
 |
50 | 48, 49 | ifex 3940 |
. . . 4
       ..^     
  ..^                         |
51 | 46, 50 | dmmpt2 6882 |
. . 3
substr      |
52 | 45, 51 | eleq2s 2567 |
. 2
       substr  substr  
    |
53 | | df-ov 6311 |
. . 3
 substr  
  substr          |
54 | | ndmfv 5903 |
. . 3
       substr substr           |
55 | 53, 54 | syl5eq 2517 |
. 2
       substr  substr  
    |
56 | 52, 55 | pm2.61i 169 |
1
 substr  
   |