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

  |
2 | | sseq2 3179 |
. . . . 5


   |
3 | | ss0 3463 |
. . . . 5

  |
4 | 2, 3 | syl6bi 163 |
. . . 4

    |
5 | | prodeq1 11545 |
. . . . . 6


   |
6 | | prodeq1 11545 |
. . . . . . 7


   |
7 | 6 | eqcomd 2183 |
. . . . . 6

    |
8 | 5, 7 | sylan9eq 2230 |
. . . . 5
    
  |
9 | 8 | expcom 116 |
. . . 4



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

  
   |
11 | 1, 10 | syl5com 29 |
. 2
  
    |
12 | | cnvimass 4987 |
. . . . . . . . 9
    
 |
13 | | simprr 531 |
. . . . . . . . . 10
 
 ♯       ♯            ♯       |
14 | | f1of 5457 |
. . . . . . . . . 10
      ♯          ♯       |
15 | 13, 14 | syl 14 |
. . . . . . . . 9
 
 ♯       ♯            ♯       |
16 | 12, 15 | fssdm 5376 |
. . . . . . . 8
 
 ♯       ♯               ♯     |
17 | | f1ofn 5458 |
. . . . . . . . . . . 12
      ♯        ♯     |
18 | | elpreima 5631 |
. . . . . . . . . . . 12
    ♯  
     
    ♯           |
19 | 13, 17, 18 | 3syl 17 |
. . . . . . . . . . 11
 
 ♯       ♯                 ♯           |
20 | 15 | ffvelcdmda 5647 |
. . . . . . . . . . . . 13
    ♯       ♯          ♯          |
21 | 20 | ex 115 |
. . . . . . . . . . . 12
 
 ♯       ♯           ♯          |
22 | 21 | adantrd 279 |
. . . . . . . . . . 11
 
 ♯       ♯            ♯               |
23 | 19, 22 | sylbid 150 |
. . . . . . . . . 10
 
 ♯       ♯            
       |
24 | 23 | imp 124 |
. . . . . . . . 9
    ♯       ♯                   |
25 | | fprodss.2 |
. . . . . . . . . . . . . . 15
 
   |
26 | 25 | ex 115 |
. . . . . . . . . . . . . 14
     |
27 | 26 | adantr 276 |
. . . . . . . . . . . . 13
 
 
   |
28 | | eldif 3138 |
. . . . . . . . . . . . . . 15
  

   |
29 | | fprodss.3 |
. . . . . . . . . . . . . . . 16
 

 
  |
30 | | ax-1cn 7895 |
. . . . . . . . . . . . . . . 16
 |
31 | 29, 30 | eqeltrdi 2268 |
. . . . . . . . . . . . . . 15
 

 
  |
32 | 28, 31 | sylan2br 288 |
. . . . . . . . . . . . . 14
 

 
  |
33 | 32 | expr 375 |
. . . . . . . . . . . . 13
 
 
   |
34 | | eleq1 2240 |
. . . . . . . . . . . . . . . 16
 
   |
35 | 34 | dcbid 838 |
. . . . . . . . . . . . . . 15
 DECID
DECID
   |
36 | | fprodssdc.a |
. . . . . . . . . . . . . . . 16
  DECID   |
37 | 36 | adantr 276 |
. . . . . . . . . . . . . . 15
 
 
DECID
  |
38 | | simpr 110 |
. . . . . . . . . . . . . . 15
 
   |
39 | 35, 37, 38 | rspcdva 2846 |
. . . . . . . . . . . . . 14
 

DECID
  |
40 | | exmiddc 836 |
. . . . . . . . . . . . . 14
DECID

   |
41 | 39, 40 | syl 14 |
. . . . . . . . . . . . 13
 
 
   |
42 | 27, 33, 41 | mpjaod 718 |
. . . . . . . . . . . 12
 
   |
43 | 42 | adantlr 477 |
. . . . . . . . . . 11
    ♯       ♯          |
44 | 43 | fmpttd 5667 |
. . . . . . . . . 10
 
 ♯       ♯               |
45 | 44 | ffvelcdmda 5647 |
. . . . . . . . 9
    ♯       ♯                        |
46 | 24, 45 | syldan 282 |
. . . . . . . 8
    ♯       ♯                         |
47 | | eqid 2177 |
. . . . . . . . 9
         |
48 | | simprl 529 |
. . . . . . . . . 10
 
 ♯       ♯       ♯    |
