Step | Hyp | Ref
| Expression |
1 | | simplr 528 |
. . . . 5
              DECID         
                |
2 | | oveq1 5881 |
. . . . . . . 8
       |
3 | 2 | oveq1d 5889 |
. . . . . . 7
           |
4 | 3 | eleq1d 2246 |
. . . . . 6
     
       |
5 | 4 | elrab 2893 |
. . . . 5
      
        |
6 | 1, 5 | sylib 122 |
. . . 4
              DECID         
                |
7 | 6 | simprd 114 |
. . 3
              DECID         
              |
8 | | breq2 4007 |
. . . . . . 7
     
       |
9 | | simplr 528 |
. . . . . . 7
        

     DECID        
        
           |
10 | | oveq1 5881 |
. . . . . . . . . 10
               |
11 | 10 | oveq1d 5889 |
. . . . . . . . 9
                   |
12 | 11 | eleq1d 2246 |
. . . . . . . 8
         
           |
13 | | simp1 997 |
. . . . . . . . . . . . . 14
 
    
     DECID        |
14 | 13 | ad3antrrr 492 |
. . . . . . . . . . . . 13
        

     DECID        
        
       |
15 | | simpr 110 |
. . . . . . . . . . . . 13
        

     DECID        
        
   |
16 | 14, 15 | sseldd 3156 |
. . . . . . . . . . . 12
        

     DECID        
        
       |
17 | | eluzelz 9536 |
. . . . . . . . . . . 12
    
  |
18 | 16, 17 | syl 14 |
. . . . . . . . . . 11
        

     DECID        
        
   |
19 | | simp2 998 |
. . . . . . . . . . . . 13
 
    
     DECID  
  |
20 | | ssel2 3150 |
. . . . . . . . . . . . . . . 16
 
           |
21 | | eluzel2 9532 |
. . . . . . . . . . . . . . . 16
    
  |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . . . . 15
 
       |
23 | 22 | ex 115 |
. . . . . . . . . . . . . 14
    

   |
24 | 23 | exlimdv 1819 |
. . . . . . . . . . . . 13
    
 
   |
25 | 13, 19, 24 | sylc 62 |
. . . . . . . . . . . 12
 
    
     DECID    |
26 | 25 | ad3antrrr 492 |
. . . . . . . . . . 11
        

     DECID        
        
   |
27 | 18, 26 | zsubcld 9379 |
. . . . . . . . . 10
        

     DECID        
        
     |
28 | | eluzle 9539 |
. . . . . . . . . . . 12
    
  |
29 | 16, 28 | syl 14 |
. . . . . . . . . . 11
        

     DECID        
        
   |
30 | 18 | zred 9374 |
. . . . . . . . . . . 12
        

     DECID        
        
   |
31 | 26 | zred 9374 |
. . . . . . . . . . . 12
        

     DECID        
        
   |
32 | 30, 31 | subge0d 8491 |
. . . . . . . . . . 11
        

     DECID        
        
 
 
   |
33 | 29, 32 | mpbird 167 |
. . . . . . . . . 10
        

     DECID        
        
     |
34 | | elnn0z 9265 |
. . . . . . . . . 10
  
        |
35 | 27, 33, 34 | sylanbrc 417 |
. . . . . . . . 9
        

     DECID        
        
     |
36 | | nn0p1nn 9214 |
. . . . . . . . 9
  
      |
37 | 35, 36 | syl 14 |
. . . . . . . 8
        

     DECID        
        
       |
38 | 27 | zcnd 9375 |
. . . . . . . . . . . 12
        

     DECID        
        
     |
39 | | 1cnd 7972 |
. . . . . . . . . . . 12
        

     DECID        
        
   |
40 | 38, 39 | pncand 8268 |
. . . . . . . . . . 11
        

     DECID        
        
           |
41 | 40 | oveq1d 5889 |
. . . . . . . . . 10
        

     DECID        
        
               |
42 | 18 | zcnd 9375 |
. . . . . . . . . . 11
        

     DECID        
        
   |
