Step | Hyp | Ref
| Expression |
1 | | nnre 10623 |
. . . . . . . . 9
   |
2 | 1 | renegcld 10053 |
. . . . . . . 8
    |
3 | | opelxpi 4869 |
. . . . . . . 8
            |
4 | 2, 1, 3 | syl2anc 667 |
. . . . . . 7
         |
5 | 4 | ad2antlr 734 |
. . . . . 6
             |
6 | | eqid 2453 |
. . . . . 6
             |
7 | 5, 6 | fmptd 6051 |
. . . . 5
 

              |
8 | | reex 9635 |
. . . . . . . . 9
 |
9 | 8, 8 | xpex 6600 |
. . . . . . . 8
   |
10 | 9 | a1i 11 |
. . . . . . 7
  
  |
11 | | hoicvrrex.fi |
. . . . . . 7
   |
12 | | elmapg 7490 |
. . . . . . 7
   
       
   

              |
13 | 10, 11, 12 | syl2anc 667 |
. . . . . 6
       
   

              |
14 | 13 | adantr 467 |
. . . . 5
 

          

              |
15 | 7, 14 | mpbird 236 |
. . . 4
 

        
   |
16 | | eqid 2453 |
. . . 4
                 |
17 | 15, 16 | fmptd 6051 |
. . 3
               
   |
18 | | ovex 6323 |
. . . 4
     |
19 | | nnex 10622 |
. . . 4
 |
20 | 18, 19 | elmap 7505 |
. . 3
            
 
              
   |
21 | 17, 20 | sylibr 216 |
. 2
            
    |
22 | | hoicvrrex.y |
. . . 4

    |
23 | | eqid 2453 |
. . . . . 6
                 |
24 | 23, 11 | hoicvr 38380 |
. . . . 5
  
                      |
25 | | eqidd 2454 |
. . . . . . . . . . . . 13
           |
26 | 25 | cbvmptv 4498 |
. . . . . . . . . . . 12
             |
27 | 26 | mpteq2i 4489 |
. . . . . . . . . . 11
                 |
28 | 27 | a1i 11 |
. . . . . . . . . 10
                   |
29 | 28 | fveq1d 5872 |
. . . . . . . . 9
                           |
30 | 29 | coeq2d 5000 |
. . . . . . . 8
                               |
31 | 30 | fveq1d 5872 |
. . . . . . 7
                                       |
32 | 31 | ixpeq2dv 7543 |
. . . . . 6
                    
                    |
33 | 32 | iuneq2d 4308 |
. . . . 5
                                           |
34 | 24, 33 | sseqtrd 3470 |
. . . 4
  
                      |
35 | 22, 34 | sstrd 3444 |
. . 3

                      |
36 | | simpr 463 |
. . . . . . . . . . . . . . 15
 

  |
37 | 15 | elexd 3058 |
. . . . . . . . . . . . . . 15
 

        |
38 | 16 | fvmpt2 5962 |
. . . . . . . . . . . . . . 15
       
                     |
39 | 36, 37, 38 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

                    |
40 | 39, 5 | fmpt3d 6052 |
. . . . . . . . . . . . 13
 

                    |
41 | 40 | adantr 467 |
. . . . . . . . . . . 12
                         |
42 | | simpr 463 |
. . . . . . . . . . . 12
       |
43 | 41, 42 | fvovco 37479 |
. . . . . . . . . . 11
      
                                                              |
44 | 39 | fveq1d 5872 |
. . . . . . . . . . . . . . . 16
 

                            |
45 | 44 | adantr 467 |
. . . . . . . . . . . . . . 15
                                 |
46 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
47 | | opex 4667 |
. . . . . . . . . . . . . . . . . 18
     |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
       |
49 | 6 | fvmpt2 5962 |
. . . . . . . . . . . . . . . . 17
                       |
50 | 46, 48, 49 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
                 |
51 | 50 | adantlr 722 |
. . . . . . . . . . . . . . 15
                     |
52 | 45, 51 | eqtrd 2487 |
. . . . . . . . . . . . . 14
                           |
53 | 52 | fveq2d 5874 |
. . . . . . . . . . . . 13
                                   |
54 | | negex 9878 |
. . . . . . . . . . . . . . 15
  |
55 | | vex 3050 |
. . . . . . . . . . . . . . 15
 |
