Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . . . 8
            DECID            #         
      |
2 | | simplr 528 |
. . . . . . . 8
            DECID            #         
     DECID   |
3 | | simprr 531 |
. . . . . . . 8
            DECID            #         
     |
4 | 1, 2, 3 | 3jca 1177 |
. . . . . . 7
            DECID            #         
          DECID       |
5 | 4 | reximi 2574 |
. . . . . 6
             DECID            #         
           DECID       |
6 | | simpll 527 |
. . . . . . . 8
            DECID            #         
      |
7 | | simplr 528 |
. . . . . . . 8
            DECID            #         
     DECID   |
8 | | simprr 531 |
. . . . . . . 8
            DECID            #         
     |
9 | 6, 7, 8 | 3jca 1177 |
. . . . . . 7
            DECID            #         
          DECID       |
10 | 9 | reximi 2574 |
. . . . . 6
             DECID            #         
           DECID       |
11 | | fveq2 5515 |
. . . . . . . . . . . 12
           |
12 | 11 | sseq2d 3185 |
. . . . . . . . . . 11
     
       |
13 | 11 | raleqdv 2678 |
. . . . . . . . . . 11
  
    DECID      DECID    |
14 | | seqeq1 10447 |
. . . . . . . . . . . 12
         |
15 | 14 | breq1d 4013 |
. . . . . . . . . . 11
   
      |
16 | 12, 13, 15 | 3anbi123d 1312 |
. . . . . . . . . 10
            DECID               DECID        |
17 | 16 | cbvrexvw 2708 |
. . . . . . . . 9
      
     DECID
   
           DECID       |
18 | 17 | anbi2i 457 |
. . . . . . . 8
   
    
    DECID                DECID                  DECID          
     DECID
       |
19 | | reeanv 2646 |
. . . . . . . 8
  
           DECID               DECID                  DECID          
     DECID
       |
20 | 18, 19 | bitr4i 187 |
. . . . . . 7
   
    
    DECID                DECID      
            DECID               DECID        |
21 | | simprl3 1044 |
. . . . . . . . . . . . 13
         
     DECID
    
    
    DECID            |
22 | 21 | adantl 277 |
. . . . . . . . . . . 12
 
 
            DECID     
    
    DECID             |
23 | | prodmo.1 |
. . . . . . . . . . . . 13
        |
24 | | prodmo.2 |
. . . . . . . . . . . . . 14
 
   |
25 | 24 | adantlr 477 |
. . . . . . . . . . . . 13
           
     DECID
    
    
    DECID       
   |
26 | | simprll 537 |
. . . . . . . . . . . . 13
 
 
            DECID     
    
    DECID       
  |
27 | | simprlr 538 |
. . . . . . . . . . . . 13
 
 
            DECID     
    
    DECID       
  |
28 | | simprl1 1042 |
. . . . . . . . . . . . . 14
         
     DECID
    
    
    DECID             |
29 | 28 | adantl 277 |
. . . . . . . . . . . . 13
 
 
            DECID     
    
    DECID              |
30 | | simprr1 1045 |
. . . . . . . . . . . . . 14
         
     DECID
    
    
    DECID             |
31 | 30 | adantl 277 |
. . . . . . . . . . . . 13
 
 
            DECID     
    
    DECID              |
32 | | eleq1w 2238 |
. . . . . . . . . . . . . . 15
 
   |
33 | 32 | dcbid 838 |
. . . . . . . . . . . . . 14
 DECID
DECID
   |
34 | | simprl2 1043 |
. . . . . . . . . . . . . . 15
         
     DECID
    
    
    DECID            DECID   |
35 | 34 | ad2antlr 489 |
. . . . . . . . . . . . . 14
           
     DECID
    
    
    DECID       
     
    DECID   |
36 | | simpr 110 |
. . . . . . . . . . . . . 14
           
     DECID
    
    
    DECID       
           |
37 | 33, 35, 36 | rspcdva 2846 |
. . . . . . . . . . . . 13
           
     DECID
    
    
    DECID       
     DECID   |
38 | | simprr2 1046 |
. . . . . . . . . . . . . . 15
         
     DECID
    
    
    DECID            DECID   |
39 | 38 | ad2antlr 489 |
. . . . . . . . . . . . . 14
           
     DECID
    
    
    DECID       
     
    DECID   |
40 | | simpr 110 |
. . . . . . . . . . . . . 14
           
     DECID
    
    
    DECID       
           |
41 | 33, 39, 40 | rspcdva 2846 |
. . . . . . . . . . . . 13
           
     DECID
    
    
    DECID       
     DECID   |
42 | 23, 25, 26, 27, 29, 31, 37, 41 | prodrbdc 11581 |
. . . . . . . . . . . 12
 
 
            DECID     
    
    DECID          
      |
43 | 22, 42 | mpbid 147 |
. . . . . . . . . . 11
 
 
            DECID     
    
    DECID             |
44 | | simprr3 1047 |
. . . . . . . . . . . 12
         
     DECID
    
    
    DECID            |
