Step | Hyp | Ref
| Expression |
1 | | 3simpb 986 |
. . . . . . 7
 
    
                    
      |
2 | 1 | reximi 2929 |
. . . . . 6
      
                  
          |
3 | | 3simpb 986 |
. . . . . . 7
 
    
                    
      |
4 | 3 | reximi 2929 |
. . . . . 6
      
                  
          |
5 | | fveq2 5800 |
. . . . . . . . . . . 12
           |
6 | 5 | sseq2d 3493 |
. . . . . . . . . . 11
     
       |
7 | | seqeq1 11927 |
. . . . . . . . . . . 12
         |
8 | 7 | breq1d 4411 |
. . . . . . . . . . 11
   
      |
9 | 6, 8 | anbi12d 710 |
. . . . . . . . . 10
                       |
10 | 9 | cbvrexv 3054 |
. . . . . . . . 9
      
   
            |
11 | 10 | anbi2i 694 |
. . . . . . . 8
   
                                           |
12 | | reeanv 2994 |
. . . . . . . 8
  
                                            |
13 | 11, 12 | bitr4i 252 |
. . . . . . 7
   
                                           |
14 | | simprlr 762 |
. . . . . . . . . . . . 13
         
    
               |
15 | 14 | adantl 466 |
. . . . . . . . . . . 12
 
 
                            |
16 | | prodmo.1 |
. . . . . . . . . . . . 13
        |
17 | | prodmo.2 |
. . . . . . . . . . . . . 14
 
   |
18 | 17 | adantlr 714 |
. . . . . . . . . . . . 13
           
    
          
   |
19 | | simprll 761 |
. . . . . . . . . . . . 13
 
 
                      
  |
20 | | simprlr 762 |
. . . . . . . . . . . . 13
 
 
                      
  |
21 | | simprll 761 |
. . . . . . . . . . . . . 14
         
    
                |
22 | 21 | adantl 466 |
. . . . . . . . . . . . 13
 
 
                             |
23 | | simprrl 763 |
. . . . . . . . . . . . . 14
         
    
                |
24 | 23 | adantl 466 |
. . . . . . . . . . . . 13
 
 
                             |
25 | 16, 18, 19, 20, 22, 24 | prodrb 27590 |
. . . . . . . . . . . 12
 
 
                         
      |
26 | 15, 25 | mpbid 210 |
. . . . . . . . . . 11
 
 
                            |
27 | | simprrr 764 |
. . . . . . . . . . . 12
         
    
               |
28 | 27 | adantl 466 |
. . . . . . . . . . 11
 
 
                            |
29 | | climuni 13149 |
. . . . . . . . . . 11
          |
30 | 26, 28, 29 | syl2anc 661 |
. . . . . . . . . 10
 
 
                      
  |
31 | 30 | expcom 435 |
. . . . . . . . 9
         
    
              |
32 | 31 | ex 434 |
. . . . . . . 8
 
       
    
        
     |
33 | 32 | rexlimivv 2952 |
. . . . . . 7
  
                   
    |
34 | 13, 33 | sylbi 195 |
. . . . . 6
   
                  
    |
35 | 2, 4, 34 | syl2an 477 |
. . . . 5
   
    
                
    
                 
    |
36 | | prodmo.3 |
. . . . . . . . . 10
       ![]_ ]_](_urbrack.gif)   |
37 | 16, 17, 36 | prodmolem2 27593 |
. . . . . . . . 9
 
                       
 
                     |
38 | | equcomi 1733 |
. . . . . . . . 9
   |
39 | 37, 38 | syl6 33 |
. . . . . . . 8
 
                       
 
                 
   |
40 | 39 | expimpd 603 |
. . . . . . 7
                                     
       
   |
41 | 40 | com12 31 |
. . . . . 6
   
    
                
                       |
42 | 41 | ancoms 453 |
. . . . 5
                          
                 
    |
43 | 16, 17, 36 | prodmolem2 27593 |
. . . . . . 7
 
                       
 
                 
   |
44 | 43 | expimpd 603 |
. . . . . 6
                                     
       
   |
45 | 44 | com12 31 |
. . . . 5
   
    
                
                       |
46 | | reeanv 2994 |
. . . . . . . 8
  
                                       ![]_ ]_](_urbrack.gif)                    
       
                    ![]_ ]_](_urbrack.gif)          |
47 | | eeanv 1944 |
. . . . . . . . 9
                                        ![]_ ]_](_urbrack.gif)                   
                           ![]_ ]_](_urbrack.gif)          |
48 | 47 | 2rexbii 2863 |
. . . . . . . 8
  
                                       ![]_ ]_](_urbrack.gif)        
                                        ![]_ ]_](_urbrack.gif)          |
49 | | oveq2 6209 |
. . . . . . . . . . . . . 14
           |
50 | | f1oeq2 5742 |
. . . . . . . . . . . . . 14
                 
           |
51 | 49, 50 | syl 16 |
. . . . . . . . . . . . 13
         
           |
52 | | fveq2 5800 |
. . . . . . . . . . . . . 14
               |
53 | 52 | eqeq2d 2468 |
. . . . . . . . . . . . 13
                 |
54 | 51, 53 | anbi12d 710 |
. . . . . . . . . . . 12
                 
                   |
