Step | Hyp | Ref
| Expression |
1 | | eqidd 2463 |
. . . . . . . . 9
 
    
                                |
2 | | 0zd 10978 |
. . . . . . . . . . . . 13
 
    
          |
3 | | dvnprodlem1.j |
. . . . . . . . . . . . . . 15
   |
4 | 3 | nn0zd 11067 |
. . . . . . . . . . . . . 14
   |
5 | 4 | adantr 471 |
. . . . . . . . . . . . 13
 
    
       
  |
6 | | fzssz 11830 |
. . . . . . . . . . . . . . . 16
     |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
 
    
           
  |
8 | | dvnprodlem1.c |
. . . . . . . . . . . . . . . . . . . . . . 23
          
        |
9 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
           
         |
10 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       |
11 | | rabeq 3050 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
      
         
            
     
       |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
            
     
       |
13 | | sumeq1 13804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                      |
14 | 13 | eqeq1d 2464 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
             |
15 | 14 | rabbidv 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
     
           
                 |
16 | 12, 15 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
            
                  |
17 | 16 | mpteq2dv 4504 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
        
      
                  |
18 | 17 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 

          
        
      
                  |
19 | | dvnprodlem1.rzt |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
20 | | dvnprodlem1.t |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
21 | | ssexg 4563 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
22 | 19, 20, 21 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
23 | | elpwg 3971 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
       |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
       |
25 | 19, 24 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
26 | | nn0ex 10904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
27 | 26 | mptex 6161 |
. . . . . . . . . . . . . . . . . . . . . . 23

      
                 |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                   |
29 | 9, 18, 25, 28 | fvmptd 5977 |
. . . . . . . . . . . . . . . . . . . . 21
    
          
                   |
30 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
31 | 30 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                 |
32 | | rabeq 3050 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                     
                                       |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                                       |
34 | | eqeq2 2473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                         |
35 | 34 | rabbidv 3048 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                                       |
36 | 33, 35 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                                       |
37 | 36 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
 
       
                                       |
38 | | ovex 6343 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
39 | 38 | rabex 4568 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
      
                  |
41 | 29, 37, 3, 40 | fvmptd 5977 |
. . . . . . . . . . . . . . . . . . . 20
     
                               |
42 | | ssrab2 3526 |
. . . . . . . . . . . . . . . . . . . . 21
      
                   
      |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
      
                    
       |
44 | 41, 43 | eqsstrd 3478 |
. . . . . . . . . . . . . . . . . . 19
     
           
       |
45 | 44 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
 
    
            
           
       |
46 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
 
    
                      |
47 | 45, 46 | sseldd 3445 |
. . . . . . . . . . . . . . . . 17
 
    
                    |
48 | | elmapi 7519 |
. . . . . . . . . . . . . . . . 17
      
                  |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
                      |
50 | | dvnprodlem1.z |
. . . . . . . . . . . . . . . . . . 19
   |
51 | | snidg 4006 |
. . . . . . . . . . . . . . . . . . 19
     |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
53 | | elun2 3614 |
. . . . . . . . . . . . . . . . . 18
         |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
55 | 54 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
    
       
      |
56 | 49, 55 | ffvelrnd 6046 |
. . . . . . . . . . . . . . 15
 
    
                  |
57 | 7, 56 | sseldd 3445 |
. . . . . . . . . . . . . 14
 
    
              |
58 | 5, 57 | zsubcld 11074 |
. . . . . . . . . . . . 13
 
    
                |
59 | 2, 5, 58 | 3jca 1194 |
. . . . . . . . . . . 12
 
    
         
        |
60 | | elfzle2 11832 |
. . . . . . . . . . . . . 14
               |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . 13
 
    
           
  |
62 | 5 | zred 11069 |
. . . . . . . . . . . . . 14
 
    
       
  |
63 | 57 | zred 11069 |
. . . . . . . . . . . . . 14
 
    
              |
64 | 62, 63 | subge0d 10231 |
. . . . . . . . . . . . 13
 
    
         
    
       |
65 | 61, 64 | mpbird 240 |
. . . . . . . . . . . 12
 
    
       
        |
66 | | elfzle1 11831 |
. . . . . . . . . . . . . 14
               |
67 | 56, 66 | syl 17 |
. . . . . . . . . . . . 13
 
    
       
      |
