Step | Hyp | Ref
| Expression |
1 | | df-sumdc 11361 |
. 2

         
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
2 | | nnuz 9562 |
. . . . 5
     |
3 | | 1zzd 9279 |
. . . . 5
   |
4 | | elnnuz 9563 |
. . . . . 6

      |
5 | 2 | eqimss2i 3212 |
. . . . . . . . . 10
     |
6 | 5 | sseli 3151 |
. . . . . . . . 9
    
  |
7 | 6 | adantl 277 |
. . . . . . . 8
 
    
  |
8 | | fveq2 5515 |
. . . . . . . . . . 11
           |
9 | 8 | eleq1d 2246 |
. . . . . . . . . 10
     
       |
10 | | fsum.1 |
. . . . . . . . . . . 12
       |
11 | | fsum.2 |
. . . . . . . . . . . 12
   |
12 | | fsum.3 |
. . . . . . . . . . . 12
           |
13 | | fsum.4 |
. . . . . . . . . . . 12
 
   |
14 | | fsum.5 |
. . . . . . . . . . . 12
 
           |
15 | 10, 11, 12, 13, 14 | fsumgcl 11393 |
. . . . . . . . . . 11
             |
16 | 15 | ad2antrr 488 |
. . . . . . . . . 10
       

            |
17 | | 1zzd 9279 |
. . . . . . . . . . . 12
       

  |
18 | 11 | nnzd 9373 |
. . . . . . . . . . . . 13
   |
19 | 18 | ad2antrr 488 |
. . . . . . . . . . . 12
       

  |
20 | | eluzelz 9536 |
. . . . . . . . . . . . 13
    
  |
21 | 20 | ad2antlr 489 |
. . . . . . . . . . . 12
       

  |
22 | 17, 19, 21 | 3jca 1177 |
. . . . . . . . . . 11
       

    |
23 | | eluzle 9539 |
. . . . . . . . . . . . 13
    
  |
24 | 23 | ad2antlr 489 |
. . . . . . . . . . . 12
       

  |
25 | | simpr 110 |
. . . . . . . . . . . 12
       

  |
26 | 24, 25 | jca 306 |
. . . . . . . . . . 11
       

    |
27 | | elfz2 10014 |
. . . . . . . . . . 11
    
 
 
    |
28 | 22, 26, 27 | sylanbrc 417 |
. . . . . . . . . 10
       

      |
29 | 9, 16, 28 | rspcdva 2846 |
. . . . . . . . 9
       

      |
30 | | 0cnd 7949 |
. . . . . . . . 9
       
   |
31 | 7 | nnzd 9373 |
. . . . . . . . . 10
 
    
  |
32 | 18 | adantr 276 |
. . . . . . . . . 10
 
    
  |
33 | | zdcle 9328 |
. . . . . . . . . 10
 
 DECID   |
34 | 31, 32, 33 | syl2anc 411 |
. . . . . . . . 9
 
    
DECID
  |
35 | 29, 30, 34 | ifcldadc 3563 |
. . . . . . . 8
 
    
 
         |
36 | | breq1 4006 |
. . . . . . . . . 10
 
   |
37 | 36, 8 | ifbieq1d 3556 |
. . . . . . . . 9
  
                  |
38 | | eqid 2177 |
. . . . . . . . 9
  
          
         |
39 | 37, 38 | fvmptg 5592 |
. . . . . . . 8
               
                      |
40 | 7, 35, 39 | syl2anc 411 |
. . . . . . 7
 
    
                
         |
41 | 40, 35 | eqeltrd 2254 |
. . . . . 6
 
    
                 |
42 | 4, 41 | sylan2b 287 |
. . . . 5
 

                 |
43 | 2, 3, 42 | serf 10473 |
. . . 4
                     |
44 | 43, 11 | ffvelcdmd 5652 |
. . 3
     
              |
45 | 44 | adantr 276 |
. . . . . . . 8
 
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                              |
46 | | eleq1w 2238 |
. . . . . . . . . . . . 13
 
   |
