Step | Hyp | Ref
| Expression |
1 | | 3simpb 947 |
. . . . . . . 8
 
    
    DECID         ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)        |
2 | | eleq1w 2160 |
. . . . . . . . . . . . 13
 
   |
3 | | csbeq1 2958 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
4 | 2, 3 | ifbieq1d 3441 |
. . . . . . . . . . . 12
  
   ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
5 | 4 | cbvmptv 3964 |
. . . . . . . . . . 11
    
 ![]_ ]_](_urbrack.gif)        
 ![]_ ]_](_urbrack.gif)     |
6 | | simpr 109 |
. . . . . . . . . . . 12
   

    
   |
7 | | zisum.5 |
. . . . . . . . . . . . . 14
 
   |
8 | 7 | ralrimiva 2464 |
. . . . . . . . . . . . 13
 
  |
9 | 8 | ad3antrrr 479 |
. . . . . . . . . . . 12
   

    
 
  |
10 | | nfcsb1v 2985 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
11 | 10 | nfel1 2251 |
. . . . . . . . . . . . 13
    ![]_ ]_](_urbrack.gif)
 |
12 | | csbeq1a 2963 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
13 | 12 | eleq1d 2168 |
. . . . . . . . . . . . 13
 
  ![]_ ]_](_urbrack.gif)    |
14 | 11, 13 | rspc 2738 |
. . . . . . . . . . . 12
  
  ![]_ ]_](_urbrack.gif)
   |
15 | 6, 9, 14 | sylc 62 |
. . . . . . . . . . 11
   

    
   ![]_ ]_](_urbrack.gif)
  |
16 | | simplr 500 |
. . . . . . . . . . 11
        
  |
17 | | zisum.2 |
. . . . . . . . . . . 12
   |
18 | 17 | ad2antrr 475 |
. . . . . . . . . . 11
        
  |
19 | | simpr 109 |
. . . . . . . . . . 11
        
      |
20 | | zisum.3 |
. . . . . . . . . . . . 13

  |
21 | | zisum.1 |
. . . . . . . . . . . . 13
     |
22 | 20, 21 | syl6sseq 3095 |
. . . . . . . . . . . 12

      |
23 | 22 | ad2antrr 475 |
. . . . . . . . . . 11
        
      |
24 | | zisum.dc |
. . . . . . . . . . . . . . . . . 18
  DECID   |
25 | 21 | raleqi 2588 |
. . . . . . . . . . . . . . . . . 18
 
DECID
     DECID   |
26 | 24, 25 | sylib 121 |
. . . . . . . . . . . . . . . . 17
      DECID   |
27 | | eleq1w 2160 |
. . . . . . . . . . . . . . . . . . 19
 
   |
28 | 27 | dcbid 792 |
. . . . . . . . . . . . . . . . . 18
 DECID
DECID
   |
29 | 28 | cbvralv 2612 |
. . . . . . . . . . . . . . . . 17
 
    DECID
     DECID   |
30 | 26, 29 | sylib 121 |
. . . . . . . . . . . . . . . 16
      DECID   |
31 | 30 | r19.21bi 2479 |
. . . . . . . . . . . . . . 15
 
    
DECID
  |
32 | 31 | adantlr 464 |
. . . . . . . . . . . . . 14
        
DECID
  |
33 | 32 | adantlr 464 |
. . . . . . . . . . . . 13
   

    
     DECID   |
34 | 33 | adantlr 464 |
. . . . . . . . . . . 12
                     DECID   |
35 | | simp-4l 511 |
. . . . . . . . . . . . . . 15
                    
  |
36 | | simpr 109 |
. . . . . . . . . . . . . . 15
                    
      |
37 | 22 | ssneld 3049 |
. . . . . . . . . . . . . . 15
         |
38 | 35, 36, 37 | sylc 62 |
. . . . . . . . . . . . . 14
                    
  |
39 | 38 | olcd 694 |
. . . . . . . . . . . . 13
                    

   |
40 | | df-dc 787 |
. . . . . . . . . . . . 13
DECID     |
41 | 39, 40 | sylibr 133 |
. . . . . . . . . . . 12
                    
DECID
  |
42 | | eluzelz 9185 |
. . . . . . . . . . . . . 14
    
  |