56 | 54, 55 | op1st 6806 |
. . . . . . . . . . . . . 14
       
  |
57 | 56 | a1i 11 |
. . . . . . . . . . . . 13
            
   |
58 | 53, 57 | eqtrd 2487 |
. . . . . . . . . . . 12
                            |
59 | 52 | fveq2d 5874 |
. . . . . . . . . . . . 13
                                   |
60 | 54, 55 | op2nd 6807 |
. . . . . . . . . . . . . 14
       
 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
            
  |
62 | 59, 61 | eqtrd 2487 |
. . . . . . . . . . . 12
                           |
63 | 58, 62 | oveq12d 6313 |
. . . . . . . . . . 11
                                                        |
64 | 43, 63 | eqtrd 2487 |
. . . . . . . . . 10
      
                       |
65 | 64 | fveq2d 5874 |
. . . . . . . . 9
                                      |
66 | | volico 38373 |
. . . . . . . . . . . 12
                        |
67 | 2, 1, 66 | syl2anc 667 |
. . . . . . . . . . 11
                     |
68 | | nnrp 11318 |
. . . . . . . . . . . . 13
   |
69 | | neglt 37504 |
. . . . . . . . . . . . 13

   |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
    |
71 | 70 | iftrued 3891 |
. . . . . . . . . . 11
               |
72 | 1 | recnd 9674 |
. . . . . . . . . . . . 13
   |
73 | 72, 72 | subnegd 9998 |
. . . . . . . . . . . 12
        |
74 | 72 | 2timesd 10862 |
. . . . . . . . . . . 12
       |
75 | 73, 74 | eqtr4d 2490 |
. . . . . . . . . . 11
        |
76 | 67, 71, 75 | 3eqtrd 2491 |
. . . . . . . . . 10
              |
77 | 76 | ad2antlr 734 |
. . . . . . . . 9
                  |
78 | 65, 77 | eqtrd 2487 |
. . . . . . . 8
                               |
79 | 78 | prodeq2dv 13989 |
. . . . . . 7
 


                           |
80 | 11 | adantr 467 |
. . . . . . . 8
 

  |
81 | | 2cnd 10689 |
. . . . . . . . 9
 

  |
82 | 72 | adantl 468 |
. . . . . . . . 9
 

  |
83 | 81, 82 | mulcld 9668 |
. . . . . . . 8
 

    |
84 | | fprodconst 14044 |
. . . . . . . 8
                    |
85 | 80, 83, 84 | syl2anc 667 |
. . . . . . 7
 


              |
86 | 79, 85 | eqtrd 2487 |
. . . . . 6
 


                                  |
87 | 86 | mpteq2dva 4492 |
. . . . 5
                                        |
88 | 87 | fveq2d 5874 |
. . . 4
 Σ^                           Σ^                |
89 | 19 | a1i 11 |
. . . . . 6
   |
90 | 68 | ssriv 3438 |
. . . . . . . . . 10
 |
91 | | ioorp 11719 |
. . . . . . . . . . 11
    |
92 | 91 | eqcomi 2462 |
. . . . . . . . . 10
    |
93 | 90, 92 | sseqtri 3466 |
. . . . . . . . 9
    |
94 | | ioossicc 11727 |
. . . . . . . . 9
       |
95 | 93, 94 | sstri 3443 |
. . . . . . . 8
    |
96 | | 2nn 10774 |
. . . . . . . . . . 11
 |
97 | 96 | a1i 11 |
. . . . . . . . . 10
 

  |
98 | 97, 36 | nnmulcld 10664 |
. . . . . . . . 9
 

    |
99 | | hashcl 12545 |
. . . . . . . . . . 11
       |
100 | 11, 99 | syl 17 |
. . . . . . . . . 10
       |
101 | 100 | adantr 467 |
. . . . . . . . 9
 

      |
102 | | nnexpcl 12292 |
. . . . . . . . 9
                     |
103 | 98, 101, 102 | syl2anc 667 |
. . . . . . . 8
 

            |
104 | 95, 103 | sseldi 3432 |
. . . . . . 7
 

               |
105 | | eqid 2453 |
. . . . . . 7
                         |
106 | 104, 105 | fmptd 6051 |
. . . . . 6
                      |
107 | 89, 106 | sge0xrcl 38237 |
. . . . 5
 Σ^                |