47 | | csbeq1 3060 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
48 | 46, 47 | ifbieq1d 3556 |
. . . . . . . . . . . 12
  
   ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
49 | 48 | cbvmptv 4099 |
. . . . . . . . . . 11
    
 ![]_ ]_](_urbrack.gif)        
 ![]_ ]_](_urbrack.gif)     |
50 | 13 | ralrimiva 2550 |
. . . . . . . . . . . 12
 
  |
51 | | nfcsb1v 3090 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
52 | 51 | nfel1 2330 |
. . . . . . . . . . . . 13
    ![]_ ]_](_urbrack.gif)
 |
53 | | csbeq1a 3066 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
54 | 53 | eleq1d 2246 |
. . . . . . . . . . . . 13
 
  ![]_ ]_](_urbrack.gif)    |
55 | 52, 54 | rspc 2835 |
. . . . . . . . . . . 12
  
  ![]_ ]_](_urbrack.gif)
   |
56 | 50, 55 | mpan9 281 |
. . . . . . . . . . 11
 
   ![]_ ]_](_urbrack.gif)   |
57 | | breq1 4006 |
. . . . . . . . . . . . 13
 
♯  ♯     |
58 | | fveq2 5515 |
. . . . . . . . . . . . . . 15
           |
59 | 58 | csbeq1d 3064 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
60 | | csbco 3067 |
. . . . . . . . . . . . . 14
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  |
61 | 59, 60 | eqtr4di 2228 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
62 | 57, 61 | ifbieq1d 3556 |
. . . . . . . . . . . 12
  
♯         ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
63 | 62 | cbvmptv 4099 |
. . . . . . . . . . 11
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
64 | 49, 56, 63, 63 | summodc 11390 |
. . . . . . . . . 10
         
     DECID
        ![]_ ]_](_urbrack.gif)                 
     ♯         ![]_ ]_](_urbrack.gif) 
          |
65 | | eleq1w 2238 |
. . . . . . . . . . . . . . . 16
 
   |
66 | 65 | dcbid 838 |
. . . . . . . . . . . . . . 15
 DECID
DECID
   |
67 | 66 | cbvralv 2703 |
. . . . . . . . . . . . . 14
 
    DECID
     DECID   |
68 | 67 | 3anbi2i 1191 |
. . . . . . . . . . . . 13
 
    
    DECID         ![]_ ]_](_urbrack.gif)                DECID         ![]_ ]_](_urbrack.gif)        |
69 | 68 | rexbii 2484 |
. . . . . . . . . . . 12
      
     DECID
        ![]_ ]_](_urbrack.gif)      

    
    DECID         ![]_ ]_](_urbrack.gif)        |
70 | | 1zzd 9279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
71 | | nnz 9271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
72 | 70, 71 | fzfigd 10430 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
73 | | fihasheqf1oi 10766 |
. . . . . . . . . . . . . . . . . . . . . . 23
               ♯      ♯    |
74 | 72, 73 | sylan 283 |
. . . . . . . . . . . . . . . . . . . . . 22
           ♯      ♯    |
75 | | nnnn0 9182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
76 | 75 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
77 | | hashfz1 10762 |
. . . . . . . . . . . . . . . . . . . . . . 23

♯        |
78 | 76, 77 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
           ♯        |
79 | 74, 78 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . . . . 21
           ♯    |
80 | 79 | breq2d 4015 |
. . . . . . . . . . . . . . . . . . . 20
           
♯ 
   |
81 | 80 | ifbid 3555 |
. . . . . . . . . . . . . . . . . . 19
            
♯         ![]_ ]_](_urbrack.gif)     
      ![]_ ]_](_urbrack.gif)     |
82 | 81 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . . 18
              ♯         ![]_ ]_](_urbrack.gif) 
    
       ![]_ ]_](_urbrack.gif) 
    |
83 | 82 | seqeq3d 10452 |
. . . . . . . . . . . . . . . . 17
                ♯         ![]_ ]_](_urbrack.gif) 
               ![]_ ]_](_urbrack.gif)       |
