Proof of Theorem 2vmadivsumlem
Step | Hyp | Ref
| Expression |
1 | | vmalogdivsum2 22919 |
. . 3
   
  
           Λ                           |
2 | 1 | a1i 11 |
. 2
                   Λ                            |
3 | | fzfid 11911 |
. . . . . . 7
 
              |
4 | | elfznn 11594 |
. . . . . . . . . . 11
           |
5 | 4 | adantl 466 |
. . . . . . . . . 10
               
  |
6 | | vmacl 22588 |
. . . . . . . . . 10
 Λ    |
7 | 5, 6 | syl 16 |
. . . . . . . . 9
               
Λ    |
8 | 7, 5 | nndivred 10480 |
. . . . . . . 8
               
 Λ     |
9 | | fzfid 11911 |
. . . . . . . . 9
               
      
     |
10 | | elfznn 11594 |
. . . . . . . . . . . 12
             |
11 | 10 | adantl 466 |
. . . . . . . . . . 11
   
                       
  |
12 | | vmacl 22588 |
. . . . . . . . . . 11
 Λ    |
13 | 11, 12 | syl 16 |
. . . . . . . . . 10
   
                       
Λ    |
14 | 13, 11 | nndivred 10480 |
. . . . . . . . 9
   
                       
 Λ     |
15 | 9, 14 | fsumrecl 13328 |
. . . . . . . 8
               
             Λ     |
16 | 8, 15 | remulcld 9524 |
. . . . . . 7
               
  Λ                Λ      |
17 | 3, 16 | fsumrecl 13328 |
. . . . . 6
 
                Λ                Λ      |
18 | | elioore 11440 |
. . . . . . . 8
   
  |
19 | 18 | adantl 466 |
. . . . . . 7
 
      |
20 | | eliooord 11465 |
. . . . . . . . 9
   
    |
21 | 20 | adantl 466 |
. . . . . . . 8
 
    
   |
22 | 21 | simpld 459 |
. . . . . . 7
 
      |
23 | 19, 22 | rplogcld 22210 |
. . . . . 6
 
          |
24 | 17, 23 | rerpdivcld 11164 |
. . . . 5
 
                 Λ                Λ           |
25 | | 1rp 11105 |
. . . . . . . . 9
 |
26 | 25 | a1i 11 |
. . . . . . . 8
 
      |
27 | | 1red 9511 |
. . . . . . . . 9
 
      |
28 | 27, 19, 22 | ltled 9632 |
. . . . . . . 8
 
      |
29 | 19, 26, 28 | rpgecld 11172 |
. . . . . . 7
 
      |
30 | 29 | relogcld 22204 |
. . . . . 6
 
          |
31 | 30 | rehalfcld 10681 |
. . . . 5
 
            |
32 | 24, 31 | resubcld 9886 |
. . . 4
 
                  Λ                Λ                  |
33 | 32 | recnd 9522 |
. . 3
 
                  Λ                Λ                  |
34 | 29 | adantr 465 |
. . . . . . . . . 10
               
  |
35 | 5 | nnrpd 11136 |
. . . . . . . . . 10
               
  |
36 | 34, 35 | rpdivcld 11154 |
. . . . . . . . 9
               
    |
37 | 36 | relogcld 22204 |
. . . . . . . 8
               
        |
38 | 8, 37 | remulcld 9524 |
. . . . . . 7
               
  Λ            |
39 | 3, 38 | fsumrecl 13328 |
. . . . . 6
 
                Λ            |
40 | 39, 23 | rerpdivcld 11164 |
. . . . 5
 
                 Λ                 |
41 | 40, 31 | resubcld 9886 |
. . . 4
 
                  Λ                        |
42 | 41 | recnd 9522 |
. . 3
 
                  Λ                        |
43 | 17 | recnd 9522 |
. . . . . . 7
 
                Λ                Λ      |
44 | 39 | recnd 9522 |
. . . . . . 7
 
                Λ            |
45 | 30 | recnd 9522 |
. . . . . . 7
 
          |
46 | 23 | rpne0d 11142 |
. . . . . . 7
 
          |
47 | 43, 44, 45, 46 | divsubdird 10256 |
. . . . . 6
 
                  Λ                Λ                Λ                              Λ                Λ                      Λ                  |
48 | 8 | recnd 9522 |
. . . . . . . . . 10
               
 Λ     |
49 | 15 | recnd 9522 |
. . . . . . . . . 10
               
             Λ     |
50 | 37 | recnd 9522 |
. . . . . . . . . 10
               
        |
51 | 48, 49, 50 | subdid 9910 |
. . . . . . . . 9
               
  Λ           
     Λ              Λ                Λ      Λ             |
