Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . . . . 9
            DECID            #       
          
    
      |
2 | | simprr 531 |
. . . . . . . . 9
            DECID            #       
          
    
            |
3 | 1, 2 | jca 306 |
. . . . . . . 8
            DECID            #       
          
    
                  |
4 | | nfcv 2319 |
. . . . . . . . . . . 12
        |
5 | | nfv 1528 |
. . . . . . . . . . . . 13
  |
6 | | nfcsb1v 3090 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
7 | | nfcv 2319 |
. . . . . . . . . . . . 13
   |
8 | 5, 6, 7 | nfif 3562 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)    |
9 | | eleq1w 2238 |
. . . . . . . . . . . . 13
 
   |
10 | | csbeq1a 3066 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
11 | 9, 10 | ifbieq1d 3556 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)     |
12 | 4, 8, 11 | cbvmpt 4098 |
. . . . . . . . . . 11
    
      
 ![]_ ]_](_urbrack.gif)     |
13 | | simpll 527 |
. . . . . . . . . . . 12
        
  |
14 | | zprod.6 |
. . . . . . . . . . . . . 14
 
   |
15 | 14 | ralrimiva 2550 |
. . . . . . . . . . . . 13
 
  |
16 | 6 | nfel1 2330 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif)
 |
17 | 10 | eleq1d 2246 |
. . . . . . . . . . . . . 14
 
  ![]_ ]_](_urbrack.gif)    |
18 | 16, 17 | rspc 2835 |
. . . . . . . . . . . . 13
  
  ![]_ ]_](_urbrack.gif)
   |
19 | 15, 18 | syl5 32 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
   |
20 | 13, 19 | mpan9 281 |
. . . . . . . . . . 11
   

    
   ![]_ ]_](_urbrack.gif)
  |
21 | | simplr 528 |
. . . . . . . . . . 11
        
  |
22 | | zprod.2 |
. . . . . . . . . . . 12
   |
23 | 22 | ad2antrr 488 |
. . . . . . . . . . 11
        
  |
24 | | simpr 110 |
. . . . . . . . . . 11
        
      |
25 | | zprod.4 |
. . . . . . . . . . . . 13

  |
26 | | zprod.1 |
. . . . . . . . . . . . 13
     |
27 | 25, 26 | sseqtrdi 3203 |
. . . . . . . . . . . 12

      |
28 | 27 | ad2antrr 488 |
. . . . . . . . . . 11
        
      |
29 | | zproddc.dc |
. . . . . . . . . . . . . . . . . 18
  DECID   |
30 | 26 | raleqi 2676 |
. . . . . . . . . . . . . . . . . 18
 
DECID
     DECID   |
31 | 29, 30 | sylib 122 |
. . . . . . . . . . . . . . . . 17
      DECID   |
32 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . . . 19
 
   |
33 | 32 | dcbid 838 |
. . . . . . . . . . . . . . . . . 18
 DECID
DECID
   |
34 | 33 | cbvralv 2703 |
. . . . . . . . . . . . . . . . 17
 
    DECID
     DECID   |
35 | 31, 34 | sylib 122 |
. . . . . . . . . . . . . . . 16
      DECID   |
36 | 35 | r19.21bi 2565 |
. . . . . . . . . . . . . . 15
 
    
DECID
  |
37 | 36 | adantlr 477 |
. . . . . . . . . . . . . 14
        
DECID
  |
38 | 37 | adantlr 477 |
. . . . . . . . . . . . 13
   

    
     DECID   |
39 | 38 | adantlr 477 |
. . . . . . . . . . . 12
                     DECID   |
40 | | simp-4l 541 |
. . . . . . . . . . . . . . 15
                    
  |
41 | | simpr 110 |
. . . . . . . . . . . . . . 15
                    
      |
42 | 27 | ssneld 3157 |
. . . . . . . . . . . . . . 15
         |
43 | 40, 41, 42 | sylc 62 |
. . . . . . . . . . . . . 14
                    
  |
44 | 43 | olcd 734 |
. . . . . . . . . . . . 13
                    

   |
45 | | df-dc 835 |
. . . . . . . . . . . . 13
DECID     |
46 | 44, 45 | sylibr 134 |
. . . . . . . . . . . 12
                    
