Step | Hyp | Ref
| Expression |
1 | | efadd.4 |
. . . 4
   |
2 | | efadd.5 |
. . . 4
   |
3 | 1, 2 | addcld 7976 |
. . 3
     |
4 | | efadd.3 |
. . . 4
               |
5 | 4 | efcvg 11673 |
. . 3
              |
6 | 3, 5 | syl 14 |
. 2
            |
7 | | efadd.1 |
. . . . . 6
             |
8 | 7 | eftvalcn 11664 |
. . . . 5
 
                 |
9 | 1, 8 | sylan 283 |
. . . 4
 

                |
10 | | absexp 11087 |
. . . . . . 7
 
                   |
11 | 1, 10 | sylan 283 |
. . . . . 6
 

                  |
12 | | faccl 10714 |
. . . . . . . 8

      |
13 | 12 | adantl 277 |
. . . . . . 7
 

      |
14 | | nnre 8925 |
. . . . . . . 8
           |
15 | | nnnn0 9182 |
. . . . . . . . 9
           |
16 | 15 | nn0ge0d 9231 |
. . . . . . . 8
           |
17 | 14, 16 | absidd 11175 |
. . . . . . 7
                   |
18 | 13, 17 | syl 14 |
. . . . . 6
 

              |
19 | 11, 18 | oveq12d 5892 |
. . . . 5
 

                                  |
20 | | expcl 10537 |
. . . . . . 7
 
       |
21 | 1, 20 | sylan 283 |
. . . . . 6
 

      |
22 | 13 | nncnd 8932 |
. . . . . 6
 

      |
23 | 13 | nnap0d 8964 |
. . . . . 6
 

    #   |
24 | 21, 22, 23 | absdivapd 11203 |
. . . . 5
 

                                  |
25 | 1 | abscld 11189 |
. . . . . . 7
       |
26 | 25 | recnd 7985 |
. . . . . 6
       |
27 | | eqid 2177 |
. . . . . . 7

                                |
28 | 27 | eftvalcn 11664 |
. . . . . 6
     
                                     |
29 | 26, 28 | sylan 283 |
. . . . 5
 

                                    |
30 | 19, 24, 29 | 3eqtr4rd 2221 |
. . . 4
 

                                    |
31 | | eftcl 11661 |
. . . . 5
 
             |
32 | 1, 31 | sylan 283 |
. . . 4
 

            |
33 | | efadd.2 |
. . . . . 6
             |
34 | 33 | eftvalcn 11664 |
. . . . 5
 
                 |
35 | 2, 34 | sylan 283 |
. . . 4
 

                |
36 | | eftcl 11661 |
. . . . 5
 
             |
37 | 2, 36 | sylan 283 |
. . . 4
 

            |
38 | 4 | eftvalcn 11664 |
. . . . . 6
   
                   |
39 | 3, 38 | sylan 283 |
. . . . 5
 

                  |
40 | 1 | adantr 276 |
. . . . . . . 8
 

  |
41 | 2 | adantr 276 |
. . . . . . . 8
 

  |
42 | | simpr 110 |
. . . . . . . 8
 

  |
43 | | binom 11491 |
. . . . . . . 8
 
                               |
44 | 40, 41, 42, 43 | syl3anc 1238 |
. . . . . . 7
 

 
                            |
45 | 44 | oveq1d 5889 |
. . . . . 6
 

                                          |
46 | | 0zd 9264 |
. . . . . . . . 9
 

  |
47 | 42 | nn0zd 9372 |
. . . . . . . . 9
 

  |
48 | 46, 47 | fzfigd 10430 |
. . . . . . . 8
 

      |
49 | | faccl 10714 |
. . . . . . . . . 10

      |
50 | 49 | adantl 277 |
. . . . . . . . 9
 

      |
51 | 50 | nncnd 8932 |
. . . . . . . 8
 

      |
52 | | bccl2 10747 |
. . . . . . . . . . 11
         |
53 | 52 | adantl 277 |
. . . . . . . . . 10
             |
54 | 53 | nncnd 8932 |
. . . . . . . . 9
             |
55 | 1 | ad2antrr 488 |
. . . . . . . . . . 11
           |
56 | | fznn0sub 10056 |
. . . . . . . . . . . 12
         |
57 | 56 | adantl 277 |
. . . . . . . . . . 11
             |
58 | 55, 57 | expcld 10653 |
. . . . . . . . . 10
                 |