49 | | nnuz 9552 |
. . . . . . . . . 10
     |
50 | 48, 49 | eleqtrdi 2270 |
. . . . . . . . 9
 
 ♯       ♯       ♯        |
51 | | ssidd 3176 |
. . . . . . . . 9
 
 ♯       ♯          ♯      ♯     |
52 | 47, 50, 51 | fprodntrivap 11576 |
. . . . . . . 8
 
 ♯       ♯       
        #             ♯                     |
53 | | eleq1 2240 |
. . . . . . . . . . . . 13
     
       |
54 | 53 | dcbid 838 |
. . . . . . . . . . . 12
     DECID
DECID        |
55 | 36 | ad3antrrr 492 |
. . . . . . . . . . . 12
     ♯       ♯           
   ♯     DECID   |
56 | 13 | ad2antrr 488 |
. . . . . . . . . . . . . 14
     ♯       ♯           
   ♯         ♯       |
57 | 56, 14 | syl 14 |
. . . . . . . . . . . . 13
     ♯       ♯           
   ♯         ♯       |
58 | | simpr 110 |
. . . . . . . . . . . . 13
     ♯       ♯           
   ♯       ♯     |
59 | 57, 58 | ffvelcdmd 5648 |
. . . . . . . . . . . 12
     ♯       ♯           
   ♯          |
60 | 54, 55, 59 | rspcdva 2846 |
. . . . . . . . . . 11
     ♯       ♯           
   ♯    DECID       |
61 | | f1ocnv 5470 |
. . . . . . . . . . . . . . 15
      ♯             ♯     |
62 | | f1of1 5456 |
. . . . . . . . . . . . . . 15
         ♯           ♯     |
63 | 56, 61, 62 | 3syl 17 |
. . . . . . . . . . . . . 14
     ♯       ♯           
   ♯            ♯     |
64 | 1 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
     ♯       ♯           
   ♯      |
65 | | f1elima 5768 |
. . . . . . . . . . . . . 14
          ♯      
                       |
66 | 63, 59, 64, 65 | syl3anc 1238 |
. . . . . . . . . . . . 13
     ♯       ♯           
   ♯                  
       |
67 | | f1ocnvfv1 5772 |
. . . . . . . . . . . . . . 15
       ♯        ♯               |
68 | 56, 58, 67 | syl2anc 411 |
. . . . . . . . . . . . . 14
     ♯       ♯           
   ♯               |
69 | 68 | eleq1d 2246 |
. . . . . . . . . . . . 13
     ♯       ♯           
   ♯                  
        |
70 | 66, 69 | bitr3d 190 |
. . . . . . . . . . . 12
     ♯       ♯           
   ♯        
        |
71 | 70 | dcbid 838 |
. . . . . . . . . . 11
     ♯       ♯           
   ♯    DECID    
DECID
        |
72 | 60, 71 | mpbid 147 |
. . . . . . . . . 10
     ♯       ♯           
   ♯    DECID        |
73 | 16 | ad2antrr 488 |
. . . . . . . . . . . . 13
     ♯       ♯           
   ♯            ♯     |
74 | | simpr 110 |
. . . . . . . . . . . . 13
     ♯       ♯           
   ♯   
   ♯     |
75 | 73, 74 | ssneldd 3158 |
. . . . . . . . . . . 12
     ♯       ♯           
   ♯   
       |
76 | 75 | olcd 734 |
. . . . . . . . . . 11
     ♯       ♯           
   ♯         
        |
77 | | df-dc 835 |
. . . . . . . . . . 11
DECID     
     
        |
78 | 76, 77 | sylibr 134 |
. . . . . . . . . 10
     ♯       ♯           
   ♯    DECID        |
79 | | eluzelz 9526 |
. . . . . . . . . . . . 13
    
  |
80 | 79 | adantl 277 |
. . . . . . . . . . . 12
    ♯       ♯           
  |
81 | | 1zzd 9269 |
. . . . . . . . . . . 12
    ♯       ♯           
  |
82 | 48 | adantr 276 |
. . . . . . . . . . . . 13
    ♯       ♯           
♯    |
83 | 82 | nnzd 9363 |
. . . . . . . . . . . 12
    ♯       ♯           
♯    |
84 | | fzdcel 10026 |
. . . . . . . . . . . 12
 
♯   DECID    ♯     |
85 | 80, 81, 83, 84 | syl3anc 1238 |
. . . . . . . . . . 11
    ♯       ♯           
