Step | Hyp | Ref
| Expression |
1 | | fveq2 5865 |
. . . . . . . . . . . . 13
 Λ  Λ    |
2 | | oveq2 6298 |
. . . . . . . . . . . . . 14
       |
3 | 2 | fveq2d 5869 |
. . . . . . . . . . . . 13
 ψ    ψ      |
4 | 1, 3 | oveq12d 6308 |
. . . . . . . . . . . 12
  Λ  ψ      Λ  ψ 
     |
5 | 4 | cbvsumv 13762 |
. . . . . . . . . . 11
           Λ  ψ 
              Λ  ψ 
    |
6 | | fzfid 12186 |
. . . . . . . . . . . . . 14
          
      
     |
7 | | elfznn 11828 |
. . . . . . . . . . . . . . . . 17
           |
8 | 7 | adantl 468 |
. . . . . . . . . . . . . . . 16
          
  |
9 | | vmacl 24045 |
. . . . . . . . . . . . . . . 16
 Λ    |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . 15
          
Λ    |
11 | 10 | recnd 9669 |
. . . . . . . . . . . . . 14
          
Λ    |
12 | | elfznn 11828 |
. . . . . . . . . . . . . . . . 17
             |
13 | 12 | adantl 468 |
. . . . . . . . . . . . . . . 16
                      
  |
14 | | vmacl 24045 |
. . . . . . . . . . . . . . . 16
 Λ    |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . 15
                      
Λ    |
16 | 15 | recnd 9669 |
. . . . . . . . . . . . . 14
                      
Λ    |
17 | 6, 11, 16 | fsummulc2 13845 |
. . . . . . . . . . . . 13
          
 Λ              Λ                Λ  Λ     |
18 | 7 | nnrpd 11339 |
. . . . . . . . . . . . . . . . 17
           |
19 | | rpdivcl 11325 |
. . . . . . . . . . . . . . . . 17
       |
20 | 18, 19 | sylan2 477 |
. . . . . . . . . . . . . . . 16
          
    |
21 | 20 | rpred 11341 |
. . . . . . . . . . . . . . 15
          
    |
22 | | chpval 24049 |
. . . . . . . . . . . . . . 15
   ψ                Λ    |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
          
ψ                Λ    |
24 | 23 | oveq2d 6306 |
. . . . . . . . . . . . 13
          
 Λ  ψ      Λ              Λ     |
25 | 13 | nncnd 10625 |
. . . . . . . . . . . . . . . . 17
                      
  |
26 | 7 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
                      
  |
27 | 26 | nncnd 10625 |
. . . . . . . . . . . . . . . . 17
                      
  |
28 | 26 | nnne0d 10654 |
. . . . . . . . . . . . . . . . 17
                      
  |
29 | 25, 27, 28 | divcan3d 10388 |
. . . . . . . . . . . . . . . 16
                      
      |
30 | 29 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                      
Λ      Λ    |
31 | 30 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                      
 Λ  Λ        Λ  Λ     |
32 | 31 | sumeq2dv 13769 |
. . . . . . . . . . . . 13
          
             Λ  Λ                    Λ  Λ     |
33 | 17, 24, 32 | 3eqtr4d 2495 |
. . . . . . . . . . . 12
          
 Λ  ψ     
      
     Λ  Λ         |
34 | 33 | sumeq2dv 13769 |
. . . . . . . . . . 11

           Λ  ψ 
             
      
     Λ  Λ         |
35 | 5, 34 | syl5eq 2497 |
. . . . . . . . . 10

           Λ  ψ 
             
      
     Λ  Λ         |
36 | | oveq1 6297 |
. . . . . . . . . . . . 13
           |
37 | 36 | fveq2d 5869 |
. . . . . . . . . . . 12
   Λ    Λ        |
38 | 37 | oveq2d 6306 |
. . . . . . . . . . 11
    Λ  Λ      Λ  Λ         |
39 | | rpre 11308 |
. . . . . . . . . . 11

  |
40 | | ssrab2 3514 |
. . . . . . . . . . . . . . . . 17
   |