59 | 2 | ad2antrr 488 |
. . . . . . . . . . 11
           |
60 | | elfznn0 10113 |
. . . . . . . . . . . 12
       |
61 | 60 | adantl 277 |
. . . . . . . . . . 11
           |
62 | 59, 61 | expcld 10653 |
. . . . . . . . . 10
               |
63 | 58, 62 | mulcld 7977 |
. . . . . . . . 9
                       |
64 | 54, 63 | mulcld 7977 |
. . . . . . . 8
                           |
65 | 50 | nnap0d 8964 |
. . . . . . . 8
 

    #   |
66 | 48, 51, 64, 65 | fsumdivapc 11457 |
. . . . . . 7
 

 
                                                        |
67 | 55, 61 | expcld 10653 |
. . . . . . . . . . 11
               |
68 | 61, 12 | syl 14 |
. . . . . . . . . . . 12
               |
69 | 68 | nncnd 8932 |
. . . . . . . . . . 11
               |
70 | 68 | nnap0d 8964 |
. . . . . . . . . . 11
             #   |
71 | 67, 69, 70 | divclapd 8746 |
. . . . . . . . . 10
                     |
72 | 33 | eftvalcn 11664 |
. . . . . . . . . . . 12
                           |
73 | 59, 57, 72 | syl2anc 411 |
. . . . . . . . . . 11
                               |
74 | 59, 57 | expcld 10653 |
. . . . . . . . . . . 12
                 |
75 | | faccl 10714 |
. . . . . . . . . . . . . 14
  
        |
76 | 57, 75 | syl 14 |
. . . . . . . . . . . . 13
                 |
77 | 76 | nncnd 8932 |
. . . . . . . . . . . 12
                 |
78 | 76 | nnap0d 8964 |
. . . . . . . . . . . 12
               #   |
79 | 74, 77, 78 | divclapd 8746 |
. . . . . . . . . . 11
                         |
80 | 73, 79 | eqeltrd 2254 |
. . . . . . . . . 10
                 |
81 | 71, 80 | mulcld 7977 |
. . . . . . . . 9
                             |
82 | | oveq2 5882 |
. . . . . . . . . . 11
                   |
83 | | fveq2 5515 |
. . . . . . . . . . 11
                   |
84 | 82, 83 | oveq12d 5892 |
. . . . . . . . . 10
                                   |
85 | | oveq2 5882 |
. . . . . . . . . . 11
               |
86 | 85 | fveq2d 5519 |
. . . . . . . . . 10
                       |
87 | 84, 86 | oveq12d 5892 |
. . . . . . . . 9
                                                       |
88 | 46, 47, 81, 87 | fisumrev2 11453 |
. . . . . . . 8
 

                                                              |
89 | 33 | eftvalcn 11664 |
. . . . . . . . . . . . . 14
 
                 |
90 | 59, 61, 89 | syl2anc 411 |
. . . . . . . . . . . . 13
                         |
91 | 90 | oveq2d 5890 |
. . . . . . . . . . . 12
                                                         |
92 | 76, 68 | nnmulcld 8967 |
. . . . . . . . . . . . . . 15
                       |
93 | 92 | nncnd 8932 |
. . . . . . . . . . . . . 14
                       |
94 | 77, 69, 78, 70 | mulap0d 8614 |
. . . . . . . . . . . . . 14
                     #   |
95 | 63, 93, 94 | divrecap2d 8750 |
. . . . . . . . . . . . 13
                                                                 |
96 | 58, 77, 62, 69, 78, 70 | divmuldivapd 8788 |
. . . . . . . . . . . . 13
                                                               |
97 | | bcval2 10729 |
. . . . . . . . . . . . . . . . 17
                           |
98 | 97 | adantl 277 |
. . . . . . . . . . . . . . . 16
                               |
99 | 98 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
                                           |
100 | 51 | adantr 276 |
. . . . . . . . . . . . . . . . 17
               |
101 | 65 | adantr 276 |
. . . . . . . . . . . . . . . . 17
             #   |
102 | 100, 93, 100, 94, 101 | divdiv32apd 8772 |
. . . . . . . . . . . . . . . 16
                                                           |
103 | 100, 101 | dividapd 8742 |
. . . . . . . . . . . . . . . . 17
                     |
104 | 103 | oveq1d 5889 |
. . . . . . . . . . . . . . . 16
                                                 |