DECID
  |
47 | | eluzelz 9535 |
. . . . . . . . . . . . . 14
    
  |
48 | | eluzdc 9608 |
. . . . . . . . . . . . . 14
 
 DECID       |
49 | 23, 47, 48 | syl2an 289 |
. . . . . . . . . . . . 13
   

    
     DECID       |
50 | | exmiddc 836 |
. . . . . . . . . . . . 13
DECID                 |
51 | 49, 50 | syl 14 |
. . . . . . . . . . . 12
   

    
                 |
52 | 39, 46, 51 | mpjaodan 798 |
. . . . . . . . . . 11
   

    
     DECID   |
53 | 12, 20, 21, 23, 24, 28, 52, 38 | prodrbdc 11577 |
. . . . . . . . . 10
        
         
      
      |
54 | 53 | biimpd 144 |
. . . . . . . . 9
        
                       |
55 | 54 | expimpd 363 |
. . . . . . . 8
 

 
                            |
56 | 3, 55 | syl5 32 |
. . . . . . 7
 

            DECID            #       
          
    
      
      |
57 | 56 | rexlimdva 2594 |
. . . . . 6
        
     DECID   
        #       
          
    
      
      |
58 | | uzssz 9545 |
. . . . . . . . . . . . . 14
     |
59 | 27, 58 | sstrdi 3167 |
. . . . . . . . . . . . 13

  |
60 | 59 | ad2antrr 488 |
. . . . . . . . . . . 12
               |
61 | | 1zzd 9278 |
. . . . . . . . . . . . . 14
               |
62 | | nnz 9270 |
. . . . . . . . . . . . . . . 16
   |
63 | 62 | adantl 277 |
. . . . . . . . . . . . . . 15
 

  |
64 | 63 | adantr 276 |
. . . . . . . . . . . . . 14
               |
65 | 61, 64 | fzfigd 10428 |
. . . . . . . . . . . . 13
                   |
66 | | simpr 110 |
. . . . . . . . . . . . . . 15
                       |
67 | | f1oeng 6756 |
. . . . . . . . . . . . . . 15
                     |
68 | 65, 66, 67 | syl2anc 411 |
. . . . . . . . . . . . . 14
                   |
69 | 68 | ensymd 6782 |
. . . . . . . . . . . . 13
                   |
70 | | enfii 6873 |
. . . . . . . . . . . . 13
          
  |
71 | 65, 69, 70 | syl2anc 411 |
. . . . . . . . . . . 12
               |
72 | | zfz1iso 10816 |
. . . . . . . . . . . 12
 
 
    ♯       |
73 | 60, 71, 72 | syl2anc 411 |
. . . . . . . . . . 11
             
    ♯       |
74 | | simpll 527 |
. . . . . . . . . . . . . . . 16
            
    ♯         |
75 | 74, 19 | mpan9 281 |
. . . . . . . . . . . . . . 15
   
              ♯      
   ![]_ ]_](_urbrack.gif)
  |
76 | | breq1 4006 |
. . . . . . . . . . . . . . . . . 18
 
♯  ♯     |
77 | | fveq2 5515 |
. . . . . . . . . . . . . . . . . . 19
           |
78 | 77 | csbeq1d 3064 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
79 | 76, 78 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . 17
  
♯         ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)     |
80 | | csbcow 3068 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
81 | | ifeq1 3537 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
   ♯         ![]_ ]_](_urbrack.gif)     |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 
♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)    |
83 | 79, 82 | eqtr4di 2228 |
. . . . . . . . . . . . . . . 16
  
♯         ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
84 | 83 | cbvmptv 4099 |
. . . . . . . . . . . . . . 15
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
85 | | eqid 2177 |
. . . . . . . . . . . . . . 15
  
♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
86 | 36 | ad4ant14 514 |
. . . . . . . . . . . . . . 15
   
              ♯      
     DECID   |
87 | | simplr 528 |
. . . . . . . . . . . . . . 15
            
    ♯         |
88 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
            
    ♯         |
89 | 27 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
            
    ♯             |
90 | | simprl 529 |
. . . . . . . . . . . . . . 15
            
    ♯                 |