84 | 83 | fveq1d 5517 |
. . . . . . . . . . . . . . . 16
                ♯         ![]_ ]_](_urbrack.gif) 
                  ![]_ ]_](_urbrack.gif)          |
85 | 84 | eqeq2d 2189 |
. . . . . . . . . . . . . . 15
                 ♯         ![]_ ]_](_urbrack.gif) 
     
            ![]_ ]_](_urbrack.gif)           |
86 | 85 | pm5.32da 452 |
. . . . . . . . . . . . . 14
                ♯         ![]_ ]_](_urbrack.gif)        
             
       ![]_ ]_](_urbrack.gif) 
          |
87 | 86 | exbidv 1825 |
. . . . . . . . . . . . 13
                  ♯         ![]_ ]_](_urbrack.gif)        
                       ![]_ ]_](_urbrack.gif) 
          |
88 | 87 | rexbiia 2492 |
. . . . . . . . . . . 12
                  ♯         ![]_ ]_](_urbrack.gif)        
           
            ![]_ ]_](_urbrack.gif)           |
89 | 69, 88 | orbi12i 764 |
. . . . . . . . . . 11
   
    
    DECID         ![]_ ]_](_urbrack.gif)                 
     ♯         ![]_ ]_](_urbrack.gif) 
       
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
90 | 89 | mobii 2063 |
. . . . . . . . . 10
               DECID         ![]_ ]_](_urbrack.gif)                 
     ♯         ![]_ ]_](_urbrack.gif) 
       
              DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
91 | 64, 90 | sylib 122 |
. . . . . . . . 9
         
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
92 | 91 | adantr 276 |
. . . . . . . 8
 
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)               
    
    DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
93 | | simpr 110 |
. . . . . . . 8
 
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                       DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            |
94 | | f1of 5461 |
. . . . . . . . . . . . . 14
        
          |
95 | 12, 94 | syl 14 |
. . . . . . . . . . . . 13
           |
96 | 3, 18 | fzfigd 10430 |
. . . . . . . . . . . . 13
       |
97 | | fex 5745 |
. . . . . . . . . . . . 13
                 |
98 | 95, 96, 97 | syl2anc 411 |
. . . . . . . . . . . 12
   |
99 | 11, 2 | eleqtrdi 2270 |
. . . . . . . . . . . . . 14
       |
100 | 14 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . 17
             |
101 | | nfv 1528 |
. . . . . . . . . . . . . . . . . 18
       |
102 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]_ ]_](_urbrack.gif)  |
103 | 102 | nfeq2 2331 |
. . . . . . . . . . . . . . . . . 18
        ![]_ ]_](_urbrack.gif)  |
104 | | fveq2 5515 |
. . . . . . . . . . . . . . . . . . 19
           |
105 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)   |
106 | 104, 105 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . 18
     
      ![]_ ]_](_urbrack.gif)    |
107 | 101, 103,
106 | cbvral 2699 |
. . . . . . . . . . . . . . . . 17
 
        
            ![]_ ]_](_urbrack.gif)   |
108 | 100, 107 | sylib 122 |
. . . . . . . . . . . . . . . 16
             ![]_ ]_](_urbrack.gif)   |
109 | 108 | r19.21bi 2565 |
. . . . . . . . . . . . . . 15
 
           ![]_ ]_](_urbrack.gif)   |
110 | | elfznn 10053 |
. . . . . . . . . . . . . . . . . 18
       |
111 | 110 | adantl 277 |
. . . . . . . . . . . . . . . . 17
 
       |
112 | | elfzle2 10027 |
. . . . . . . . . . . . . . . . . . . 20
       |
113 | 112 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
 
       |
114 | 113 | iftrued 3541 |
. . . . . . . . . . . . . . . . . 18
 
                    |
115 | 104 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . 19
     
       |
116 | 15 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
117 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
 
           |