105 | 102, 104 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
                                                 |
106 | 99, 105 | eqtrd 2210 |
. . . . . . . . . . . . . 14
                                 |
107 | 106 | oveq1d 5889 |
. . . . . . . . . . . . 13
                                                             |
108 | 95, 96, 107 | 3eqtr4rd 2221 |
. . . . . . . . . . . 12
                                                           |
109 | 91, 108 | eqtr4d 2213 |
. . . . . . . . . . 11
                                                     |
110 | | nn0cn 9185 |
. . . . . . . . . . . . . . . . 17

  |
111 | 110 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
           |
112 | 111 | addid2d 8106 |
. . . . . . . . . . . . . . 15
             |
113 | 112 | oveq1d 5889 |
. . . . . . . . . . . . . 14
                 |
114 | 113 | oveq2d 5890 |
. . . . . . . . . . . . 13
                         |
115 | 113 | fveq2d 5519 |
. . . . . . . . . . . . 13
                         |
116 | 114, 115 | oveq12d 5892 |
. . . . . . . . . . . 12
                                           |
117 | 113 | oveq2d 5890 |
. . . . . . . . . . . . . 14
                     |
118 | | nn0cn 9185 |
. . . . . . . . . . . . . . . 16

  |
119 | 61, 118 | syl 14 |
. . . . . . . . . . . . . . 15
           |
120 | 111, 119 | nncand 8272 |
. . . . . . . . . . . . . 14
               |
121 | 117, 120 | eqtrd 2210 |
. . . . . . . . . . . . 13
                 |
122 | 121 | fveq2d 5519 |
. . . . . . . . . . . 12
                         |
123 | 116, 122 | oveq12d 5892 |
. . . . . . . . . . 11
                                                             |
124 | 54, 63, 100, 101 | div23apd 8784 |
. . . . . . . . . . 11
                                                       |
125 | 109, 123,
124 | 3eqtr4rd 2221 |
. . . . . . . . . 10
                                                               |
126 | 125 | sumeq2dv 11375 |
. . . . . . . . 9
 

                            
                                     |
127 | | oveq2 5882 |
. . . . . . . . . . . . 13
           |
128 | 127 | oveq2d 5890 |
. . . . . . . . . . . 12
                   |
129 | 127 | fveq2d 5519 |
. . . . . . . . . . . 12
                   |
130 | 128, 129 | oveq12d 5892 |
. . . . . . . . . . 11
                                       |
131 | 127 | oveq2d 5890 |
. . . . . . . . . . . 12
               |
132 | 131 | fveq2d 5519 |
. . . . . . . . . . 11
                       |
133 | 130, 132 | oveq12d 5892 |
. . . . . . . . . 10
                                                               |
134 | 133 | cbvsumv 11368 |
. . . . . . . . 9
                                                                         |
135 | 126, 134 | eqtrdi 2226 |
. . . . . . . 8
 

                                                                  |
136 | 88, 135 | eqtr4d 2213 |
. . . . . . 7
 

                        
                             |
137 | 66, 136 | eqtr4d 2213 |
. . . . . 6
 

 
                                                    |
138 | 45, 137 | eqtrd 2210 |
. . . . 5
 

                                      |
139 | 39, 138 | eqtrd 2210 |
. . . 4
 

    
                         |
140 | 27 | efcllem 11666 |
. . . . 5
                         |
141 | 26, 140 | syl 14 |
. . . 4
                     |
142 | 33 | efcllem 11666 |
. . . . 5
     |
143 | 2, 142 | syl 14 |
. . . 4
     |
144 | 7 | efcllem 11666 |
. . . . 5
     |
145 | 1, 144 | syl 14 |
. . . 4
     |
146 | 9, 30, 32, 35, 37, 139, 141, 143, 145 | mertensabs 11544 |
. . 3
     
                        |
147 | | efval 11668 |
. . . . 5
                  |
148 | 1, 147 | syl 14 |
. . . 4
                  |
149 | | efval 11668 |
. . . . 5
                  |
150 | 2, 149 | syl 14 |
. . . 4
                  |
151 | 148, 150 | oveq12d 5892 |
. . 3
                                     |
152 | 146, 151 | breqtrrd 4031 |
. 2
                |
153 | | climuni 11300 |
. 2
                           
              |
154 | 6, 152, 153 | syl2anc 411 |
1
    
              |