45 | 44 | adantl 277 |
. . . . . . . . . . 11
 
 
            DECID     
    
    DECID             |
46 | | climuni 11300 |
. . . . . . . . . . 11
          |
47 | 43, 45, 46 | syl2anc 411 |
. . . . . . . . . 10
 
 
            DECID     
    
    DECID       
  |
48 | 47 | expcom 116 |
. . . . . . . . 9
         
     DECID
    
    
    DECID           |
49 | 48 | ex 115 |
. . . . . . . 8
 
       
     DECID
    
    
    DECID     
     |
50 | 49 | rexlimivv 2600 |
. . . . . . 7
  
           DECID               DECID          |
51 | 20, 50 | sylbi 121 |
. . . . . 6
   
    
    DECID                DECID          |
52 | 5, 10, 51 | syl2an 289 |
. . . . 5
              DECID   
        #                
     DECID   
        #               |
53 | | prodmodc.3 |
. . . . . . . . . 10
   ♯         ![]_ ]_](_urbrack.gif) 
   |
54 | 23, 24, 53 | prodmodclem2 11584 |
. . . . . . . . 9
 
      
     DECID   
        #            
                     |
55 | | equcomi 1704 |
. . . . . . . . 9
   |
56 | 54, 55 | syl6 33 |
. . . . . . . 8
 
      
     DECID   
        #            
                 
   |
57 | 56 | expimpd 363 |
. . . . . . 7
         
     DECID   
        #                     
       
   |
58 | 57 | com12 30 |
. . . . . 6
              DECID   
        #                     
        
   |
59 | 58 | ancoms 268 |
. . . . 5
                                 DECID            #               |
60 | 23, 24, 53 | prodmodclem2 11584 |
. . . . . . 7
 
      
     DECID   
        #            
                 
   |
61 | 60 | expimpd 363 |
. . . . . 6
         
     DECID   
        #                     
       
   |
62 | 61 | com12 30 |
. . . . 5
              DECID   
        #                     
        
   |
63 | | reeanv 2646 |
. . . . . . . 8
  
                                   ♯         ![]_ ]_](_urbrack.gif)         
 
                                   ♯         ![]_ ]_](_urbrack.gif)            |
64 | | exdistrv 1910 |
. . . . . . . . 9
                                    ♯         ![]_ ]_](_urbrack.gif)         
                                   ♯         ![]_ ]_](_urbrack.gif)            |
65 | 64 | 2rexbii 2486 |
. . . . . . . 8
  
                                   ♯         ![]_ ]_](_urbrack.gif)         
                                     ♯         ![]_ ]_](_urbrack.gif)            |
66 | | oveq2 5882 |
. . . . . . . . . . . . . 14
           |
67 | 66 | f1oeq2d 5457 |
. . . . . . . . . . . . 13
         
           |
68 | | fveq2 5515 |
. . . . . . . . . . . . . 14
               |
69 | 68 | eqeq2d 2189 |
. . . . . . . . . . . . 13
                 |
70 | 67, 69 | anbi12d 473 |
. . . . . . . . . . . 12
                 
                   |
71 | 70 | exbidv 1825 |
. . . . . . . . . . 11
                   
                     |
72 | | f1oeq1 5449 |
. . . . . . . . . . . . 13
         
           |
73 | | fveq1 5514 |
. . . . . . . . . . . . . . . . . . . 20
           |
74 | 73 | csbeq1d 3064 |
. . . . . . . . . . . . . . . . . . 19
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
75 | 74 | ifeq1d 3551 |
. . . . . . . . . . . . . . . . . 18
   ♯         ![]_ ]_](_urbrack.gif) 
   ♯         ![]_ ]_](_urbrack.gif)     |
76 | 75 | mpteq2dv 4094 |
. . . . . . . . . . . . . . . . 17
    ♯         ![]_ ]_](_urbrack.gif) 
    
♯         ![]_ ]_](_urbrack.gif)      |
77 | 53, 76 | eqtrid 2222 |
. . . . . . . . . . . . . . . 16
    ♯         ![]_ ]_](_urbrack.gif)      |
78 | 77 | seqeq3d 10452 |
. . . . . . . . . . . . . . 15
         ♯         ![]_ ]_](_urbrack.gif) 
     |
79 | 78 | fveq1d 5517 |
. . . . . . . . . . . . . 14
            ♯         ![]_ ]_](_urbrack.gif) 
        |
80 | 79 | eqeq2d 2189 |
. . . . . . . . . . . . 13
             ♯         ![]_ ]_](_urbrack.gif)           |
81 | 72, 80 | anbi12d 473 |
. . . . . . . . . . . 12
                 
             
♯         ![]_ ]_](_urbrack.gif)            |
82 | 81 | cbvexvw 1920 |
. . . . . . . . . . 11
                  
                ♯         ![]_ ]_](_urbrack.gif)           |
83 | 71, 82 | bitrdi 196 |
. . . . . . . . . 10
                   
                ♯         ![]_ ]_](_urbrack.gif)            |
84 | 83 | cbvrexvw 2708 |
. . . . . . . . 9
                   
           
     ♯         ![]_ ]_](_urbrack.gif) 
         |