108 | | pnfxr 11419 |
. . . . . . 7
 |
109 | 108 | a1i 11 |
. . . . . 6
   |
110 | | 1nn 10627 |
. . . . . . . . . 10
 |
111 | 95, 110 | sselii 3431 |
. . . . . . . . 9
    |
112 | 111 | a1i 11 |
. . . . . . . 8
 

     |
113 | | eqid 2453 |
. . . . . . . 8
     |
114 | 112, 113 | fmptd 6051 |
. . . . . . 7
            |
115 | 89, 114 | sge0xrcl 38237 |
. . . . . 6
 Σ^      |
116 | | nnnfi 37419 |
. . . . . . . . . 10
 |
117 | 116 | a1i 11 |
. . . . . . . . 9
   |
118 | | 1rp 11313 |
. . . . . . . . . 10
 |
119 | 118 | a1i 11 |
. . . . . . . . 9
   |
120 | 89, 117, 119 | sge0rpcpnf 38273 |
. . . . . . . 8
 Σ^      |
121 | 120 | eqcomd 2459 |
. . . . . . 7
 Σ^      |
122 | 109, 121 | xreqled 37563 |
. . . . . 6

Σ^      |
123 | | nfv 1763 |
. . . . . . 7
   |
124 | 114 | mptex2 37443 |
. . . . . . 7
 

     |
125 | 103 | nnge1d 10659 |
. . . . . . 7
 

            |
126 | 123, 89, 124, 104, 125 | sge0lempt 38262 |
. . . . . 6
 Σ^    Σ^                |
127 | 109, 115,
107, 122, 126 | xrletrd 11466 |
. . . . 5

Σ^                |
128 | 107, 127 | xrgepnfd 37564 |
. . . 4
 Σ^                |
129 | | eqidd 2454 |
. . . 4
   |
130 | 88, 128, 129 | 3eqtrrd 2492 |
. . 3
 Σ^                             |
131 | 35, 130 | jca 535 |
. 2
                     
Σ^                              |
132 | | nfcv 2594 |
. . . . . . 7
   |
133 | | nfmpt1 4495 |
. . . . . . 7
           |
134 | 132, 133 | nfeq 2605 |
. . . . . 6
          |
135 | | nfcv 2594 |
. . . . . . . . 9
   |
136 | | nfcv 2594 |
. . . . . . . . . 10
   |
137 | | nfmpt1 4495 |
. . . . . . . . . 10
         |
138 | 136, 137 | nfmpt 4494 |
. . . . . . . . 9
           |
139 | 135, 138 | nfeq 2605 |
. . . . . . . 8
          |
140 | | fveq1 5869 |
. . . . . . . . . . 11
                           |
141 | 140 | coeq2d 5000 |
. . . . . . . . . 10
                               |
142 | 141 | fveq1d 5872 |
. . . . . . . . 9
          
                            |
143 | 142 | adantr 467 |
. . . . . . . 8
         
  
                            |
144 | 139, 143 | ixpeq2d 37420 |
. . . . . . 7
         
          
 
                  |
145 | 144 | adantr 467 |
. . . . . 6
         


          
 
                  |
146 | 134, 145 | iuneq2df 37392 |
. . . . 5
                                           |
147 | 146 | sseq2d 3462 |
. . . 4
                     
                       |
148 | 142 | fveq2d 5874 |
. . . . . . . . . . 11
                           
                   |
149 | 148 | a1d 26 |
. . . . . . . . . 10
              
                                  |
150 | 139, 149 | ralrimi 2790 |
. . . . . . . . 9
         
                                      |
151 | 150 | adantr 467 |
. . . . . . . 8
         


                                      |
152 | 151 | prodeq2d 13988 |
. . . . . . 7
         


                                       |
153 | 134, 152 | mpteq2da 4491 |
. . . . . 6
                           
                         |
154 | 153 | fveq2d 5874 |
. . . . 5
         Σ^                   Σ^                             |
155 | 154 | eqeq2d 2463 |
. . . 4
        
Σ^                  
Σ^                              |
156 | 147, 155 | anbi12d 718 |
. . 3
                      
Σ^                   
                    
Σ^                               |
157 | 156 | rspcev 3152 |
. 2
             
  
                   
Σ^                                       
 
        Σ^                      |
158 | 21, 131, 157 | syl2anc 667 |
1
     
   
           
Σ^                      |