52 | 51 | sumeq2dv 13297 |
. . . . . . . 8
 
                Λ                 Λ           
            Λ                Λ      Λ             |
53 | 16 | recnd 9522 |
. . . . . . . . 9
               
  Λ                Λ      |
54 | 38 | recnd 9522 |
. . . . . . . . 9
               
  Λ            |
55 | 3, 53, 54 | fsumsub 13372 |
. . . . . . . 8
 
                 Λ                Λ      Λ                        Λ                Λ                Λ             |
56 | 52, 55 | eqtrd 2495 |
. . . . . . 7
 
                Λ                 Λ                        Λ                Λ                Λ             |
57 | 56 | oveq1d 6214 |
. . . . . 6
 
                 Λ                 Λ                              Λ                Λ                Λ                  |
58 | 24 | recnd 9522 |
. . . . . . 7
 
                 Λ                Λ           |
59 | 40 | recnd 9522 |
. . . . . . 7
 
                 Λ                 |
60 | 31 | recnd 9522 |
. . . . . . 7
 
            |
61 | 58, 59, 60 | nnncan2d 9864 |
. . . . . 6
 
                   Λ                Λ                  
           Λ                                     Λ                Λ                      Λ                  |
62 | 47, 57, 61 | 3eqtr4d 2505 |
. . . . 5
 
                 Λ                 Λ                               Λ                Λ                  
           Λ                         |
63 | 62 | mpteq2dva 4485 |
. . . 4
                  Λ                 Λ                                    Λ                Λ                              Λ                          |
64 | | 1red 9511 |
. . . . 5
   |
65 | 3, 8 | fsumrecl 13328 |
. . . . . . 7
 
               Λ     |
66 | 65, 23 | rerpdivcld 11164 |
. . . . . 6
 
                Λ          |
67 | | 2vmadivsum.1 |
. . . . . . . 8
   |
68 | 67 | rpred 11137 |
. . . . . . 7
   |
69 | 68 | adantr 465 |
. . . . . 6
 
      |
70 | | ioossre 11467 |
. . . . . . . 8
    |
71 | | 1cnd 9512 |
. . . . . . . 8
   |
72 | | o1const 13214 |
. . . . . . . 8
                |
73 | 70, 71, 72 | sylancr 663 |
. . . . . . 7
           |
74 | 66 | recnd 9522 |
. . . . . . . 8
 
                Λ          |
75 | | 1cnd 9512 |
. . . . . . . 8
 
      |
76 | 65 | recnd 9522 |
. . . . . . . . . . . 12
 
               Λ     |
77 | 76, 45, 45, 46 | divsubdird 10256 |
. . . . . . . . . . 11
 
                 Λ                          Λ                     |
78 | 76, 45 | subcld 9829 |
. . . . . . . . . . . 12
 
                Λ          |
79 | 78, 45, 46 | divrecd 10220 |
. . . . . . . . . . 11
 
                 Λ                          Λ                 |
80 | 45, 46 | dividd 10215 |
. . . . . . . . . . . 12
 
                |
81 | 80 | oveq2d 6215 |
. . . . . . . . . . 11
 
                 Λ                                Λ           |
82 | 77, 79, 81 | 3eqtr3d 2503 |
. . . . . . . . . 10
 
                 Λ                            Λ           |
83 | 82 | mpteq2dva 4485 |
. . . . . . . . 9
                  Λ                   
  
          Λ            |
84 | 65, 30 | resubcld 9886 |
. . . . . . . . . 10
 
                Λ          |
85 | 27, 23 | rerpdivcld 11164 |
. . . . . . . . . 10
 
            |
86 | 29 | ex 434 |
. . . . . . . . . . . 12
        |
87 | 86 | ssrdv 3469 |
. . . . . . . . . . 11
      |
88 | | vmadivsum 22863 |
. . . . . . . . . . . 12

            Λ             |
89 | 88 | a1i 11 |
. . . . . . . . . . 11
              Λ              |
90 | 87, 89 | o1res2 13158 |
. . . . . . . . . 10
                 Λ              |
91 | | divlogrlim 22212 |
. . . . . . . . . . 11
   
         |
92 | | rlimo1 13211 |
. . . . . . . . . . 11
                             |
93 | 91, 92 | mp1i 12 |
. . . . . . . . . 10
                 |
94 | 84, 85, 90, 93 | o1mul2 13219 |
. . . . . . . . 9
                  Λ                     |
95 | 83, 94 | eqeltrrd 2543 |
. . . . . . . 8
                  Λ               |
96 | 74, 75, 95 | o1dif 13224 |
. . . . . . 7
                  Λ                       |