68 | 62, 63 | subge02d 10233 |
. . . . . . . . . . . . 13
 
    
                      |
69 | 67, 68 | mpbid 215 |
. . . . . . . . . . . 12
 
    
             
  |
70 | 59, 65, 69 | jca32 542 |
. . . . . . . . . . 11
 
    
                 
      
    
    |
71 | | elfz2 11820 |
. . . . . . . . . . 11
          
 

      
      
    
    |
72 | 70, 71 | sylibr 217 |
. . . . . . . . . 10
 
    
                    |
73 | | elmapfn 7520 |
. . . . . . . . . . . . . . . . . 18
      
          |
74 | 47, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
    
              |
75 | | ssun1 3609 |
. . . . . . . . . . . . . . . . . 18

    |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
    
              |
77 | | fnssres 5711 |
. . . . . . . . . . . . . . . . 17
     

        |
78 | 74, 76, 77 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
 
    
            |
79 | | nfv 1772 |
. . . . . . . . . . . . . . . . . 18
   |
80 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . 19
   |
81 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
82 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
83 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
84 | 83 | nfsum1 13805 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        |
85 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
86 | 84, 85 | nfeq 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        |
87 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
88 | 86, 87 | nfrab 2984 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
        |
89 | 82, 88 | nfmpt 4505 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
         |
90 | 81, 89 | nfmpt 4505 |
. . . . . . . . . . . . . . . . . . . . . 22
            
        |
91 | 8, 90 | nfcxfr 2601 |
. . . . . . . . . . . . . . . . . . . . 21
   |
92 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . 21
       |
93 | 91, 92 | nffv 5895 |
. . . . . . . . . . . . . . . . . . . 20
     
     |
94 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . 20
   |
95 | 93, 94 | nffv 5895 |
. . . . . . . . . . . . . . . . . . 19
      
        |
96 | 80, 95 | nfel 2615 |
. . . . . . . . . . . . . . . . . 18
              |
97 | 79, 96 | nfan 2022 |
. . . . . . . . . . . . . . . . 17
       
         |
98 | | fvres 5902 |
. . . . . . . . . . . . . . . . . . . 20
             |
99 | 98 | adantl 472 |
. . . . . . . . . . . . . . . . . . 19
       
       
             |
100 | 2 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
   |
101 | 58 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
         |
102 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
       
    
  |
103 | 49 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
       
               |
104 | 76 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
       
       |
105 | 103, 104 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
       
           |
106 | 102, 105 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
       |
107 | 100, 101,
106 | 3jca 1194 |
. . . . . . . . . . . . . . . . . . . . 21
       
       
               |
108 | | elfzle1 11831 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
109 | 105, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
       
       

      |
110 | 19 | unssad 3623 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
111 | | ssfi 7818 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
  |
112 | 20, 110, 111 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
113 | 112 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
       
   |
114 | | zssre 10973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
115 | 6, 114 | sstri 3453 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
       
    
  |
117 | 49 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
       
               |
118 | 76 | sselda 3444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
       
       |
119 | 117, 118 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
       
           |
120 | 116, 119 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
       
       |
121 | 120 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                     |
122 | | elfzle1 11831 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
123 | 119, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
       

      |
124 | 123 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                     |
125 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
126 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
       
   |
127 | 113, 121,
124, 125, 126 | fsumge1 13906 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
    
       |
128 | 112 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
    
       
  |
129 | 120 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
       
       |
130 | 128, 129 | fsumcl 13848 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    
               |
131 | 63 | recnd 9695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    
              |
132 | 130, 131 | pncand 10013 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
          
                     |
133 | | nfv 1772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
         |
134 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
135 | 50 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
       
  |
136 | | dvnprodlem1.zr |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
137 | 136 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
       
  |
138 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
139 | 133, 134,
128, 135, 137, 129, 138, 131 | fsumsplitsn 37687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
    
                               |
140 | 139 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
    
                               |
141 | 125 | cbvsumv 13811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                     |
142 | 141 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
    
                  
           |
143 | 41 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
    
            
                               |
144 | 46, 143 | eleqtrd 2542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
    
              
                 |
145 | | rabid 2979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
              
      
                 |
146 | 144, 145 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    
             
                  |
147 | 146 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
    
                    |
148 | 142, 147 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
    
                    |
149 | 140, 148 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    
                     |
150 | 149 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
    
          
                      |
