Step | Hyp | Ref
| Expression |
1 | | fprodss.1 |
. . 3

  |
2 | | sseq2 3440 |
. . . . 5


   |
3 | | ss0 3768 |
. . . . 5

  |
4 | 2, 3 | syl6bi 236 |
. . . 4

    |
5 | | prodeq1 14040 |
. . . . . 6


   |
6 | | prodeq1 14040 |
. . . . . . 7


   |
7 | 6 | eqcomd 2477 |
. . . . . 6

    |
8 | 5, 7 | sylan9eq 2525 |
. . . . 5
    
  |
9 | 8 | expcom 442 |
. . . 4



    |
10 | 4, 9 | syld 44 |
. . 3

  
   |
11 | 1, 10 | syl5com 30 |
. 2
  
    |
12 | | cnvimass 5194 |
. . . . . . . . 9
    
 |
13 | | simprr 774 |
. . . . . . . . . . 11
 
                                 |
14 | | f1of 5828 |
. . . . . . . . . . 11
            
              |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
 
                                 |
16 | | fdm 5745 |
. . . . . . . . . 10
            
          |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
 
                  
          |
18 | 12, 17 | syl5sseq 3466 |
. . . . . . . 8
 
                       
          |
19 | | f1ofn 5829 |
. . . . . . . . . . . . 13
            
          |
20 | 13, 19 | syl 17 |
. . . . . . . . . . . 12
 
                             |
21 | | elpreima 6017 |
. . . . . . . . . . . 12
                                |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
 
                                          |
23 | 15 | ffvelrnda 6037 |
. . . . . . . . . . . . 13
                     
               |
24 | 23 | ex 441 |
. . . . . . . . . . . 12
 
                                   |
25 | 24 | adantrd 475 |
. . . . . . . . . . 11
 
                                         |
26 | 22, 25 | sylbid 223 |
. . . . . . . . . 10
 
                                |
27 | 26 | imp 436 |
. . . . . . . . 9
                     
            |
28 | | fprodss.2 |
. . . . . . . . . . . . . . 15
 
   |
29 | 28 | ex 441 |
. . . . . . . . . . . . . 14
     |
30 | 29 | adantr 472 |
. . . . . . . . . . . . 13
 
 
   |
31 | | eldif 3400 |
. . . . . . . . . . . . . . 15
  

   |
32 | | fprodss.3 |
. . . . . . . . . . . . . . . 16
 

 
  |
33 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . 16
 |
34 | 32, 33 | syl6eqel 2557 |
. . . . . . . . . . . . . . 15
 

 
  |
35 | 31, 34 | sylan2br 484 |
. . . . . . . . . . . . . 14
 

 
  |
36 | 35 | expr 626 |
. . . . . . . . . . . . 13
 
 
   |
37 | 30, 36 | pm2.61d 163 |
. . . . . . . . . . . 12
 
   |
38 | 37 | adantlr 729 |
. . . . . . . . . . 11
                     
   |
39 | | eqid 2471 |
. . . . . . . . . . 11
     |
40 | 38, 39 | fmptd 6061 |
. . . . . . . . . 10
 
                           |
41 | 40 | ffvelrnda 6037 |
. . . . . . . . 9
                                       |
42 | 27, 41 | syldan 478 |
. . . . . . . 8
                     
                  |
43 | | eqid 2471 |
. . . . . . . . 9
         |
44 | | simprl 772 |
. . . . . . . . . 10
 
                         |
45 | | nnuz 11218 |
. . . . . . . . . 10
     |
46 | 44, 45 | syl6eleq 2559 |
. . . . . . . . 9
 
                             |
47 | | ssid 3437 |
. . . . . . . . . 10
                 |
48 | 47 | a1i 11 |
. . . . . . . . 9
 
                                     |
49 | 43, 46, 48 | fprodntriv 14073 |
. . . . . . . 8
 
                                                               |
50 | | eldifi 3544 |
. . . . . . . . . . . 12
                          |
51 | 50, 23 | sylan2 482 |
. . . . . . . . . . 11
                     
                      |
52 | | eldifn 3545 |
. . . . . . . . . . . . 13
               
       |
53 | 52 | adantl 473 |
. . . . . . . . . . . 12
                     
               
       |
54 | 22 | adantr 472 |
. . . . . . . . . . . . 13
                     
                                       |
55 | 50 | adantl 473 |
. . . . . . . . . . . . . 14
                     
               
          |
56 | 55 | biantrurd 516 |
. . . . . . . . . . . . 13
                     
                                      |
57 | 54, 56 | bitr4d 264 |
. . . . . . . . . . . 12
                     
                             |
58 | 53, 57 | mtbid 307 |
. . . . . . . . . . 11
                     
                      |
59 | 51, 58 | eldifd 3401 |
. . . . . . . . . 10
                     
                        |
60 | | difss 3549 |
. . . . . . . . . . . . 13
   |
61 | | resmpt 5160 |
. . . . . . . . . . . . 13
               |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . 12
  
        |