41 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
          
        |
42 | 40, 41 | sseldi 3430 |
. . . . . . . . . . . . . . . 16
          
      |
43 | 42 | anassrs 654 |
. . . . . . . . . . . . . . 15
            
 
  |
44 | 43, 9 | syl 17 |
. . . . . . . . . . . . . 14
            
 
Λ    |
45 | | elfznn 11828 |
. . . . . . . . . . . . . . . . . 18
           |
46 | 45 | adantl 468 |
. . . . . . . . . . . . . . . . 17
          
  |
47 | | dvdsdivcl 24110 |
. . . . . . . . . . . . . . . . 17
 
         |
48 | 46, 47 | sylan 474 |
. . . . . . . . . . . . . . . 16
            
 
  
   |
49 | 40, 48 | sseldi 3430 |
. . . . . . . . . . . . . . 15
            
 
    |
50 | | vmacl 24045 |
. . . . . . . . . . . . . . 15
   Λ      |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
            
 
Λ      |
52 | 44, 51 | remulcld 9671 |
. . . . . . . . . . . . 13
            
 
 Λ  Λ       |
53 | 52 | recnd 9669 |
. . . . . . . . . . . 12
            
 
 Λ  Λ       |
54 | 53 | anasss 653 |
. . . . . . . . . . 11
          
     Λ  Λ       |
55 | 38, 39, 54 | dvdsflsumcom 24117 |
. . . . . . . . . 10

           
  Λ  Λ               
      
     Λ  Λ         |
56 | 35, 55 | eqtr4d 2488 |
. . . . . . . . 9

           Λ  ψ 
   
         
 
 Λ  Λ       |
57 | 56 | oveq1d 6305 |
. . . . . . . 8

            Λ  ψ     
          Λ                    
  Λ  Λ                Λ          |
58 | | fzfid 12186 |
. . . . . . . . 9

          |
59 | | vmacl 24045 |
. . . . . . . . . . . 12
 Λ    |
60 | 46, 59 | syl 17 |
. . . . . . . . . . 11
          
Λ    |
61 | 60 | recnd 9669 |
. . . . . . . . . 10
          
Λ    |
62 | 45 | nnrpd 11339 |
. . . . . . . . . . . . . 14
           |
63 | | rpdivcl 11325 |
. . . . . . . . . . . . . 14
       |
64 | 62, 63 | sylan2 477 |
. . . . . . . . . . . . 13
          
    |
65 | 64 | rpred 11341 |
. . . . . . . . . . . 12
          
    |
66 | | chpcl 24051 |
. . . . . . . . . . . 12
   ψ      |
67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
          
ψ      |
68 | 67 | recnd 9669 |
. . . . . . . . . 10
          
ψ      |
69 | 61, 68 | mulcld 9663 |
. . . . . . . . 9
          
 Λ  ψ       |
70 | 46 | nnrpd 11339 |
. . . . . . . . . . . 12
          
  |
71 | | relogcl 23525 |
. . . . . . . . . . . 12

      |
72 | 70, 71 | syl 17 |
. . . . . . . . . . 11
          
      |
73 | 72 | recnd 9669 |
. . . . . . . . . 10
          
      |
74 | 61, 73 | mulcld 9663 |
. . . . . . . . 9
          
 Λ         |
75 | 58, 69, 74 | fsumadd 13805 |
. . . . . . . 8

            Λ  ψ 
    Λ                    Λ  ψ 
   
          Λ          |
76 | | fzfid 12186 |
. . . . . . . . . . . 12
          
      |
77 | | sgmss 24033 |
. . . . . . . . . . . . 13
         |
78 | 46, 77 | syl 17 |
. . . . . . . . . . . 12
          
 
      |
79 | | ssfi 7792 |
. . . . . . . . . . . 12
      
          |
80 | 76, 78, 79 | syl2anc 667 |
. . . . . . . . . . 11
          
 
  |
81 | 80, 52 | fsumrecl 13800 |
. . . . . . . . . 10
          
 
  Λ  Λ       |