97 | 73, 96 | mpbird 232 |
. . . . . 6
                 Λ              |
98 | 68 | recnd 9522 |
. . . . . . 7
   |
99 | | o1const 13214 |
. . . . . . 7
                |
100 | 70, 98, 99 | sylancr 663 |
. . . . . 6
           |
101 | 66, 69, 97, 100 | o1mul2 13219 |
. . . . 5
                  Λ               |
102 | 66, 69 | remulcld 9524 |
. . . . 5
 
                 Λ           |
103 | 15, 37 | resubcld 9886 |
. . . . . . . . 9
               
              Λ            |
104 | 8, 103 | remulcld 9524 |
. . . . . . . 8
               
  Λ           
     Λ             |
105 | 3, 104 | fsumrecl 13328 |
. . . . . . 7
 
                Λ                 Λ             |
106 | 105 | recnd 9522 |
. . . . . 6
 
                Λ                 Λ             |
107 | 106, 45, 46 | divcld 10217 |
. . . . 5
 
                 Λ                 Λ                  |
108 | 106 | abscld 13039 |
. . . . . . . 8
 
                   Λ                 Λ              |
109 | 65, 69 | remulcld 9524 |
. . . . . . . 8
 
                Λ      |
110 | 104 | recnd 9522 |
. . . . . . . . . . 11
               
  Λ           
     Λ             |
111 | 110 | abscld 13039 |
. . . . . . . . . 10
               
     Λ                 Λ              |
112 | 3, 111 | fsumrecl 13328 |
. . . . . . . . 9
 
                   Λ           
     Λ              |
113 | 3, 110 | fsumabs 13381 |
. . . . . . . . 9
 
                   Λ                 Λ                           Λ           
     Λ              |
114 | 69 | adantr 465 |
. . . . . . . . . . . 12
               
  |
115 | 8, 114 | remulcld 9524 |
. . . . . . . . . . 11
               
  Λ      |
116 | 103 | recnd 9522 |
. . . . . . . . . . . . . 14
               
              Λ            |
117 | 48, 116 | absmuld 13057 |
. . . . . . . . . . . . 13
               
     Λ                 Λ                 Λ                     Λ              |
118 | | vmage0 22591 |
. . . . . . . . . . . . . . . . 17
 Λ    |
119 | 5, 118 | syl 16 |
. . . . . . . . . . . . . . . 16
               
Λ    |
120 | 7, 35, 119 | divge0d 11173 |
. . . . . . . . . . . . . . 15
               
 Λ     |
121 | 8, 120 | absidd 13026 |
. . . . . . . . . . . . . 14
               
    Λ     Λ     |
122 | 121 | oveq1d 6214 |
. . . . . . . . . . . . 13
               
     Λ                     Λ              Λ                    Λ              |
123 | 117, 122 | eqtrd 2495 |
. . . . . . . . . . . 12
               
     Λ                 Λ              Λ                    Λ              |
124 | 116 | abscld 13039 |
. . . . . . . . . . . . 13
               
                 Λ             |
125 | 36 | rpred 11137 |
. . . . . . . . . . . . . . 15
               
    |
126 | 5 | nncnd 10448 |
. . . . . . . . . . . . . . . . . 18
               
  |
127 | 126 | mulid2d 9514 |
. . . . . . . . . . . . . . . . 17
               
    |
128 | | fznnfl 11817 |
. . . . . . . . . . . . . . . . . . 19
         
     |
129 | 19, 128 | syl 16 |
. . . . . . . . . . . . . . . . . 18
 
            
     |
130 | 129 | simplbda 624 |
. . . . . . . . . . . . . . . . 17
               
  |
131 | 127, 130 | eqbrtrd 4419 |
. . . . . . . . . . . . . . . 16
               
    |
132 | | 1red 9511 |
. . . . . . . . . . . . . . . . 17
               
  |
133 | 19 | adantr 465 |
. . . . . . . . . . . . . . . . 17
               
  |
134 | 132, 133,
35 | lemuldivd 11182 |
. . . . . . . . . . . . . . . 16
               
  
     |
135 | 131, 134 | mpbid 210 |
. . . . . . . . . . . . . . 15
               
    |
136 | | 1re 9495 |
. . . . . . . . . . . . . . . 16
 |
137 | | elicopnf 11501 |
. . . . . . . . . . . . . . . 16
      
         |
138 | 136, 137 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     
        |
139 | 125, 135,
138 | sylanbrc 664 |
. . . . . . . . . . . . . 14
               
       |
140 | | 2vmadivsum.2 |
. . . . . . . . . . . . . . 15
                     Λ           |
141 | 140 | ad2antrr 725 |
. . . . . . . . . . . . . 14
               
                    Λ           |