43 | | eluzdc 9254 |
. . . . . . . . . . . . . 14
 
 DECID       |
44 | 18, 42, 43 | syl2an 285 |
. . . . . . . . . . . . 13
   

    
     DECID       |
45 | | exmiddc 788 |
. . . . . . . . . . . . 13
DECID                 |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . 12
   

    
                 |
47 | 34, 41, 46 | mpjaodan 753 |
. . . . . . . . . . 11
   

    
     DECID   |
48 | 5, 15, 16, 18, 19, 23, 47, 33 | sumrbdc 10986 |
. . . . . . . . . 10
        
        ![]_ ]_](_urbrack.gif)    
      
 ![]_ ]_](_urbrack.gif)        |
49 | 48 | biimpd 143 |
. . . . . . . . 9
        
        ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)        |
50 | 49 | expimpd 358 |
. . . . . . . 8
 

 
            ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)        |
51 | 1, 50 | syl5 32 |
. . . . . . 7
 

 
    
    DECID         ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)        |
52 | 51 | rexlimdva 2508 |
. . . . . 6
             DECID         ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)        |
53 | | uzssz 9195 |
. . . . . . . . . . . . . 14
     |
54 | 22, 53 | syl6ss 3059 |
. . . . . . . . . . . . 13

  |
55 | 54 | ad2antrr 475 |
. . . . . . . . . . . 12
               |
56 | | 1zzd 8933 |
. . . . . . . . . . . . . 14
               |
57 | | simplr 500 |
. . . . . . . . . . . . . . 15
               |
58 | 57 | nnzd 9024 |
. . . . . . . . . . . . . 14
               |
59 | 56, 58 | fzfigd 10045 |
. . . . . . . . . . . . 13
                   |
60 | | simpr 109 |
. . . . . . . . . . . . . . 15
                       |
61 | | f1oeng 6581 |
. . . . . . . . . . . . . . 15
                     |
62 | 59, 60, 61 | syl2anc 406 |
. . . . . . . . . . . . . 14
                   |
63 | 62 | ensymd 6607 |
. . . . . . . . . . . . 13
                   |
64 | | enfii 6697 |
. . . . . . . . . . . . 13
          
  |
65 | 59, 63, 64 | syl2anc 406 |
. . . . . . . . . . . 12
               |
66 | | zfz1iso 10425 |
. . . . . . . . . . . 12
 
 
    ♯       |
67 | 55, 65, 66 | syl2anc 406 |
. . . . . . . . . . 11
             
    ♯       |
68 | | simpr 109 |
. . . . . . . . . . . . . . . 16
   
              ♯      
   |
69 | 8 | ad3antrrr 479 |
. . . . . . . . . . . . . . . 16
   
              ♯      
 
  |
70 | 68, 69, 14 | sylc 62 |
. . . . . . . . . . . . . . 15
   
              ♯      
   ![]_ ]_](_urbrack.gif)
  |
71 | 31 | adantlr 464 |
. . . . . . . . . . . . . . . 16
        
DECID
  |
72 | 71 | adantlr 464 |
. . . . . . . . . . . . . . 15
   
              ♯      
     DECID   |
73 | | breq1 3878 |
. . . . . . . . . . . . . . . . 17
 
♯  ♯     |
74 | | fveq2 5353 |
. . . . . . . . . . . . . . . . . . 19
           |
75 | 74 | csbeq1d 2961 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
76 | | csbco 2964 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
77 | 75, 76 | syl6eqr 2150 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
78 | 73, 77 | ifbieq1d 3441 |
. . . . . . . . . . . . . . . 16
  
♯         ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
79 | 78 | cbvmptv 3964 |
. . . . . . . . . . . . . . 15
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
80 | | eqid 2100 |
. . . . . . . . . . . . . . 15
  
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
    
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
   |
81 | | simplr 500 |
. . . . . . . . . . . . . . 15
            
    ♯         |
82 | 17 | ad2antrr 475 |
. . . . . . . . . . . . . . 15
            
    ♯         |
83 | 22 | ad2antrr 475 |
. . . . . . . . . . . . . . 15
            
    ♯             |
84 | 60 | adantrr 466 |
. . . . . . . . . . . . . . 15
            
    ♯                 |
85 | | simprr 502 |
. . . . . . . . . . . . . . 15
            
    ♯           ♯       |
