Step | Hyp | Ref
| Expression |
1 | | fveq2 5353 |
. . . . . . . . . 10
           |
2 | 1 | sseq2d 3077 |
. . . . . . . . 9
     
       |
3 | 1 | raleqdv 2590 |
. . . . . . . . 9
  
    DECID      DECID    |
4 | | seqeq1 10062 |
. . . . . . . . . 10
         |
5 | 4 | breq1d 3885 |
. . . . . . . . 9
   
      |
6 | 2, 3, 5 | 3anbi123d 1258 |
. . . . . . . 8
            DECID               DECID        |
7 | 6 | cbvrexv 2613 |
. . . . . . 7
      
     DECID
   
           DECID       |
8 | | reeanv 2558 |
. . . . . . . . 9
  
           DECID               DECID                  DECID          
     DECID
       |
9 | | simprl3 996 |
. . . . . . . . . . . . 13
   
 
     
     DECID
    
    
    DECID            |
10 | | isummo.1 |
. . . . . . . . . . . . . 14
        |
11 | | simpll 499 |
. . . . . . . . . . . . . . 15
   
 
     
     DECID
    
    
    DECID         |
12 | | isummo.2 |
. . . . . . . . . . . . . . 15
 
   |
13 | 11, 12 | sylan 279 |
. . . . . . . . . . . . . 14
    
   
    
    DECID               DECID          |
14 | | simplrl 505 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
    
    
    DECID         |
15 | | simplrr 506 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
    
    
    DECID         |
16 | | simprl1 994 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
    
    
    DECID             |
17 | | simprr1 997 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
    
    
    DECID             |
18 | | eleq1w 2160 |
. . . . . . . . . . . . . . . 16
 
   |
19 | 18 | dcbid 792 |
. . . . . . . . . . . . . . 15
 DECID
DECID
   |
20 | | simprl2 995 |
. . . . . . . . . . . . . . . 16
   
 
     
     DECID
    
    
    DECID            DECID   |
21 | 20 | adantr 272 |
. . . . . . . . . . . . . . 15
    
   
    
    DECID               DECID           
     DECID   |
22 | | simpr 109 |
. . . . . . . . . . . . . . 15
    
   
    
    DECID               DECID           
      |
23 | 19, 21, 22 | rspcdva 2749 |
. . . . . . . . . . . . . 14
    
   
    
    DECID               DECID           
DECID
  |
24 | | simprr2 998 |
. . . . . . . . . . . . . . . 16
   
 
     
     DECID
    
    
    DECID            DECID   |
25 | 24 | adantr 272 |
. . . . . . . . . . . . . . 15
    
   
    
    DECID               DECID           
     DECID   |
26 | | simpr 109 |
. . . . . . . . . . . . . . 15
    
   
    
    DECID               DECID           
      |
27 | 19, 25, 26 | rspcdva 2749 |
. . . . . . . . . . . . . 14
    
   
    
    DECID               DECID           
DECID
  |
28 | 10, 13, 14, 15, 16, 17, 23, 27 | sumrbdc 10986 |
. . . . . . . . . . . . 13
   
 
     
     DECID
    
    
    DECID         
      |
29 | 9, 28 | mpbid 146 |
. . . . . . . . . . . 12
   
 
     
     DECID
    
    
    DECID            |
30 | | simprr3 999 |
. . . . . . . . . . . 12
   
 
     
     DECID
    
    
    DECID            |
31 | | climuni 10901 |
. . . . . . . . . . . 12
          |
32 | 29, 30, 31 | syl2anc 406 |
. . . . . . . . . . 11
   
 
     
     DECID
    
    
    DECID         |
33 | 32 | exp31 359 |
. . . . . . . . . 10
                DECID     
    
    DECID     
    |
34 | 33 | rexlimdvv 2515 |
. . . . . . . . 9
         
     DECID
    
    
    DECID     
   |
35 | 8, 34 | syl5bir 152 |
. . . . . . . 8
              DECID          
     DECID
        |
36 | 35 | expdimp 257 |
. . . . . . 7
 
           DECID                  DECID    
   |
37 | 7, 36 | syl5bi 151 |
. . . . . 6
 
           DECID                  DECID    
   |
38 | | summodc.3 |
. . . . . . 7
   ♯         ![]_ ]_](_urbrack.gif) 
   |