91 | | simprr 531 |
. . . . . . . . . . . . . . 15
            
    ♯           ♯       |
92 | 12, 75, 84, 85, 86, 87, 88, 89, 90, 91 | prodmodclem2a 11579 |
. . . . . . . . . . . . . 14
            
    ♯                      ♯         ![]_ ]_](_urbrack.gif) 
        |
93 | 65 | adantrr 479 |
. . . . . . . . . . . . . . . . . . . . 21
            
    ♯             |
94 | 93, 90 | fihasheqf1od 10764 |
. . . . . . . . . . . . . . . . . . . 20
            
    ♯       ♯      ♯    |
95 | 87 | nnnn0d 9227 |
. . . . . . . . . . . . . . . . . . . . 21
            
    ♯         |
96 | | hashfz1 10758 |
. . . . . . . . . . . . . . . . . . . . 21

♯        |
97 | 95, 96 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
            
    ♯       ♯        |
98 | 94, 97 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . . 19
            
    ♯       ♯    |
99 | 98 | breq2d 4015 |
. . . . . . . . . . . . . . . . . 18
            
    ♯        ♯ 
   |
100 | 99 | ifbid 3555 |
. . . . . . . . . . . . . . . . 17
            
    ♯         ♯         ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif) 
   |
101 | 100 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . 16
            
    ♯          ♯         ![]_ ]_](_urbrack.gif)      
       ![]_ ]_](_urbrack.gif) 
    |
102 | 101 | seqeq3d 10450 |
. . . . . . . . . . . . . . 15
            
    ♯            ♯         ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)       |
103 | 102 | fveq1d 5517 |
. . . . . . . . . . . . . 14
            
    ♯            ♯         ![]_ ]_](_urbrack.gif) 
                  ![]_ ]_](_urbrack.gif)          |
104 | 92, 103 | breqtrd 4029 |
. . . . . . . . . . . . 13
            
    ♯                             ![]_ ]_](_urbrack.gif)          |
105 | 104 | expr 375 |
. . . . . . . . . . . 12
             
    ♯                           ![]_ ]_](_urbrack.gif)           |
106 | 105 | exlimdv 1819 |
. . . . . . . . . . 11
              
    ♯    
      
               ![]_ ]_](_urbrack.gif)           |
107 | 73, 106 | mpd 13 |
. . . . . . . . . 10
                                   ![]_ ]_](_urbrack.gif)          |
108 | | breq2 4007 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)       
         
      
               ![]_ ]_](_urbrack.gif)           |
109 | 107, 108 | syl5ibrcom 157 |
. . . . . . . . 9
                          ![]_ ]_](_urbrack.gif)       
      
      |
110 | 109 | expimpd 363 |
. . . . . . . 8
 

         
            ![]_ ]_](_urbrack.gif)                      |
111 | 110 | exlimdv 1819 |
. . . . . . 7
 

                        ![]_ ]_](_urbrack.gif) 
                    |
112 | 111 | rexlimdva 2594 |
. . . . . 6
             
            ![]_ ]_](_urbrack.gif)                      |
113 | 57, 112 | jaod 717 |
. . . . 5
         
     DECID   
        #       
          
                
            ![]_ ]_](_urbrack.gif)                       |
114 | 22 | adantr 276 |
. . . . . . . 8
 
      
      |
115 | 27 | adantr 276 |
. . . . . . . . 9
 
      
          |
116 | 31 | adantr 276 |
. . . . . . . . 9
 
      
         DECID   |
117 | 115, 116 | jca 306 |
. . . . . . . 8
 
      
              DECID    |
118 | | zproddc.3 |
. . . . . . . . . . 11
     #       |
119 | 26 | eleq2i 2244 |
. . . . . . . . . . . . 13

      |
120 | | eluzelz 9535 |
. . . . . . . . . . . . . . . . . 18
    
  |
121 | 120 | adantl 277 |
. . . . . . . . . . . . . . . . 17
 
    
  |
122 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
       
    
      |
123 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . 21
       
    
      |
124 | | uztrn 9542 |
. . . . . . . . . . . . . . . . . . . . 21
          
      |
125 | 122, 123,
124 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
       
    
      |