118 | 115, 116,
117 | rspcdva 2846 |
. . . . . . . . . . . . . . . . . 18
 
           |
119 | 114, 118 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . 17
 
                |
120 | | breq1 4006 |
. . . . . . . . . . . . . . . . . . 19
 
   |
121 | 120, 104 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . . 18
  
                  |
122 | 121, 38 | fvmptg 5592 |
. . . . . . . . . . . . . . . . 17
               
                      |
123 | 111, 119,
122 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
                     
         |
124 | 123, 114 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
 
                          |
125 | 113 | iftrued 3541 |
. . . . . . . . . . . . . . . . . 18
 
          ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
126 | 95 | ffvelcdmda 5651 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           |
127 | 10 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
            
  |
128 | 126, 127 | csbied 3103 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           ![]_ ]_](_urbrack.gif)   |
129 | 50 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
  |
130 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        ![]_ ]_](_urbrack.gif)  |
131 | 130 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        ![]_ ]_](_urbrack.gif)
 |
132 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           ![]_ ]_](_urbrack.gif)   |
133 | 132 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
      ![]_ ]_](_urbrack.gif)    |
134 | 131, 133 | rspc 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
      ![]_ ]_](_urbrack.gif)
   |
135 | 126, 129,
134 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           ![]_ ]_](_urbrack.gif)   |
136 | 128, 135 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
137 | 136 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . . . . 20
         |
138 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . 21
  |
139 | 102 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . . . 21
  
 ![]_ ]_](_urbrack.gif)
 |
140 | 105 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ![]_ ]_](_urbrack.gif)    |
141 | 138, 139,
140 | cbvral 2699 |
. . . . . . . . . . . . . . . . . . . 20
 
    
        ![]_ ]_](_urbrack.gif)
  |
142 | 137, 141 | sylib 122 |
. . . . . . . . . . . . . . . . . . 19
         ![]_ ]_](_urbrack.gif)
  |
143 | 142 | r19.21bi 2565 |
. . . . . . . . . . . . . . . . . 18
 
       ![]_ ]_](_urbrack.gif)   |
144 | 125, 143 | eqeltrd 2254 |
. . . . . . . . . . . . . . . . 17
 
          ![]_ ]_](_urbrack.gif)     |
145 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . 18
   |
146 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . 19
  |
147 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . . 19
   |
148 | 146, 102,
147 | nfif 3562 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)    |
149 | 120, 105 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . . 18
  
 
      ![]_ ]_](_urbrack.gif)     |
150 | | eqid 2177 |
. . . . . . . . . . . . . . . . . 18
  
 
    
 
   |
151 | 145, 148,
149, 150 | fvmptf 5608 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)                 
  ![]_ ]_](_urbrack.gif)     |
152 | 111, 144,
151 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
 
                     ![]_ ]_](_urbrack.gif)     |
153 | 152, 125 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
 
                  ![]_ ]_](_urbrack.gif)   |
154 | 109, 124,
153 | 3eqtr4d 2220 |
. . . . . . . . . . . . . 14
 
                                 |
155 | 137 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
       

        |
156 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . . . 20
  
 ![]_ ]_](_urbrack.gif)  |
157 | 156 | nfel1 2330 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]_ ]_](_urbrack.gif)
 |
158 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   |
159 | 158 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . 19
 
  ![]_ ]_](_urbrack.gif)    |
160 | 157, 159 | rspc 2835 |
. . . . . . . . . . . . . . . . . 18
      
       ![]_ ]_](_urbrack.gif)    |
161 | 28, 155, 160 | sylc 62 |
. . . . . . . . . . . . . . . . 17
       

  ![]_ ]_](_urbrack.gif)   |
162 | 161, 30, 34 | ifcldadc 3563 |
. . . . . . . . . . . . . . . 16
 
    
 
 
 ![]_ ]_](_urbrack.gif)     |
163 | | nfcv 2319 |
. . . . . . . . . . . . . . . . 17
   |
164 | | nfv 1528 |
. . . . . . . . . . . . . . . . . 18
  |