43 | 26 | zcnd 9375 |
. . . . . . . . . . 11
        

     DECID        
        
   |
44 | 42, 43 | npcand 8271 |
. . . . . . . . . 10
        

     DECID        
        
       |
45 | 41, 44 | eqtrd 2210 |
. . . . . . . . 9
        

     DECID        
        
           |
46 | 45, 15 | eqeltrd 2254 |
. . . . . . . 8
        

     DECID        
        
           |
47 | 12, 37, 46 | elrabd 2895 |
. . . . . . 7
        

     DECID        
        
             |
48 | 8, 9, 47 | rspcdva 2846 |
. . . . . 6
        

     DECID        
        
       |
49 | | elrabi 2890 |
. . . . . . . . 9
         |
50 | 49 | ad3antlr 493 |
. . . . . . . 8
        

     DECID        
        
   |
51 | 50 | nnred 8931 |
. . . . . . 7
        

     DECID        
        
   |
52 | | 1red 7971 |
. . . . . . 7
        

     DECID        
        
   |
53 | 30, 31 | resubcld 8337 |
. . . . . . 7
        

     DECID        
        
     |
54 | 51, 52, 53 | lesubaddd 8498 |
. . . . . 6
        

     DECID        
        
   
 
       |
55 | 48, 54 | mpbird 167 |
. . . . 5
        

     DECID        
        
       |
56 | 51, 52 | resubcld 8337 |
. . . . . 6
        

     DECID        
        
     |
57 | | leaddsub 8394 |
. . . . . 6
   
     
       |
58 | 56, 31, 30, 57 | syl3anc 1238 |
. . . . 5
        

     DECID        
        
     
       |
59 | 55, 58 | mpbird 167 |
. . . 4
        

     DECID        
        
       |
60 | 59 | ralrimiva 2550 |
. . 3
              DECID         
        
      |
61 | | breq1 4006 |
. . . . 5
     
       |
62 | 61 | ralbidv 2477 |
. . . 4
      

       |
63 | 62 | rspcev 2841 |
. . 3
            

  |
64 | 7, 60, 63 | syl2anc 411 |
. 2
              DECID         
        

  |
65 | | ssrab2 3240 |
. . 3
       |
66 | | eluzelz 9536 |
. . . . . . . . . . 11
    
  |
67 | 20, 66 | syl 14 |
. . . . . . . . . 10
 
       |
68 | 67, 22 | zsubcld 9379 |
. . . . . . . . 9
 
         |
69 | | 1zzd 9279 |
. . . . . . . . 9
 
       |
70 | 68, 69 | zaddcld 9378 |
. . . . . . . 8
 
           |
71 | | oveq1 5881 |
. . . . . . . . . . 11
               |
72 | 71 | oveq1d 5889 |
. . . . . . . . . 10
                   |
73 | 72 | eleq1d 2246 |
. . . . . . . . 9
         
           |
74 | | eluzle 9539 |
. . . . . . . . . . . . 13
    
  |
75 | 20, 74 | syl 14 |
. . . . . . . . . . . 12
 
       |
76 | 67 | zred 9374 |
. . . . . . . . . . . . 13
 
       |
77 | 22 | zred 9374 |
. . . . . . . . . . . . 13
 
       |
78 | 76, 77 | subge0d 8491 |
. . . . . . . . . . . 12
 
     
 
   |
79 | 75, 78 | mpbird 167 |
. . . . . . . . . . 11
 
         |
80 | | elnn0z 9265 |
. . . . . . . . . . 11
  
        |
81 | 68, 79, 80 | sylanbrc 417 |
. . . . . . . . . 10
 
         |
82 | | nn0p1nn 9214 |
. . . . . . . . . 10
  
      |
83 | 81, 82 | syl 14 |
. . . . . . . . 9
 
           |
84 | 68 | zcnd 9375 |
. . . . . . . . . . . . 13
 
         |
85 | | 1cnd 7972 |
. . . . . . . . . . . . 13
 
       |
86 | 84, 85 | pncand 8268 |
. . . . . . . . . . . 12
 
               |