126 | 125, 26 | eleqtrrdi 2271 |
. . . . . . . . . . . . . . . . . . 19
       
    
  |
127 | | zprod.5 |
. . . . . . . . . . . . . . . . . . . . 21
 
            |
128 | 127 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . . . . 20
             |
129 | 128 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
       
    

           |
130 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
131 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 ![]_ ]_](_urbrack.gif)  |
132 | 130, 131,
7 | nfif 3562 |
. . . . . . . . . . . . . . . . . . . . 21
       ![]_ ]_](_urbrack.gif)    |
133 | 132 | nfeq2 2331 |
. . . . . . . . . . . . . . . . . . . 20
         
 ![]_ ]_](_urbrack.gif)    |
134 | | fveq2 5515 |
. . . . . . . . . . . . . . . . . . . . 21
           |
135 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
136 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)   |
137 | 135, 136 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . . . . . 21
           ![]_ ]_](_urbrack.gif)     |
138 | 134, 137 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . 20
         
        
 ![]_ ]_](_urbrack.gif)      |
139 | 133, 138 | rspc 2835 |
. . . . . . . . . . . . . . . . . . 19
  
                
 ![]_ ]_](_urbrack.gif)      |
140 | 126, 129,
139 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
       
    
         ![]_ ]_](_urbrack.gif)     |
141 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
   
    
    
   |
142 | 15 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . 20
   
    
    
 
  |
143 | 131 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . . . 21
    ![]_ ]_](_urbrack.gif)
 |
144 | 136 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ![]_ ]_](_urbrack.gif)    |
145 | 143, 144 | rspc 2835 |
. . . . . . . . . . . . . . . . . . . 20
  
  ![]_ ]_](_urbrack.gif)
   |
146 | 141, 142,
145 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
   
    
    
   ![]_ ]_](_urbrack.gif)
  |
147 | | 1cnd 7972 |
. . . . . . . . . . . . . . . . . . 19
   
    
    

  |
148 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
149 | 148 | dcbid 838 |
. . . . . . . . . . . . . . . . . . . 20
 DECID
DECID
   |
150 | 29 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
       
    

DECID
  |
151 | 149, 150,
126 | rspcdva 2846 |
. . . . . . . . . . . . . . . . . . 19
       
    
DECID
  |
152 | 146, 147,
151 | ifcldadc 3563 |
. . . . . . . . . . . . . . . . . 18
       
    
   
 ![]_ ]_](_urbrack.gif)     |
153 | 140, 152 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . 17
       
    
      |
154 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
       
    
      |
155 | | simplr 528 |
. . . . . . . . . . . . . . . . . . . . 21
       
    
      |
156 | | uztrn 9542 |
. . . . . . . . . . . . . . . . . . . . 21
          
      |
157 | 154, 155,
156 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
       
    
      |
158 | 157, 26 | eleqtrrdi 2271 |
. . . . . . . . . . . . . . . . . . 19
       
    
  |
159 | 128 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
       
    

           |
160 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
161 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 ![]_ ]_](_urbrack.gif)  |
162 | 160, 161,
7 | nfif 3562 |
. . . . . . . . . . . . . . . . . . . . 21
       ![]_ ]_](_urbrack.gif)    |
163 | 162 | nfeq2 2331 |
. . . . . . . . . . . . . . . . . . . 20
         
 ![]_ ]_](_urbrack.gif)    |
164 | | fveq2 5515 |
. . . . . . . . . . . . . . . . . . . . 21
           |
165 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
166 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)   |
167 | 165, 166 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . . . . . 21
           ![]_ ]_](_urbrack.gif)     |
168 | 164, 167 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . 20
         
        
 ![]_ ]_](_urbrack.gif)      |
169 | 163, 168 | rspc 2835 |
. . . . . . . . . . . . . . . . . . 19
  
                
 ![]_ ]_](_urbrack.gif)      |
170 | 158, 159,
169 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
       
    
         ![]_ ]_](_urbrack.gif)     |
171 | 58, 157 | sselid 3153 |
. . . . . . . . . . . . . . . . . . 19
       
    
  |
172 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
    
   |
173 | 15 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
    
 
  |
174 | 161 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . . . . 22
    ![]_ ]_](_urbrack.gif)
 |