82 | 81 | recnd 9669 |
. . . . . . . . 9
          
 
  Λ  Λ       |
83 | 58, 82, 74 | fsumadd 13805 |
. . . . . . . 8

            
  Λ  Λ      Λ                    
  Λ  Λ                Λ          |
84 | 57, 75, 83 | 3eqtr4d 2495 |
. . . . . . 7

            Λ  ψ 
    Λ                    
  Λ  Λ      Λ          |
85 | 73, 68 | addcomd 9835 |
. . . . . . . . . 10
          
     ψ      ψ 
         |
86 | 85 | oveq2d 6306 |
. . . . . . . . 9
          
 Λ       ψ 
     Λ   ψ            |
87 | 61, 68, 73 | adddid 9667 |
. . . . . . . . 9
          
 Λ   ψ            Λ  ψ 
    Λ          |
88 | 86, 87 | eqtrd 2485 |
. . . . . . . 8
          
 Λ       ψ 
      Λ  ψ      Λ          |
89 | 88 | sumeq2dv 13769 |
. . . . . . 7

           Λ       ψ      
           Λ  ψ 
    Λ          |
90 | | logsqvma2 24381 |
. . . . . . . . 9
  
                  
 
 Λ  Λ      Λ          |
91 | 46, 90 | syl 17 |
. . . . . . . 8
          
 
                  
 
 Λ  Λ      Λ          |
92 | 91 | sumeq2dv 13769 |
. . . . . . 7

           
                             
  Λ  Λ      Λ          |
93 | 84, 89, 92 | 3eqtr4d 2495 |
. . . . . 6

           Λ       ψ      
         
 
                  |
94 | 36 | fveq2d 5869 |
. . . . . . . . 9
                   |
95 | 94 | oveq1d 6305 |
. . . . . . . 8
                           |
96 | 95 | oveq2d 6306 |
. . . . . . 7
                                       |
97 | | mucl 24068 |
. . . . . . . . . 10
       |
98 | 42, 97 | syl 17 |
. . . . . . . . 9
          
          |
99 | 98 | zcnd 11041 |
. . . . . . . 8
          
          |
100 | 62 | ad2antrl 734 |
. . . . . . . . . . 11
          
   
  |
101 | 42 | nnrpd 11339 |
. . . . . . . . . . 11
          
      |
102 | 100, 101 | rpdivcld 11358 |
. . . . . . . . . 10
          
        |
103 | | relogcl 23525 |
. . . . . . . . . . 11
  
        |
104 | 103 | recnd 9669 |
. . . . . . . . . 10
  
        |
105 | 102, 104 | syl 17 |
. . . . . . . . 9
          
            |
106 | 105 | sqcld 12414 |
. . . . . . . 8
          
                |
107 | 99, 106 | mulcld 9663 |
. . . . . . 7
          
                      |
108 | 96, 39, 107 | dvdsflsumcom 24117 |
. . . . . 6

           
                           
      
                        |
109 | 29 | fveq2d 5869 |
. . . . . . . . . 10
                      
              |
110 | 109 | oveq1d 6305 |
. . . . . . . . 9
                      
                      |
111 | 110 | oveq2d 6306 |
. . . . . . . 8
                      
                                  |
112 | 111 | sumeq2dv 13769 |
. . . . . . 7
          
                                                          |
113 | 112 | sumeq2dv 13769 |
. . . . . 6

          
      
                                
      
                    |
114 | 93, 108, 113 | 3eqtrd 2489 |
. . . . 5

           Λ       ψ                
      
                    |
115 | 114 | oveq1d 6305 |
. . . 4

            Λ       ψ 
                
      
                     |
116 | 115 | oveq1d 6305 |
. . 3

  
          Λ       ψ 
                        
      
                            |
117 | 116 | mpteq2ia 4485 |
. 2

  
          Λ       ψ 
                          
      
                            |
118 | | eqid 2451 |
. . 3
                                                 |
119 | 118 | selberglem2 24384 |
. 2

            
      
                               |
120 | 117, 119 | eqeltri 2525 |
1

  
          Λ       ψ 
                 |