Proof of Theorem usgra2wlkspthlem1
Step | Hyp | Ref
| Expression |
1 | | wrdf 12723 |
. . 3
 Word
   ..^      
  |
2 | | simpl 464 |
. . . . . . . . . . . . 13
     ..^                     ..^      
  |
3 | 2 | adantr 472 |
. . . . . . . . . . . 12
      ..^                                
  ..^                                ..^         |
4 | | oveq2 6316 |
. . . . . . . . . . . . . . . 16
      ..^      ..^   |
5 | | fzo0to2pr 12027 |
. . . . . . . . . . . . . . . 16
 ..^     |
6 | 4, 5 | syl6req 2522 |
. . . . . . . . . . . . . . 15
         ..^       |
7 | 6 | adantr 472 |
. . . . . . . . . . . . . 14
               ..^       |
8 | 7 | ad2antlr 741 |
. . . . . . . . . . . . 13
      ..^                                
  ..^                                 ..^       |
9 | 8 | feq2d 5725 |
. . . . . . . . . . . 12
      ..^                                
  ..^                                    
   ..^          |
10 | 3, 9 | mpbird 240 |
. . . . . . . . . . 11
      ..^                                
  ..^                                      |
11 | | preq1 4042 |
. . . . . . . . . . . . . . . . . . . 20
                         |
12 | 11 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . 19
                        
         
        |
13 | | preq2 4043 |
. . . . . . . . . . . . . . . . . . . 20
                         |
14 | 13 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . 19
                        
                  |
15 | 12, 14 | bi2anan9 890 |
. . . . . . . . . . . . . . . . . 18
                                                   
                                   |
16 | 15 | 3adant3 1050 |
. . . . . . . . . . . . . . . . 17
                                                   
                                   |
17 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
18 | 17 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                        
         
        |
19 | 18 | anbi1d 719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                         
                                   |
20 | 19 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                                                                                             |
21 | | eqtr2 2491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                 |
22 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
23 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
       |
24 | 23 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
       |
25 | 22, 24 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
26 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
28 | 25, 27 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
       |
29 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           |
30 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
31 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
       |
32 | 31 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
       |
33 | 30, 32 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
34 | 29, 33 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
   |
35 | 28, 34 | anim12i 576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
         
    |
36 | 35 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                       |
37 | | preq12bg 4146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              
  
           
 
                       |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                     
 
                       |
39 | | eqtr 2490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
  |
40 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
  |
41 | 39, 40 | jaoi 386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                         |
42 | 38, 41 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                         |
43 | 21, 42 | syl5com 30 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                           |
44 | 43 | impcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                           |
45 | 20, 44 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                     |
46 | 45 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                                 
   |
47 | 46 | necon3d 2664 |
. . . . . . . . . . . . . . . . . . . . 21
                                                         
           |
48 | 47 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
                                                             ..^                |
49 | 48 | exp31 615 |
. . . . . . . . . . . . . . . . . . 19
                                                           ..^  
               |
50 | 49 | com25 93 |
. . . . . . . . . . . . . . . . . 18
                                                 ..^  
                         |
51 | 50 | 3impia 1228 |
. . . . . . . . . . . . . . . . 17
                                                ..^  
          
             |
52 | 16, 51 | sylbid 223 |
. . . . . . . . . . . . . . . 16
                                                        ..^  
          
             |
53 | 52 | imp 436 |
. . . . . . . . . . . . . . 15
           
                                             ..^                          |
54 | 53 | com13 82 |
. . . . . . . . . . . . . 14
               ..^  
                                                                 |
55 | 4 | feq2d 5725 |
. . . . . . . . . . . . . . . 16
         ..^      
   ..^      |
56 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . 20
                   |
57 | 56 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . 19
             
       |
58 | 57 | 3anbi2d 1370 |
. . . . . . . . . . . . . . . . . 18
                   
    
   
    |
59 | 4, 5 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . 20
      ..^          |
60 | 59 | raleqdv 2979 |
. . . . . . . . . . . . . . . . . . 19
      
 ..^                                                       |
61 | | 2wlklem 25373 |
. . . . . . . . . . . . . . . . . . 19
 
                                                                  |
62 | 60, 61 | syl6bb 269 |
. . . . . . . . . . . . . . . . . 18
      
 ..^                                                                      |
63 | 58, 62 | anbi12d 725 |
. . . . . . . . . . . . . . . . 17
                    
  ..^                           
                                                       |
64 | 63 | imbi1d 324 |
. . . . . . . . . . . . . . . 16
                     
  ..^                                               
                                                      |
65 | 55, 64 | imbi12d 327 |
. . . . . . . . . . . . . . 15
          ..^                      
  ..^                                          ..^                                                                     |
66 | 65 | adantr 472 |
. . . . . . . . . . . . . 14
                ..^                      
  ..^                                          ..^                                                                     |
67 | 54, 66 | mpbird 240 |
. . . . . . . . . . . . 13
               ..^      
               
  ..^                                        |
68 | 67 | impcom 437 |
. . . . . . . . . . . 12
     ..^                                 
  ..^                                       |
69 | 68 | imp 436 |
. . . . . . . . . . 11
      ..^                                
  ..^                                       |
70 | 10, 69 | jca 541 |
. . . . . . . . . 10
      ..^                                
  ..^                                    
           |
71 | | c0ex 9655 |
. . . . . . . . . . . . 13
 |
72 | | 1ex 9656 |
. . . . . . . . . . . . 13
 |
73 | 71, 72 | pm3.2i 462 |
. . . . . . . . . . . 12
   |
74 | | 0ne1 10699 |
. . . . . . . . . . . 12
 |
75 | 73, 74 | pm3.2i 462 |
. . . . . . . . . . 11
 

  |
76 | | eqid 2471 |
. . . . . . . . . . . 12
       |
77 | 76 | f12dfv 6190 |
. . . . . . . . . . 11
   

       
       
            |
78 | 75, 77 | mp1i 13 |
. . . . . . . . . 10
      ..^                                
  ..^                                    
       
            |
79 | 70, 78 | mpbird 240 |
. . . . . . . . 9
      ..^                                
  ..^                                      |
80 | | df-f1 5594 |
. . . . . . . . 9
                    |
81 | 79, 80 | sylib 201 |
. . . . . . . 8
      ..^                                
  ..^                                    
    |
82 | 81 | simprd 470 |
. . . . . . 7
      ..^                                
  ..^                            
   |
83 | 82 | ex 441 |
. . . . . 6
     ..^                                 
  ..^                                |
84 | 83 | expcom 442 |
. . . . 5
               ..^      
               
  ..^                                 |
85 | 84 | ex 441 |
. . . 4
              ..^      
                  ..^                                  |
86 | 85 | com13 82 |
. . 3
    ..^      
    
    
                  ..^                                  |
87 | 1, 86 | syl 17 |
. 2
 Word
    
    
                  ..^                                  |
88 | 87 | 3imp 1224 |
1
  Word    
                     
 ..^                                |