55 | 54 | exbidv 1681 |
. . . . . . . . . . 11
                   
                     |
56 | | f1oeq1 5741 |
. . . . . . . . . . . . 13
         
           |
57 | | fveq1 5799 |
. . . . . . . . . . . . . . . . . . 19
           |
58 | 57 | csbeq1d 3403 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
59 | 58 | mpteq2dv 4488 |
. . . . . . . . . . . . . . . . 17
        ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)    |
60 | 36, 59 | syl5eq 2507 |
. . . . . . . . . . . . . . . 16
        ![]_ ]_](_urbrack.gif)    |
61 | 60 | seqeq3d 11932 |
. . . . . . . . . . . . . . 15
             ![]_ ]_](_urbrack.gif)     |
62 | 61 | fveq1d 5802 |
. . . . . . . . . . . . . 14
                ![]_ ]_](_urbrack.gif)        |
63 | 62 | eqeq2d 2468 |
. . . . . . . . . . . . 13
                 ![]_ ]_](_urbrack.gif)         |
64 | 56, 63 | anbi12d 710 |
. . . . . . . . . . . 12
                 
                  ![]_ ]_](_urbrack.gif)          |
65 | 64 | cbvexv 1984 |
. . . . . . . . . . 11
                  
                    ![]_ ]_](_urbrack.gif)         |
66 | 55, 65 | syl6bb 261 |
. . . . . . . . . 10
                   
                    ![]_ ]_](_urbrack.gif)          |
67 | 66 | cbvrexv 3054 |
. . . . . . . . 9
                   
           
         ![]_ ]_](_urbrack.gif)         |
68 | 67 | anbi2i 694 |
. . . . . . . 8
                                                     
       
                    ![]_ ]_](_urbrack.gif)          |
69 | 46, 48, 68 | 3bitr4i 277 |
. . . . . . 7
  
                                       ![]_ ]_](_urbrack.gif)                    
       
                     |
70 | | an4 820 |
. . . . . . . . . 10
                                    ![]_ ]_](_urbrack.gif)                                 
         ![]_ ]_](_urbrack.gif)          |
71 | | simpll 753 |
. . . . . . . . . . . . . 14
   
 
                     |
72 | 71, 17 | sylan 471 |
. . . . . . . . . . . . 13
    
                    
   |
73 | | fveq2 5800 |
. . . . . . . . . . . . . . . 16
           |
74 | 73 | csbeq1d 3403 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
75 | 74 | cbvmptv 4492 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
76 | 36, 75 | eqtri 2483 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)   |
77 | | fveq2 5800 |
. . . . . . . . . . . . . . 15
           |
78 | 77 | csbeq1d 3403 |
. . . . . . . . . . . . . 14
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
79 | 78 | cbvmptv 4492 |
. . . . . . . . . . . . 13
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
80 | | simplr 754 |
. . . . . . . . . . . . 13
   
 
                       |
81 | | simprl 755 |
. . . . . . . . . . . . 13
   
 
                             |
82 | | simprr 756 |
. . . . . . . . . . . . 13
   
 
                             |
83 | 16, 72, 76, 79, 80, 81, 82 | prodmolem3 27591 |
. . . . . . . . . . . 12
   
 
                                  ![]_ ]_](_urbrack.gif)        |
84 | | eqeq12 2473 |
. . . . . . . . . . . 12
       
         ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)         |
85 | 83, 84 | syl5ibrcom 222 |
. . . . . . . . . . 11
   
 
                          
         ![]_ ]_](_urbrack.gif)      
   |
86 | 85 | expimpd 603 |
. . . . . . . . . 10
 
                             
         ![]_ ]_](_urbrack.gif)           |
87 | 70, 86 | syl5bi 217 |
. . . . . . . . 9
 
                                       ![]_ ]_](_urbrack.gif)           |
88 | 87 | exlimdvv 1692 |
. . . . . . . 8
 
                                           ![]_ ]_](_urbrack.gif)           |
89 | 88 | rexlimdvva 2954 |
. . . . . . 7
                                           ![]_ ]_](_urbrack.gif)           |
90 | 69, 89 | syl5bir 218 |
. . . . . 6
              
       
                      |
91 | 90 | com12 31 |
. . . . 5
                                             |
92 | 35, 42, 45, 91 | ccase 937 |
. . . 4
                                     
          
    
                
                   
    |
93 | 92 | com12 31 |
. . 3
         
                            
          
    
                
                   
   |
94 | 93 | alrimivv 1687 |
. 2
             
                            
          
    
                
                   
   |
95 | | breq2 4405 |
. . . . . 6
   
      |
96 | 95 | 3anbi3d 1296 |
. . . . 5
                       
                         |
97 | 96 | rexbidv 2868 |
. . . 4
  

    
               
                          |
98 | | eqeq1 2458 |
. . . . . . 7
                 |
99 | 98 | anbi2d 703 |
. . . . . 6
                 
                   |
100 | 99 | exbidv 1681 |
. . . . 5
                   
                     |
101 | 100 | rexbidv 2868 |
. . . 4
  
                 
           
          |
102 | 97, 101 | orbi12d 709 |
. . 3
                                     
       
 
    
                            
           |
103 | 102 | mo4 2326 |
. 2
                                      
       
        
    
                
                                                      
            |
104 | 94, 103 | sylibr 212 |
1
         
                            
          |