39 | 10, 12, 38 | summodclem2 10990 |
. . . . . 6
 
           DECID                  
          |
40 | 37, 39 | jaod 678 |
. . . . 5
 
           DECID             
     DECID
                           |
41 | 10, 12, 38 | summodclem2 10990 |
. . . . . . . 8
 
           DECID                  
          |
42 | | equcom 1650 |
. . . . . . . 8

  |
43 | 41, 42 | syl6ib 160 |
. . . . . . 7
 
           DECID                  
          |
44 | 43 | impancom 258 |
. . . . . 6
 
           
                    DECID    
   |
45 | | oveq2 5714 |
. . . . . . . . . . . 12
           |
46 | | f1oeq2 5293 |
. . . . . . . . . . . 12
                 
           |
47 | 45, 46 | syl 14 |
. . . . . . . . . . 11
         
           |
48 | | fveq2 5353 |
. . . . . . . . . . . 12
               |
49 | 48 | eqeq2d 2111 |
. . . . . . . . . . 11
                 |
50 | 47, 49 | anbi12d 460 |
. . . . . . . . . 10
                 
                   |
51 | 50 | exbidv 1764 |
. . . . . . . . 9
                   
                     |
52 | | f1oeq1 5292 |
. . . . . . . . . . 11
         
           |
53 | | breq1 3878 |
. . . . . . . . . . . . . . . . . 18
 
♯  ♯     |
54 | | fveq2 5353 |
. . . . . . . . . . . . . . . . . . 19
           |
55 | 54 | csbeq1d 2961 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
56 | 53, 55 | ifbieq1d 3441 |
. . . . . . . . . . . . . . . . 17
  
♯         ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)     |
57 | 56 | cbvmptv 3964 |
. . . . . . . . . . . . . . . 16
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)     |
58 | | fveq1 5352 |
. . . . . . . . . . . . . . . . . . 19
           |
59 | 58 | csbeq1d 2961 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
60 | 59 | ifeq1d 3436 |
. . . . . . . . . . . . . . . . 17
   ♯         ![]_ ]_](_urbrack.gif) 
   ♯         ![]_ ]_](_urbrack.gif)     |
61 | 60 | mpteq2dv 3959 |
. . . . . . . . . . . . . . . 16
    ♯         ![]_ ]_](_urbrack.gif) 
    
♯         ![]_ ]_](_urbrack.gif)      |
62 | 57, 61 | syl5eq 2144 |
. . . . . . . . . . . . . . 15
    ♯         ![]_ ]_](_urbrack.gif) 
    
♯         ![]_ ]_](_urbrack.gif)      |
63 | 38, 62 | syl5eq 2144 |
. . . . . . . . . . . . . 14
    ♯         ![]_ ]_](_urbrack.gif)      |
64 | 63 | seqeq3d 10067 |
. . . . . . . . . . . . 13
         ♯         ![]_ ]_](_urbrack.gif) 
     |
65 | 64 | fveq1d 5355 |
. . . . . . . . . . . 12
            ♯         ![]_ ]_](_urbrack.gif) 
        |
66 | 65 | eqeq2d 2111 |
. . . . . . . . . . 11
             ♯         ![]_ ]_](_urbrack.gif)           |
67 | 52, 66 | anbi12d 460 |
. . . . . . . . . 10
                 
             
♯         ![]_ ]_](_urbrack.gif)            |
68 | 67 | cbvexv 1855 |
. . . . . . . . 9
                  
                ♯         ![]_ ]_](_urbrack.gif)           |
69 | 51, 68 | syl6bb 195 |
. . . . . . . 8
                   
                ♯         ![]_ ]_](_urbrack.gif)            |
70 | 69 | cbvrexv 2613 |
. . . . . . 7
                   
           
     ♯         ![]_ ]_](_urbrack.gif) 
         |
71 | | reeanv 2558 |
. . . . . . . . 9
  
                                   ♯         ![]_ ]_](_urbrack.gif)         
 
                                   ♯         ![]_ ]_](_urbrack.gif)            |
72 | | eeanv 1867 |
. . . . . . . . . . 11
                                    ♯         ![]_ ]_](_urbrack.gif)         
                                   ♯         ![]_ ]_](_urbrack.gif)            |
73 | | an4 556 |
. . . . . . . . . . . . 13
                                ♯         ![]_ ]_](_urbrack.gif)         
                         
     ♯         ![]_ ]_](_urbrack.gif)            |