86 | 5, 70, 72, 79, 80, 81, 82, 83, 84, 85 | summodclem2a 10989 |
. . . . . . . . . . . . . 14
            
    ♯               ![]_ ]_](_urbrack.gif)          ♯         ![]_ ]_](_urbrack.gif) 
        |
87 | 59 | adantrr 466 |
. . . . . . . . . . . . . . . . . . . . 21
            
    ♯             |
88 | 87, 84 | fihasheqf1od 10377 |
. . . . . . . . . . . . . . . . . . . 20
            
    ♯       ♯      ♯    |
89 | 81 | nnnn0d 8882 |
. . . . . . . . . . . . . . . . . . . . 21
            
    ♯         |
90 | | hashfz1 10370 |
. . . . . . . . . . . . . . . . . . . . 21

♯        |
91 | 89, 90 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
            
    ♯       ♯        |
92 | 88, 91 | eqtr3d 2134 |
. . . . . . . . . . . . . . . . . . 19
            
    ♯       ♯    |
93 | 92 | breq2d 3887 |
. . . . . . . . . . . . . . . . . 18
            
    ♯        ♯ 
   |
94 | 93 | ifbid 3440 |
. . . . . . . . . . . . . . . . 17
            
    ♯         ♯         ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif) 
   |
95 | 94 | mpteq2dv 3959 |
. . . . . . . . . . . . . . . 16
            
    ♯          ♯         ![]_ ]_](_urbrack.gif)      
       ![]_ ]_](_urbrack.gif) 
    |
96 | 95 | seqeq3d 10067 |
. . . . . . . . . . . . . . 15
            
    ♯            ♯         ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)       |
97 | 96 | fveq1d 5355 |
. . . . . . . . . . . . . 14
            
    ♯            ♯         ![]_ ]_](_urbrack.gif) 
                  ![]_ ]_](_urbrack.gif)          |
98 | 86, 97 | breqtrd 3899 |
. . . . . . . . . . . . 13
            
    ♯               ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)          |
99 | 98 | expr 370 |
. . . . . . . . . . . 12
             
    ♯             ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)           |
100 | 99 | exlimdv 1758 |
. . . . . . . . . . 11
              
    ♯    
      
 ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)           |
101 | 67, 100 | mpd 13 |
. . . . . . . . . 10
                     ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)          |
102 | | breq2 3879 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)       
        ![]_ ]_](_urbrack.gif)    
      
 ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)           |
103 | 101, 102 | syl5ibrcom 156 |
. . . . . . . . 9
                          ![]_ ]_](_urbrack.gif)       
      
 ![]_ ]_](_urbrack.gif)        |
104 | 103 | expimpd 358 |
. . . . . . . 8
 

         
            ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)        |
105 | 104 | exlimdv 1758 |
. . . . . . 7
 

                        ![]_ ]_](_urbrack.gif) 
               ![]_ ]_](_urbrack.gif)        |
106 | 105 | rexlimdva 2508 |
. . . . . 6
             
            ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)        |
107 | 52, 106 | jaod 678 |
. . . . 5
              DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)        |
108 | 17 | adantr 272 |
. . . . . . . 8
 
      
 ![]_ ]_](_urbrack.gif)        |
109 | 22 | adantr 272 |
. . . . . . . 8
 
      
 ![]_ ]_](_urbrack.gif)            |
110 | | eleq1w 2160 |
. . . . . . . . . . . 12
 
   |
111 | 110 | dcbid 792 |
. . . . . . . . . . 11
 DECID
DECID
   |
112 | 111 | cbvralv 2612 |
. . . . . . . . . 10
 
    DECID
     DECID   |
113 | 26, 112 | sylib 121 |
. . . . . . . . 9
      DECID   |
114 | 113 | adantr 272 |
. . . . . . . 8
 
      
 ![]_ ]_](_urbrack.gif)           DECID   |
115 | | simpr 109 |
. . . . . . . 8
 
      
 ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)       |
116 | | fveq2 5353 |
. . . . . . . . . . 11
           |
117 | 116 | sseq2d 3077 |
. . . . . . . . . 10
     
       |
118 | 116 | raleqdv 2590 |
. . . . . . . . . 10
  
    DECID      DECID    |