175 | 166 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  ![]_ ]_](_urbrack.gif)    |
176 | 174, 175 | rspc 2835 |
. . . . . . . . . . . . . . . . . . . . 21
  
  ![]_ ]_](_urbrack.gif)
   |
177 | 172, 173,
176 | sylc 62 |
. . . . . . . . . . . . . . . . . . . 20
   
    
    
   ![]_ ]_](_urbrack.gif)
  |
178 | | 1cnd 7972 |
. . . . . . . . . . . . . . . . . . . 20
   
    
    

  |
179 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
180 | 179 | dcbid 838 |
. . . . . . . . . . . . . . . . . . . . 21
 DECID
DECID
   |
181 | 29 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . 21
       
    

DECID
  |
182 | 180, 181,
158 | rspcdva 2846 |
. . . . . . . . . . . . . . . . . . . 20
       
    
DECID
  |
183 | 177, 178,
182 | ifcldadc 3563 |
. . . . . . . . . . . . . . . . . . 19
       
    
   
 ![]_ ]_](_urbrack.gif)     |
184 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . . . 20
   |
185 | | eqid 2177 |
. . . . . . . . . . . . . . . . . . . 20
    
      
   |
186 | 184, 162,
167, 185 | fvmptf 5608 |
. . . . . . . . . . . . . . . . . . 19
       ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)     |
187 | 171, 183,
186 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
       
    
                ![]_ ]_](_urbrack.gif)     |
188 | 170, 187 | eqtr4d 2213 |
. . . . . . . . . . . . . . . . 17
       
    
                 |
189 | | mulcl 7937 |
. . . . . . . . . . . . . . . . . 18
 
     |
190 | 189 | adantl 277 |
. . . . . . . . . . . . . . . . 17
       
       |
191 | 121, 153,
188, 190 | seq3feq 10469 |
. . . . . . . . . . . . . . . 16
 
    
               |
192 | 191 | breq1d 4013 |
. . . . . . . . . . . . . . 15
 
    
  
             |
193 | 192 | anbi2d 464 |
. . . . . . . . . . . . . 14
 
    
  #      #               |
194 | 193 | exbidv 1825 |
. . . . . . . . . . . . 13
 
    
    #    
   #               |
195 | 119, 194 | sylan2b 287 |
. . . . . . . . . . . 12
 
     #    
   #               |
196 | 195 | rexbidva 2474 |
. . . . . . . . . . 11
      #     
   #       
       |
197 | 118, 196 | mpbid 147 |
. . . . . . . . . 10
     #       
      |
198 | 26 | rexeqi 2677 |
. . . . . . . . . 10
     #       
    
        #       
      |
199 | 197, 198 | sylib 122 |
. . . . . . . . 9
          #       
      |
200 | 199 | anim1i 340 |
. . . . . . . 8
 
      
              #       
          
      |
201 | | fveq2 5515 |
. . . . . . . . . . . 12
           |
202 | 201 | sseq2d 3185 |
. . . . . . . . . . 11
     
       |
203 | 201 | raleqdv 2678 |
. . . . . . . . . . 11
  
    DECID      DECID    |
204 | 202, 203 | anbi12d 473 |
. . . . . . . . . 10
            DECID            DECID     |
205 | 201 | rexeqdv 2679 |
. . . . . . . . . . 11
  
        #       
    
        #       
       |
206 | | seqeq1 10445 |
. . . . . . . . . . . 12
                       |
207 | 206 | breq1d 4013 |
. . . . . . . . . . 11
          
      
      |
208 | 205, 207 | anbi12d 473 |
. . . . . . . . . 10
            #       
          
              #       
          
       |
209 | 204, 208 | anbi12d 473 |
. . . . . . . . 9
             DECID   
        #       
          
          
     DECID   
        #       
          
        |
210 | 209 | rspcev 2841 |
. . . . . . . 8
             DECID   
        #       
          
            
     DECID   
        #       
          
       |
211 | 114, 117,
200, 210 | syl12anc 1236 |
. . . . . . 7
 
      
                DECID   
        #       
          
       |
212 | 211 | orcd 733 |
. . . . . 6
 
      
           
     DECID   
        #       
          
                
            ![]_ ]_](_urbrack.gif)            |