74 | | 1zzd 8933 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
                     |
75 | | simplrr 506 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
 
                  
  |
76 | 75 | nnzd 9024 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
                  
  |
77 | 74, 76 | fzfigd 10045 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
                         |
78 | | simprr 502 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
                             |
79 | 77, 78 | fihasheqf1od 10377 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
                   ♯      ♯    |
80 | 75 | nnnn0d 8882 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 
                  
  |
81 | | hashfz1 10370 |
. . . . . . . . . . . . . . . . . . . . . . . 24

♯        |
82 | 80, 81 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
                   ♯        |
83 | 79, 82 | eqtr3d 2134 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 
                   ♯    |
84 | 83 | breq2d 3887 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
                    ♯ 
   |
85 | 84 | ifbid 3440 |
. . . . . . . . . . . . . . . . . . . 20
   
 
                     ♯         ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif) 
   |
86 | 85 | mpteq2dv 3959 |
. . . . . . . . . . . . . . . . . . 19
   
 
                      ♯         ![]_ ]_](_urbrack.gif) 
    
       ![]_ ]_](_urbrack.gif) 
    |
87 | 86 | seqeq3d 10067 |
. . . . . . . . . . . . . . . . . 18
   
 
                        ♯         ![]_ ]_](_urbrack.gif) 
               ![]_ ]_](_urbrack.gif)       |
88 | 87 | fveq1d 5355 |
. . . . . . . . . . . . . . . . 17
   
 
                        ♯         ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)          |
89 | 88 | eqeq2d 2111 |
. . . . . . . . . . . . . . . 16
   
 
                         ♯         ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif) 
         |
90 | 89 | anbi2d 455 |
. . . . . . . . . . . . . . 15
   
 
                          
     ♯         ![]_ ]_](_urbrack.gif) 
      

     
            ![]_ ]_](_urbrack.gif)            |
91 | | simplrl 505 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
                  
  |
92 | 91 | nnnn0d 8882 |
. . . . . . . . . . . . . . . . . . . 20
   
 
                  
  |
93 | | hashfz1 10370 |
. . . . . . . . . . . . . . . . . . . 20

♯        |
94 | 92, 93 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
   
 
                   ♯        |
95 | 91 | nnzd 9024 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
                  
  |
96 | 74, 95 | fzfigd 10045 |
. . . . . . . . . . . . . . . . . . . 20
   
 
                         |
97 | | simprl 501 |
. . . . . . . . . . . . . . . . . . . 20
   
 
                             |
98 | 96, 97 | fihasheqf1od 10377 |
. . . . . . . . . . . . . . . . . . 19
   
 
                   ♯      ♯    |
99 | 94, 98 | eqtr3d 2134 |
. . . . . . . . . . . . . . . . . 18
   
 
                  
♯    |
100 | 99 | fveq2d 5357 |
. . . . . . . . . . . . . . . . 17
   
 
                              ♯     |
101 | | simpll 499 |
. . . . . . . . . . . . . . . . . . 19
   
 
                     |
102 | 101, 12 | sylan 279 |
. . . . . . . . . . . . . . . . . 18
    
                    
   |
103 | 99, 91 | eqeltrrd 2177 |
. . . . . . . . . . . . . . . . . . 19
   
 
                   ♯    |
104 | 103, 75 | jca 302 |
. . . . . . . . . . . . . . . . . 18
   
 
                    ♯ 
   |
105 | 99 | oveq2d 5722 |
. . . . . . . . . . . . . . . . . . . 20
   
 
                          ♯     |
106 | | f1oeq2 5293 |
. . . . . . . . . . . . . . . . . . . 20
        ♯  
              ♯        |
107 | 105, 106 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
   
 
                                 ♯        |
108 | 97, 107 | mpbid 146 |
. . . . . . . . . . . . . . . . . 18
   
 
                        ♯       |
109 | | breq1 3878 |
. . . . . . . . . . . . . . . . . . . . 21
 
♯  ♯     |
110 | | fveq2 5353 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
111 | 110 | csbeq1d 2961 |
. . . . . . . . . . . . . . . . . . . . 21
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
112 | 109, 111 | ifbieq1d 3441 |
. . . . . . . . . . . . . . . . . . . 20
  