85 | 84 | anbi2i 457 |
. . . . . . . 8
                                                     
       
                ♯         ![]_ ]_](_urbrack.gif)            |
86 | 63, 65, 85 | 3bitr4i 212 |
. . . . . . 7
  
                                   ♯         ![]_ ]_](_urbrack.gif)         
 
                                        |
87 | | an4 586 |
. . . . . . . . . 10
                                ♯         ![]_ ]_](_urbrack.gif)         
                         
     ♯         ![]_ ]_](_urbrack.gif)            |
88 | 24 | ad4ant14 514 |
. . . . . . . . . . . . 13
    
                    
   |
89 | | breq1 4006 |
. . . . . . . . . . . . . . . 16
 
♯  ♯     |
90 | | fveq2 5515 |
. . . . . . . . . . . . . . . . 17
           |
91 | 90 | csbeq1d 3064 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
92 | 89, 91 | ifbieq1d 3556 |
. . . . . . . . . . . . . . 15
   ♯         ![]_ ]_](_urbrack.gif) 
   ♯         ![]_ ]_](_urbrack.gif)     |
93 | 92 | cbvmptv 4099 |
. . . . . . . . . . . . . 14
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)     |
94 | 53, 93 | eqtri 2198 |
. . . . . . . . . . . . 13
   ♯         ![]_ ]_](_urbrack.gif) 
   |
95 | | fveq2 5515 |
. . . . . . . . . . . . . . . 16
           |
96 | 95 | csbeq1d 3064 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
97 | 89, 96 | ifbieq1d 3556 |
. . . . . . . . . . . . . 14
   ♯         ![]_ ]_](_urbrack.gif) 
   ♯         ![]_ ]_](_urbrack.gif)     |
98 | 97 | cbvmptv 4099 |
. . . . . . . . . . . . 13
  
♯         ![]_ ]_](_urbrack.gif)       ♯         ![]_ ]_](_urbrack.gif)     |
99 | | simplr 528 |
. . . . . . . . . . . . 13
   
 
                       |
100 | | simprl 529 |
. . . . . . . . . . . . 13
   
 
                             |
101 | | simprr 531 |
. . . . . . . . . . . . 13
   
 
                             |
102 | 23, 88, 94, 98, 99, 100, 101 | prodmodclem3 11582 |
. . . . . . . . . . . 12
   
 
                              ♯         ![]_ ]_](_urbrack.gif)          |
103 | | eqeq12 2190 |
. . . . . . . . . . . 12
       
     ♯         ![]_ ]_](_urbrack.gif)         
           ♯         ![]_ ]_](_urbrack.gif) 
         |
104 | 102, 103 | syl5ibrcom 157 |
. . . . . . . . . . 11
   
 
                          
     ♯         ![]_ ]_](_urbrack.gif) 
          |
105 | 104 | expimpd 363 |
. . . . . . . . . 10
 
                             
     ♯         ![]_ ]_](_urbrack.gif)         
   |
106 | 87, 105 | biimtrid 152 |
. . . . . . . . 9
 
                                   ♯         ![]_ ]_](_urbrack.gif)         
   |
107 | 106 | exlimdvv 1897 |
. . . . . . . 8
 
                                       ♯         ![]_ ]_](_urbrack.gif)         
   |
108 | 107 | rexlimdvva 2602 |
. . . . . . 7
                                       ♯         ![]_ ]_](_urbrack.gif)         
   |
109 | 86, 108 | biimtrrid 153 |
. . . . . 6
              
       
                      |
110 | 109 | com12 30 |
. . . . 5
                                             |
111 | 52, 59, 62, 110 | ccase 964 |
. . . 4
         
     DECID   
        #                     
                     DECID   
        #                     
             |
112 | 111 | com12 30 |
. . 3
                DECID            #                     
                     DECID   
        #                     
            |
113 | 112 | alrimivv 1875 |
. 2
                    DECID            #                     
                     DECID   
        #                     
            |
114 | | breq2 4007 |
. . . . . . 7
   
      |
115 | 114 | anbi2d 464 |
. . . . . 6
            #                   #            |
116 | 115 | anbi2d 464 |
. . . . 5
             DECID   
        #               
     DECID   
        #             |
117 | 116 | rexbidv 2478 |
. . . 4
  
           DECID   
        #                      DECID   
        #             |
118 | | eqeq1 2184 |
. . . . . . 7
                 |
119 | 118 | anbi2d 464 |
. . . . . 6
                 
                   |
120 | 119 | exbidv 1825 |
. . . . 5
                   
                     |
121 | 120 | rexbidv 2478 |
. . . 4
  
                 
           
          |
122 | 117, 121 | orbi12d 793 |
. . 3
         
     DECID   
        #                     
       
 
           DECID            #                     
           |
123 | 122 | mo4 2087 |
. 2
          
     DECID   
        #                     
       
                   DECID   
        #                     
                     DECID   
        #                     
            |
124 | 113, 123 | sylibr 134 |
1
                DECID            #                     
          |