165 | 164, 156,
147 | nfif 3562 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)    |
166 | 36, 158 | ifbieq1d 3556 |
. . . . . . . . . . . . . . . . 17
  
 
      ![]_ ]_](_urbrack.gif)     |
167 | 163, 165,
166, 150 | fvmptf 5608 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)                 
  ![]_ ]_](_urbrack.gif)     |
168 | 7, 162, 167 | syl2anc 411 |
. . . . . . . . . . . . . . 15
 
    
                ![]_ ]_](_urbrack.gif)     |
169 | 168, 162 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
 
    
             |
170 | | addcl 7935 |
. . . . . . . . . . . . . . 15
 
     |
171 | 170 | adantl 277 |
. . . . . . . . . . . . . 14
 
       |
172 | 99, 154, 41, 169, 171 | seq3fveq 10470 |
. . . . . . . . . . . . 13
     
                           |
173 | 12, 172 | jca 306 |
. . . . . . . . . . . 12
                                           |
174 | | f1oeq1 5449 |
. . . . . . . . . . . . . 14
         
           |
175 | | fveq1 5514 |
. . . . . . . . . . . . . . . . . . . . 21
           |
176 | 175 | csbeq1d 3064 |
. . . . . . . . . . . . . . . . . . . 20
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
177 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
178 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
179 | 177, 178 | fvex 5535 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
180 | 175, 179 | eqeltrrdi 2269 |
. . . . . . . . . . . . . . . . . . . . 21
       |
181 | 10 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
  |
182 | 180, 181 | csbied 3103 |
. . . . . . . . . . . . . . . . . . . 20
       ![]_ ]_](_urbrack.gif)   |
183 | 176, 182 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . 19
       ![]_ ]_](_urbrack.gif)   |
184 | 183 | ifeq1d 3551 |
. . . . . . . . . . . . . . . . . 18
  
       ![]_ ]_](_urbrack.gif) 
        |
185 | 184 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . 17
           ![]_ ]_](_urbrack.gif)      
 
    |
186 | 185 | seqeq3d 10452 |
. . . . . . . . . . . . . . . 16
             ![]_ ]_](_urbrack.gif)                 |
187 | 186 | fveq1d 5517 |
. . . . . . . . . . . . . . 15
             ![]_ ]_](_urbrack.gif)                       |
188 | 187 | eqeq2d 2189 |
. . . . . . . . . . . . . 14
                               ![]_ ]_](_urbrack.gif)                                         |
189 | 174, 188 | anbi12d 473 |
. . . . . . . . . . . . 13
                                        ![]_ ]_](_urbrack.gif) 
      
                                           |
190 | 189 | spcegv 2825 |
. . . . . . . . . . . 12
                                         
                                        ![]_ ]_](_urbrack.gif) 
          |
191 | 98, 173, 190 | sylc 62 |
. . . . . . . . . . 11
                                         ![]_ ]_](_urbrack.gif) 
         |
192 | | oveq2 5882 |
. . . . . . . . . . . . . . 15
           |
193 | | f1oeq2 5450 |
. . . . . . . . . . . . . . 15
                 
           |
194 | 192, 193 | syl 14 |
. . . . . . . . . . . . . 14
         
           |
195 | | breq2 4007 |
. . . . . . . . . . . . . . . . . . 19
 
   |
196 | 195 | ifbid 3555 |
. . . . . . . . . . . . . . . . . 18
  
       ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif) 
   |
197 | 196 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . 17
           ![]_ ]_](_urbrack.gif)      
       ![]_ ]_](_urbrack.gif) 
    |
198 | 197 | seqeq3d 10452 |
. . . . . . . . . . . . . . . 16
             ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)       |
199 | | id 19 |
. . . . . . . . . . . . . . . 16
   |
200 | 198, 199 | fveq12d 5522 |
. . . . . . . . . . . . . . 15
             ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)          |