119 | | seqeq1 10062 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       |
120 | 119 | breq1d 3885 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif)    
      
 ![]_ ]_](_urbrack.gif)        |
121 | 117, 118,
120 | 3anbi123d 1258 |
. . . . . . . . 9
            DECID         ![]_ ]_](_urbrack.gif)                DECID         ![]_ ]_](_urbrack.gif)         |
122 | 121 | rspcev 2744 |
. . . . . . . 8
  
    
    DECID         ![]_ ]_](_urbrack.gif)      
           DECID         ![]_ ]_](_urbrack.gif)        |
123 | 108, 109,
114, 115, 122 | syl13anc 1186 |
. . . . . . 7
 
      
 ![]_ ]_](_urbrack.gif)       
    
    DECID         ![]_ ]_](_urbrack.gif)        |
124 | 123 | orcd 693 |
. . . . . 6
 
      
 ![]_ ]_](_urbrack.gif)                  DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
125 | 124 | ex 114 |
. . . . 5
       
 ![]_ ]_](_urbrack.gif)                 DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)             |
126 | 107, 125 | impbid 128 |
. . . 4
              DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)         
      
 ![]_ ]_](_urbrack.gif)        |
127 | | eluzelz 9185 |
. . . . . . . 8
    
  |
128 | | simpr 109 |
. . . . . . . . . 10
       
   |
129 | 8 | ad2antrr 475 |
. . . . . . . . . 10
       
 
  |
130 | | nfcsb1v 2985 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
131 | 130 | nfel1 2251 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
 |
132 | | csbeq1a 2963 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
133 | 132 | eleq1d 2168 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)    |
134 | 131, 133 | rspc 2738 |
. . . . . . . . . 10
  
  ![]_ ]_](_urbrack.gif)
   |
135 | 128, 129,
134 | sylc 62 |
. . . . . . . . 9
       
   ![]_ ]_](_urbrack.gif)   |
136 | | 0cnd 7631 |
. . . . . . . . 9
       
   |
137 | | eleq1w 2160 |
. . . . . . . . . . . . 13
 
   |
138 | 137 | dcbid 792 |
. . . . . . . . . . . 12
 DECID
DECID
   |
139 | 138 | cbvralv 2612 |
. . . . . . . . . . 11
 
    DECID
     DECID   |
140 | 26, 139 | sylib 121 |
. . . . . . . . . 10
      DECID   |
141 | 140 | r19.21bi 2479 |
. . . . . . . . 9
 
    
DECID
  |
142 | 135, 136,
141 | ifcldadc 3448 |
. . . . . . . 8
 
    
   
 ![]_ ]_](_urbrack.gif)     |
143 | | eleq1w 2160 |
. . . . . . . . . 10
 
   |
144 | | csbeq1 2958 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
145 | 143, 144 | ifbieq1d 3441 |
. . . . . . . . 9
  
   ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
146 | | eqid 2100 |
. . . . . . . . 9
    
 ![]_ ]_](_urbrack.gif)        
 ![]_ ]_](_urbrack.gif)     |
147 | 145, 146 | fvmptg 5429 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)     |
148 | 127, 142,
147 | syl2an2 564 |
. . . . . . 7
 
    
       ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)     |
149 | 148, 142 | eqeltrd 2176 |
. . . . . 6
 
    
       ![]_ ]_](_urbrack.gif)         |
150 | | simpr 109 |
. . . . . . . . 9
 
    
      |
151 | 53, 150 | sseldi 3045 |
. . . . . . . 8
 
    
  |
152 | | vex 2644 |
. . . . . . . . . 10
 |
153 | | nfv 1476 |
. . . . . . . . . . 11
  |
154 | | nfcsb1v 2985 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
155 | | nfcv 2240 |
. . . . . . . . . . 11
   |
156 | 153, 154,
155 | nfif 3447 |
. . . . . . . . . 10
       ![]_ ]_](_urbrack.gif)    |
157 | | eleq1w 2160 |
. . . . . . . . . . 11
 
   |
158 | | csbeq1a 2963 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   |
159 | 157, 158 | ifbieq1d 3441 |
. . . . . . . . . 10
           ![]_ ]_](_urbrack.gif)     |
160 | 152, 156,
159 | csbief 2994 |
. . . . . . . . 9
  ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)    |
