Proof of Theorem clwlkisclwwlklem2a
Step | Hyp | Ref
| Expression |
1 | | simpl 463 |
. . . . . . . . . 10
           USGrph Word
     
lastS        
 ..^                                              ..^                 |
2 | | usgraf1o 25141 |
. . . . . . . . . . . . . 14
 USGrph       |
3 | 2 | 3ad2ant1 1035 |
. . . . . . . . . . . . 13
  USGrph
Word            |
4 | 3 | adantr 471 |
. . . . . . . . . . . 12
   USGrph
Word       lastS      
 
 ..^                                                   |
5 | 4 | ad2antrl 739 |
. . . . . . . . . . 11
           USGrph Word
     
lastS        
 ..^                                              ..^               |
6 | | elfzo0 11993 |
. . . . . . . . . . . . . . . . . . . . 21
  ..^       
               |
7 | | lencl 12728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 Word       |
8 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
  |
9 | 8 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                    
  |
10 | | elnn0z 10984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38

    |
11 | | 0red 9675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
         |
12 | | zre 10975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
   |
13 | 12 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
      
  |
14 | | nn0re 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
    
      |
15 | | 2re 10712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
    
  |
17 | 14, 16 | resubcld 10080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
    
        |
18 | 17 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
               |
19 | | lelttr 9755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
        
                |
20 | 11, 13, 18, 19 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
                         |
21 | | nn0z 10994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
    
      |
22 | | 2z 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
    
  |
24 | 21, 23 | zsubcld 11079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
    
        |
25 | 24 | anim1i 576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
                             |
26 | | elnnz 10981 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
      
                |
27 | 25, 26 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
                     |
28 | | nn0cn 10913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
    
      |
29 | | peano2cnm 9971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
    
        |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
    
        |
31 | 30 | subid1d 10006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
    
                |
32 | 31 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
    
                    |
33 | | 1cnd 9690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
    
  |
34 | 28, 33, 33 | subsub4d 10048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
    
                  |
35 | | 1p1e2 10756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
   |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
    
    |
37 | 36 | oveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
    
                |
38 | 34, 37 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
    
                |
39 | 32, 38 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
    
                  |
40 | 39 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
    
                    |
41 | 40 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
                       
         |
42 | 27, 41 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
                         |
43 | 42 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    
      
             |
44 | 43 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
                           |
45 | 20, 44 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
                             |
46 | 45 | exp4b 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     
 
                     |
47 | 46 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 
                           |
48 | 47 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                             |
49 | 10, 48 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37

    
                     |
50 | 49 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                           |
51 | 50 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
                    |
52 | 51 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                 |
53 | 52 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                 |
54 | | df-2 10701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
    
    |
56 | 55 | oveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    
                |
57 | 31 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
    
                |
58 | 57 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    
                    |
59 | 56, 34, 58 | 3eqtr2d 2502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
                  |
60 | 59 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                         |
61 | 60 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             
             |
62 | 61 | biimpcd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
                    |
63 | 62 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                 |
64 | 63 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                 |
65 | | elfzo0 11993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  ..^                                   |
66 | 9, 53, 64, 65 | syl3anbrc 1198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                    
 ..^             |
67 | 66 | exp32 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  
 ..^               |
68 | 67 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                         
 ..^                |
69 | 68 | com24 90 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                         
 ..^                |
70 | 69 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    
    
               ..^                 |
71 | 70 | com25 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

      
    
             ..^                 |
72 | 71 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
   
             ..^                |
73 | 72 | 3adant2 1033 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              
    
             ..^                |
74 | 73 | com14 91 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
    
        
            
 ..^                |
75 | 7, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Word 
   
        
            
 ..^                |
76 | 75 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . 22
  Word      
                    
 ..^               |
77 | 76 | 3adant1 1032 |
. . . . . . . . . . . . . . . . . . . . 21
  USGrph
Word              
            
 ..^               |
78 | 6, 77 | syl7bi 238 |
. . . . . . . . . . . . . . . . . . . 20
  USGrph
Word               ..^        ..^               |
79 | 78 | com13 83 |
. . . . . . . . . . . . . . . . . . 19
  ..^      
         USGrph Word
    
 ..^               |
80 | 79 | imp31 438 |
. . . . . . . . . . . . . . . . . 18
    ..^               USGrph Word
       ..^             |
81 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . 21
           |
82 | | oveq1 6327 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
83 | 82 | fveq2d 5896 |
. . . . . . . . . . . . . . . . . . . . 21
          
    |
84 | 81, 83 | preq12d 4072 |
. . . . . . . . . . . . . . . . . . . 20
                             |
85 | 84 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . 19
                               |
86 | 85 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
     ..^               USGrph
Word      
                               |
87 | 80, 86 | rspcdv 3165 |
. . . . . . . . . . . . . . . . 17
    ..^               USGrph Word
         ..^                                         |
88 | 87 | ex 440 |
. . . . . . . . . . . . . . . 16
   ..^             
  USGrph Word         ..^                                          |
89 | 88 | com13 83 |
. . . . . . . . . . . . . . 15
 
 ..^                        
  USGrph Word         ..^             
         
       |