63 | 62 | fveq1i 5880 |
. . . . . . . . . . 11
                           |
64 | | fvres 5893 |
. . . . . . . . . . 11
           
                     |
65 | 63, 64 | syl5eqr 2519 |
. . . . . . . . . 10
                               |
66 | 59, 65 | syl 17 |
. . . . . . . . 9
                     
                                        |
67 | | 1ex 9656 |
. . . . . . . . . . . . . . 15
 |
68 | 67 | elsnc2 3991 |
. . . . . . . . . . . . . 14
     |
69 | 32, 68 | sylibr 217 |
. . . . . . . . . . . . 13
 

 
    |
70 | | eqid 2471 |
. . . . . . . . . . . . 13
         |
71 | 69, 70 | fmptd 6061 |
. . . . . . . . . . . 12
               |
72 | 71 | ad2antrr 740 |
. . . . . . . . . . 11
                     
                              |
73 | 72, 59 | ffvelrnd 6038 |
. . . . . . . . . 10
                     
                                |
74 | | elsni 3985 |
. . . . . . . . . 10
              
              |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
                     
                              |
76 | 66, 75 | eqtr3d 2507 |
. . . . . . . 8
                     
                            |
77 | | fzssuz 11865 |
. . . . . . . . 9
             |
78 | 77 | a1i 11 |
. . . . . . . 8
 
                                 |
79 | 18, 42, 49, 76, 78 | prodss 14078 |
. . . . . . 7
 
                                                          |
80 | 1 | adantr 472 |
. . . . . . . . . . . 12
 
                     |
81 | 80 | resmptd 5162 |
. . . . . . . . . . 11
 
                           |
82 | 81 | fveq1d 5881 |
. . . . . . . . . 10
 
                                   |
83 | | fvres 5893 |
. . . . . . . . . 10
                 |
84 | 82, 83 | sylan9req 2526 |
. . . . . . . . 9
                     
               |
85 | 84 | prodeq2dv 14054 |
. . . . . . . 8
 
                                   |
86 | | fveq2 5879 |
. . . . . . . . 9
                       |
87 | | fzfid 12224 |
. . . . . . . . . 10
 
                             |
88 | 87, 15 | fisuppfi 7909 |
. . . . . . . . 9
 
                          |
89 | | f1of1 5827 |
. . . . . . . . . . . 12
            
              |
90 | 13, 89 | syl 17 |
. . . . . . . . . . 11
 
                                 |
91 | | f1ores 5842 |
. . . . . . . . . . 11
                  
                                    |
92 | 90, 18, 91 | syl2anc 673 |
. . . . . . . . . 10
 
                                              |
93 | | f1ofo 5835 |
. . . . . . . . . . . . 13
            
              |
94 | 13, 93 | syl 17 |
. . . . . . . . . . . 12
 
                                 |
95 | | foimacnv 5845 |
. . . . . . . . . . . 12
                          |
96 | 94, 80, 95 | syl2anc 673 |
. . . . . . . . . . 11
 
                              |
97 | | f1oeq3 5820 |
. . . . . . . . . . 11
                                   
                   |
98 | 96, 97 | syl 17 |
. . . . . . . . . 10
 
                                            
                   |
99 | 92, 98 | mpbid 215 |
. . . . . . . . 9
 
                                     |
100 | | fvres 5893 |
. . . . . . . . . 10
                       |
101 | 100 | adantl 473 |
. . . . . . . . 9
                     
                       |
102 | 80 | sselda 3418 |
. . . . . . . . . 10
                     
   |
103 | 40 | ffvelrnda 6037 |
. . . . . . . . . 10
                     
         |
104 | 102, 103 | syldan 478 |
. . . . . . . . 9
                     
         |
105 | 86, 88, 99, 101, 104 | fprodf1o 14077 |
. . . . . . . 8
 
                                             |
106 | 85, 105 | eqtrd 2505 |
. . . . . . 7
 
                                             |
107 | | eqidd 2472 |
. . . . . . . 8
                     
                   |
108 | 86, 87, 13, 107, 103 | fprodf1o 14077 |
. . . . . . 7
 
                                                |
109 | 79, 106, 108 | 3eqtr4d 2515 |
. . . . . 6
 
                                   |
110 | | prodfc 14076 |
. . . . . 6

        |
111 | | prodfc 14076 |
. . . . . 6

        |
112 | 109, 110,
111 | 3eqtr3g 2528 |
. . . . 5
 
                    
  |
113 | 112 | expr 626 |
. . . 4
 
                  
    |
114 | 113 | exlimdv 1787 |
. . 3
 
                  
     |
115 | 114 | expimpd 614 |
. 2
                    
     |
116 | | fprodss.4 |
. . 3
   |
117 | | fz1f1o 13853 |
. . 3
 
                      |
118 | 116, 117 | syl 17 |
. 2
                        |
119 | 11, 115, 118 | mpjaod 388 |
1
 
   |