151 | 132, 150 | eqtr3d 2498 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
                     |
152 | 151 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
              |
153 | 127, 152 | breqtrd 4441 |
. . . . . . . . . . . . . . . . . . . . 21
       
       
    
        |
154 | 107, 109,
153 | jca32 542 |
. . . . . . . . . . . . . . . . . . . 20
       
       
              
                  |
155 | | elfz2 11820 |
. . . . . . . . . . . . . . . . . . . 20
              
  
              
    
         |
156 | 154, 155 | sylibr 217 |
. . . . . . . . . . . . . . . . . . 19
       
       
                 |
157 | 99, 156 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . 18
       
       
                   |
158 | 157 | ex 440 |
. . . . . . . . . . . . . . . . 17
 
    
                            |
159 | 97, 158 | ralrimi 2800 |
. . . . . . . . . . . . . . . 16
 
    
        
                  |
160 | 78, 159 | jca 539 |
. . . . . . . . . . . . . . 15
 
    
                               |
161 | | ffnfv 6072 |
. . . . . . . . . . . . . . 15
 
              
   
                   |
162 | 160, 161 | sylibr 217 |
. . . . . . . . . . . . . 14
 
    
                          |
163 | | ovex 6343 |
. . . . . . . . . . . . . . . 16
           |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . 15
 
    
           
        |
165 | 20, 110 | ssexd 4564 |
. . . . . . . . . . . . . . . 16
   |
166 | 165 | adantr 471 |
. . . . . . . . . . . . . . 15
 
    
       
  |
167 | 164, 166 | elmapd 7512 |
. . . . . . . . . . . . . 14
 
    
               
      
         
         |
168 | 162, 167 | mpbird 240 |
. . . . . . . . . . . . 13
 
    
                        |
169 | 98 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
    
                      |
170 | 97, 169 | ralrimi 2800 |
. . . . . . . . . . . . . . 15
 
    
        
            |
171 | 170 | sumeq2d 13817 |
. . . . . . . . . . . . . 14
 
    
                      |
172 | 125 | cbvsumv 13811 |
. . . . . . . . . . . . . . . 16

    
     |
173 | 172 | eqcomi 2471 |
. . . . . . . . . . . . . . 15

    
     |
174 | 173 | a1i 11 |
. . . . . . . . . . . . . 14
 
    
                    |
175 | 151 | idi 2 |
. . . . . . . . . . . . . 14
 
    
                     |
176 | 171, 174,
175 | 3eqtrd 2500 |
. . . . . . . . . . . . 13
 
    
                       |
177 | 168, 176 | jca 539 |
. . . . . . . . . . . 12
 
    
               
                       |
178 | | eqidd 2463 |
. . . . . . . . . . . . . . 15
     |
179 | | simpl 463 |
. . . . . . . . . . . . . . . 16
         |
180 | 179 | fveq1d 5890 |
. . . . . . . . . . . . . . 15
                 |
181 | 178, 180 | sumeq12rdv 13822 |
. . . . . . . . . . . . . 14
   
    
        |
182 | 181 | eqeq1d 2464 |
. . . . . . . . . . . . 13
              
                |
183 | 182 | elrab 3208 |
. . . . . . . . . . . 12
 
      
                          
                       |
184 | 177, 183 | sylibr 217 |
. . . . . . . . . . 11
 
    
                       
             |
185 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
186 | | rabeq 3050 |
. . . . . . . . . . . . . . . . . . . 20
     
              
                    |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
        
                    |
188 | | sumeq1 13804 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
      |
189 | 188 | eqeq1d 2464 |
. . . . . . . . . . . . . . . . . . . 20
      
        |
190 | 189 | rabbidv 3048 |
. . . . . . . . . . . . . . . . . . 19
        
                    |
191 | 187, 190 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . 18
        
                    |
192 | 191 | mpteq2dv 4504 |
. . . . . . . . . . . . . . . . 17
         
            
          |
193 | 192 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
         
            
          |
194 | | elpwg 3971 |
. . . . . . . . . . . . . . . . . 18
 
    |
195 | 165, 194 | syl 17 |
. . . . . . . . . . . . . . . . 17
  
   |
196 | 110, 195 | mpbird 240 |
. . . . . . . . . . . . . . . 16
    |
197 | 26 | mptex 6161 |
. . . . . . . . . . . . . . . . 17

       
       |