87 | 86 | oveq1d 5889 |
. . . . . . . . . . 11
 
                   |
88 | 67 | zcnd 9375 |
. . . . . . . . . . . 12
 
       |
89 | 22 | zcnd 9375 |
. . . . . . . . . . . 12
 
       |
90 | 88, 89 | npcand 8271 |
. . . . . . . . . . 11
 
           |
91 | 87, 90 | eqtrd 2210 |
. . . . . . . . . 10
 
               |
92 | | simpr 110 |
. . . . . . . . . 10
 
       |
93 | 91, 92 | eqeltrd 2254 |
. . . . . . . . 9
 
               |
94 | 73, 83, 93 | elrabd 2895 |
. . . . . . . 8
 
                 |
95 | | eleq1 2240 |
. . . . . . . . 9
           
             |
96 | 95 | spcegv 2825 |
. . . . . . . 8
                          |
97 | 70, 94, 96 | sylc 62 |
. . . . . . 7
 
              |
98 | 97 | ex 115 |
. . . . . 6
    

          |
99 | 98 | exlimdv 1819 |
. . . . 5
    
 
          |
100 | 99 | imp 124 |
. . . 4
 
    

         |
101 | 100 | 3adant3 1017 |
. . 3
 
    
     DECID           |
102 | | eleq1 2240 |
. . . . . . 7
     
       |
103 | 102 | dcbid 838 |
. . . . . 6
     DECID
DECID        |
104 | | simpl3 1002 |
. . . . . 6
             DECID        DECID   |
105 | 24 | imp 124 |
. . . . . . . . 9
 
    

  |
106 | 105 | 3adant3 1017 |
. . . . . . . 8
 
    
     DECID    |
107 | 106 | adantr 276 |
. . . . . . 7
             DECID     |
108 | | simpr 110 |
. . . . . . . . . 10
             DECID     |
109 | 108 | nnzd 9373 |
. . . . . . . . 9
             DECID     |
110 | | 1zzd 9279 |
. . . . . . . . 9
             DECID     |
111 | 109, 110 | zsubcld 9379 |
. . . . . . . 8
             DECID       |
112 | 111, 107 | zaddcld 9378 |
. . . . . . 7
             DECID         |
113 | | nnm1ge0 9338 |
. . . . . . . . 9
     |
114 | 113 | adantl 277 |
. . . . . . . 8
             DECID       |
115 | 107 | zred 9374 |
. . . . . . . . 9
             DECID     |
116 | 111 | zred 9374 |
. . . . . . . . 9
             DECID       |
117 | 115, 116 | addge02d 8490 |
. . . . . . . 8
             DECID   
 
       |
118 | 114, 117 | mpbid 147 |
. . . . . . 7
             DECID         |
119 | | eluz2 9533 |
. . . . . . 7
                     |
120 | 107, 112,
118, 119 | syl3anbrc 1181 |
. . . . . 6
             DECID             |
121 | 103, 104,
120 | rspcdva 2846 |
. . . . 5
             DECID  
DECID       |
122 | | oveq1 5881 |
. . . . . . . . . 10
       |
123 | 122 | oveq1d 5889 |
. . . . . . . . 9
           |
124 | 123 | eleq1d 2246 |
. . . . . . . 8
     
       |
125 | 124 | elrab3 2894 |
. . . . . . 7
       
       |
126 | 125 | dcbid 838 |
. . . . . 6
 DECID       DECID        |
127 | 126 | adantl 277 |
. . . . 5
             DECID   DECID       DECID        |
128 | 121, 127 | mpbird 167 |
. . . 4
             DECID  
DECID
        |
129 | 128 | ralrimiva 2550 |
. . 3
 
    
     DECID   DECID         |
130 | | nnwodc 12036 |
. . 3
        
      
DECID
       
                 |
131 | 65, 101, 129, 130 | mp3an2i 1342 |
. 2
 
    
     DECID                 
  |
132 | 64, 131 | r19.29a 2620 |
1
 
    
     DECID  

  |