90 | 89 | ad2antrl 739 |
. . . . . . . . . . . . . 14
  lastS        
 ..^                                              USGrph
Word         ..^             
         
       |
91 | 90 | impcom 436 |
. . . . . . . . . . . . 13
   USGrph
Word       lastS      
 
 ..^                                                ..^             
         
      |
92 | 91 | expdimp 443 |
. . . . . . . . . . . 12
    USGrph
Word       lastS      
 
 ..^                                              ..^                               |
93 | 92 | impcom 436 |
. . . . . . . . . . 11
           USGrph Word
     
lastS        
 ..^                                              ..^                        |
94 | | f1ocnvdm 6213 |
. . . . . . . . . . 11
                   
             
      |
95 | 5, 93, 94 | syl2anc 671 |
. . . . . . . . . 10
           USGrph Word
     
lastS        
 ..^                                              ..^                             |
96 | 1, 95 | jca 539 |
. . . . . . . . 9
           USGrph Word
     
lastS        
 ..^                                              ..^                                     |
97 | 96 | orcd 398 |
. . . . . . . 8
           USGrph Word
     
lastS        
 ..^                                              ..^                              
                                |
98 | | simpl 463 |
. . . . . . . . . 10
           USGrph Word
     
lastS        
 ..^                                              ..^        
        |
99 | 4 | ad2antrl 739 |
. . . . . . . . . . 11
           USGrph Word
     
lastS        
 ..^                                              ..^               |
100 | | nn0z 10994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40

  |
101 | | peano2zm 11014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
    
        |
102 | 21, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
    
        |
103 | 100, 102 | anim12i 574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                 |
104 | | zltlem1 11023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
               
           |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
             
           |
106 | 38 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
                       |
107 | 106 | breq2d 4430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
               
         |
108 | 107 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                         |
109 | 105, 108 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                       |
110 | 109 | impancom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             
         |
111 | 110 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
              
        |
112 | | nn0re 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38

  |
113 | 112 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
           |
114 | 113, 17 | anim12i 574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                         |
115 | | lenlt 9743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
               
         |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                     
         |
117 | 111, 116 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       |
118 | 117 | anim1i 576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
                  
                |
119 | 114 | ancomd 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                     
   |
120 | 119 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
                  
          |
121 | | lttri3 9748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               
                 |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
                  
             
          |
123 | 118, 122 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
                  
        |
124 | 123 | exp31 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
                 |
125 | 124 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
                     |
126 | 125 | 3adant2 1033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
              
      
               |
127 | 6, 126 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  ..^      
      
               |
128 | 127 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
 ..^            
         |
129 | 128 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
 
     
 ..^                 |
130 | 7, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 Word          ..^                 |
131 | 130 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  USGrph
Word             
 ..^                 |
132 | 131 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . 23
   USGrph
Word      
     
 ..^                 |
133 | 132 | fveq2d 5896 |
. . . . . . . . . . . . . . . . . . . . . 22
   USGrph
Word      
     
 ..^                         |
134 | 133 | preq1d 4070 |
. . . . . . . . . . . . . . . . . . . . 21
   USGrph
Word      
     
 ..^                                       |
135 | 134 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . 20
   USGrph
Word      
     
 ..^                                         |
136 | 135 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
   USGrph
Word      
     
 ..^                                         |
137 | 136 | exp32 614 |
. . . . . . . . . . . . . . . . . 18
  USGrph
Word               ..^                        
                |
138 | 137 | com12 32 |
. . . . . . . . . . . . . . . . 17
         USGrph
Word        ..^      
                 
                |
139 | 138 | com14 91 |
. . . . . . . . . . . . . . . 16
                 
  USGrph Word        ..^                              |
140 | 139 | adantl 472 |
. . . . . . . . . . . . . . 15
    ..^                                             USGrph
Word        ..^      
      
                |
141 | 140 | adantl 472 |
. . . . . . . . . . . . . 14
  lastS        
 ..^                                              USGrph
Word        ..^      
      
                |
142 | 141 | com12 32 |
. . . . . . . . . . . . 13
  USGrph
Word        lastS          ..^                                              ..^       
                      |
143 | 142 | imp31 438 |
. . . . . . . . . . . 12
    USGrph
Word       lastS      
 
 ..^                                              ..^                             |
144 | 143 | impcom 436 |
. . . . . . . . . . 11
           USGrph Word
     
lastS        
 ..^                                              ..^                      |
145 | | f1ocnvdm 6213 |
. . . . . . . . . . 11
                 
                  |
146 | 99, 144, 145 | syl2anc 671 |
. . . . . . . . . 10
           USGrph Word
     
lastS        
 ..^                                              ..^                           |
147 | 98, 146 | jca 539 |
. . . . . . . . 9
           USGrph Word
     
lastS        
 ..^                                              ..^                                   |
148 | 147 | olcd 399 |
. . . . . . . 8
           USGrph Word
     
lastS        
 ..^                                              ..^                              
                                |
149 | 97, 148 | pm2.61ian 804 |
. . . . . . 7
    USGrph