201 | 200 | eqeq2d 2189 |
. . . . . . . . . . . . . 14
                               ![]_ ]_](_urbrack.gif)                                     ![]_ ]_](_urbrack.gif) 
         |
202 | 194, 201 | anbi12d 473 |
. . . . . . . . . . . . 13
                                        ![]_ ]_](_urbrack.gif) 
      
                                      ![]_ ]_](_urbrack.gif) 
          |
203 | 202 | exbidv 1825 |
. . . . . . . . . . . 12
                                          ![]_ ]_](_urbrack.gif) 
      
                                        ![]_ ]_](_urbrack.gif) 
          |
204 | 203 | rspcev 2841 |
. . . . . . . . . . 11
                                          ![]_ ]_](_urbrack.gif) 
        
                                        ![]_ ]_](_urbrack.gif) 
         |
205 | 11, 191, 204 | syl2anc 411 |
. . . . . . . . . 10
                                          ![]_ ]_](_urbrack.gif) 
         |
206 | 205 | olcd 734 |
. . . . . . . . 9
             DECID         ![]_ ]_](_urbrack.gif)                                                                ![]_ ]_](_urbrack.gif) 
          |
207 | 206 | adantr 276 |
. . . . . . . 8
 
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                       DECID         ![]_ ]_](_urbrack.gif)                                                                ![]_ ]_](_urbrack.gif) 
          |
208 | | breq2 4007 |
. . . . . . . . . . . 12
                          ![]_ ]_](_urbrack.gif)    
        ![]_ ]_](_urbrack.gif)                         |
209 | 208 | 3anbi3d 1318 |
. . . . . . . . . . 11
                             DECID         ![]_ ]_](_urbrack.gif)                DECID         ![]_ ]_](_urbrack.gif)                          |
210 | 209 | rexbidv 2478 |
. . . . . . . . . 10
                   

    
    DECID         ![]_ ]_](_urbrack.gif)      

    
    DECID         ![]_ ]_](_urbrack.gif)                          |
211 | | eqeq1 2184 |
. . . . . . . . . . . . 13
                               ![]_ ]_](_urbrack.gif)                                     ![]_ ]_](_urbrack.gif) 
         |
212 | 211 | anbi2d 464 |
. . . . . . . . . . . 12
                                        ![]_ ]_](_urbrack.gif) 
      
                                      ![]_ ]_](_urbrack.gif) 
          |
213 | 212 | exbidv 1825 |
. . . . . . . . . . 11
                                          ![]_ ]_](_urbrack.gif) 
      
                                        ![]_ ]_](_urbrack.gif) 
          |
214 | 213 | rexbidv 2478 |
. . . . . . . . . 10
                   
                       ![]_ ]_](_urbrack.gif) 
      
                                         ![]_ ]_](_urbrack.gif)            |
215 | 210, 214 | orbi12d 793 |
. . . . . . . . 9
                               DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)         
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                                                                ![]_ ]_](_urbrack.gif) 
           |
216 | 215 | moi2 2918 |
. . . . . . . 8
                            
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                  
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)            
    
    DECID         ![]_ ]_](_urbrack.gif)                                                                ![]_ ]_](_urbrack.gif) 
         
                   |
217 | 45, 92, 93, 207, 216 | syl22anc 1239 |
. . . . . . 7
 
 
    
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                              |
218 | 217 | ex 115 |
. . . . . 6
              DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)         
                    |
219 | 206, 215 | syl5ibrcom 157 |
. . . . . 6
                               DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)             |
220 | 218, 219 | impbid 129 |
. . . . 5
              DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)         
                    |
221 | 220 | adantr 276 |
. . . 4
 
                         
     DECID
        ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)         
                    |
222 | 221 | iota5 5198 |
. . 3
 
                                 DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                              |
223 | 44, 222 | mpdan 421 |
. 2
      
    
    DECID         ![]_ ]_](_urbrack.gif)                 
            ![]_ ]_](_urbrack.gif)                              |
224 | 1, 223 | eqtrid 2222 |
1
 
                   |