Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . 4
            DECID            #         
      |
2 | | simplr 528 |
. . . 4
            DECID            #         
     DECID   |
3 | | simprr 531 |
. . . 4
            DECID            #         
     |
4 | 1, 2, 3 | 3jca 1177 |
. . 3
            DECID            #         
          DECID       |
5 | 4 | reximi 2574 |
. 2
             DECID            #         
           DECID       |
6 | | fveq2 5510 |
. . . . . 6
           |
7 | 6 | sseq2d 3185 |
. . . . 5
     
       |
8 | 6 | raleqdv 2678 |
. . . . 5
  
    DECID      DECID    |
9 | | seqeq1 10421 |
. . . . . 6
         |
10 | 9 | breq1d 4010 |
. . . . 5
   
      |
11 | 7, 8, 10 | 3anbi123d 1312 |
. . . 4
            DECID               DECID        |
12 | 11 | cbvrexvw 2708 |
. . 3
      
     DECID
   
           DECID       |
13 | | reeanv 2646 |
. . . . 5
  
           DECID               
       
 
    
     DECID
                          |
14 | | simprl3 1044 |
. . . . . . . . . . . 12
   
 
     
     DECID
                   |
15 | | simprl1 1042 |
. . . . . . . . . . . . . . 15
   
 
     
     DECID
                    |
16 | | uzssz 9523 |
. . . . . . . . . . . . . . 15
     |
17 | 15, 16 | sstrdi 3167 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
                |
18 | | 1zzd 9256 |
. . . . . . . . . . . . . . . 16
   
 
     
     DECID
                |
19 | | simplrr 536 |
. . . . . . . . . . . . . . . . 17
   
 
     
     DECID
             
  |
20 | 19 | nnzd 9350 |
. . . . . . . . . . . . . . . 16
   
 
     
     DECID
             
  |
21 | 18, 20 | fzfigd 10404 |
. . . . . . . . . . . . . . 15
   
 
     
     DECID
                    |
22 | | simprr 531 |
. . . . . . . . . . . . . . . . 17
   
 
     
     DECID
                        |
23 | | f1oeng 6750 |
. . . . . . . . . . . . . . . . 17
                     |
24 | 21, 22, 23 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
   
 
     
     DECID
                 
  |
25 | 24 | ensymd 6776 |
. . . . . . . . . . . . . . 15
   
 
     
     DECID
                    |
26 | | enfii 6867 |
. . . . . . . . . . . . . . 15
          
  |
27 | 21, 25, 26 | syl2anc 411 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
             
  |
28 | | zfz1iso 10792 |
. . . . . . . . . . . . . 14
 
 
    ♯       |
29 | 17, 27, 28 | syl2anc 411 |
. . . . . . . . . . . . 13
   
 
     
     DECID
              
    ♯       |
30 | | prodmo.1 |
. . . . . . . . . . . . . . . 16
        |
31 | | prodmo.2 |
. . . . . . . . . . . . . . . . 17
 
   |
32 | 31 | ad4ant14 514 |
. . . . . . . . . . . . . . . 16
    
              DECID                  ♯      
   |
33 | | prodmodc.3 |
. . . . . . . . . . . . . . . 16
   ♯         ![]_ ]_](_urbrack.gif) 
   |
34 | | eqid 2177 |
. . . . . . . . . . . . . . . 16
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)     |
35 | | simpll2 1037 |
. . . . . . . . . . . . . . . . . 18
             DECID                  ♯      
    DECID   |
36 | 35 | adantl 277 |
. . . . . . . . . . . . . . . . 17
   
 
            DECID                  ♯       
    DECID   |
37 | | eleq1w 2238 |
. . . . . . . . . . . . . . . . . . 19
 
   |
38 | 37 | dcbid 838 |
. . . . . . . . . . . . . . . . . 18
 DECID
DECID
   |
39 | 38 | rspcv 2837 |
. . . . . . . . . . . . . . . . 17
    
 
    DECID DECID    |
40 | 36, 39 | mpan9 281 |
. . . . . . . . . . . . . . . 16
    
              DECID                  ♯      
     DECID   |
41 | | simplrr 536 |
. . . . . . . . . . . . . . . 16
   
 
            DECID                  ♯      
  |
42 | | simplrl 535 |
. . . . . . . . . . . . . . . 16
   
 
            DECID                  ♯      
  |
43 | 15 | adantrr 479 |
. . . . . . . . . . . . . . . 16
   
 
            DECID                  ♯             |
44 | | simprlr 538 |
. . . . . . . . . . . . . . . 16
   
 
            DECID                  ♯                 |
45 | | simprr 531 |
. . . . . . . . . . . . . . . 16
   
 
            DECID                  ♯      
    ♯       |
46 | 30, 32, 33, 34, 40, 41, 42, 43, 44, 45 | prodmodclem2a 11555 |
. . . . . . . . . . . . . . 15
   
 
            DECID                  ♯                  |
47 | 46 | expr 375 |
. . . . . . . . . . . . . 14
   
 
     
     DECID
                   ♯    
            |
48 | 47 | exlimdv 1819 |
. . . . . . . . . . . . 13
   
 
     
     DECID
                    ♯                 |
49 | 29, 48 | mpd 13 |
. . . . . . . . . . . 12
   
 
     
     DECID
                         |
50 | | climuni 11272 |
. . . . . . . . . . . 12
             
        |
51 | 14, 49, 50 | syl2anc 411 |
. . . . . . . . . . 11
   
 
     
     DECID
             
        |
52 | | eqeq2 2187 |
. . . . . . . . . . 11
                 |
53 | 51, 52 | syl5ibrcom 157 |
. . . . . . . . . 10
   
 
     
     DECID
                        |
54 | 53 | expr 375 |
. . . . . . . . 9
   
 
          DECID                     
    |
55 | 54 | impd 254 |
. . . . . . . 8
   
 
          DECID                          |
56 | 55 | exlimdv 1819 |
. . . . . . 7
   
 
          DECID                        
   |
57 | 56 | expimpd 363 |
. . . . . 6
 
         
     DECID
                          |
58 | 57 | rexlimdvva 2602 |
. . . . 5
         
     DECID
                          |
59 | 13, 58 | biimtrrid 153 |
. . . 4
              DECID                            |
60 | 59 | expdimp 259 |
. . 3
 
           DECID                  
          |
61 | 12, 60 | sylan2b 287 |
. 2
 
           DECID                  
          |
62 | 5, 61 | sylan2 286 |
1
 
      
     DECID   
        #            
                 
   |