198 | 197 | a1i 11 |
. . . . . . . . . . . . . . . 16
       
          |
199 | 9, 193, 196, 198 | fvmptd 5977 |
. . . . . . . . . . . . . . 15
     
       
        |
200 | 199 | adantr 471 |
. . . . . . . . . . . . . 14
 
    
            
       
        |
201 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . 19
           |
202 | 201 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . 18
     
         |
203 | | rabeq 3050 |
. . . . . . . . . . . . . . . . . 18
     
              
                    |
204 | 202, 203 | syl 17 |
. . . . . . . . . . . . . . . . 17
        
                    |
205 | | eqeq2 2473 |
. . . . . . . . . . . . . . . . . 18
      
        |
206 | 205 | rabbidv 3048 |
. . . . . . . . . . . . . . . . 17
        
                    |
207 | 204, 206 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
        
                    |
208 | 207 | cbvmptv 4509 |
. . . . . . . . . . . . . . 15

       
            
         |
209 | 208 | a1i 11 |
. . . . . . . . . . . . . 14
 
    
              
        
       
        |
210 | 200, 209 | eqtrd 2496 |
. . . . . . . . . . . . 13
 
    
            
       
        |
211 | | fveq1 5887 |
. . . . . . . . . . . . . . . . . . 19
           |
212 | 211 | sumeq2ad 37682 |
. . . . . . . . . . . . . . . . . 18
 
    
      |
213 | 212 | eqeq1d 2464 |
. . . . . . . . . . . . . . . . 17
      
        |
214 | 213 | cbvrabv 3056 |
. . . . . . . . . . . . . . . 16
       
                   |
215 | 214 | a1i 11 |
. . . . . . . . . . . . . . 15
              
                    |
216 | | oveq2 6323 |
. . . . . . . . . . . . . . . . 17
              
        |
217 | 216 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
           
               |
218 | | rabeq 3050 |
. . . . . . . . . . . . . . . 16
     
                    
                          |
219 | 217, 218 | syl 17 |
. . . . . . . . . . . . . . 15
              
                          |
220 | | eqeq2 2473 |
. . . . . . . . . . . . . . . 16
            
              |
221 | 220 | rabbidv 3048 |
. . . . . . . . . . . . . . 15
                    
                                |
222 | 215, 219,
221 | 3eqtrd 2500 |
. . . . . . . . . . . . . 14
              
                                |
223 | 222 | adantl 472 |
. . . . . . . . . . . . 13
       
       
              
                  
             |
224 | 58, 65 | jca 539 |
. . . . . . . . . . . . . 14
 
    
              
         |
225 | | elnn0z 10979 |
. . . . . . . . . . . . . 14
      
                |
226 | 224, 225 | sylibr 217 |
. . . . . . . . . . . . 13
 
    
                |
227 | | ovex 6343 |
. . . . . . . . . . . . . . 15
             |
228 | 227 | rabex 4568 |
. . . . . . . . . . . . . 14
             
            |
229 | 228 | a1i 11 |
. . . . . . . . . . . . 13
 
    
             
                     |
230 | 210, 223,
226, 229 | fvmptd 5977 |
. . . . . . . . . . . 12
 
    
               
                   
             |
231 | 230 | eqcomd 2468 |
. . . . . . . . . . 11
 
    
             
                          
        |
232 | 184, 231 | eleqtrd 2542 |
. . . . . . . . . 10
 
    
                 
        |
233 | 72, 232 | jca 539 |
. . . . . . . . 9
 
    
                                      |
234 | 1, 233 | jca 539 |
. . . . . . . 8
 
    
                 
          
            
                    |
235 | 232 | elfvexd 5916 |
. . . . . . . . 9
 
    
                |
236 | | vex 3060 |
. . . . . . . . . . 11
 |
237 | 236 | resex 5167 |
. . . . . . . . . 10
   |
238 | 237 | a1i 11 |
. . . . . . . . 9
 
    
            |
239 | | opeq12 4182 |
. . . . . . . . . . . 12
       
              
    |
240 | 239 | eqeq2d 2472 |
. . . . . . . . . . 11
       
            
                              |
241 | | eleq1 2528 |
. . . . . . . . . . . . 13
           
             |
242 | 241 | adantr 471 |
. . . . . . . . . . . 12
       
                     |
