Step | Hyp | Ref
| Expression |
1 | | 1re 10039 |
. . . . . . . . . . 11
|
2 | | elicopnf 12269 |
. . . . . . . . . . 11
|
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
|
4 | 3 | simplbi 476 |
. . . . . . . . 9
|
5 | | 0red 10041 |
. . . . . . . . . 10
|
6 | | 1red 10055 |
. . . . . . . . . 10
|
7 | | 0lt1 10550 |
. . . . . . . . . . 11
|
8 | 7 | a1i 11 |
. . . . . . . . . 10
|
9 | 3 | simprbi 480 |
. . . . . . . . . 10
|
10 | 5, 6, 4, 8, 9 | ltletrd 10197 |
. . . . . . . . 9
|
11 | 4, 10 | elrpd 11869 |
. . . . . . . 8
|
12 | 11 | ssriv 3607 |
. . . . . . 7
|
13 | 12 | a1i 11 |
. . . . . 6
|
14 | | rpssre 11843 |
. . . . . 6
|
15 | 13, 14 | syl6ss 3615 |
. . . . 5
|
16 | 15 | resmptd 5452 |
. . . 4
|
17 | | oveq2 6658 |
. . . . . . . . . . . 12
|
18 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
19 | 18 | fveq2d 6195 |
. . . . . . . . . . . . 13
ψ ψ |
20 | 19, 18 | oveq12d 6668 |
. . . . . . . . . . . 12
ψ ψ |
21 | 17, 20 | jca 554 |
. . . . . . . . . . 11
ψ ψ |
22 | | oveq2 6658 |
. . . . . . . . . . . 12
|
23 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
24 | 23 | fveq2d 6195 |
. . . . . . . . . . . . 13
ψ ψ |
25 | 24, 23 | oveq12d 6668 |
. . . . . . . . . . . 12
ψ ψ |
26 | 22, 25 | jca 554 |
. . . . . . . . . . 11
ψ ψ |
27 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
28 | | 1div1e1 10717 |
. . . . . . . . . . . . 13
|
29 | 27, 28 | syl6eq 2672 |
. . . . . . . . . . . 12
|
30 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
31 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . 17
|
32 | 30, 31 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
33 | 32 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
ψ ψ |
34 | | 2pos 11112 |
. . . . . . . . . . . . . . . 16
|
35 | | 0re 10040 |
. . . . . . . . . . . . . . . . 17
|
36 | | chpeq0 24933 |
. . . . . . . . . . . . . . . . 17
ψ
|
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
ψ |
38 | 34, 37 | mpbir 221 |
. . . . . . . . . . . . . . 15
ψ |
39 | 33, 38 | syl6eq 2672 |
. . . . . . . . . . . . . 14
ψ |
40 | 39, 32 | oveq12d 6668 |
. . . . . . . . . . . . 13
ψ |
41 | | 0m0e0 11130 |
. . . . . . . . . . . . 13
|
42 | 40, 41 | syl6eq 2672 |
. . . . . . . . . . . 12
ψ |
43 | 29, 42 | jca 554 |
. . . . . . . . . . 11
ψ |
44 | | oveq2 6658 |
. . . . . . . . . . . 12
|
45 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
46 | 45 | fveq2d 6195 |
. . . . . . . . . . . . 13
ψ ψ |
47 | 46, 45 | oveq12d 6668 |
. . . . . . . . . . . 12
ψ ψ |
48 | 44, 47 | jca 554 |
. . . . . . . . . . 11
ψ ψ |
49 | 11 | rprege0d 11879 |
. . . . . . . . . . . . . 14
|
50 | | flge0nn0 12621 |
. . . . . . . . . . . . . 14
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . 13
|
52 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
|
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
|
54 | | nnuz 11723 |
. . . . . . . . . . . 12
|
55 | 53, 54 | syl6eleq 2711 |
. . . . . . . . . . 11
|
56 | | elfznn 12370 |
. . . . . . . . . . . . . 14
|
57 | 56 | adantl 482 |
. . . . . . . . . . . . 13
|
58 | 57 | nnrecred 11066 |
. . . . . . . . . . . 12
|
59 | 58 | recnd 10068 |
. . . . . . . . . . 11
|
60 | 57 | nnred 11035 |
. . . . . . . . . . . . . . 15
|
61 | | peano2rem 10348 |
. . . . . . . . . . . . . . 15
|
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . 14
|
63 | | chpcl 24850 |
. . . . . . . . . . . . . 14
ψ |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
ψ |
65 | 64, 62 | resubcld 10458 |
. . . . . . . . . . . 12
ψ
|
66 | 65 | recnd 10068 |
. . . . . . . . . . 11
ψ
|
67 | 21, 26, 43, 48, 55, 59, 66 | fsumparts 14538 |
. . . . . . . . . 10
..^ ψ ψ
ψ ..^ ψ |
68 | 4 | flcld 12599 |
. . . . . . . . . . . . 13
|
69 | | fzval3 12536 |
. . . . . . . . . . . . 13
..^ |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
..^ |
71 | 70 | eqcomd 2628 |
. . . . . . . . . . 11
..^ |
72 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 73 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
75 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
|
76 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 74, 75, 76 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
78 | 73 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
|
79 | 77, 78 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
80 | | chpcl 24850 |
. . . . . . . . . . . . . . . . 17
ψ |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . 16
ψ |
82 | 81 | recnd 10068 |
. . . . . . . . . . . . . . 15
ψ |
83 | 79 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
84 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . 18
|
85 | 78, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
86 | | chpcl 24850 |
. . . . . . . . . . . . . . . . 17
ψ |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
ψ |
88 | 87 | recnd 10068 |
. . . . . . . . . . . . . . 15
ψ |
89 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
90 | 74, 89 | subcld 10392 |
. . . . . . . . . . . . . . 15
|
91 | 82, 83, 88, 90 | sub4d 10441 |
. . . . . . . . . . . . . 14
ψ ψ ψ ψ
|
92 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | 73, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
94 | | chpp1 24881 |
. . . . . . . . . . . . . . . . . . 19
ψ ψ Λ |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ψ ψ Λ |
96 | | npcan 10290 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 74, 75, 96 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 97, 77 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
ψ ψ |
100 | 97 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
Λ Λ |
101 | 100 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
ψ
Λ ψ Λ |
102 | 95, 99, 101 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . 17
ψ ψ Λ |
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
ψ ψ ψ
Λ ψ |
104 | | vmacl 24844 |
. . . . . . . . . . . . . . . . . . 19
Λ |
105 | 73, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Λ |
106 | 105 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
Λ |
107 | 88, 106 | pncan2d 10394 |
. . . . . . . . . . . . . . . 16
ψ Λ ψ Λ |
108 | 103, 107 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
ψ ψ Λ |
109 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . . 18
|
110 | 74, 109 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
111 | 110, 74, 89 | nnncan2d 10427 |
. . . . . . . . . . . . . . . 16
|
112 | | pncan2 10288 |
. . . . . . . . . . . . . . . . 17
|
113 | 74, 75, 112 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
114 | 111, 113 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
115 | 108, 114 | oveq12d 6668 |
. . . . . . . . . . . . . 14
ψ ψ Λ |
116 | 91, 115 | eqtrd 2656 |
. . . . . . . . . . . . 13
ψ ψ Λ |
117 | 116 | oveq2d 6666 |
. . . . . . . . . . . 12
ψ ψ Λ |
118 | | peano2rem 10348 |
. . . . . . . . . . . . . . 15
Λ Λ |
119 | 105, 118 | syl 17 |
. . . . . . . . . . . . . 14
Λ |
120 | 119 | recnd 10068 |
. . . . . . . . . . . . 13
Λ |
121 | 73 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
122 | 120, 74, 121 | divrec2d 10805 |
. . . . . . . . . . . 12
Λ Λ |
123 | 117, 122 | eqtr4d 2659 |
. . . . . . . . . . 11
ψ ψ Λ |
124 | 71, 123 | sumeq12rdv 14438 |
. . . . . . . . . 10
..^ ψ ψ
Λ |
125 | 51 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 125, 75, 126 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 127 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
ψ ψ |
129 | | chpfl 24876 |
. . . . . . . . . . . . . . . . . . 19
ψ ψ |
130 | 4, 129 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ψ ψ |
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
ψ ψ |
132 | 131 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
ψ ψ |
133 | | chpcl 24850 |
. . . . . . . . . . . . . . . . . . 19
ψ |
134 | 4, 133 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ψ |
135 | 134 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
ψ |
136 | 53 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
137 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
|
138 | 135, 136,
137 | subsub3d 10422 |
. . . . . . . . . . . . . . . 16
ψ ψ |
139 | 132, 138 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
ψ ψ |
140 | 139 | oveq2d 6666 |
. . . . . . . . . . . . . 14
ψ ψ |
141 | 53 | nnrecred 11066 |
. . . . . . . . . . . . . . . 16
|
142 | 141 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
143 | | peano2cn 10208 |
. . . . . . . . . . . . . . . 16
ψ ψ |
144 | 135, 143 | syl 17 |
. . . . . . . . . . . . . . 15
ψ |
145 | 142, 144,
136 | subdid 10486 |
. . . . . . . . . . . . . 14
ψ ψ |
146 | 53 | nnne0d 11065 |
. . . . . . . . . . . . . . . . 17
|
147 | 144, 136,
146 | divrec2d 10805 |
. . . . . . . . . . . . . . . 16
ψ ψ |
148 | 147 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
ψ ψ |
149 | 136, 146 | recid2d 10797 |
. . . . . . . . . . . . . . 15
|
150 | 148, 149 | oveq12d 6668 |
. . . . . . . . . . . . . 14
ψ ψ |
151 | 140, 145,
150 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
ψ ψ |
152 | 75 | mul01i 10226 |
. . . . . . . . . . . . . 14
|
153 | 152 | a1i 11 |
. . . . . . . . . . . . 13
|
154 | 151, 153 | oveq12d 6668 |
. . . . . . . . . . . 12
ψ ψ |
155 | | peano2re 10209 |
. . . . . . . . . . . . . . . . 17
ψ ψ |
156 | 134, 155 | syl 17 |
. . . . . . . . . . . . . . . 16
ψ |
157 | 156, 53 | nndivred 11069 |
. . . . . . . . . . . . . . 15
ψ |
158 | 157 | recnd 10068 |
. . . . . . . . . . . . . 14
ψ |
159 | | subcl 10280 |
. . . . . . . . . . . . . 14
ψ ψ |
160 | 158, 75, 159 | sylancl 694 |
. . . . . . . . . . . . 13
ψ |
161 | 160 | subid1d 10381 |
. . . . . . . . . . . 12
ψ ψ |
162 | 154, 161 | eqtrd 2656 |
. . . . . . . . . . 11
ψ ψ |
163 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . . 19
|
164 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 163, 164 | mpdan 702 |
. . . . . . . . . . . . . . . . . 18
|
166 | 73, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
167 | 166 | nnrecred 11066 |
. . . . . . . . . . . . . . . 16
|
168 | 167 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
169 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . 18
|
170 | | pntrval.r |
. . . . . . . . . . . . . . . . . . . 20
ψ |
171 | 170 | pntrf 25252 |
. . . . . . . . . . . . . . . . . . 19
|
172 | 171 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . 18
|
173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
174 | 73, 173 | syl 17 |
. . . . . . . . . . . . . . . 16
|
175 | 174 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
176 | 168, 175 | mulneg1d 10483 |
. . . . . . . . . . . . . 14
|
177 | 74, 89 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
|
178 | 74, 110 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
|
179 | 166 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . 19
|
180 | 110, 177,
178, 179 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . 18
|
181 | 74 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . 21
|
182 | 181 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
|
183 | 182, 113 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
184 | 183 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
185 | 110 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . 21
|
186 | 110, 74 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . . 21
|
187 | 185, 186 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
|
188 | 73, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
189 | 188 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . 21
|
190 | 89, 74, 110, 121, 189 | divcan5d 10827 |
. . . . . . . . . . . . . . . . . . . 20
|
191 | 187, 190 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
|
192 | 89, 110, 74, 189, 121 | divcan5d 10827 |
. . . . . . . . . . . . . . . . . . 19
|
193 | 191, 192 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
194 | 180, 184,
193 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . 17
|
195 | 194 | negeqd 10275 |
. . . . . . . . . . . . . . . 16
|
196 | 73 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . 18
|
197 | 196 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
198 | 188 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . 18
|
199 | 198 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
200 | 197, 199 | negsubdi2d 10408 |
. . . . . . . . . . . . . . . 16
|
201 | 195, 200 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
|
202 | 73 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
|
203 | 77, 202 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
204 | 170 | pntrval 25251 |
. . . . . . . . . . . . . . . . 17
ψ |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . 16
ψ |
206 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
207 | 205, 206 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
ψ |
208 | 201, 207 | oveq12d 6668 |
. . . . . . . . . . . . . 14
ψ |
209 | 175, 178,
179 | divrec2d 10805 |
. . . . . . . . . . . . . . 15
|
210 | 209 | negeqd 10275 |
. . . . . . . . . . . . . 14
|
211 | 176, 208,
210 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
ψ |
212 | 71, 211 | sumeq12rdv 14438 |
. . . . . . . . . . . 12
..^ ψ |
213 | | fzfid 12772 |
. . . . . . . . . . . . 13
|
214 | 173, 165 | nndivred 11069 |
. . . . . . . . . . . . . . 15
|
215 | 73, 214 | syl 17 |
. . . . . . . . . . . . . 14
|
216 | 215 | recnd 10068 |
. . . . . . . . . . . . 13
|
217 | 213, 216 | fsumneg 14519 |
. . . . . . . . . . . 12
|
218 | 212, 217 | eqtrd 2656 |
. . . . . . . . . . 11
..^ ψ |
219 | 162, 218 | oveq12d 6668 |
. . . . . . . . . 10
ψ ..^ ψ ψ |
220 | 67, 124, 219 | 3eqtr3d 2664 |
. . . . . . . . 9
Λ ψ |
221 | | fzfid 12772 |
. . . . . . . . . . . . 13
|
222 | 72 | adantl 482 |
. . . . . . . . . . . . . 14
|
223 | 222, 214 | syl 17 |
. . . . . . . . . . . . 13
|
224 | 221, 223 | fsumrecl 14465 |
. . . . . . . . . . . 12
|
225 | 224 | recnd 10068 |
. . . . . . . . . . 11
|
226 | 4, 225 | syl 17 |
. . . . . . . . . 10
|
227 | 160, 226 | subnegd 10399 |
. . . . . . . . 9
ψ
ψ
|
228 | 220, 227 | eqtrd 2656 |
. . . . . . . 8
Λ ψ |
229 | 228 | oveq1d 6665 |
. . . . . . 7
Λ ψ ψ
ψ |
230 | 160, 226 | pncan2d 10394 |
. . . . . . 7
ψ
ψ
|
231 | 229, 230 | eqtrd 2656 |
. . . . . 6
Λ ψ |
232 | 231 | mpteq2ia 4740 |
. . . . 5
Λ ψ
|
233 | | fzfid 12772 |
. . . . . . . 8
|
234 | 72 | adantl 482 |
. . . . . . . . . . 11
|
235 | 234, 104 | syl 17 |
. . . . . . . . . 10
Λ |
236 | 235, 118 | syl 17 |
. . . . . . . . 9
Λ |
237 | 236, 234 | nndivred 11069 |
. . . . . . . 8
Λ |
238 | 233, 237 | fsumrecl 14465 |
. . . . . . 7
Λ |
239 | | rpre 11839 |
. . . . . . . . . . . 12
|
240 | 239 | adantl 482 |
. . . . . . . . . . 11
|
241 | 240, 133 | syl 17 |
. . . . . . . . . 10
ψ |
242 | 241, 155 | syl 17 |
. . . . . . . . 9
ψ |
243 | | rprege0 11847 |
. . . . . . . . . . . 12
|
244 | 243, 50 | syl 17 |
. . . . . . . . . . 11
|
245 | 244 | adantl 482 |
. . . . . . . . . 10
|
246 | 245, 52 | syl 17 |
. . . . . . . . 9
|
247 | 242, 246 | nndivred 11069 |
. . . . . . . 8
ψ |
248 | | peano2rem 10348 |
. . . . . . . 8
ψ
ψ |
249 | 247, 248 | syl 17 |
. . . . . . 7
ψ |
250 | | reex 10027 |
. . . . . . . . . . . 12
|
251 | 250, 14 | ssexi 4803 |
. . . . . . . . . . 11
|
252 | 251 | a1i 11 |
. . . . . . . . . 10
|
253 | 235, 234 | nndivred 11069 |
. . . . . . . . . . . . 13
Λ |
254 | 253 | recnd 10068 |
. . . . . . . . . . . 12
Λ |
255 | 233, 254 | fsumcl 14464 |
. . . . . . . . . . 11
Λ |
256 | | relogcl 24322 |
. . . . . . . . . . . . 13
|
257 | 256 | adantl 482 |
. . . . . . . . . . . 12
|
258 | 257 | recnd 10068 |
. . . . . . . . . . 11
|
259 | 255, 258 | subcld 10392 |
. . . . . . . . . 10
Λ |
260 | 234 | nnrecred 11066 |
. . . . . . . . . . . 12
|
261 | 233, 260 | fsumrecl 14465 |
. . . . . . . . . . 11
|
262 | 261, 257 | resubcld 10458 |
. . . . . . . . . 10
|
263 | | eqidd 2623 |
. . . . . . . . . 10
Λ Λ |
264 | | eqidd 2623 |
. . . . . . . . . 10
|
265 | 252, 259,
262, 263, 264 | offval2 6914 |
. . . . . . . . 9
Λ
Λ |
266 | 260 | recnd 10068 |
. . . . . . . . . . . 12
|
267 | 233, 254,
266 | fsumsub 14520 |
. . . . . . . . . . 11
Λ Λ |
268 | 235 | recnd 10068 |
. . . . . . . . . . . . 13
Λ |
269 | | 1cnd 10056 |
. . . . . . . . . . . . 13
|
270 | 234 | nncnd 11036 |
. . . . . . . . . . . . 13
|
271 | 234 | nnne0d 11065 |
. . . . . . . . . . . . 13
|
272 | 268, 269,
270, 271 | divsubdird 10840 |
. . . . . . . . . . . 12
Λ Λ |
273 | 272 | sumeq2dv 14433 |
. . . . . . . . . . 11
Λ
Λ |
274 | 261 | recnd 10068 |
. . . . . . . . . . . 12
|
275 | 255, 274,
258 | nnncan2d 10427 |
. . . . . . . . . . 11
Λ Λ |
276 | 267, 273,
275 | 3eqtr4rd 2667 |
. . . . . . . . . 10
Λ Λ |
277 | 276 | mpteq2dva 4744 |
. . . . . . . . 9
Λ Λ |
278 | 265, 277 | eqtrd 2656 |
. . . . . . . 8
Λ
Λ |
279 | | vmadivsum 25171 |
. . . . . . . . 9
Λ |
280 | 14 | a1i 11 |
. . . . . . . . . 10
|
281 | 262 | recnd 10068 |
. . . . . . . . . 10
|
282 | | 1red 10055 |
. . . . . . . . . 10
|
283 | | harmoniclbnd 24735 |
. . . . . . . . . . . . . 14
|
284 | 283 | adantl 482 |
. . . . . . . . . . . . 13
|
285 | 257, 261,
284 | abssubge0d 14170 |
. . . . . . . . . . . 12
|
286 | 285 | adantrr 753 |
. . . . . . . . . . 11
|
287 | 239 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
288 | | simprr 796 |
. . . . . . . . . . . . 13
|
289 | | harmonicubnd 24736 |
. . . . . . . . . . . . 13
|
290 | 287, 288,
289 | syl2anc 693 |
. . . . . . . . . . . 12
|
291 | | 1red 10055 |
. . . . . . . . . . . . . 14
|
292 | 261, 257,
291 | lesubadd2d 10626 |
. . . . . . . . . . . . 13
|
293 | 292 | adantrr 753 |
. . . . . . . . . . . 12
|
294 | 290, 293 | mpbird 247 |
. . . . . . . . . . 11
|
295 | 286, 294 | eqbrtrd 4675 |
. . . . . . . . . 10
|
296 | 280, 281,
282, 282, 295 | elo1d 14267 |
. . . . . . . . 9
|
297 | | o1sub 14346 |
. . . . . . . . 9
Λ Λ
|
298 | 279, 296,
297 | sylancr 695 |
. . . . . . . 8
Λ
|
299 | 278, 298 | eqeltrrd 2702 |
. . . . . . 7
Λ |
300 | 247 | recnd 10068 |
. . . . . . . 8
ψ |
301 | | 1cnd 10056 |
. . . . . . . 8
|
302 | 241 | recnd 10068 |
. . . . . . . . . . . 12
ψ |
303 | | rpcnne0 11850 |
. . . . . . . . . . . . 13
|
304 | 303 | adantl 482 |
. . . . . . . . . . . 12
|
305 | | divdir 10710 |
. . . . . . . . . . . 12
ψ ψ ψ |
306 | 302, 301,
304, 305 | syl3anc 1326 |
. . . . . . . . . . 11
ψ ψ |
307 | 306 | mpteq2dva 4744 |
. . . . . . . . . 10
ψ
ψ |
308 | | simpr 477 |
. . . . . . . . . . . . 13
|
309 | 241, 308 | rerpdivcld 11903 |
. . . . . . . . . . . 12
ψ |
310 | | rpreccl 11857 |
. . . . . . . . . . . . 13
|
311 | 310 | adantl 482 |
. . . . . . . . . . . 12
|
312 | | eqidd 2623 |
. . . . . . . . . . . 12
ψ ψ |
313 | | eqidd 2623 |
. . . . . . . . . . . 12
|
314 | 252, 309,
311, 312, 313 | offval2 6914 |
. . . . . . . . . . 11
ψ ψ |
315 | | chpo1ub 25169 |
. . . . . . . . . . . 12
ψ |
316 | | divrcnv 14584 |
. . . . . . . . . . . . . 14
|
317 | 75, 316 | ax-mp 5 |
. . . . . . . . . . . . 13
|
318 | | rlimo1 14347 |
. . . . . . . . . . . . 13
|
319 | 317, 318 | mp1i 13 |
. . . . . . . . . . . 12
|
320 | | o1add 14344 |
. . . . . . . . . . . 12
ψ
ψ |
321 | 315, 319,
320 | sylancr 695 |
. . . . . . . . . . 11
ψ |
322 | 314, 321 | eqeltrrd 2702 |
. . . . . . . . . 10
ψ |
323 | 307, 322 | eqeltrd 2701 |
. . . . . . . . 9
ψ |
324 | 242, 308 | rerpdivcld 11903 |
. . . . . . . . 9
ψ |
325 | | chpge0 24852 |
. . . . . . . . . . . . . . . 16
ψ |
326 | 240, 325 | syl 17 |
. . . . . . . . . . . . . . 15
ψ |
327 | 241, 326 | ge0p1rpd 11902 |
. . . . . . . . . . . . . 14
ψ |
328 | 327 | rprege0d 11879 |
. . . . . . . . . . . . 13
ψ ψ |
329 | 246 | nnrpd 11870 |
. . . . . . . . . . . . . 14
|
330 | 329 | rpregt0d 11878 |
. . . . . . . . . . . . 13
|
331 | | divge0 10892 |
. . . . . . . . . . . . 13
ψ ψ ψ |
332 | 328, 330,
331 | syl2anc 693 |
. . . . . . . . . . . 12
ψ |
333 | 247, 332 | absidd 14161 |
. . . . . . . . . . 11
ψ ψ |
334 | 324 | recnd 10068 |
. . . . . . . . . . . . 13
ψ |
335 | 334 | abscld 14175 |
. . . . . . . . . . . 12
ψ |
336 | | fllep1 12602 |
. . . . . . . . . . . . . 14
|
337 | 240, 336 | syl 17 |
. . . . . . . . . . . . 13
|
338 | | rpregt0 11846 |
. . . . . . . . . . . . . . 15
|
339 | 338 | adantl 482 |
. . . . . . . . . . . . . 14
|
340 | 327 | rpregt0d 11878 |
. . . . . . . . . . . . . 14
ψ ψ |
341 | | lediv2 10913 |
. . . . . . . . . . . . . 14
ψ ψ
ψ ψ |
342 | 339, 330,
340, 341 | syl3anc 1326 |
. . . . . . . . . . . . 13
ψ ψ |
343 | 337, 342 | mpbid 222 |
. . . . . . . . . . . 12
ψ ψ |
344 | 324 | leabsd 14153 |
. . . . . . . . . . . 12
ψ ψ |
345 | 247, 324,
335, 343, 344 | letrd 10194 |
. . . . . . . . . . 11
ψ ψ |
346 | 333, 345 | eqbrtrd 4675 |
. . . . . . . . . 10
ψ
ψ |
347 | 346 | adantrr 753 |
. . . . . . . . 9
ψ ψ |
348 | 282, 323,
324, 300, 347 | o1le 14383 |
. . . . . . . 8
ψ |
349 | | o1const 14350 |
. . . . . . . . . 10
|
350 | 14, 75, 349 | mp2an 708 |
. . . . . . . . 9
|
351 | 350 | a1i 11 |
. . . . . . . 8
|
352 | 300, 301,
348, 351 | o1sub2 14356 |
. . . . . . 7
ψ |
353 | 238, 249,
299, 352 | o1sub2 14356 |
. . . . . 6
Λ ψ |
354 | 13, 353 | o1res2 14294 |
. . . . 5
Λ ψ |
355 | 232, 354 | syl5eqelr 2706 |
. . . 4
|
356 | 16, 355 | eqeltrd 2701 |
. . 3
|
357 | | eqid 2622 |
. . . . . 6
|
358 | 357, 225 | fmpti 6383 |
. . . . 5
|
359 | 358 | a1i 11 |
. . . 4
|
360 | | ssid 3624 |
. . . . 5
|
361 | 360 | a1i 11 |
. . . 4
|
362 | 359, 361,
282 | o1resb 14297 |
. . 3
|
363 | 356, 362 | mpbird 247 |
. 2
|
364 | 363 | trud 1493 |
1
|