DECID
   ♯     |
86 | | exmiddc 836 |
. . . . . . . . . . 11
DECID    ♯       ♯  
   ♯      |
87 | 85, 86 | syl 14 |
. . . . . . . . . 10
    ♯       ♯           
    ♯      ♯      |
88 | 72, 78, 87 | mpjaodan 798 |
. . . . . . . . 9
    ♯       ♯           
DECID
       |
89 | 88 | ralrimiva 2550 |
. . . . . . . 8
 
 ♯       ♯       
    DECID        |
90 | | 1zzd 9269 |
. . . . . . . 8
 
 ♯       ♯         |
91 | | eldifi 3257 |
. . . . . . . . . . . 12
     ♯            ♯     |
92 | 91, 20 | sylan2 286 |
. . . . . . . . . . 11
    ♯       ♯           ♯  
      
      |
93 | | eldifn 3258 |
. . . . . . . . . . . . 13
     ♯        
       |
94 | 93 | adantl 277 |
. . . . . . . . . . . 12
    ♯       ♯           ♯  
      
       |
95 | 91 | adantl 277 |
. . . . . . . . . . . . 13
    ♯       ♯           ♯  
      
   ♯     |
96 | 19 | adantr 276 |
. . . . . . . . . . . . 13
    ♯       ♯           ♯  
      
     
    ♯           |
97 | 95, 96 | mpbirand 441 |
. . . . . . . . . . . 12
    ♯       ♯           ♯  
      
     
       |
98 | 94, 97 | mtbid 672 |
. . . . . . . . . . 11
    ♯       ♯           ♯  
      
      |
99 | 92, 98 | eldifd 3139 |
. . . . . . . . . 10
    ♯       ♯           ♯  
      
        |
100 | | difss 3261 |
. . . . . . . . . . . . 13
   |
101 | | resmpt 4951 |
. . . . . . . . . . . . 13
               |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . 12
  
        |
103 | 102 | fveq1i 5512 |
. . . . . . . . . . 11
                           |
104 | | fvres 5535 |
. . . . . . . . . . 11
           
                     |
105 | 103, 104 | eqtr3id 2224 |
. . . . . . . . . 10
                               |
106 | 99, 105 | syl 14 |
. . . . . . . . 9
    ♯       ♯           ♯  
      
                        |
107 | | 1ex 7943 |
. . . . . . . . . . . . . . 15
 |
108 | 107 | elsn2 3625 |
. . . . . . . . . . . . . 14
     |
109 | 29, 108 | sylibr 134 |
. . . . . . . . . . . . 13
 

 
    |
110 | 109 | fmpttd 5667 |
. . . . . . . . . . . 12
               |
111 | 110 | ad2antrr 488 |
. . . . . . . . . . 11
    ♯       ♯           ♯  
      
              |
112 | 111, 99 | ffvelcdmd 5648 |
. . . . . . . . . 10
    ♯       ♯           ♯  
      
                |
113 | | elsni 3609 |
. . . . . . . . . 10
              
              |
114 | 112, 113 | syl 14 |
. . . . . . . . 9
    ♯       ♯           ♯  
      
              |
115 | 106, 114 | eqtr3d 2212 |
. . . . . . . 8
    ♯       ♯           ♯  
      
            |
116 | | fzssuz 10051 |
. . . . . . . . 9
   ♯        |
117 | 116 | a1i 9 |
. . . . . . . 8
 
 ♯       ♯          ♯         |
118 | 85 | ralrimiva 2550 |
. . . . . . . 8
 
 ♯       ♯       
    DECID    ♯     |
119 | 16, 46, 52, 89, 90, 115, 117, 118 | prodssdc 11581 |
. . . . . . 7
 
 ♯       ♯                            ♯                |
120 | 1 | adantr 276 |
. . . . . . . . . . . 12
 
 ♯       ♯         |
121 | 120 | resmptd 4954 |
. . . . . . . . . . 11
 
 ♯       ♯               |
122 | 121 | fveq1d 5513 |
. . . . . . . . . 10
 
 ♯       ♯                       |
123 | | fvres 5535 |
. . . . . . . . . 10
                 |
124 | 122, 123 | sylan9req 2231 |
. . . . . . . . 9
    ♯       ♯                      |
125 | 124 | prodeq2dv 11558 |
. . . . . . . 8
 
 ♯       ♯              
        |