243 | | simpr 467 |
. . . . . . . . . . . . 13
       
       |
244 | | fveq2 5888 |
. . . . . . . . . . . . . 14
                      
        |
245 | 244 | adantr 471 |
. . . . . . . . . . . . 13
       
                           |
246 | 243, 245 | eleq12d 2534 |
. . . . . . . . . . . 12
       
            
        
         |
247 | 242, 246 | anbi12d 722 |
. . . . . . . . . . 11
       
        
        
 
        
                    |
248 | 240, 247 | anbi12d 722 |
. . . . . . . . . 10
       
      
        
  
    
                   
          
            
                     |
249 | 248 | spc2egv 3148 |
. . . . . . . . 9
              
        
                     
                        
        
  
    
             |
250 | 235, 238,
249 | syl2anc 671 |
. . . . . . . 8
 
    
           
        
                     
                        
        
  
    
             |
251 | 234, 250 | mpd 15 |
. . . . . . 7
 
    
                               
            |
252 | | eliunxp 4991 |
. . . . . . 7
            
                
      
        
  
    
            |
253 | 251, 252 | sylibr 217 |
. . . . . 6
 
    
                   
                   |
254 | | dvnprodlem1.d |
. . . . . 6
     
        
           |
255 | 253, 254 | fmptd 6069 |
. . . . 5
                                     |
256 | 95 | nfcri 2597 |
. . . . . . . . . . . 12
              |
257 | 96, 256 | nfan 2022 |
. . . . . . . . . . 11
       
           
         |
258 | 79, 257 | nfan 2022 |
. . . . . . . . . 10
               
    
          |
259 | | nfv 1772 |
. . . . . . . . . 10
           |
260 | 258, 259 | nfan 2022 |
. . . . . . . . 9
         
           
                   |
261 | 99 | eqcomd 2468 |
. . . . . . . . . . . . . . 15
       
       
      
      |
262 | 261 | adantlrr 732 |
. . . . . . . . . . . . . 14
               
    
         
            |
263 | 262 | adantlr 726 |
. . . . . . . . . . . . 13
         
           
                               |
264 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
                            |
265 | | opex 4678 |
. . . . . . . . . . . . . . . . . . . 20
 
          |
266 | 265 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
    
                     |
267 | 264, 266 | fvmpt2d 5982 |
. . . . . . . . . . . . . . . . . 18
 
    
             
           |
268 | 267 | fveq2d 5892 |
. . . . . . . . . . . . . . . . 17
 
    
                           
     |
269 | 268 | fveq1d 5890 |
. . . . . . . . . . . . . . . 16
 
    
                                
        |
270 | | ovex 6343 |
. . . . . . . . . . . . . . . . . . 19
       |
271 | 270, 237 | op2nd 6829 |
. . . . . . . . . . . . . . . . . 18
           
      |
272 | 271 | fveq1i 5889 |
. . . . . . . . . . . . . . . . 17
     
                    |
273 | 272 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
    
                                   |
274 | 269, 273 | eqtr2d 2497 |
. . . . . . . . . . . . . . 15
 
    
                            |
275 | 274 | adantrr 728 |
. . . . . . . . . . . . . 14
 
     
           
                             |
276 | 275 | ad2antrr 737 |
. . . . . . . . . . . . 13
         
           
                                       |
277 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . 20
       
                           |
278 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
       
     
        
            |
279 | | fveq1 5887 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
280 | 279 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
             |
281 | | reseq1 5118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
282 | 280, 281 | opeq12d 4188 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
        
             |
283 | 282 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
       
       
                         |
284 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
                      |
285 | | opex 4678 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
          |
286 | 285 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
                     |
287 | 278, 283,
284, 286 | fvmptd 5977 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
             
           |
288 | 287 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
       
                      
           |
289 | 277, 288 | eqtrd 2496 |
. . . . . . . . . . . . . . . . . . 19
       
                      
           |
290 | 289 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
       
                                    
     |
291 | 290 | adantlrl 731 |
. . . . . . . . . . . . . . . . 17
               
    
                 
            
            |
292 | 291 | adantr 471 |
. . . . . . . . . . . . . . . 16
         
           
                                            |
293 | | ovex 6343 |
. . . . . . . . . . . . . . . . . 18
       |
294 | | vex 3060 |
. . . . . . . . . . . . . . . . . . 19
 |