Word       lastS      
 
 ..^                                              ..^                                                              |
150 | | ifel 3934 |
. . . . . . 7
                                                                   
                                |
151 | 149, 150 | sylibr 217 |
. . . . . 6
    USGrph
Word       lastS      
 
 ..^                                              ..^                                                       |
152 | | clwlkisclwwlklem2.f |
. . . . . 6
  ..^                                                      |
153 | 151, 152 | fmptd 6074 |
. . . . 5
   USGrph
Word       lastS      
 
 ..^                                                ..^           |
154 | | iswrdi 12714 |
. . . . 5
    ..^        
Word
  |
155 | 153, 154 | syl 17 |
. . . 4
   USGrph
Word       lastS      
 
 ..^                                             Word   |
156 | | wrdf 12715 |
. . . . . . . 8
 Word    ..^         |
157 | 156 | adantr 471 |
. . . . . . 7
  Word         ..^         |
158 | 152 | clwlkisclwwlklem2a2 25564 |
. . . . . . . . 9
  Word                  |
159 | | fzoval 11958 |
. . . . . . . . . . 11
    
 ..^                 |
160 | 7, 21, 159 | 3syl 18 |
. . . . . . . . . 10
 Word  ..^                 |
161 | | oveq2 6328 |
. . . . . . . . . . 11
          
                    |
162 | 161 | eqcoms 2470 |
. . . . . . . . . 10
          
                    |
163 | 160, 162 | sylan9eq 2516 |
. . . . . . . . 9
  Word             ..^               |
164 | 158, 163 | syldan 477 |
. . . . . . . 8
  Word       ..^               |
165 | 164 | feq2d 5741 |
. . . . . . 7
  Word          ..^      
               |
166 | 157, 165 | mpbid 215 |
. . . . . 6
  Word                    |
167 | 166 | 3adant1 1032 |
. . . . 5
  USGrph
Word                    |
168 | 167 | adantr 471 |
. . . 4
   USGrph
Word       lastS      
 
 ..^                                                           |
169 | | clwlkisclwwlklem2a1 25563 |
. . . . . 6
  USGrph
Word        lastS          ..^                                            
 ..^                        |
170 | 169 | imp 435 |
. . . . 5
   USGrph
Word       lastS      
 
 ..^                                               ..^                       |
171 | 158 | 3adant1 1032 |
. . . . . . . 8
  USGrph
Word                  |
172 | 171 | adantr 471 |
. . . . . . 7
   USGrph
Word      lastS       
            |
173 | 152 | clwlkisclwwlklem2a4 25568 |
. . . . . . . . . 10
  USGrph
Word        lastS        ..^                                               |
174 | 173 | impl 630 |
. . . . . . . . 9
    USGrph
Word      lastS         ..^       
                                      |
175 | 174 | ralimdva 2808 |
. . . . . . . 8
   USGrph
Word      lastS       
 
 ..^                       ..^                                |
176 | | oveq2 6328 |
. . . . . . . . . 10
          
 ..^      ..^         |
177 | 176 | raleqdv 3005 |
. . . . . . . . 9
          
 
 ..^                             ..^                                |
178 | 177 | imbi2d 322 |
. . . . . . . 8
          
  
 ..^                    
  ..^                           
 
 ..^                       ..^                                 |
179 | 175, 178 | syl5ibr 229 |
. . . . . . 7
          
   USGrph
Word      lastS       
 
 ..^                       ..^                               |
180 | 172, 179 | mpcom 37 |
. . . . . 6
   USGrph
Word      lastS       
 
 ..^                       ..^                              |
181 | 180 | adantrr 728 |
. . . . 5
   USGrph
Word       lastS      
 
 ..^                                                ..^                       ..^                              |
182 | 170, 181 | mpd 15 |
. . . 4
   USGrph
Word       lastS      
 
 ..^                                               ..^                             |
183 | 155, 168,
182 | 3jca 1194 |
. . 3
   USGrph
Word       lastS      
 
 ..^                                              Word               ..^                              |
184 | 152 | clwlkisclwwlklem2a3 25565 |
. . . . . . . . . 10
  Word              lastS     |
185 | 184 | 3adant1 1032 |
. . . . . . . . 9
  USGrph
Word              lastS     |
186 | 185 | eqcomd 2468 |
. . . . . . . 8
  USGrph
Word      lastS
            |
187 | 186 | eqeq2d 2472 |
. . . . . . 7
  USGrph
Word           lastS                  |
188 | 187 | biimpcd 232 |
. . . . . 6
     lastS  
  USGrph Word                     |
189 | 188 | eqcoms 2470 |
. . . . 5
 lastS         USGrph Word
                    |
190 | 189 | adantr 471 |
. . . 4
  lastS        
 ..^                                              USGrph
Word                     |
191 | 190 | impcom 436 |
. . 3
   USGrph
Word       lastS      
 
 ..^                                                           |
192 | 183, 191 | jca 539 |
. 2
   USGrph
Word       lastS      
 
 ..^                                               Word
              ..^                                           |
193 | 192 | ex 440 |
1
  USGrph
Word        lastS          ..^                                              Word               ..^                                            |