Proof of Theorem 2vmadivsumlem
Step | Hyp | Ref
| Expression |
1 | | vmalogdivsum2 25227 |
. . 3
Λ |
2 | 1 | a1i 11 |
. 2
Λ |
3 | | fzfid 12772 |
. . . . . . 7
|
4 | | elfznn 12370 |
. . . . . . . . . . 11
|
5 | 4 | adantl 482 |
. . . . . . . . . 10
|
6 | | vmacl 24844 |
. . . . . . . . . 10
Λ |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
Λ |
8 | 7, 5 | nndivred 11069 |
. . . . . . . 8
Λ |
9 | | fzfid 12772 |
. . . . . . . . 9
|
10 | | elfznn 12370 |
. . . . . . . . . . . 12
|
11 | 10 | adantl 482 |
. . . . . . . . . . 11
|
12 | | vmacl 24844 |
. . . . . . . . . . 11
Λ |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
Λ |
14 | 13, 11 | nndivred 11069 |
. . . . . . . . 9
Λ |
15 | 9, 14 | fsumrecl 14465 |
. . . . . . . 8
Λ |
16 | 8, 15 | remulcld 10070 |
. . . . . . 7
Λ Λ |
17 | 3, 16 | fsumrecl 14465 |
. . . . . 6
Λ Λ |
18 | | elioore 12205 |
. . . . . . . 8
|
19 | 18 | adantl 482 |
. . . . . . 7
|
20 | | eliooord 12233 |
. . . . . . . . 9
|
21 | 20 | adantl 482 |
. . . . . . . 8
|
22 | 21 | simpld 475 |
. . . . . . 7
|
23 | 19, 22 | rplogcld 24375 |
. . . . . 6
|
24 | 17, 23 | rerpdivcld 11903 |
. . . . 5
Λ Λ |
25 | | 1rp 11836 |
. . . . . . . . 9
|
26 | 25 | a1i 11 |
. . . . . . . 8
|
27 | | 1red 10055 |
. . . . . . . . 9
|
28 | 27, 19, 22 | ltled 10185 |
. . . . . . . 8
|
29 | 19, 26, 28 | rpgecld 11911 |
. . . . . . 7
|
30 | 29 | relogcld 24369 |
. . . . . 6
|
31 | 30 | rehalfcld 11279 |
. . . . 5
|
32 | 24, 31 | resubcld 10458 |
. . . 4
Λ Λ |
33 | 32 | recnd 10068 |
. . 3
Λ Λ |
34 | 29 | adantr 481 |
. . . . . . . . . 10
|
35 | 5 | nnrpd 11870 |
. . . . . . . . . 10
|
36 | 34, 35 | rpdivcld 11889 |
. . . . . . . . 9
|
37 | 36 | relogcld 24369 |
. . . . . . . 8
|
38 | 8, 37 | remulcld 10070 |
. . . . . . 7
Λ |
39 | 3, 38 | fsumrecl 14465 |
. . . . . 6
Λ |
40 | 39, 23 | rerpdivcld 11903 |
. . . . 5
Λ |
41 | 40, 31 | resubcld 10458 |
. . . 4
Λ |
42 | 41 | recnd 10068 |
. . 3
Λ |
43 | 17 | recnd 10068 |
. . . . . . 7
Λ Λ |
44 | 39 | recnd 10068 |
. . . . . . 7
Λ |
45 | 30 | recnd 10068 |
. . . . . . 7
|
46 | 23 | rpne0d 11877 |
. . . . . . 7
|
47 | 43, 44, 45, 46 | divsubdird 10840 |
. . . . . 6
Λ Λ Λ Λ Λ Λ |
48 | 8 | recnd 10068 |
. . . . . . . . . 10
Λ |
49 | 15 | recnd 10068 |
. . . . . . . . . 10
Λ |
50 | 37 | recnd 10068 |
. . . . . . . . . 10
|
51 | 48, 49, 50 | subdid 10486 |
. . . . . . . . 9
Λ
Λ Λ Λ Λ |
52 | 51 | sumeq2dv 14433 |
. . . . . . . 8
Λ Λ
Λ Λ Λ |
53 | 16 | recnd 10068 |
. . . . . . . . 9
Λ Λ |
54 | 38 | recnd 10068 |
. . . . . . . . 9
Λ |
55 | 3, 53, 54 | fsumsub 14520 |
. . . . . . . 8
Λ Λ Λ Λ Λ Λ |
56 | 52, 55 | eqtrd 2656 |
. . . . . . 7
Λ Λ Λ Λ Λ |
57 | 56 | oveq1d 6665 |
. . . . . 6
Λ Λ Λ Λ Λ |
58 | 24 | recnd 10068 |
. . . . . . 7
Λ Λ |
59 | 40 | recnd 10068 |
. . . . . . 7
Λ |
60 | 31 | recnd 10068 |
. . . . . . 7
|
61 | 58, 59, 60 | nnncan2d 10427 |
. . . . . 6
Λ Λ
Λ Λ Λ Λ |
62 | 47, 57, 61 | 3eqtr4d 2666 |
. . . . 5
Λ Λ Λ Λ
Λ |
63 | 62 | mpteq2dva 4744 |
. . . 4
Λ Λ Λ Λ Λ |
64 | | 1red 10055 |
. . . . 5
|
65 | 3, 8 | fsumrecl 14465 |
. . . . . . 7
Λ |
66 | 65, 23 | rerpdivcld 11903 |
. . . . . 6
Λ |
67 | | 2vmadivsum.1 |
. . . . . . . 8
|
68 | 67 | rpred 11872 |
. . . . . . 7
|
69 | 68 | adantr 481 |
. . . . . 6
|
70 | | ioossre 12235 |
. . . . . . . 8
|
71 | | 1cnd 10056 |
. . . . . . . 8
|
72 | | o1const 14350 |
. . . . . . . 8
|
73 | 70, 71, 72 | sylancr 695 |
. . . . . . 7
|
74 | 66 | recnd 10068 |
. . . . . . . 8
Λ |
75 | | 1cnd 10056 |
. . . . . . . 8
|
76 | 65 | recnd 10068 |
. . . . . . . . . . . 12
Λ |
77 | 76, 45, 45, 46 | divsubdird 10840 |
. . . . . . . . . . 11
Λ Λ |
78 | 76, 45 | subcld 10392 |
. . . . . . . . . . . 12
Λ |
79 | 78, 45, 46 | divrecd 10804 |
. . . . . . . . . . 11
Λ Λ |
80 | 45, 46 | dividd 10799 |
. . . . . . . . . . . 12
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . . 11
Λ Λ |
82 | 77, 79, 81 | 3eqtr3d 2664 |
. . . . . . . . . 10
Λ Λ |
83 | 82 | mpteq2dva 4744 |
. . . . . . . . 9
Λ
Λ |
84 | 65, 30 | resubcld 10458 |
. . . . . . . . . 10
Λ |
85 | 27, 23 | rerpdivcld 11903 |
. . . . . . . . . 10
|
86 | 29 | ex 450 |
. . . . . . . . . . . 12
|
87 | 86 | ssrdv 3609 |
. . . . . . . . . . 11
|
88 | | vmadivsum 25171 |
. . . . . . . . . . . 12
Λ |
89 | 88 | a1i 11 |
. . . . . . . . . . 11
Λ |
90 | 87, 89 | o1res2 14294 |
. . . . . . . . . 10
Λ |
91 | | divlogrlim 24381 |
. . . . . . . . . . 11
|
92 | | rlimo1 14347 |
. . . . . . . . . . 11
|
93 | 91, 92 | mp1i 13 |
. . . . . . . . . 10
|
94 | 84, 85, 90, 93 | o1mul2 14355 |
. . . . . . . . 9
Λ |
95 | 83, 94 | eqeltrrd 2702 |
. . . . . . . 8
Λ |
96 | 74, 75, 95 | o1dif 14360 |
. . . . . . 7
Λ |
97 | 73, 96 | mpbird 247 |
. . . . . 6
Λ |
98 | 68 | recnd 10068 |
. . . . . . 7
|
99 | | o1const 14350 |
. . . . . . 7
|
100 | 70, 98, 99 | sylancr 695 |
. . . . . 6
|
101 | 66, 69, 97, 100 | o1mul2 14355 |
. . . . 5
Λ |
102 | 66, 69 | remulcld 10070 |
. . . . 5
Λ |
103 | 15, 37 | resubcld 10458 |
. . . . . . . . 9
Λ |
104 | 8, 103 | remulcld 10070 |
. . . . . . . 8
Λ
Λ |
105 | 3, 104 | fsumrecl 14465 |
. . . . . . 7
Λ Λ |
106 | 105 | recnd 10068 |
. . . . . 6
Λ Λ |
107 | 106, 45, 46 | divcld 10801 |
. . . . 5
Λ Λ |
108 | 106 | abscld 14175 |
. . . . . . . 8
Λ Λ |
109 | 65, 69 | remulcld 10070 |
. . . . . . . 8
Λ |
110 | 104 | recnd 10068 |
. . . . . . . . . . 11
Λ
Λ |
111 | 110 | abscld 14175 |
. . . . . . . . . 10
Λ Λ |
112 | 3, 111 | fsumrecl 14465 |
. . . . . . . . 9
Λ
Λ |
113 | 3, 110 | fsumabs 14533 |
. . . . . . . . 9
Λ Λ Λ
Λ |
114 | 69 | adantr 481 |
. . . . . . . . . . . 12
|
115 | 8, 114 | remulcld 10070 |
. . . . . . . . . . 11
Λ |
116 | 103 | recnd 10068 |
. . . . . . . . . . . . . 14
Λ |
117 | 48, 116 | absmuld 14193 |
. . . . . . . . . . . . 13
Λ Λ Λ Λ |
118 | | vmage0 24847 |
. . . . . . . . . . . . . . . . 17
Λ |
119 | 5, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
Λ |
120 | 7, 35, 119 | divge0d 11912 |
. . . . . . . . . . . . . . 15
Λ |
121 | 8, 120 | absidd 14161 |
. . . . . . . . . . . . . 14
Λ Λ |
122 | 121 | oveq1d 6665 |
. . . . . . . . . . . . 13
Λ Λ Λ Λ |
123 | 117, 122 | eqtrd 2656 |
. . . . . . . . . . . 12
Λ Λ Λ Λ |
124 | 116 | abscld 14175 |
. . . . . . . . . . . . 13
Λ |
125 | 36 | rpred 11872 |
. . . . . . . . . . . . . . 15
|
126 | 5 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
|
127 | 126 | mulid2d 10058 |
. . . . . . . . . . . . . . . . 17
|
128 | | fznnfl 12661 |
. . . . . . . . . . . . . . . . . . 19
|
129 | 19, 128 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
130 | 129 | simplbda 654 |
. . . . . . . . . . . . . . . . 17
|
131 | 127, 130 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . 16
|
132 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
|
133 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
134 | 132, 133,
35 | lemuldivd 11921 |
. . . . . . . . . . . . . . . 16
|
135 | 131, 134 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
136 | | 1re 10039 |
. . . . . . . . . . . . . . . 16
|
137 | | elicopnf 12269 |
. . . . . . . . . . . . . . . 16
|
138 | 136, 137 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
139 | 125, 135,
138 | sylanbrc 698 |
. . . . . . . . . . . . . 14
|
140 | | 2vmadivsum.2 |
. . . . . . . . . . . . . . 15
Λ |
141 | 140 | ad2antrr 762 |
. . . . . . . . . . . . . 14
Λ |
142 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
Λ Λ |
143 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
|
144 | 142, 143 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
Λ Λ |
145 | 144 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . . 19
Λ Λ |
146 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
147 | 146 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
|
148 | 147 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . . 19
Λ Λ |
149 | 145, 148 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
Λ Λ |
150 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
151 | 149, 150 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
Λ Λ |
152 | 151 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
Λ
Λ |
153 | 152 | breq1d 4663 |
. . . . . . . . . . . . . . 15
Λ Λ |
154 | 153 | rspcv 3305 |
. . . . . . . . . . . . . 14
Λ
Λ
|
155 | 139, 141,
154 | sylc 65 |
. . . . . . . . . . . . 13
Λ |
156 | 124, 114,
8, 120, 155 | lemul2ad 10964 |
. . . . . . . . . . . 12
Λ Λ Λ |
157 | 123, 156 | eqbrtrd 4675 |
. . . . . . . . . . 11
Λ Λ Λ |
158 | 3, 111, 115, 157 | fsumle 14531 |
. . . . . . . . . 10
Λ
Λ Λ |
159 | 98 | adantr 481 |
. . . . . . . . . . 11
|
160 | 3, 159, 48 | fsummulc1 14517 |
. . . . . . . . . 10
Λ Λ |
161 | 158, 160 | breqtrrd 4681 |
. . . . . . . . 9
Λ
Λ Λ |
162 | 108, 112,
109, 113, 161 | letrd 10194 |
. . . . . . . 8
Λ Λ Λ |
163 | 108, 109,
23, 162 | lediv1dd 11930 |
. . . . . . 7
Λ
Λ Λ |
164 | 106, 45, 46 | absdivd 14194 |
. . . . . . . 8
Λ Λ Λ
Λ |
165 | 23 | rpge0d 11876 |
. . . . . . . . . 10
|
166 | 30, 165 | absidd 14161 |
. . . . . . . . 9
|
167 | 166 | oveq2d 6666 |
. . . . . . . 8
Λ
Λ Λ
Λ |
168 | 164, 167 | eqtrd 2656 |
. . . . . . 7
Λ Λ Λ
Λ |
169 | 3, 8, 120 | fsumge0 14527 |
. . . . . . . . . . 11
Λ |
170 | 65, 23, 169 | divge0d 11912 |
. . . . . . . . . 10
Λ |
171 | 67 | adantr 481 |
. . . . . . . . . . 11
|
172 | 171 | rpge0d 11876 |
. . . . . . . . . 10
|
173 | 66, 69, 170, 172 | mulge0d 10604 |
. . . . . . . . 9
Λ |
174 | 102, 173 | absidd 14161 |
. . . . . . . 8
Λ Λ |
175 | 76, 159, 45, 46 | div23d 10838 |
. . . . . . . 8
Λ Λ |
176 | 174, 175 | eqtr4d 2659 |
. . . . . . 7
Λ Λ |
177 | 163, 168,
176 | 3brtr4d 4685 |
. . . . . 6
Λ Λ Λ |
178 | 177 | adantrr 753 |
. . . . 5
Λ Λ Λ |
179 | 64, 101, 102, 107, 178 | o1le 14383 |
. . . 4
Λ Λ |
180 | 63, 179 | eqeltrrd 2702 |
. . 3
Λ Λ Λ |
181 | 33, 42, 180 | o1dif 14360 |
. 2
Λ Λ Λ |
182 | 2, 181 | mpbird 247 |
1
Λ Λ |