295 | 294 | resex 5167 |
. . . . . . . . . . . . . . . . . 18
   |
296 | 293, 295 | op2nd 6829 |
. . . . . . . . . . . . . . . . 17
           
      |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . . 16
         
           
                              
       |
298 | 292, 297 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
         
           
                               |
299 | 298 | fveq1d 5890 |
. . . . . . . . . . . . . 14
         
           
                                       |
300 | | fvres 5902 |
. . . . . . . . . . . . . . 15
             |
301 | 300 | adantl 472 |
. . . . . . . . . . . . . 14
         
           
                               |
302 | 299, 301 | eqtrd 2496 |
. . . . . . . . . . . . 13
         
           
                                     |
303 | 263, 276,
302 | 3eqtrd 2500 |
. . . . . . . . . . . 12
         
           
                             |
304 | 303 | adantlr 726 |
. . . . . . . . . . 11
          
           
                      
           |
305 | | simpl 463 |
. . . . . . . . . . . 12
          
           
                      

  
            
    
                         |
306 | | elunnel1 3587 |
. . . . . . . . . . . . . 14
     
     |
307 | | elsni 4005 |
. . . . . . . . . . . . . 14
     |
308 | 306, 307 | syl 17 |
. . . . . . . . . . . . 13
     
   |
309 | 308 | adantll 725 |
. . . . . . . . . . . 12
          
           
                      

  |
310 | | simpr 467 |
. . . . . . . . . . . . . . 15
         
           
                     |
311 | 310 | fveq2d 5892 |
. . . . . . . . . . . . . 14
         
           
                             |
312 | 3 | nn0cnd 10956 |
. . . . . . . . . . . . . . . . . . . . 21
   |
313 | 312 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
    
       
  |
314 | 313, 131 | nncand 10017 |
. . . . . . . . . . . . . . . . . . 19
 
    
         
            |
315 | 314 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . 18
 
    
                      |
316 | 315 | adantrr 728 |
. . . . . . . . . . . . . . . . 17
 
     
           
                       |
317 | 316 | adantr 471 |
. . . . . . . . . . . . . . . 16
               
    
                 
              |
318 | 267 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                           
     |
319 | 270, 237 | op1st 6828 |
. . . . . . . . . . . . . . . . . . . . 21
           
          |
320 | 319 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
    
                               |
321 | 318, 320 | eqtr2d 2497 |
. . . . . . . . . . . . . . . . . . 19
 
    
                        |
322 | 321 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . 18
 
    
         
                  |
323 | 322 | adantrr 728 |
. . . . . . . . . . . . . . . . 17
 
     
           
          
                  |
324 | 323 | adantr 471 |
. . . . . . . . . . . . . . . 16
               
    
                 
                    |
325 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
326 | 325 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
       
                                   |
327 | 287 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
                           
     |
328 | 327 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
       
                                    
     |
329 | 293, 295 | op1st 6828 |
. . . . . . . . . . . . . . . . . . . . 21
           
          |
330 | 329 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
       
                                        |
331 | 326, 328,
330 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . . 19
       
                                 |
332 | 331 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . 18
       
                            
        |
333 | 312 | adantr 471 |
. . . . . . . . . . . . . . . . . . . 20
 
    
       
  |
334 | | zsscn 10974 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
335 | 6, 334 | sstri 3453 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
336 | 335 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
           
  |
337 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  
          |
338 | 337 | anbi2d 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    
       
                 |
339 | | feq1 5732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
               |
340 | 338, 339 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
            
              
            
                |
341 | 340, 49 | chvarv 2118 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
                      |
342 | 54 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
       
      |
343 | 341, 342 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
                  |
344 | 336, 343 | sseldd 3445 |
. . . . . . . . . . . . . . . . . . . 20
 
    
              |
345 | 333, 344 | nncand 10017 |
. . . . . . . . . . . . . . . . . . 19
 
    
         
            |
346 | 345 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
       
                  
            |
347 | | eqidd 2463 |
. . . . . . . . . . . . . . . . . 18
       
                           |
348 | 332, 346,
347 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . 17
       
                                 |
349 | 348 | adantlrl 731 |
. . . . . . . . . . . . . . . 16
               
    
                 
                |
350 | 317, 324,
349 | 3eqtrd 2500 |
. . . . . . . . . . . . . . 15
        |