161 | | simpr 109 |
. . . . . . . . . . 11
       
   |
162 | 8 | ad2antrr 475 |
. . . . . . . . . . 11
       
 
  |
163 | 154 | nfel1 2251 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
 |
164 | 158 | eleq1d 2168 |
. . . . . . . . . . . 12
 
  ![]_ ]_](_urbrack.gif)    |
165 | 163, 164 | rspc 2738 |
. . . . . . . . . . 11
  
  ![]_ ]_](_urbrack.gif)
   |
166 | 161, 162,
165 | sylc 62 |
. . . . . . . . . 10
       
   ![]_ ]_](_urbrack.gif)   |
167 | | 0cnd 7631 |
. . . . . . . . . 10
       
   |
168 | 113 | r19.21bi 2479 |
. . . . . . . . . 10
 
    
DECID
  |
169 | 166, 167,
168 | ifcldadc 3448 |
. . . . . . . . 9
 
    
   
 ![]_ ]_](_urbrack.gif)     |
170 | 160, 169 | syl5eqel 2186 |
. . . . . . . 8
 
    
  ![]_ ]_](_urbrack.gif)        |
171 | | nfcv 2240 |
. . . . . . . . . . 11
        |
172 | | nfv 1476 |
. . . . . . . . . . . 12
  |
173 | | nfcsb1v 2985 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
174 | 172, 173,
155 | nfif 3447 |
. . . . . . . . . . 11
       ![]_ ]_](_urbrack.gif)    |
175 | | eleq1w 2160 |
. . . . . . . . . . . 12
 
   |
176 | | csbeq1a 2963 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
177 | 175, 176 | ifbieq1d 3441 |
. . . . . . . . . . 11
           ![]_ ]_](_urbrack.gif)     |
178 | 171, 174,
177 | cbvmpt 3963 |
. . . . . . . . . 10
    
      
 ![]_ ]_](_urbrack.gif)     |
179 | 178 | eqcomi 2104 |
. . . . . . . . 9
    
 ![]_ ]_](_urbrack.gif)        
   |
180 | 179 | fvmpts 5431 |
. . . . . . . 8
    ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)        |
181 | 151, 170,
180 | syl2anc 406 |
. . . . . . 7
 
    
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)        |
182 | 150, 21 | syl6eleqr 2193 |
. . . . . . . 8
 
    
  |
183 | | zisum.4 |
. . . . . . . . . 10
 
            |
184 | 183 | ralrimiva 2464 |
. . . . . . . . 9
             |
185 | 184 | adantr 272 |
. . . . . . . 8
 
    

           |
186 | | nfcsb1v 2985 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)       |
187 | 186 | nfeq2 2252 |
. . . . . . . . 9
        ![]_ ]_](_urbrack.gif)       |
188 | | fveq2 5353 |
. . . . . . . . . 10
           |
189 | | csbeq1a 2963 |
. . . . . . . . . 10
        ![]_ ]_](_urbrack.gif)        |
190 | 188, 189 | eqeq12d 2114 |
. . . . . . . . 9
         
       ![]_ ]_](_urbrack.gif)         |
191 | 187, 190 | rspc 2738 |
. . . . . . . 8
  
               ![]_ ]_](_urbrack.gif)         |
192 | 182, 185,
191 | sylc 62 |
. . . . . . 7
 
    
      ![]_ ]_](_urbrack.gif)        |
193 | 181, 192 | eqtr4d 2135 |
. . . . . 6
 
    
       ![]_ ]_](_urbrack.gif)             |
194 | | addcl 7617 |
. . . . . . 7
 
     |
195 | 194 | adantl 273 |
. . . . . 6
 
       |
196 | 17, 149, 193, 195 | seq3feq 10086 |
. . . . 5
         ![]_ ]_](_urbrack.gif)          |
197 | 196 | breq1d 3885 |
. . . 4
       
 ![]_ ]_](_urbrack.gif)    
      |
198 | 126, 197 | bitrd 187 |
. . 3
              DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)         
      |
199 | 198 | iotabidv 5045 |
. 2
      
    
    DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                   |
200 | | df-sumdc 10962 |
. 2

         
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
201 | | df-fv 5067 |
. 2
           |
202 | 199, 200,
201 | 3eqtr4g 2157 |
1
 
      |