126 | | fveq2 5511 |
. . . . . . . . 9
                       |
127 | | fprodss.4 |
. . . . . . . . . . . 12
   |
128 | 127 | adantr 276 |
. . . . . . . . . . 11
 
 ♯       ♯      
  |
129 | 36 | adantr 276 |
. . . . . . . . . . 11
 
 ♯       ♯       
DECID   |
130 | | ssfidc 6928 |
. . . . . . . . . . 11
  
DECID
   |
131 | 128, 120,
129, 130 | syl3anc 1238 |
. . . . . . . . . 10
 
 ♯       ♯      
  |
132 | 120, 13, 131 | preimaf1ofi 6944 |
. . . . . . . . 9
 
 ♯       ♯              |
133 | | f1of1 5456 |
. . . . . . . . . . . 12
      ♯          ♯       |
134 | 13, 133 | syl 14 |
. . . . . . . . . . 11
 
 ♯       ♯            ♯       |
135 | | f1ores 5472 |
. . . . . . . . . . 11
       ♯         
   ♯                               |
136 | 134, 16, 135 | syl2anc 411 |
. . . . . . . . . 10
 
 ♯       ♯                                  |
137 | | f1ofo 5464 |
. . . . . . . . . . . . 13
      ♯          ♯       |
138 | 13, 137 | syl 14 |
. . . . . . . . . . . 12
 
 ♯       ♯            ♯       |
139 | | foimacnv 5475 |
. . . . . . . . . . . 12
       ♯                 |
140 | 138, 120,
139 | syl2anc 411 |
. . . . . . . . . . 11
 
 ♯       ♯                  |
141 | 140 | f1oeq3d 5454 |
. . . . . . . . . 10
 
 ♯       ♯                                
                   |
142 | 136, 141 | mpbid 147 |
. . . . . . . . 9
 
 ♯       ♯                         |
143 | | fvres 5535 |
. . . . . . . . . 10
                       |
144 | 143 | adantl 277 |
. . . . . . . . 9
    ♯       ♯                              |
145 | 120 | sselda 3155 |
. . . . . . . . . 10
    ♯       ♯          |
146 | 44 | ffvelcdmda 5647 |
. . . . . . . . . 10
    ♯       ♯                |
147 | 145, 146 | syldan 282 |
. . . . . . . . 9
    ♯       ♯                |
148 | 126, 132,
142, 144, 147 | fprodf1o 11580 |
. . . . . . . 8
 
 ♯       ♯                                 |
149 | 125, 148 | eqtrd 2210 |
. . . . . . 7
 
 ♯       ♯                                 |
150 | 48 | nnzd 9363 |
. . . . . . . . 9
 
 ♯       ♯       ♯    |
151 | 90, 150 | fzfigd 10417 |
. . . . . . . 8
 
 ♯       ♯          ♯     |
152 | | eqidd 2178 |
. . . . . . . 8
    ♯       ♯          ♯              |
153 | 126, 151,
13, 152, 146 | fprodf1o 11580 |
. . . . . . 7
 
 ♯       ♯                  ♯                |
154 | 119, 149,
153 | 3eqtr4d 2220 |
. . . . . 6
 
 ♯       ♯              
        |
155 | 25 | ralrimiva 2550 |
. . . . . . . 8
 
  |
156 | 155 | adantr 276 |
. . . . . . 7
 
 ♯       ♯       
  |
157 | | prodfct 11579 |
. . . . . . 7
 
       
  |
158 | 156, 157 | syl 14 |
. . . . . 6
 
 ♯       ♯              
  |
159 | 43 | ralrimiva 2550 |
. . . . . . 7
 
 ♯       ♯       
  |
160 | | prodfct 11579 |
. . . . . . 7
 
       
  |
161 | 159, 160 | syl 14 |
. . . . . 6
 
 ♯       ♯              
  |
162 | 154, 158,
161 | 3eqtr3d 2218 |
. . . . 5
 
 ♯       ♯           |
163 | 162 | expr 375 |
. . . 4
 
♯         ♯          |
164 | 163 | exlimdv 1819 |
. . 3
 
♯          ♯    
     |
165 | 164 | expimpd 363 |
. 2
   ♯        ♯       
   |
166 | | fz1f1o 11367 |
. . 3
 
 ♯        ♯         |
167 | 127, 166 | syl 14 |
. 2
   ♯        ♯         |
168 | 11, 165, 167 | mpjaod 718 |
1
 
   |