Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . 6
Word     |
2 | | efgval.r |
. . . . . 6
~FG    |
3 | | efgval2.m |
. . . . . 6
 
       |
4 | | efgval2.t |
. . . . . 6
              splice                  |
5 | | efgred.d |
. . . . . 6
 
      |
6 | | efgred.s |
. . . . . 6
  Word           ..^                                  |
7 | 1, 2, 3, 4, 5, 6 | efgsdm 17392 |
. . . . 5

 Word       
  ..^                       |
8 | 7 | simp1bi 1024 |
. . . 4

Word      |
9 | | eldifsn 4100 |
. . . . 5
 Word   
 Word    |
10 | | lennncl 12695 |
. . . . 5
  Word        |
11 | 9, 10 | sylbi 199 |
. . . 4
 Word          |
12 | | fzo0end 12010 |
. . . 4
    
       ..^       |
13 | 8, 11, 12 | 3syl 18 |
. . 3
        ..^       |
14 | | nnm1nn0 10918 |
. . . . 5
    
        |
15 | 8, 11, 14 | 3syl 18 |
. . . 4
         |
16 | | eleq1 2519 |
. . . . . . 7
   ..^    
 ..^        |
17 | | fveq2 5870 |
. . . . . . . 8
           |
18 | 17 | breq2d 4417 |
. . . . . . 7
     
   
           |
19 | 16, 18 | imbi12d 322 |
. . . . . 6
    ..^             
  ..^    
            |
20 | 19 | imbi2d 318 |
. . . . 5
     ..^        
         ..^        
         |
21 | | eleq1 2519 |
. . . . . . 7
   ..^    
 ..^        |
22 | | fveq2 5870 |
. . . . . . . 8
           |
23 | 22 | breq2d 4417 |
. . . . . . 7
     
   
           |
24 | 21, 23 | imbi12d 322 |
. . . . . 6
    ..^             
  ..^        
        |
25 | 24 | imbi2d 318 |
. . . . 5
     ..^        
         ..^        
         |
26 | | eleq1 2519 |
. . . . . . 7
     ..^    
   ..^        |
27 | | fveq2 5870 |
. . . . . . . 8
               |
28 | 27 | breq2d 4417 |
. . . . . . 7
       
   
             |
29 | 26, 28 | imbi12d 322 |
. . . . . 6
      ..^             
    ..^    
              |
30 | 29 | imbi2d 318 |
. . . . 5
       ..^        
           ..^        
           |
31 | | eleq1 2519 |
. . . . . . 7
      
  ..^    
       ..^        |
32 | | fveq2 5870 |
. . . . . . . 8
      
                |
33 | 32 | breq2d 4417 |
. . . . . . 7
      
                          |
34 | 31, 33 | imbi12d 322 |
. . . . . 6
      
   ..^             
        ..^        
              |
35 | 34 | imbi2d 318 |
. . . . 5
      
 
  ..^              
         ..^    
                   |
36 | 1, 2 | efger 17380 |
. . . . . . . 8
 |
37 | 36 | a1i 11 |
. . . . . . 7
 
 ..^        |
38 | | eldifi 3557 |
. . . . . . . . 9
 Word   
Word   |
39 | | wrdf 12683 |
. . . . . . . . 9
 Word    ..^         |
40 | 8, 38, 39 | 3syl 18 |
. . . . . . . 8
    ..^         |
41 | 40 | ffvelrnda 6027 |
. . . . . . 7
 
 ..^            |
42 | 37, 41 | erref 7388 |
. . . . . 6
 
 ..^         
      |
43 | 42 | ex 436 |
. . . . 5
   ..^                |
44 | | elnn0uz 11203 |
. . . . . . . . . . . 12

      |
45 | | peano2fzor 12023 |
. . . . . . . . . . . 12
         ..^       ..^       |
46 | 44, 45 | sylanb 475 |
. . . . . . . . . . 11
     ..^       ..^       |
47 | 46 | 3adant1 1027 |
. . . . . . . . . 10
 
   ..^       ..^       |
48 | 47 | 3expia 1211 |
. . . . . . . . 9
 
     ..^      ..^        |
49 | 48 | imim1d 78 |
. . . . . . . 8
 
    ..^    
        
    ..^    
            |