213 | 212 | ex 115 |
. . . . 5
       
          
     DECID   
        #       
          
                
            ![]_ ]_](_urbrack.gif)             |
214 | 113, 213 | impbid 129 |
. . . 4
         
     DECID   
        #       
          
                
            ![]_ ]_](_urbrack.gif)         
      
      |
215 | | eluzelz 9535 |
. . . . . . . 8
    
  |
216 | | simpr 110 |
. . . . . . . . . 10
       
   |
217 | 15 | ad2antrr 488 |
. . . . . . . . . 10
       
 
  |
218 | 216, 217,
145 | sylc 62 |
. . . . . . . . 9
       
   ![]_ ]_](_urbrack.gif)   |
219 | | 1cnd 7972 |
. . . . . . . . 9
       
   |
220 | 29 | adantr 276 |
. . . . . . . . . 10
 
    

DECID
  |
221 | 26 | eleq2i 2244 |
. . . . . . . . . . . 12

      |
222 | 221 | biimpri 133 |
. . . . . . . . . . 11
    
  |
223 | 222 | adantl 277 |
. . . . . . . . . 10
 
    
  |
224 | 149, 220,
223 | rspcdva 2846 |
. . . . . . . . 9
 
    
DECID
  |
225 | 218, 219,
224 | ifcldadc 3563 |
. . . . . . . 8
 
    
   
 ![]_ ]_](_urbrack.gif)     |
226 | | nfcv 2319 |
. . . . . . . . 9
   |
227 | 226, 132,
137, 185 | fvmptf 5608 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)     |
228 | 215, 225,
227 | syl2an2 594 |
. . . . . . 7
 
    
                ![]_ ]_](_urbrack.gif)     |
229 | 228, 225 | eqeltrd 2254 |
. . . . . 6
 
    
             |
230 | | eluzelz 9535 |
. . . . . . . 8
    
  |
231 | | simpr 110 |
. . . . . . . . . 10
       
   |
232 | 15 | ad2antrr 488 |
. . . . . . . . . 10
       
 
  |
233 | 231, 232,
176 | sylc 62 |
. . . . . . . . 9
       
   ![]_ ]_](_urbrack.gif)   |
234 | | 1cnd 7972 |
. . . . . . . . 9
       
   |
235 | 29 | adantr 276 |
. . . . . . . . . 10
 
    

DECID
  |
236 | 26 | eleq2i 2244 |
. . . . . . . . . . . 12

      |
237 | 236 | biimpri 133 |
. . . . . . . . . . 11
    
  |
238 | 237 | adantl 277 |
. . . . . . . . . 10
 
    
  |
239 | 180, 235,
238 | rspcdva 2846 |
. . . . . . . . 9
 
    
DECID
  |
240 | 233, 234,
239 | ifcldadc 3563 |
. . . . . . . 8
 
    
   
 ![]_ ]_](_urbrack.gif)     |
241 | 230, 240,
186 | syl2an2 594 |
. . . . . . 7
 
    
                ![]_ ]_](_urbrack.gif)     |
242 | 128 | adantr 276 |
. . . . . . . 8
 
    

           |
243 | 238, 242,
169 | sylc 62 |
. . . . . . 7
 
    
         ![]_ ]_](_urbrack.gif)     |
244 | 241, 243 | eqtr4d 2213 |
. . . . . 6
 
    
                 |
245 | 189 | adantl 277 |
. . . . . 6
 
       |
246 | 22, 229, 244, 245 | seq3feq 10469 |
. . . . 5
                |
247 | 246 | breq1d 4013 |
. . . 4
       
  
      |
248 | 214, 247 | bitrd 188 |
. . 3
         
     DECID   
        #       
          
                
            ![]_ ]_](_urbrack.gif)         
      |
249 | 248 | iotabidv 5199 |
. 2
                 DECID   
        #       
          
                
            ![]_ ]_](_urbrack.gif)                   |
250 | | df-proddc 11554 |
. 2

                DECID            #       
          
                
            ![]_ ]_](_urbrack.gif)            |
251 | | df-fv 5224 |
. 2
           |
252 | 249, 250,
251 | 3eqtr4g 2235 |
1
 
      |