142 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . 21
 Λ  Λ    |
143 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
   |
144 | 142, 143 | oveq12d 6217 |
. . . . . . . . . . . . . . . . . . . 20
  Λ    Λ     |
145 | 144 | cbvsumv 13290 |
. . . . . . . . . . . . . . . . . . 19
           Λ              Λ    |
146 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . 21
               |
147 | 146 | oveq2d 6215 |
. . . . . . . . . . . . . . . . . . . 20
                       |
148 | 147 | sumeq1d 13295 |
. . . . . . . . . . . . . . . . . . 19
              Λ                Λ     |
149 | 145, 148 | syl5eq 2507 |
. . . . . . . . . . . . . . . . . 18
              Λ                Λ     |
150 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . 18
               |
151 | 149, 150 | oveq12d 6217 |
. . . . . . . . . . . . . . . . 17
               Λ                      Λ            |
152 | 151 | fveq2d 5802 |
. . . . . . . . . . . . . . . 16
                  Λ                    
     Λ             |
153 | 152 | breq1d 4409 |
. . . . . . . . . . . . . . 15
                   Λ                          Λ              |
154 | 153 | rspcv 3173 |
. . . . . . . . . . . . . 14
     
 
        
          Λ                    
     Λ          
   |
155 | 139, 141,
154 | sylc 60 |
. . . . . . . . . . . . 13
               
                 Λ             |
156 | 124, 114,
8, 120, 155 | lemul2ad 10383 |
. . . . . . . . . . . 12
               
  Λ                    Λ              Λ      |
157 | 123, 156 | eqbrtrd 4419 |
. . . . . . . . . . 11
               
     Λ                 Λ              Λ      |
158 | 3, 111, 115, 157 | fsumle 13379 |
. . . . . . . . . 10
 
                   Λ           
     Λ                        Λ      |
159 | 98 | adantr 465 |
. . . . . . . . . . 11
 
      |
160 | 3, 159, 48 | fsummulc1 13369 |
. . . . . . . . . 10
 
                Λ                Λ      |
161 | 158, 160 | breqtrrd 4425 |
. . . . . . . . 9
 
                   Λ           
     Λ                        Λ      |
162 | 108, 112,
109, 113, 161 | letrd 9638 |
. . . . . . . 8
 
                   Λ                 Λ                        Λ      |
163 | 108, 109,
23, 162 | lediv1dd 11191 |
. . . . . . 7
 
                    Λ           
     Λ                              Λ           |
164 | 106, 45, 46 | absdivd 13058 |
. . . . . . . 8
 
                    Λ                 Λ                                 Λ           
     Λ                       |
165 | 23 | rpge0d 11141 |
. . . . . . . . . 10
 
          |
166 | 30, 165 | absidd 13026 |
. . . . . . . . 9
 
                  |
167 | 166 | oveq2d 6215 |
. . . . . . . 8
 
                    Λ           
     Λ                                     Λ           
     Λ                   |
168 | 164, 167 | eqtrd 2495 |
. . . . . . 7
 
                    Λ                 Λ                                 Λ           
     Λ                   |
169 | 3, 8, 120 | fsumge0 13375 |
. . . . . . . . . . 11
 
    
          Λ     |
170 | 65, 23, 169 | divge0d 11173 |
. . . . . . . . . 10
 
                Λ          |
171 | 67 | adantr 465 |
. . . . . . . . . . 11
 
      |
172 | 171 | rpge0d 11141 |
. . . . . . . . . 10
 
      |
173 | 66, 69, 170, 172 | mulge0d 10026 |
. . . . . . . . 9
 
                 Λ           |
174 | 102, 173 | absidd 13026 |
. . . . . . . 8
 
                    Λ                       Λ           |
175 | 76, 159, 45, 46 | div23d 10254 |
. . . . . . . 8
 
                 Λ                      Λ           |
176 | 174, 175 | eqtr4d 2498 |
. . . . . . 7
 
                    Λ                       Λ           |
177 | 163, 168,
176 | 3brtr4d 4429 |
. . . . . 6
 
                    Λ                 Λ                                 Λ            |
178 | 177 | adantrr 716 |
. . . . 5
 
                      Λ                 Λ                                 Λ            |
179 | 64, 101, 102, 107, 178 | o1le 13247 |
. . . 4
                  Λ                 Λ                      |
180 | 63, 179 | eqeltrrd 2543 |
. . 3
                    Λ                Λ                              Λ                             |
181 | 33, 42, 180 | o1dif 13224 |
. 2
                    Λ                Λ                                      Λ                             |
182 | 2, 181 | mpbird 232 |
1
                   Λ                Λ                      |