50 | 40 | 3ad2ant1 1030 |
. . . . . . . . . . . . 13
 
   ..^         ..^         |
51 | 50, 47 | ffvelrnd 6028 |
. . . . . . . . . . . 12
 
   ..^            |
52 | | nn0p1nn 10916 |
. . . . . . . . . . . . . . . . 17

    |
53 | 52 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . 16
 
   ..^          |
54 | | nnuz 11201 |
. . . . . . . . . . . . . . . 16
     |
55 | 53, 54 | syl6eleq 2541 |
. . . . . . . . . . . . . . 15
 
   ..^              |
56 | | elfzolt2b 11938 |
. . . . . . . . . . . . . . . 16
    ..^    
     ..^       |
57 | 56 | 3ad2ant3 1032 |
. . . . . . . . . . . . . . 15
 
   ..^           ..^       |
58 | | elfzo3 11943 |
. . . . . . . . . . . . . . 15
    ..^                 ..^        |
59 | 55, 57, 58 | sylanbrc 671 |
. . . . . . . . . . . . . 14
 
   ..^         ..^       |
60 | 7 | simp3bi 1026 |
. . . . . . . . . . . . . . 15
 
 ..^                      |
61 | 60 | 3ad2ant1 1030 |
. . . . . . . . . . . . . 14
 
   ..^      
 ..^                      |
62 | | oveq1 6302 |
. . . . . . . . . . . . . . . . . . 19
           |
63 | 62 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . 18
                   |
64 | 63 | fveq2d 5874 |
. . . . . . . . . . . . . . . . 17
                           |
65 | 64 | rneqd 5065 |
. . . . . . . . . . . . . . . 16
                           |
66 | 27, 65 | eleq12d 2525 |
. . . . . . . . . . . . . . 15
                 
                     |
67 | 66 | rspcv 3148 |
. . . . . . . . . . . . . 14
    ..^    
 
 ..^                   
                     |
68 | 59, 61, 67 | sylc 62 |
. . . . . . . . . . . . 13
 
   ..^                          |
69 | | nn0cn 10886 |
. . . . . . . . . . . . . . . . . 18

  |
70 | 69 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . 17
 
   ..^        |
71 | | ax-1cn 9602 |
. . . . . . . . . . . . . . . . 17
 |
72 | | pncan 9886 |
. . . . . . . . . . . . . . . . 17
 
       |
73 | 70, 71, 72 | sylancl 669 |
. . . . . . . . . . . . . . . 16
 
   ..^            |
74 | 73 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
 
   ..^                    |
75 | 74 | fveq2d 5874 |
. . . . . . . . . . . . . 14
 
   ..^                            |
76 | 75 | rneqd 5065 |
. . . . . . . . . . . . 13
 
   ..^                            |
77 | 68, 76 | eleqtrd 2533 |
. . . . . . . . . . . 12
 
   ..^                      |
78 | 1, 2, 3, 4 | efgi2 17387 |
. . . . . . . . . . . 12
                                 |
79 | 51, 77, 78 | syl2anc 667 |
. . . . . . . . . . 11
 
   ..^         
        |
80 | 36 | a1i 11 |
. . . . . . . . . . . 12
 
   ..^        |
81 | 80 | ertr 7383 |
. . . . . . . . . . 11
 
   ..^                          
             |
82 | 79, 81 | mpan2d 681 |
. . . . . . . . . 10
 
   ..^                  
         |
83 | 82 | 3expia 1211 |
. . . . . . . . 9
 
     ..^                 
          |
84 | 83 | a2d 29 |
. . . . . . . 8
 
      ..^    
        
    ..^    
              |
85 | 49, 84 | syld 45 |
. . . . . . 7
 
    ..^    
        
    ..^    
              |
86 | 85 | expcom 437 |
. . . . . 6

    ..^        
         ..^                    |
87 | 86 | a2d 29 |
. . . . 5

    ..^                    ..^        
           |
88 | 20, 25, 30, 35, 43, 87 | nn0ind 11037 |
. . . 4
      
         ..^                       |
89 | 15, 88 | mpcom 37 |
. . 3
         ..^                      |
90 | 13, 89 | mpd 15 |
. 2
    
            |
91 | 1, 2, 3, 4, 5, 6 | efgsval 17393 |
. 2
                 |
92 | 90, 91 | breqtrrd 4432 |
1
    
      |