Step | Hyp | Ref
| Expression |
1 | | o1fsum.2 |
. . 3
|
2 | | nnssre 11024 |
. . . . 5
|
3 | 2 | a1i 11 |
. . . 4
|
4 | | o1fsum.1 |
. . . . 5
|
5 | 4, 1 | o1mptrcl 14353 |
. . . 4
|
6 | | 1red 10055 |
. . . 4
|
7 | 3, 5, 6 | elo1mpt2 14266 |
. . 3
|
8 | 1, 7 | mpbid 222 |
. 2
|
9 | | rpssre 11843 |
. . . . . 6
|
10 | 9 | a1i 11 |
. . . . 5
|
11 | | nfcv 2764 |
. . . . . . . 8
|
12 | | nfcsb1v 3549 |
. . . . . . . 8
|
13 | | csbeq1a 3542 |
. . . . . . . 8
|
14 | 11, 12, 13 | cbvsumi 14427 |
. . . . . . 7
|
15 | | fzfid 12772 |
. . . . . . . 8
|
16 | | o1f 14260 |
. . . . . . . . . . . . 13
|
17 | 1, 16 | syl 17 |
. . . . . . . . . . . 12
|
18 | 4 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
|
19 | | dmmptg 5632 |
. . . . . . . . . . . . . 14
|
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . 13
|
21 | 20 | feq2d 6031 |
. . . . . . . . . . . 12
|
22 | 17, 21 | mpbid 222 |
. . . . . . . . . . 11
|
23 | | eqid 2622 |
. . . . . . . . . . . 12
|
24 | 23 | fmpt 6381 |
. . . . . . . . . . 11
|
25 | 22, 24 | sylibr 224 |
. . . . . . . . . 10
|
26 | 25 | ad3antrrr 766 |
. . . . . . . . 9
|
27 | | elfznn 12370 |
. . . . . . . . 9
|
28 | 12 | nfel1 2779 |
. . . . . . . . . . 11
|
29 | 13 | eleq1d 2686 |
. . . . . . . . . . 11
|
30 | 28, 29 | rspc 3303 |
. . . . . . . . . 10
|
31 | 30 | impcom 446 |
. . . . . . . . 9
|
32 | 26, 27, 31 | syl2an 494 |
. . . . . . . 8
|
33 | 15, 32 | fsumcl 14464 |
. . . . . . 7
|
34 | 14, 33 | syl5eqel 2705 |
. . . . . 6
|
35 | | rpcn 11841 |
. . . . . . 7
|
36 | 35 | adantl 482 |
. . . . . 6
|
37 | | rpne0 11848 |
. . . . . . 7
|
38 | 37 | adantl 482 |
. . . . . 6
|
39 | 34, 36, 38 | divcld 10801 |
. . . . 5
|
40 | | simplrl 800 |
. . . . . . 7
|
41 | | 1re 10039 |
. . . . . . . 8
|
42 | | elicopnf 12269 |
. . . . . . . 8
|
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
|
44 | 40, 43 | sylib 208 |
. . . . . 6
|
45 | 44 | simpld 475 |
. . . . 5
|
46 | | fzfid 12772 |
. . . . . . 7
|
47 | 25 | ad2antrr 762 |
. . . . . . . . 9
|
48 | | elfznn 12370 |
. . . . . . . . 9
|
49 | 47, 48, 31 | syl2an 494 |
. . . . . . . 8
|
50 | 49 | abscld 14175 |
. . . . . . 7
|
51 | 46, 50 | fsumrecl 14465 |
. . . . . 6
|
52 | | simplrr 801 |
. . . . . 6
|
53 | 51, 52 | readdcld 10069 |
. . . . 5
|
54 | 34, 36, 38 | absdivd 14194 |
. . . . . . . 8
|
55 | 54 | adantrr 753 |
. . . . . . 7
|
56 | | rprege0 11847 |
. . . . . . . . . 10
|
57 | 56 | ad2antrl 764 |
. . . . . . . . 9
|
58 | | absid 14036 |
. . . . . . . . 9
|
59 | 57, 58 | syl 17 |
. . . . . . . 8
|
60 | 59 | oveq2d 6666 |
. . . . . . 7
|
61 | 55, 60 | eqtrd 2656 |
. . . . . 6
|
62 | 34 | adantrr 753 |
. . . . . . . . 9
|
63 | 62 | abscld 14175 |
. . . . . . . 8
|
64 | | fzfid 12772 |
. . . . . . . . 9
|
65 | 47, 27, 31 | syl2an 494 |
. . . . . . . . . . 11
|
66 | 65 | adantlr 751 |
. . . . . . . . . 10
|
67 | 66 | abscld 14175 |
. . . . . . . . 9
|
68 | 64, 67 | fsumrecl 14465 |
. . . . . . . 8
|
69 | 57 | simpld 475 |
. . . . . . . . 9
|
70 | 51 | adantr 481 |
. . . . . . . . . 10
|
71 | 52 | adantr 481 |
. . . . . . . . . 10
|
72 | 70, 71 | readdcld 10069 |
. . . . . . . . 9
|
73 | 69, 72 | remulcld 10070 |
. . . . . . . 8
|
74 | 14 | fveq2i 6194 |
. . . . . . . . 9
|
75 | 64, 66 | fsumabs 14533 |
. . . . . . . . 9
|
76 | 74, 75 | syl5eqbr 4688 |
. . . . . . . 8
|
77 | | fzfid 12772 |
. . . . . . . . . . 11
|
78 | | ssun2 3777 |
. . . . . . . . . . . . . 14
|
79 | | flge1nn 12622 |
. . . . . . . . . . . . . . . . . 18
|
80 | 44, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
|
83 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
84 | | flle 12600 |
. . . . . . . . . . . . . . . . . 18
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
86 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
|
87 | 82, 83, 69, 85, 86 | letrd 10194 |
. . . . . . . . . . . . . . . 16
|
88 | | fznnfl 12661 |
. . . . . . . . . . . . . . . . 17
|
89 | 69, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
|
90 | 81, 87, 89 | mpbir2and 957 |
. . . . . . . . . . . . . . 15
|
91 | | fzsplit 12367 |
. . . . . . . . . . . . . . 15
|
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . 14
|
93 | 78, 92 | syl5sseqr 3654 |
. . . . . . . . . . . . 13
|
94 | 93 | sselda 3603 |
. . . . . . . . . . . 12
|
95 | 65 | abscld 14175 |
. . . . . . . . . . . . 13
|
96 | 95 | adantlr 751 |
. . . . . . . . . . . 12
|
97 | 94, 96 | syldan 487 |
. . . . . . . . . . 11
|
98 | 77, 97 | fsumrecl 14465 |
. . . . . . . . . 10
|
99 | 69, 70 | remulcld 10070 |
. . . . . . . . . 10
|
100 | 69, 71 | remulcld 10070 |
. . . . . . . . . 10
|
101 | 70 | recnd 10068 |
. . . . . . . . . . . 12
|
102 | 101 | mulid2d 10058 |
. . . . . . . . . . 11
|
103 | | 1red 10055 |
. . . . . . . . . . . 12
|
104 | 49 | absge0d 14183 |
. . . . . . . . . . . . . . 15
|
105 | 46, 50, 104 | fsumge0 14527 |
. . . . . . . . . . . . . 14
|
106 | 51, 105 | jca 554 |
. . . . . . . . . . . . 13
|
107 | 106 | adantr 481 |
. . . . . . . . . . . 12
|
108 | 44 | simprd 479 |
. . . . . . . . . . . . . 14
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . 13
|
110 | 103, 83, 69, 109, 86 | letrd 10194 |
. . . . . . . . . . . 12
|
111 | | lemul1a 10877 |
. . . . . . . . . . . 12
|
112 | 103, 69, 107, 110, 111 | syl31anc 1329 |
. . . . . . . . . . 11
|
113 | 102, 112 | eqbrtrrd 4677 |
. . . . . . . . . 10
|
114 | | hashcl 13147 |
. . . . . . . . . . . . 13
|
115 | | nn0re 11301 |
. . . . . . . . . . . . 13
|
116 | 77, 114, 115 | 3syl 18 |
. . . . . . . . . . . 12
|
117 | 116, 71 | remulcld 10070 |
. . . . . . . . . . 11
|
118 | 71 | adantr 481 |
. . . . . . . . . . . . 13
|
119 | | elfzuz 12338 |
. . . . . . . . . . . . . 14
|
120 | 81 | peano2nnd 11037 |
. . . . . . . . . . . . . . . 16
|
121 | | eluznn 11758 |
. . . . . . . . . . . . . . . 16
|
122 | 120, 121 | sylan 488 |
. . . . . . . . . . . . . . 15
|
123 | | simpllr 799 |
. . . . . . . . . . . . . . 15
|
124 | 83 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
125 | | reflcl 12597 |
. . . . . . . . . . . . . . . . 17
|
126 | | peano2re 10209 |
. . . . . . . . . . . . . . . . 17
|
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
128 | 122 | nnred 11035 |
. . . . . . . . . . . . . . . 16
|
129 | | fllep1 12602 |
. . . . . . . . . . . . . . . . 17
|
130 | 124, 129 | syl 17 |
. . . . . . . . . . . . . . . 16
|
131 | | eluzle 11700 |
. . . . . . . . . . . . . . . . 17
|
132 | 131 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
133 | 124, 127,
128, 130, 132 | letrd 10194 |
. . . . . . . . . . . . . . 15
|
134 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
135 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
136 | 135, 12 | nffv 6198 |
. . . . . . . . . . . . . . . . . 18
|
137 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
138 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
139 | 136, 137,
138 | nfbr 4699 |
. . . . . . . . . . . . . . . . 17
|
140 | 134, 139 | nfim 1825 |
. . . . . . . . . . . . . . . 16
|
141 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
142 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
143 | 142 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
144 | 141, 143 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
145 | 140, 144 | rspc 3303 |
. . . . . . . . . . . . . . 15
|
146 | 122, 123,
133, 145 | syl3c 66 |
. . . . . . . . . . . . . 14
|
147 | 119, 146 | sylan2 491 |
. . . . . . . . . . . . 13
|
148 | 77, 97, 118, 147 | fsumle 14531 |
. . . . . . . . . . . 12
|
149 | 71 | recnd 10068 |
. . . . . . . . . . . . 13
|
150 | | fsumconst 14522 |
. . . . . . . . . . . . 13
|
151 | 77, 149, 150 | syl2anc 693 |
. . . . . . . . . . . 12
|
152 | 148, 151 | breqtrd 4679 |
. . . . . . . . . . 11
|
153 | 120 | nnzd 11481 |
. . . . . . . . . . . . . 14
|
154 | | uzid 11702 |
. . . . . . . . . . . . . 14
|
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . 13
|
156 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
157 | 47, 30 | mpan9 486 |
. . . . . . . . . . . . . . . . . 18
|
158 | 157 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
159 | 122, 158 | syldan 487 |
. . . . . . . . . . . . . . . 16
|
160 | 159 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
161 | 71 | adantr 481 |
. . . . . . . . . . . . . . 15
|
162 | 159 | absge0d 14183 |
. . . . . . . . . . . . . . 15
|
163 | 156, 160,
161, 162, 146 | letrd 10194 |
. . . . . . . . . . . . . 14
|
164 | 163 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
165 | | biidd 252 |
. . . . . . . . . . . . . 14
|
166 | 165 | rspcv 3305 |
. . . . . . . . . . . . 13
|
167 | 155, 164,
166 | sylc 65 |
. . . . . . . . . . . 12
|
168 | | reflcl 12597 |
. . . . . . . . . . . . . 14
|
169 | 69, 168 | syl 17 |
. . . . . . . . . . . . 13
|
170 | | ssdomg 8001 |
. . . . . . . . . . . . . . . 16
|
171 | 64, 93, 170 | sylc 65 |
. . . . . . . . . . . . . . 15
|
172 | | hashdomi 13169 |
. . . . . . . . . . . . . . 15
|
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . 14
|
174 | | flge0nn0 12621 |
. . . . . . . . . . . . . . 15
|
175 | | hashfz1 13134 |
. . . . . . . . . . . . . . 15
|
176 | 57, 174, 175 | 3syl 18 |
. . . . . . . . . . . . . 14
|
177 | 173, 176 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
178 | | flle 12600 |
. . . . . . . . . . . . . 14
|
179 | 69, 178 | syl 17 |
. . . . . . . . . . . . 13
|
180 | 116, 169,
69, 177, 179 | letrd 10194 |
. . . . . . . . . . . 12
|
181 | 116, 69, 71, 167, 180 | lemul1ad 10963 |
. . . . . . . . . . 11
|
182 | 98, 117, 100, 152, 181 | letrd 10194 |
. . . . . . . . . 10
|
183 | 70, 98, 99, 100, 113, 182 | le2addd 10646 |
. . . . . . . . 9
|
184 | | ltp1 10861 |
. . . . . . . . . . 11
|
185 | | fzdisj 12368 |
. . . . . . . . . . 11
|
186 | 82, 184, 185 | 3syl 18 |
. . . . . . . . . 10
|
187 | 96 | recnd 10068 |
. . . . . . . . . 10
|
188 | 186, 92, 64, 187 | fsumsplit 14471 |
. . . . . . . . 9
|
189 | 36 | adantrr 753 |
. . . . . . . . . 10
|
190 | 189, 101,
149 | adddid 10064 |
. . . . . . . . 9
|
191 | 183, 188,
190 | 3brtr4d 4685 |
. . . . . . . 8
|
192 | 63, 68, 73, 76, 191 | letrd 10194 |
. . . . . . 7
|
193 | | rpregt0 11846 |
. . . . . . . . 9
|
194 | 193 | ad2antrl 764 |
. . . . . . . 8
|
195 | | ledivmul 10899 |
. . . . . . . 8
|
196 | 63, 72, 194, 195 | syl3anc 1326 |
. . . . . . 7
|
197 | 192, 196 | mpbird 247 |
. . . . . 6
|
198 | 61, 197 | eqbrtrd 4675 |
. . . . 5
|
199 | 10, 39, 45, 53, 198 | elo1d 14267 |
. . . 4
|
200 | 199 | ex 450 |
. . 3
|
201 | 200 | rexlimdvva 3038 |
. 2
|
202 | 8, 201 | mpd 15 |
1
|