♯         ![]_ ]_](_urbrack.gif)     ♯         ![]_ ]_](_urbrack.gif)     |
113 | 112 | cbvmptv 3964 |
. . . . . . . . . . . . . . . . . . 19
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)     |
114 | 38, 113 | eqtri 2120 |
. . . . . . . . . . . . . . . . . 18
   ♯         ![]_ ]_](_urbrack.gif) 
   |
115 | | breq1 3878 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
116 | | fveq2 5353 |
. . . . . . . . . . . . . . . . . . . . 21
           |
117 | 116 | csbeq1d 2961 |
. . . . . . . . . . . . . . . . . . . 20
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
118 | 115, 117 | ifbieq1d 3441 |
. . . . . . . . . . . . . . . . . . 19
          ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif) 
   |
119 | 118 | cbvmptv 3964 |
. . . . . . . . . . . . . . . . . 18
  
       ![]_ ]_](_urbrack.gif) 
    
       ![]_ ]_](_urbrack.gif) 
   |
120 | 10, 102, 104, 108, 78, 114, 119 | summodclem3 10988 |
. . . . . . . . . . . . . . . . 17
   
 
                        ♯               ![]_ ]_](_urbrack.gif)          |
121 | 100, 120 | eqtrd 2132 |
. . . . . . . . . . . . . . . 16
   
 
                                     ![]_ ]_](_urbrack.gif) 
        |
122 | | eqeq12 2112 |
. . . . . . . . . . . . . . . 16
       
            ![]_ ]_](_urbrack.gif) 
       
                  ![]_ ]_](_urbrack.gif)           |
123 | 121, 122 | syl5ibrcom 156 |
. . . . . . . . . . . . . . 15
   
 
                          
            ![]_ ]_](_urbrack.gif)            |
124 | 90, 123 | sylbid 149 |
. . . . . . . . . . . . . 14
   
 
                          
     ♯         ![]_ ]_](_urbrack.gif) 
          |
125 | 124 | expimpd 358 |
. . . . . . . . . . . . 13
 
                             
     ♯         ![]_ ]_](_urbrack.gif)         
   |
126 | 73, 125 | syl5bi 151 |
. . . . . . . . . . . 12
 
                                   ♯         ![]_ ]_](_urbrack.gif)         
   |
127 | 126 | exlimdvv 1836 |
. . . . . . . . . . 11
 
                                       ♯         ![]_ ]_](_urbrack.gif)         
   |
128 | 72, 127 | syl5bir 152 |
. . . . . . . . . 10
 
                                       ♯         ![]_ ]_](_urbrack.gif)         
   |
129 | 128 | rexlimdvva 2516 |
. . . . . . . . 9
                                       ♯         ![]_ ]_](_urbrack.gif)         
   |
130 | 71, 129 | syl5bir 152 |
. . . . . . . 8
              
       
                ♯         ![]_ ]_](_urbrack.gif)         
   |
131 | 130 | expdimp 257 |
. . . . . . 7
 
           
                    
     ♯         ![]_ ]_](_urbrack.gif) 
          |
132 | 70, 131 | syl5bi 151 |
. . . . . 6
 
           
                    
          |
133 | 44, 132 | jaod 678 |
. . . . 5
 
           
                     DECID                            |
134 | 40, 133 | jaodan 752 |
. . . 4
 
 
    
     DECID
                        
  

    
    DECID                
       
   |
135 | 134 | expimpd 358 |
. . 3
         
     DECID
                                    DECID                         
   |
136 | 135 | alrimivv 1814 |
. 2
             
     DECID
                                    DECID                         
   |
137 | | breq2 3879 |
. . . . . 6
   
      |
138 | 137 | 3anbi3d 1264 |
. . . . 5
            DECID               DECID        |
139 | 138 | rexbidv 2397 |
. . . 4
  

    
    DECID     

    
    DECID        |
140 | | eqeq1 2106 |
. . . . . . 7
                 |
141 | 140 | anbi2d 455 |
. . . . . 6
                 
                   |
142 | 141 | exbidv 1764 |
. . . . 5
                   
                     |
143 | 142 | rexbidv 2397 |
. . . 4
  
                 
           
          |
144 | 139, 143 | orbi12d 748 |
. . 3
              DECID                                     DECID                            |
145 | 144 | mo4 2021 |
. 2
               DECID                                           DECID                                     DECID                         
   |
146 | 136, 145 | sylibr 133 |
1
         
     DECID
                          |